to_additive #align failures

gistfile1.txt

❌ le_of_forall_neg_add_le <- ✅ le_of_forall_lt_one_mul_le
❌ le_iff_forall_neg_add_le <- ✅ le_iff_forall_lt_one_mul_le
❌ Sum.FaithfulVAddLeft <- ✅ Sum.FaithfulSMulLeft
❌ nsmul_le_nsmul_iff <- ✅ pow_le_pow_iff'
❌ Multiset.sum_zero <- ✅ Multiset.prod_zero
❌ nsmul_lt_nsmul_iff <- ✅ pow_lt_pow_iff'
❌ Part.left_dom_of_sub_dom <- ✅ Part.left_dom_of_div_dom
❌ Pi.update_eq_sub_add_single <- ✅ Pi.update_eq_div_mul_mulSingle
❌ eq_zero_or_pos <- ✅ eq_one_or_one_lt
❌ WithBot.coe_eq_zero <- ✅ WithBot.coe_eq_one
❌ Set.Nonempty.neg <- ✅ Set.Nonempty.inv
❌ Set.empty_nsmul <- ✅ Set.empty_pow
❌ Option.vadd_some <- ✅ Option.smul_some
❌ AddSubmonoid.centralizer_to_add_subsemigroup <- ✅ Submonoid.centralizer_toSubsemigroup
❌ AddSubsemigroup.mem_supₛ_of_mem <- ✅ Subsemigroup.mem_supₛ_of_mem
❌ AddCommSemigroup.IsRightCancelAdd.toIsCancelAdd <- ✅ CommSemigroup.IsRightCancelMul.toIsCancelMul
❌ Pi.existsAddOfLe <- ✅ Pi.existsMulOfLe
❌ neg_lt <- ✅ inv_lt'
❌ add_neg_le_iff_le_add <- ✅ mul_inv_le_iff_le_mul
❌ AddSubmonoid.dense_induction <- ✅ Submonoid.dense_induction
❌ Set.mem_vadd <- ✅ Set.mem_smul
❌ FreeAddMonoid.lift <- ✅ FreeMonoid.lift
❌ AddUnits.min_val <- ✅ Units.min_val
❌ AddSubmonoid.not_mem_of_not_mem_closure <- ✅ Submonoid.not_mem_of_not_mem_closure
❌ FreeAddMonoid.toList_sum <- ✅ FreeMonoid.toList_prod
❌ OneHomClass.map_one -> ✅ ZeroHomClass.map_zero
❌ Function.const_nonneg_of_nonneg <- ✅ Function.one_le_const_of_one_le
❌ Multiset.sum_replicate <- ✅ Multiset.prod_replicate
❌ List.headI_add_tail_sum_of_ne_nil <- ✅ List.headI_mul_tail_prod_of_ne_nil
❌ AddCancelMonoid.toAddLeftCancelMonoid_injective <- ✅ CancelMonoid.toLeftCancelMonoid_injective
❌ List.sum_isAddUnit_iff <- ✅ List.prod_isUnit_iff
❌ FreeAddMonoid.ofList_vadd <- ✅ FreeMonoid.ofList_smul
❌ AddMonoidHom.eqOn_closureM <- ✅ MonoidHom.eqOn_closureM
❌ IsAddHom.add <- ✅ IsMulHom.mul
❌ Multiset.sum_induction <- ✅ Multiset.prod_induction
❌ List.get?_zero_add_tail_sum <- ✅ List.get?_zero_mul_tail_prod
❌ AddRightCancelMonoid.ext <- ✅ RightCancelMonoid.ext
❌ Set.unionᵢ_op_vadd_set <- ✅ Set.unionᵢ_op_smul_set
❌ Right.nonneg_neg_iff <- ✅ Right.one_le_inv_iff
❌ List.sum_take_add_sum_drop <- ✅ List.prod_take_mul_prod_drop
❌ AddCancelCommMonoid.toAddCommMonoid_injective <- ✅ CancelCommMonoid.toCommMonoid_injective
❌ Set.inter_add_subset <- ✅ Set.inter_mul_subset
❌ AddMonoidHom.map_mul₂ <- ✅ MonoidHom.map_mul₂
❌ Set.singleton_vadd_singleton <- ✅ Set.singleton_smul_singleton
❌ IsAddGroupHom.injective_iff <- ✅ IsGroupHom.injective_iff
❌ Set.vadd_set_interᵢ_subset <- ✅ Set.smul_set_interᵢ_subset
❌ Set.unionᵢ₂_sub <- ✅ Set.unionᵢ₂_div
❌ min_add_add_left <- ✅ min_mul_mul_left
❌ nsmul_pos <- ✅ one_lt_pow'
❌ Sum.vadd_inl <- ✅ Sum.smul_inl
❌ Set.sub_interᵢ₂_subset <- ✅ Set.div_interᵢ₂_subset
❌ Set.interᵢ₂_add_subset <- ✅ Set.interᵢ₂_mul_subset
❌ AddSubsemigroup.supᵢ_induction <- ✅ Subsemigroup.supᵢ_induction
❌ LatticeOrderedCommGroup.abs_sub_sup_add_abs_sub_inf <- ✅ LatticeOrderedCommGroup.abs_div_sup_mul_abs_div_inf
❌ lt_neg_add_iff_lt <- ✅ lt_inv_mul_iff_lt
❌ IsAddGroupHom.mk' <- ✅ IsGroupHom.mk'
❌ Part.zero_mem_zero <- ✅ Part.one_mem_one
❌ Set.image_vadd <- ✅ Set.image_smul
❌ Set.interᵢ₂_vadd_subset <- ✅ Set.interᵢ₂_smul_subset
❌ WithBot.coe_lt_zero <- ✅ WithBot.coe_lt_one
❌ Right.neg_pos_iff <- ✅ Right.one_lt_inv_iff
❌ Set.preimage_sub_preimage_subset <- ✅ Set.preimage_div_preimage_subset
❌ Right.pow_nonneg <- ✅ Right.one_le_pow_of_le
❌ List.sum_lt_sum_of_ne_nil <- ✅ List.prod_lt_prod_of_ne_nil
❌ Set.nsmul_mem_nsmul <- ✅ Set.pow_mem_pow
❌ Set.union_add <- ✅ Set.union_mul
❌ FreeAddMonoid <- ✅ FreeMonoid
❌ LatticeOrderedCommGroup.abs_neg_comm <- ✅ LatticeOrderedCommGroup.abs_inv_comm
❌ AddSubmonoid.closure_singleton_le_iff_mem <- ✅ Submonoid.closure_singleton_le_iff_mem
❌ Set.add_univ <- ✅ Set.mul_univ
❌ Left.neg_le_self <- ✅ Left.inv_le_self
❌ FreeAddMonoid.lift_restrict <- ✅ FreeMonoid.lift_restrict
❌ le_neg_add_iff_add_le <- ✅ le_inv_mul_iff_mul_le
❌ Set.vadd_inter_ne_empty_iff <- ✅ Set.smul_inter_ne_empty_iff
❌ exists_pos_add_of_lt <- ✅ exists_one_lt_mul_of_lt
❌ sub_lt_iff_lt_add' <- ✅ div_lt_iff_lt_mul'
❌ Multiset.sum_eq_smul_single <- ✅ Multiset.prod_eq_pow_single
❌ VAdd.comp.vaddCommClass' <- ✅ SMul.comp.smulCommClass'
❌ exists_pos_add_of_lt' <- ✅ exists_one_lt_mul_of_lt'
❌ AddSubmonoid.mem_closure <- ✅ Submonoid.mem_closure
❌ AddAction.Supports.mono <- ✅ MulAction.Supports.mono
❌ le_sub_self_iff <- ✅ le_div_self_iff
❌ Function.const_nonneg <- ✅ Function.one_le_const
❌ AddAction.Supports.vadd <- ✅ MulAction.Supports.smul
❌ neg_vadd_eq_iff <- ✅ inv_smul_eq_iff
❌ VAdd.comp <- ✅ SMul.comp
❌ sub_lt_self_iff <- ✅ div_lt_self_iff
❌ AddCon.le_iff <- ✅ Con.le_iff
❌ Set.add_eq_empty <- ✅ Set.mul_eq_empty
❌ add_neg_le_iff_le_add' <- ✅ mul_inv_le_iff_le_mul'
❌ vadd_left_injective' <- ✅ smul_left_injective'
❌ AddSubmonoid.coe_inf <- ✅ Submonoid.coe_inf
❌ AddMonoidHom.flipHom <- ✅ MonoidHom.flipHom
❌ Set.vadd_set_inter <- ✅ Set.smul_set_inter
❌ AddSubmonoid.mem_top <- ✅ Submonoid.mem_top
❌ AddMonoidHom.map_div₂ <- ✅ MonoidHom.map_div₂
❌ Multiset.sum_nonneg <- ✅ Multiset.one_le_prod_of_one_le
❌ AddCon.quotientKerEquivOfSurjective <- ✅ Con.quotientKerEquivOfSurjective
❌ List.sum_append <- ✅ List.prod_append
❌ Multiset.sum_bind <- ✅ Multiset.prod_bind
❌ Set.unionᵢ_vadd_right_image <- ✅ Set.unionᵢ_smul_right_image
❌ Part.neg_mem_neg <- ✅ Part.inv_mem_inv
❌ Set.vaddCommClass <- ✅ Set.smulCommClass
❌ VAddAssocClass.opposite_mid <- ✅ IsScalarTower.opposite_mid
❌ AddMonoidHom.map_list_sum <- ✅ MonoidHom.map_list_prod
❌ Set.compl_neg <- ✅ Set.compl_inv
❌ AddSemigroup.to_isAssociative <- ✅ Semigroup.to_isAssociative
❌ Set.Nonempty.sub <- ✅ Set.Nonempty.div
❌ AddCon.lift_surjective_of_surjective <- ✅ Con.lift_surjective_of_surjective
❌ Set.interᵢ_vadd_subset <- ✅ Set.interᵢ_smul_subset
❌ AddCon.ker_rel <- ✅ Con.ker_rel
❌ Set.add_inter_subset <- ✅ Set.mul_inter_subset
❌ List.sum_eq_card_nsmul <- ✅ List.prod_eq_pow_card
❌ LinearOrderedAddCommGroup.add_lt_add_left <- ✅ LinearOrderedCommGroup.mul_lt_mul_left'
❌ AddSubmonoid.add_mem <- ✅ Submonoid.mul_mem
❌ Multiset.sum_map_smul <- ✅ Multiset.prod_map_pow
❌ Neg.toHasAbs <- ✅ Inv.toHasAbs
❌ AddHom.restrict <- ✅ MulHom.restrict
❌ EckmannHilton.addCommMonoid <- ✅ EckmannHilton.commMonoid
❌ List.exists_lt_of_sum_lt <- ✅ List.exists_lt_of_prod_lt'
❌ FreeAddMonoid.ofList_append <- ✅ FreeMonoid.ofList_append
❌ vadd_assoc <- ✅ smul_assoc
❌ LatticeOrderedCommGroup.abs_of_nonneg <- ✅ LatticeOrderedCommGroup.mabs_of_one_le
❌ AddSubmonoid.copy <- ✅ Submonoid.copy
❌ le_neg_iff_add_nonpos_left <- ✅ le_inv_iff_mul_le_one_left
❌ AddCon.sub <- ✅ Con.div
❌ nsmul_nonpos <- ✅ pow_le_one'
❌ AddCon.mk'_surjective <- ✅ Con.mk'_surjective
❌ sub_lt_sub_right <- ✅ div_lt_div_right'
❌ le_add_self <- ✅ le_mul_self
❌ Set.vadd_set_interᵢ₂_subset <- ✅ Set.smul_set_interᵢ₂_subset
❌ IsAddMonoidHom.neg <- ✅ IsMonoidHom.inv
❌ IsCentralVAdd.unop_vadd_eq_vadd <- ✅ IsCentralScalar.unop_smul_eq_smul
❌ Set.image_add_right' <- ✅ Set.image_mul_right'
❌ Set.op_vadd_inter_ne_empty_iff <- ✅ Set.op_smul_inter_ne_empty_iff
❌ Set.vadd_empty <- ✅ Set.smul_empty
❌ Right.nsmul_neg_iff <- ✅ Right.pow_lt_one_iff
❌ AddCon.neg <- ✅ Con.inv
❌ le_add_neg_iff_add_le <- ✅ le_mul_inv_iff_mul_le
❌ FreeAddMonoid.toList_add <- ✅ FreeMonoid.toList_mul
❌ Set.Nonempty.add <- ✅ Set.Nonempty.mul
❌ Set.Nonempty.vadd <- ✅ Set.Nonempty.smul
❌ Set.vadd_set_inter_subset <- ✅ Set.smul_set_inter_subset
❌ instVAddOrderDual' <- ✅ instSMulOrderDual'
❌ Part.add_get_eq <- ✅ Part.mul_get_eq
❌ le_of_add_le_left <- ✅ le_of_mul_le_left
❌ Set.sub_singleton <- ✅ Set.div_singleton
❌ Set.sub_empty <- ✅ Set.div_empty
❌ Set.not_zero_mem_sub_iff <- ✅ Set.not_one_mem_div_iff
❌ WithZero.add <- ✅ WithOne.mul
❌ Set.vadd_unionᵢ <- ✅ Set.smul_unionᵢ
❌ AddAction.bijective <- ✅ MulAction.bijective
❌ List.rel_sum <- ✅ List.rel_prod
❌ AddMonoidHom.ofClosureMEqTopLeft <- ✅ MonoidHom.ofClosureMEqTopLeft
❌ Set.addZeroClass <- ✅ Set.mulOneClass
❌ apply_abs_le_add_of_nonneg <- ✅ apply_abs_le_mul_of_one_le
❌ Set.vadd_mem_vadd <- ✅ Set.smul_mem_smul
❌ Set.zero <- ✅ Set.one
❌ AddCommMonoid.ext <- ✅ CommMonoid.ext
❌ apply_abs_le_add_of_nonneg' <- ✅ apply_abs_le_mul_of_one_le'
❌ max_neg_neg <- ✅ max_inv_inv'
❌ add_neg_neg_iff <- ✅ mul_inv_lt_one_iff
❌ le_iff_forall_pos_lt_add' <- ✅ le_iff_forall_one_lt_lt_mul'
❌ Set.vadd_inter_ne_empty_iff' <- ✅ Set.smul_inter_ne_empty_iff'
❌ AddEquiv.isAddGroupHom <- ✅ MulEquiv.isGroupHom
❌ LatticeOrderedCommGroup.pos_of_nonneg <- ✅ LatticeOrderedCommGroup.pos_of_one_le
❌ Part.add_mem_add <- ✅ Part.mul_mem_mul
❌ List.exists_mem_ne_zero_of_sum_ne_zero <- ✅ List.exists_mem_ne_one_of_prod_ne_one
❌ add_neg_lt_iff_lt_add <- ✅ mul_inv_lt_iff_lt_mul
❌ FreeAddMonoid.toList_ofList <- ✅ FreeMonoid.toList_ofList
❌ AddSubmonoid.nontrivial_iff <- ✅ Submonoid.nontrivial_iff
❌ Set.vadd_set_empty <- ✅ Set.smul_set_empty
❌ LatticeOrderedCommGroup.le_pos <- ✅ LatticeOrderedCommGroup.m_le_pos
❌ Fintype.decidableEqAddHomFintype <- ✅ Fintype.decidableEqMulHomFintype
❌ List.alternatingSum_cons_cons <- ✅ List.alternatingProd_cons_cons
❌ AddCon.kerLift_mk <- ✅ Con.kerLift_mk
❌ AddSubmonoid.coe_bot <- ✅ Submonoid.coe_bot
❌ WithBot.coe_pos <- ✅ WithBot.one_lt_coe
❌ AddSubsemigroup.add_mem_sup <- ✅ Subsemigroup.mul_mem_sup
❌ AddSemigroupPEmpty <- ✅ SemigroupPEmpty
❌ WithTop.coe_pos <- ✅ WithTop.one_lt_coe
❌ List.Perm.sum_eq <- ✅ List.Perm.prod_eq
❌ Set.inter_vadd_subset <- ✅ Set.inter_smul_subset
❌ Set.coe_singletonZeroHom <- ✅ Set.coe_singletonOneHom
❌ le_neg_iff_add_nonpos_right <- ✅ le_inv_iff_mul_le_one_right
❌ sub_le_neg_add_iff <- ✅ div_le_inv_mul_iff
❌ List.sum_reverse_noncomm <- ✅ List.prod_reverse_noncomm
❌ abs_eq_sup_neg <- ✅ abs_eq_sup_inv
❌ le_of_add_le_right <- ✅ le_of_mul_le_right
❌ List.alternatingSum_nil <- ✅ List.alternatingProd_nil
❌ AddAction.supports_of_mem <- ✅ MulAction.supports_of_mem
❌ List.sum_eq_zero <- ✅ List.prod_eq_one
❌ Multiset.sum_cons <- ✅ Multiset.prod_cons
❌ AddEquiv.isAddHom <- ✅ MulEquiv.isMulHom
❌ AddCon.addCommMonoid <- ✅ Con.commMonoid
❌ FreeAddMonoid.lift_of_comp_eq_map <- ✅ FreeMonoid.lift_of_comp_eq_map
❌ le_add_neg_iff_le <- ✅ le_mul_inv_iff_le
❌ Function.update_vadd <- ✅ Function.update_smul
❌ Multiset.sum <- ✅ Multiset.prod
❌ WithTop.zero_ne_top <- ✅ WithTop.one_ne_top
❌ AddOpposite.rec' <- ✅ MulOpposite.rec'
❌ IsAddGroupHom.id <- ✅ IsGroupHom.id
❌ Set.univ_add <- ✅ Set.univ_mul
❌ List.sum_eq_smul_single <- ✅ List.prod_eq_pow_single
❌ instVAddOrderDual <- ✅ instSMulOrderDual
❌ Function.vaddCommClass <- ✅ Function.smulCommClass
❌ Pi.orderedAddCancelCommMonoid <- ✅ Pi.orderedCancelCommMonoid
❌ Set.add_image_prod <- ✅ Set.image_mul_prod
❌ AddSubmonoid.center_to_add_subsemigroup <- ✅ Submonoid.center_toSubsemigroup
❌ sub_nonpos <- ✅ div_le_one'
❌ AddCommute.list_sum_right <- ✅ Commute.list_prod_right
❌ add_neg_le_add_neg_iff <- ✅ mul_inv_le_mul_inv_iff'
❌ Set.neg_mem_neg <- ✅ Set.inv_mem_inv
❌ VAddAssocClass.of_vadd_zero_add <- ✅ IsScalarTower.of_smul_one_mul
❌ List.length_pos_of_sum_pos <- ✅ List.length_pos_of_one_lt_prod
❌ Function.Injective.addAction <- ✅ Function.Injective.mulAction
❌ AddMonoidHom.compl₂ <- ✅ MonoidHom.compl₂
❌ AddSubmonoid.coe_infᵢ <- ✅ Submonoid.coe_infᵢ
❌ StrictMono.neg <- ✅ StrictMono.inv
❌ FreeAddMonoid.lift_comp_of <- ✅ FreeMonoid.lift_comp_of
❌ nsmul_lt_nsmul <- ✅ pow_lt_pow'
❌ FreeAddMonoid.of_vadd <- ✅ FreeMonoid.of_smul
❌ List.sum_le_sum <- ✅ List.prod_le_prod'
❌ Set.sub_mem_sub <- ✅ Set.div_mem_div
❌ AddSemiconjBy <- ✅ SemiconjBy
❌ LatticeOrderedCommGroup.sup_eq_add_pos_sub <- ✅ LatticeOrderedCommGroup.sup_eq_mul_pos_div
❌ VAdd.comp.vaddCommClass <- ✅ SMul.comp.smulCommClass
❌ Set.add_singleton <- ✅ Set.mul_singleton
❌ le_cinfᵢ_add_cinfᵢ <- ✅ le_cinfᵢ_mul_cinfᵢ
❌ le_sub_iff_add_le' <- ✅ le_div_iff_mul_le'
❌ Set.vadd <- ✅ Set.smul
❌ List.alternatingSum_append <- ✅ List.alternatingProd_append
❌ LatticeOrderedCommGroup.add_inf_eq_add_inf_add <- ✅ LatticeOrderedCommGroup.mul_inf_eq_mul_inf_mul
❌ Set.mem_vadd_set <- ✅ Set.mem_smul_set
❌ AddSubsemigroup.mem_supᵢ_of_directed <- ✅ Subsemigroup.mem_supᵢ_of_directed
❌ LatticeOrderedCommGroup.neg_of_nonneg <- ✅ LatticeOrderedCommGroup.neg_of_one_le
❌ Set.sub_subset_sub_right <- ✅ Set.div_subset_div_right
❌ Right.self_le_neg <- ✅ Right.self_le_inv
❌ AddMonoidHom.coe_of <- ✅ MonoidHom.coe_of
❌ le_of_forall_pos_le_add <- ✅ le_of_forall_one_lt_le_mul
❌ AddCommSemigroup.IsRightCancelAdd.toIsLeftCancelAdd <- ✅ CommSemigroup.IsRightCancelMul.toIsLeftCancelMul
❌ Set.nsmul_subset_nsmul_of_zero_mem <- ✅ Set.pow_subset_pow_of_one_mem
❌ Set.mem_zero <- ✅ Set.mem_one
❌ Set.neg_empty <- ✅ Set.inv_empty
❌ Fintype.decidableEqZeroHomFintype <- ✅ Fintype.decidableEqOneHomFintype
❌ Set.singleton_vadd <- ✅ Set.singleton_smul
❌ Set.singleton_sub <- ✅ Set.singleton_div
❌ le_map_sub_add_map_sub <- ✅ le_map_div_add_map_div
❌ VAddCommClass.op_left <- ✅ SMulCommClass.op_left
❌ IsAddGroupHom.to_isAddMonoidHom <- ✅ IsGroupHom.to_isMonoidHom
❌ Set.vadd_subset_iff <- ✅ Set.smul_subset_iff
❌ AddCancelCommMonoid.toAddCancelMonoid <- ✅ CancelCommMonoid.toCancelMonoid
❌ Set.sub_subset_sub_left <- ✅ Set.div_subset_div_left
❌ add_neg_nonpos_iff <- ✅ mul_inv_le_one_iff
❌ max_zero_sub_max_neg_zero_eq_self <- ✅ max_one_div_max_inv_one_eq_self
❌ sub_le_self_iff <- ✅ div_le_self_iff
❌ Set.unionᵢ_sub_left_image <- ✅ Set.unionᵢ_div_left_image
❌ zsmul_neg <- ✅ inv_zpow
❌ AddCommute.vadd_left <- ✅ Commute.smul_left
❌ LatticeOrderedCommGroup.pos_eq_neg_neg <- ✅ LatticeOrderedCommGroup.pos_eq_neg_inv
❌ LatticeOrderedCommGroup.neg_nonneg <- ✅ LatticeOrderedCommGroup.one_le_neg
❌ Left.self_le_neg <- ✅ Left.self_le_inv
❌ lt_add_neg_iff_lt <- ✅ lt_mul_inv_iff_lt
❌ Set.sub_unionᵢ <- ✅ Set.div_unionᵢ
❌ Multiset.sum_map_erase <- ✅ Multiset.prod_map_erase
❌ vadd_left_cancel <- ✅ smul_left_cancel
❌ lt_or_lt_of_add_lt_add <- ✅ lt_or_lt_of_mul_lt_mul
❌ AddAction.toFun_apply <- ✅ MulAction.toFun_apply
❌ AddMonoidHom.isAddGroupHom <- ✅ MonoidHom.isGroupHom
❌ Set.vadd_subset_vadd_left <- ✅ Set.smul_subset_smul_left
❌ Function.const_nonpos_of_nonpos <- ✅ Function.const_le_one_of_le_one
❌ Set.singletonAddMonoidHom_apply <- ✅ Set.singletonMonoidHom_apply
❌ AddCon.lift_comp_mk' <- ✅ Con.lift_comp_mk'
❌ List.sum_map_eq_smul_single <- ✅ List.prod_map_eq_pow_single
❌ IsAddUnit.addSubmonoid <- ✅ IsUnit.submonoid
❌ AddSubmonoid.mem_supᵢ <- ✅ Submonoid.mem_supᵢ
❌ sub_lt_sub <- ✅ div_lt_div''
❌ AddSubmonoid.closure_univ <- ✅ Submonoid.closure_univ
❌ Set.preimage_add_preimage_subset <- ✅ Set.preimage_mul_preimage_subset
❌ neg_add_le_iff_le_add' <- ✅ inv_mul_le_iff_le_mul'
❌ LatticeOrderedCommGroup.neg_zero <- ✅ LatticeOrderedCommGroup.neg_one
❌ AddLeftCancelSemigroup.toIsLeftCancelAdd <- ✅ LeftCancelSemigroup.toIsLeftCancelMul
❌ Multiset.all_zero_of_le_zero_le_of_sum_eq_zero <- ✅ Multiset.all_one_of_le_one_le_of_prod_eq_one
❌ Multiset.sum_map_le_sum <- ✅ Multiset.prod_map_le_prod
❌ Set.univ_add_univ <- ✅ Set.univ_mul_univ
❌ IsAddHom.to_isAddMonoidHom <- ✅ IsMulHom.to_isMonoidHom
❌ vadd_add_vadd <- ✅ smul_mul_smul
❌ List.sum_set <- ✅ List.prod_set
❌ AddCon.mem_coe <- ✅ Con.mem_coe
❌ min_le_add_of_nonneg_right <- ✅ min_le_mul_of_one_le_right
❌ AddCon.quotientKerEquivOfRightInverse <- ✅ Con.quotientKerEquivOfRightInverse
❌ vadd_vadd <- ✅ smul_smul
❌ AddRightCancelMonoid.faithfulVAdd <- ✅ RightCancelMonoid.faithfulSMul
❌ Set.vadd_eq_empty <- ✅ Set.smul_eq_empty
❌ Multiset.sum_hom_rel <- ✅ Multiset.prod_hom_rel
❌ nsmul_le_nsmul_of_nonpos <- ✅ pow_le_pow_of_le_one'
❌ AddSubsemigroup.coe_supₛ_of_directed_on <- ✅ Subsemigroup.coe_supₛ_of_directed_on
❌ add_ite <- ✅ mul_ite
❌ Set.unionᵢ_vadd_eq_setOf_exists <- ✅ Set.unionᵢ_smul_eq_setOf_exists
❌ lt_sub_iff_add_lt' <- ✅ lt_div_iff_mul_lt'
❌ sub_lt_sub_left <- ✅ div_lt_div_left'
❌ OrderEmbedding.addRight <- ✅ OrderEmbedding.mulRight
❌ sub_le_comm <- ✅ div_le_comm
❌ Set.range_vadd_range <- ✅ Set.range_smul_range
❌ Multiset.sum_singleton <- ✅ Multiset.prod_singleton
❌ Set.add_unionᵢ₂ <- ✅ Set.mul_unionᵢ₂
❌ unique_zero <- ✅ unique_one
❌ IsAddGroupHom.map_zero <- ✅ IsGroupHom.map_one
❌ Sigma.vadd_mk <- ✅ Sigma.smul_mk
❌ Set.image_zero <- ✅ Set.image_one
❌ min_zero <- ✅ min_one
❌ Multiset.sum_toList <- ✅ Multiset.prod_toList
❌ Set.interᵢ_neg <- ✅ Set.interᵢ_inv
❌ Function.Injective.linearOrderedAddCommMonoid <- ✅ Function.Injective.linearOrderedCommMonoid
❌ List.card_nsmul_le_sum <- ✅ List.pow_card_le_prod
❌ EckmannHilton.addCommGroup <- ✅ EckmannHilton.commGroup
❌ vadd_eq_self_of_preimage_zsmul_eq_self <- ✅ smul_eq_self_of_preimage_zpow_eq_self
❌ LatticeOrderedCommGroup.pos_nonneg <- ✅ LatticeOrderedCommGroup.one_le_pos
❌ AddMonoidHom.map_one₂ <- ✅ MonoidHom.map_one₂
❌ sub_pos <- ✅ one_lt_div'
❌ AddUnits.val_le_val <- ✅ Units.val_le_val
❌ List.SublistForall₂.sum_le_sum <- ✅ List.SublistForall₂.prod_le_prod'
❌ FreeAddMonoid.ofList_toList <- ✅ FreeMonoid.ofList_toList
❌ Set.preimage_add_left_zero <- ✅ Set.preimage_mul_left_one
❌ add_lt_add_iff_of_le_of_le <- ✅ mul_lt_mul_iff_of_le_of_le
❌ Function.const_nonpos <- ✅ Function.const_le_one
❌ neg_add_nonpos_iff <- ✅ inv_mul_le_one_iff
❌ Set.sub_eq_empty <- ✅ Set.div_eq_empty
❌ min_add_distrib' <- ✅ min_mul_distrib'
❌ vadd_vadd_vadd_comm <- ✅ smul_smul_smul_comm
❌ AddSubmonoid.mem_bot <- ✅ Submonoid.mem_bot
❌ List.sum_take_succ <- ✅ List.prod_take_succ
❌ OrderedAddCommGroup.to_contravariantClass_left_le <- ✅ OrderedCommGroup.to_contravariantClass_left_le
❌ Set.sub_inter_subset <- ✅ Set.div_inter_subset
❌ Set.isAddUnit_iff <- ✅ Set.isUnit_iff
❌ Set.Nonempty.of_sub_right <- ✅ Set.Nonempty.of_div_right
❌ IsAddMonoidHom.map_add' <- ✅ IsMonoidHom.map_mul'
❌ min_sub_sub_left <- ✅ min_div_div_left'
❌ List.Forall₂.sum_le_sum <- ✅ List.Forall₂.prod_le_prod'
❌ AddAut <- ✅ MulAut
❌ FreeAddMonoid.toList_of <- ✅ FreeMonoid.toList_of
❌ Sum.vadd_inr <- ✅ Sum.smul_inr
❌ Function.Injective.orderedAddCommGroup <- ✅ Function.Injective.orderedCommGroup
❌ Function.hasVAdd <- ✅ Function.hasSMul
❌ Set.sub_union <- ✅ Set.div_union
❌ AddSubmonoid.closure_eq_of_le <- ✅ Submonoid.closure_eq_of_le
❌ List.sum_join <- ✅ List.prod_join
❌ List.sum_map_hom <- ✅ List.prod_map_hom
❌ sub_le_sub <- ✅ div_le_div''
❌ vadd_add_assoc <- ✅ smul_mul_assoc
❌ Set.addMonoid <- ✅ Set.monoid
❌ Sum.FaithfulVAddRight <- ✅ Sum.FaithfulSMulRight
❌ AddAction.surjective_vadd <- ✅ MulAction.surjective_smul
❌ Set.image_add_right <- ✅ Set.image_mul_right
❌ Set.mem_sub <- ✅ Set.mem_div
❌ Set.Nonempty.zero_mem_sub <- ✅ Set.Nonempty.one_mem_div
❌ neg_add_neg_iff <- ✅ inv_mul_lt_one_iff
❌ Set.add_eq_zero_iff <- ✅ Set.mul_eq_one_iff
❌ List.sum_lt_sum <- ✅ List.prod_lt_prod'
❌ LatticeOrderedCommGroup.hasZeroLatticeHasNegPart <- ✅ LatticeOrderedCommGroup.hasOneLatticeHasNegPart
❌ Pi.instPow -> ✅ Pi.instSMul
❌ Set.add_image_prod <- ✅ Set.image_div_prod
❌ nsmul_nonneg <- ✅ one_le_pow_of_one_le'
❌ Set.add_subset_add_right <- ✅ Set.mul_subset_mul_right
❌ AddMonoidHom.eq_of_eqOn_denseM <- ✅ MonoidHom.eq_of_eqOn_denseM
❌ IsAddHom.comp <- ✅ IsMulHom.comp
❌ self_le_add_right <- ✅ self_le_mul_right
❌ AddEquiv.withZeroCongr_symm <- ✅ MulEquiv.withOneCongr_symm
❌ Function.const_pos <- ✅ Function.one_lt_const
❌ max_sub_sub_left <- ✅ max_div_div_left'
❌ Set.unionᵢ_add_left_image <- ✅ Set.unionᵢ_mul_left_image
❌ Set.set_vadd_subset_set_vadd_iff <- ✅ Set.set_smul_subset_set_smul_iff
❌ WithZero.zero <- ✅ WithOne.one
❌ Set.vadd_interᵢ₂_subset <- ✅ Set.smul_interᵢ₂_subset
❌ map_list_sum <- ✅ map_list_prod
❌ LatticeOrderedCommGroup.inf_eq_sub_pos_sub <- ✅ LatticeOrderedCommGroup.inf_eq_div_pos_div
❌ Set.vadd_interᵢ_subset <- ✅ Set.smul_interᵢ_subset
❌ le_add_right <- ✅ le_mul_right
❌ neg_vadd_vadd <- ✅ inv_smul_smul
❌ fn_min_add_fn_max <- ✅ fn_min_mul_fn_max
❌ VAddCommClass.symm <- ✅ SMulCommClass.symm
❌ Set.vadd_set_mono <- ✅ Set.smul_set_mono
❌ Multiset.sum_map_add <- ✅ Multiset.prod_map_mul
❌ AddSemiconjBy.eq <- ✅ SemiconjBy.eq
❌ Set.image2_sub <- ✅ Set.image2_div
❌ sub_nonneg <- ✅ one_le_div'
❌ AddSubmonoid.closure_mono <- ✅ Submonoid.closure_mono
❌ FreeAddMonoid.ofList_nil <- ✅ FreeMonoid.ofList_nil
❌ AddCon.ker_apply_eq_preimage <- ✅ Con.ker_apply_eq_preimage
❌ Set.inter_sub_subset <- ✅ Set.inter_div_subset
❌ AddCon.smulinst <- ✅ Con.smulinst
❌ le_cinfᵢ_add <- ✅ le_cinfᵢ_mul
❌ WithTop.coe_zero <- ✅ WithTop.coe_one
❌ Multiset.card_nsmul_le_sum <- ✅ Multiset.pow_card_le_prod
❌ AddMonoidHom.map_inv₂ <- ✅ MonoidHom.map_inv₂
❌ Set.inter_neg <- ✅ Set.inter_inv
❌ IsAddUnit.mem_addSubmonoid_iff <- ✅ IsUnit.mem_submonoid_iff
❌ lt_sub_iff_add_lt <- ✅ lt_div_iff_mul_lt
❌ AddAction.toPerm <- ✅ MulAction.toPerm
❌ IsAddMonoidHom.comp <- ✅ IsMonoidHom.comp
❌ FreeAddMonoid.recOn_of_add <- ✅ FreeMonoid.recOn_of_mul
❌ List.sum_range_succ <- ✅ List.prod_range_succ
❌ AddCon.addGroup <- ✅ Con.group
❌ FreeAddMonoid.of_injective <- ✅ FreeMonoid.of_injective
❌ AddCommMonoid.toAddMonoid_injective <- ✅ CommMonoid.toMonoid_injective
❌ zero_min <- ✅ one_min
❌ vadd_neg_vadd <- ✅ smul_inv_smul
❌ Set.image_add <- ✅ Set.image_mul
❌ AddSubmonoid.ext <- ✅ Submonoid.ext
❌ AddAction.Supports <- ✅ MulAction.Supports
❌ AddCancelMonoid.ext <- ✅ CancelMonoid.ext
❌ FreeAddMonoid.comp_lift <- ✅ FreeMonoid.comp_lift
❌ max_add_add_right <- ✅ max_mul_mul_right
❌ Set.zero_nonempty <- ✅ Set.one_nonempty
❌ Multiset.le_sum_of_mem <- ✅ Multiset.le_prod_of_mem
❌ sub_le_sub_iff <- ✅ div_le_div_iff'
❌ AddUnits.max_val <- ✅ Units.max_val
❌ AddSemigroup.isScalarTower <- ✅ Semigroup.isScalarTower
❌ WithBot.map_zero <- ✅ WithBot.map_one
❌ AddUnits.val_sub_eq_sub_val <- ✅ Units.val_div_eq_div_val
❌ Part.left_dom_of_add_dom <- ✅ Part.left_dom_of_mul_dom
❌ le_map_sub_add_map_sub <- ✅ le_map_div_mul_map_div
❌ neg_sup_eq_neg_inf_neg <- ✅ inv_sup_eq_inv_inf_inv
❌ Set.singletonZeroHom <- ✅ Set.singletonOneHom
❌ List.sum_range_succ' <- ✅ List.prod_range_succ'
❌ FreeAddMonoid.lift_eval_of <- ✅ FreeMonoid.lift_eval_of
❌ lt_add_neg_iff_add_lt <- ✅ lt_mul_inv_iff_mul_lt
❌ WithTop.coe_eq_zero <- ✅ WithTop.coe_eq_one
❌ Function.Surjective.addAction <- ✅ Function.Surjective.mulAction
❌ bot_eq_zero' <- ✅ bot_eq_one'
❌ FreeAddMonoid.toList_of_add <- ✅ FreeMonoid.toList_of_mul
❌ AddSubsemigroup.mem_sup_left <- ✅ Subsemigroup.mem_sup_left
❌ List.sum_erase <- ✅ List.prod_erase
❌ FreeAddMonoid.ofList_symm <- ✅ FreeMonoid.ofList_symm
❌ VAddAssocClass.op_right <- ✅ IsScalarTower.op_right
❌ IsAddHom.neg <- ✅ IsMulHom.inv
❌ AddEquiv.withZeroCongr_trans <- ✅ MulEquiv.withOneCongr_trans
❌ Set.neg_mem_Ioc_iff <- ✅ Set.inv_mem_Ioc_iff
❌ List.eq_of_sum_take_eq <- ✅ List.eq_of_prod_take_eq
❌ add_vadd_zero <- ✅ mul_smul_one
❌ Set.neg_range <- ✅ Set.inv_range
❌ Right.neg_neg_iff <- ✅ Right.inv_lt_one_iff
❌ FreeAddMonoid.ofList_cons <- ✅ FreeMonoid.ofList_cons
❌ AddSubmonoid.closure_eq <- ✅ Submonoid.closure_eq
❌ map_zsmul' <- ✅ map_zpow'
❌ AddSubmonoid.coe_top <- ✅ Submonoid.coe_top
❌ sub_le_sub_right <- ✅ div_le_div_right'
❌ Right.neg_nonpos_iff <- ✅ Right.inv_le_one_iff
❌ Multiset.sum_map_neg' <- ✅ Multiset.prod_map_inv'
❌ AddMonoid.ext <- ✅ Monoid.ext
❌ Set.Nonempty.subset_zero_iff <- ✅ Set.Nonempty.subset_one_iff
❌ AddCon.nsmul <- ✅ Con.pow
❌ Set.Nonempty.of_sub_left <- ✅ Set.Nonempty.of_div_left
❌ AddCon.kerLift_range_eq <- ✅ Con.kerLift_range_eq
❌ AddCon.vadd <- ✅ Con.smul
❌ Set.addSemigroup <- ✅ Set.semigroup
❌ add_neg_lt_iff_le_add' <- ✅ mul_inv_lt_iff_le_mul'
❌ AddMonoidHom.coe_ofClosureMEqTopLeft <- ✅ MonoidHom.coe_ofClosureMEqTopLeft
❌ Set.union_neg <- ✅ Set.union_inv
❌ List.sum_neg_reverse <- ✅ List.prod_inv_reverse
❌ self_le_add_left <- ✅ self_le_mul_left
❌ lt_neg <- ✅ lt_inv'
❌ VAddAssocClass.left <- ✅ IsScalarTower.left
❌ AddCommSemigroup.IsLeftCancelAdd.toIsRightCancelAdd <- ✅ CommSemigroup.IsLeftCancelMul.toIsRightCancelMul
❌ ofNat_zsmul <- ✅ zpow_ofNat
❌ AddCon.lift_funext <- ✅ Con.lift_funext
❌ FreeAddMonoid.toList_map <- ✅ FreeMonoid.toList_map
❌ FreeAddMonoid.mkAddAction <- ✅ FreeMonoid.mkMulAction
❌ lt_neg_iff_add_neg' <- ✅ lt_inv_iff_mul_lt_one'
❌ map_zsmul <- ✅ map_zpow
❌ vaddCommClass_self <- ✅ smulCommClass_self
❌ zero_vadd <- ✅ one_smul
❌ LatticeOrderedCommGroup.sup_sub_inf_eq_abs_sub <- ✅ LatticeOrderedCommGroup.sup_div_inf_eq_abs_div
❌ Left.neg_neg_iff <- ✅ Left.inv_lt_one_iff
❌ Set.singleton_sub_singleton <- ✅ Set.singleton_div_singleton
❌ Set.preimage_vadd <- ✅ Set.preimage_smul
❌ Set.addCommMonoid <- ✅ Set.commMonoid
❌ Set.vaddCommClass_set <- ✅ Set.smulCommClass_set
❌ vaddZeroHom <- ✅ smulOneHom
❌ zsmul_nonneg <- ✅ one_le_zpow
❌ LatticeOrderedCommGroup.pos_eq_self_of_pos_pos <- ✅ LatticeOrderedCommGroup.pos_eq_self_of_one_lt_pos
❌ Set.vadd_set_union <- ✅ Set.smul_set_union
❌ OrderMonoidHom.comp_apply -> ✅ OrderAddMonoidHom.comp_apply
❌ AddSubmonoid.zero_mem <- ✅ Submonoid.one_mem
❌ Set.empty_sub <- ✅ Set.empty_div
❌ Part.right_dom_of_sub_dom <- ✅ Part.right_dom_of_div_dom
❌ Set.preimage_vadd_neg <- ✅ Set.preimage_smul_inv
❌ max_le_add_of_nonneg <- ✅ max_le_mul_of_one_le
❌ Set.sub_subset_sub <- ✅ Set.div_subset_div
❌ Left.self_lt_neg <- ✅ Left.self_lt_inv
❌ FreeAddMonoid.ofList_join <- ✅ FreeMonoid.ofList_join
❌ Set.singletonAddHom <- ✅ Set.singletonMulHom
❌ max_add_add_left <- ✅ max_mul_mul_left
❌ smul_eq_zero_iff <- ✅ pow_eq_one_iff
❌ IsAddHom.id <- ✅ IsMulHom.id
❌ add_neg_lt_add_neg_iff <- ✅ mul_inv_lt_mul_inv_iff'
❌ Pi.orderedAddCommMonoid <- ✅ Pi.orderedCommMonoid
❌ neg_nonpos_of_nonneg <- ✅ inv_le_one_of_one_le
❌ AddCon.addCommSemigroup <- ✅ Con.commSemigroup
❌ csupᵢ_add_le <- ✅ csupᵢ_mul_le
❌ Set.mem_neg_vadd_set_iff <- ✅ Set.mem_inv_smul_set_iff
❌ nsmul_le_nsmul_of_le_right <- ✅ pow_le_pow_of_le_left'
❌ IsAddGroupHom.neg <- ✅ IsGroupHom.inv
❌ Neg.isAddGroupHom <- ✅ Inv.isGroupHom
❌ Set.add_image_prod <- ✅ Set.image_smul_prod
❌ AddCommute.list_sum_left <- ✅ Commute.list_prod_left
❌ nsmul_le_nsmul <- ✅ pow_le_pow'
❌ sub_lt_sub_iff <- ✅ div_lt_div_iff'
❌ AddSubmonoid.mem_mk <- ✅ Submonoid.mem_mk
❌ map_multiset_sum <- ✅ map_multiset_prod
❌ Part.neg_some <- ✅ Part.inv_some
❌ AddSemiconjBy.function_semiconj_add_right_swap <- ✅ SemiconjBy.function_semiconj_mul_right_swap
❌ Set.coe_singletonAddMonoidHom <- ✅ Set.coe_singletonMonoidHom
❌ List.length_pos_of_sum_ne_zero <- ✅ List.length_pos_of_prod_ne_one
❌ Set.addAction <- ✅ Set.mulAction
❌ Set.piecewise_vadd <- ✅ Set.piecewise_smul
❌ WithTop.coe_lt_zero <- ✅ WithTop.coe_lt_one
❌ Right.neg_le_self <- ✅ Right.inv_le_self
❌ LatticeOrderedCommGroup.pos_part_def <- ✅ LatticeOrderedCommGroup.m_pos_part_def
❌ LatticeOrderedCommGroup.pos_nonpos_iff <- ✅ LatticeOrderedCommGroup.pos_le_one_iff
❌ Set.vadd_set_sdiff <- ✅ Set.smul_set_sdiff
❌ Set.image2_add <- ✅ Set.image2_mul
❌ Set.vaddCommClass_set' <- ✅ Set.smulCommClass_set'
❌ VAddCommClass.opposite_mid <- ✅ SMulCommClass.opposite_mid
❌ arrowAddAction <- ✅ arrowAction
❌ AddMonoidHom.ofMapAddNeg <- ✅ MonoidHom.ofMapMulInv
❌ VAdd.comp.isScalarTower <- ✅ SMul.comp.isScalarTower
❌ Set.union_vadd <- ✅ Set.union_smul
❌ neg_le_neg_iff <- ✅ inv_le_inv_iff
❌ Set.preimage_add_right_singleton <- ✅ Set.preimage_mul_right_singleton
❌ AddCommGroup.ext <- ✅ CommGroup.ext
❌ vadd_ite <- ✅ smul_ite
❌ FreeAddMonoid.toList_symm <- ✅ FreeMonoid.toList_symm
❌ AddMonoidHom.of <- ✅ MonoidHom.of
❌ Multiset.sum_induction_nonempty <- ✅ Multiset.prod_induction_nonempty
❌ Set.Nonempty.vadd_set <- ✅ Set.Nonempty.smul_set
❌ List.sum_set' <- ✅ List.prod_set'
❌ vadd_pi <- ✅ smul_pi
❌ LatticeOrderedCommGroup.neg_eq_neg_inf_zero <- ✅ LatticeOrderedCommGroup.neg_eq_inv_inf_one
❌ AddCon.coe_vadd <- ✅ Con.coe_smul
❌ AddCon.addMonoid <- ✅ Con.monoid
❌ Monotone.neg <- ✅ Monotone.inv
❌ List.sum_concat <- ✅ List.prod_concat
❌ AddCon.lift_unique <- ✅ Con.lift_unique
❌ Sum.vadd_def <- ✅ Sum.smul_def
❌ List.sum_singleton <- ✅ List.prod_singleton
❌ Prod.smul <- ✅ Prod.pow
❌ add_sup <- ✅ mul_sup
❌ Sigma.FaithfulVAdd' <- ✅ Sigma.FaithfulSMul'
❌ Set.isAddUnit_singleton <- ✅ Set.isUnit_singleton
❌ Set.bddAbove_add <- ✅ Set.bddAbove_mul
❌ AddSubmonoid.mem_carrier <- ✅ Submonoid.mem_carrier
❌ neg_inf_eq_sup_neg <- ✅ inv_inf_eq_sup_inv
❌ LatticeOrderedCommGroup.neg_eq_zero_iff <- ✅ LatticeOrderedCommGroup.neg_eq_one_iff
❌ FreeAddMonoid.ofList <- ✅ FreeMonoid.ofList
❌ LatticeOrderedCommGroup.pos_zero <- ✅ LatticeOrderedCommGroup.pos_one
❌ AddCommute.vadd_right <- ✅ Commute.smul_right
❌ IsAddMonoidHom.id <- ✅ IsMonoidHom.id
❌ List.sum_eq_zero_iff <- ✅ List.prod_eq_one_iff
❌ LatticeOrderedCommGroup.neg_of_inv_nonneg <- ✅ LatticeOrderedCommGroup.neg_of_one_le_inv
❌ LatticeOrderedCommGroup.hasZeroLatticeHasPosPart <- ✅ LatticeOrderedCommGroup.hasOneLatticeHasPosPart
❌ AddRightCancelMonoid.toAddMonoid_injective <- ✅ RightCancelMonoid.toMonoid_injective
❌ Multiset.sum_map_zsmul <- ✅ Multiset.prod_map_zpow
❌ VAddCommClass.op_right <- ✅ SMulCommClass.op_right
❌ AntitoneOn.neg <- ✅ AntitoneOn.inv
❌ Set.image2_vadd <- ✅ Set.image2_smul
❌ IsAddGroupHom.comp <- ✅ IsGroupHom.comp
❌ lt_sub_comm <- ✅ lt_div_comm
❌ ZeroHom.withBotMap <- ✅ OneHom.withBotMap
❌ AddMonoidHom.compHom <- ✅ MonoidHom.compHom
❌ neg_lt_neg <- ✅ inv_lt_inv'
❌ sub_le_sub_iff_right <- ✅ div_le_div_iff_right
❌ FreeAddMonoid.casesOn_zero <- ✅ FreeMonoid.casesOn_one
❌ AddAction.toPerm_injective <- ✅ MulAction.toPerm_injective
❌ Set.singletonAddHom_apply <- ✅ Set.singletonMulHom_apply
❌ AddCon.ker <- ✅ Con.ker
❌ neg_neg_of_pos <- ✅ inv_lt_one_of_one_lt
❌ Set.preimage_add_right_zero <- ✅ Set.preimage_mul_right_one
❌ AddMonoidHom.ofClosureMEqTopRight <- ✅ MonoidHom.ofClosureMEqTopRight
❌ List.sum_isAddUnit <- ✅ List.prod_isUnit
❌ AddSubmonoid.supᵢ_eq_closure <- ✅ Submonoid.supᵢ_eq_closure
❌ VAdd.comp.vadd <- ✅ SMul.comp.smul
❌ AddCommSemigroup.IsLeftCancelAdd.toIsCancelAdd <- ✅ CommSemigroup.IsLeftCancelMul.toIsCancelMul
❌ sub_lt_sub_iff_right <- ✅ div_lt_div_iff_right
❌ Set.zero_subset <- ✅ Set.one_subset
❌ AddSubsemigroup.mem_supₛ_of_directed_on <- ✅ Subsemigroup.mem_supₛ_of_directed_on
❌ min_le_add_of_nonneg_left <- ✅ min_le_mul_of_one_le_left
❌ Multiset.sum_le_sum_of_rel_le <- ✅ Multiset.prod_le_prod_of_rel_le
❌ Set.add_subset_iff <- ✅ Set.mul_subset_iff
❌ le_iff_forall_pos_lt_add <- ✅ le_iff_forall_one_lt_lt_mul
❌ List.monotone_sum_take <- ✅ List.monotone_prod_take
❌ AddSubmonoid.copy_eq <- ✅ Submonoid.copy_eq
❌ Set.coe_singletonAddHom <- ✅ Set.coe_singletonMulHom
❌ MonotoneOn.neg <- ✅ MonotoneOn.inv
❌ neg_lt_iff_pos_add <- ✅ inv_lt_iff_one_lt_mul
❌ neg_lt_iff_pos_add' <- ✅ inv_lt_iff_one_lt_mul'
❌ AddCommGroup.toAddGroup_injective <- ✅ CommGroup.toGroup_injective
❌ AddCon.ker_eq_lift_of_injective <- ✅ Con.ker_eq_lift_of_injective
❌ Set.unionᵢ_vadd <- ✅ Set.unionᵢ_smul
❌ AddSubmonoid.mk_le_mk <- ✅ Submonoid.mk_le_mk
❌ StrictMonoOn.neg <- ✅ StrictMonoOn.inv
❌ neg_le_sub_iff_le_add' <- ✅ inv_le_div_iff_le_mul'
❌ LatticeOrderedCommGroup.abs_sup_sub_sup_le_abs <- ✅ LatticeOrderedCommGroup.mabs_sup_div_sup_le_mabs
❌ LatticeOrderedCommGroup.neg_eq_zero_iff' <- ✅ LatticeOrderedCommGroup.neg_eq_one_iff'
❌ Set.subtractionCommMonoid <- ✅ Set.divisionCommMonoid
❌ Set.vadd_univ <- ✅ Set.smul_univ
❌ vadd_zero_vadd <- ✅ smul_one_smul
❌ ULift.addCancelCommMonoid <- ✅ ULift.cancelCommMonoid
❌ Set.vadd_nonempty <- ✅ Set.smul_nonempty
❌ FreeAddMonoid.ofList_singleton <- ✅ FreeMonoid.ofList_singleton
❌ Set.vadd_set_univ <- ✅ Set.smul_set_univ
❌ min_add_distrib <- ✅ min_mul_distrib
❌ AddCon.comap_eq <- ✅ Con.comap_eq
❌ StrictAnti.neg <- ✅ StrictAnti.inv
❌ Left.neg_nonpos_iff <- ✅ Left.inv_le_one_iff
❌ Set.vadd_set_singleton <- ✅ Set.smul_set_singleton
❌ Set.image_add_left' <- ✅ Set.image_mul_left'
❌ neg_add_lt_iff_lt_add <- ✅ inv_mul_lt_iff_lt_mul
❌ Set.subtractionMonoid <- ✅ Set.divisionMonoid
❌ List.all_zero_of_le_zero_le_of_sum_eq_zero <- ✅ List.all_one_of_le_one_le_of_prod_eq_one
❌ Multiset.sum_map_le_sum_map <- ✅ Multiset.prod_map_le_prod_map
❌ Set.vadd_set_range <- ✅ Set.smul_set_range
❌ Set.sub_unionᵢ₂ <- ✅ Set.div_unionᵢ₂
❌ List.exists_le_of_sum_le <- ✅ List.exists_le_of_prod_le'
❌ FreeAddMonoid.toList <- ✅ FreeMonoid.toList
❌ sub_le_sub_left <- ✅ div_le_div_left'
❌ LinearOrderedAddCommGroup.to_covariantClass <- ✅ LinearOrderedCommGroup.to_covariantClass
❌ List.alternatingSum_cons_cons' <- ✅ List.alternatingProd_cons_cons'
❌ Set.image_op_neg <- ✅ Set.image_op_inv
❌ Multiset.smul_count <- ✅ Multiset.pow_count
❌ ite_add <- ✅ ite_mul
❌ List.alternatingSum_cons' <- ✅ List.alternatingProd_cons'
❌ AddGroup.ext <- ✅ Group.ext
❌ AddMonoidHom.isAddMonoidHom_coe <- ✅ MonoidHom.isMonoidHom_coe
❌ Set.neg_mem_Ioo_iff <- ✅ Set.inv_mem_Ioo_iff
❌ EckmannHilton.AddZeroClass.IsUnital <- ✅ EckmannHilton.MulOneClass.isUnital
❌ AddMonoid.toOppositeAddAction <- ✅ Monoid.toOppositeMulAction
❌ AddSubmonoid.closure_unionᵢ <- ✅ Submonoid.closure_unionᵢ
❌ VAddCommClass.of_add_vadd_zero <- ✅ SMulCommClass.of_mul_smul_one
❌ AddEquiv.isAddMonoidHom <- ✅ MulEquiv.isMonoidHom
❌ AddCon.to_addSubmonoid_inj <- ✅ Con.to_submonoid_inj
❌ List.sum_reverse <- ✅ List.prod_reverse
❌ AddMonoidHom.eval <- ✅ MonoidHom.eval
❌ AddCon.coe_mk' <- ✅ Con.coe_mk'
❌ le_iff_exists_add' <- ✅ le_iff_exists_mul'
❌ Set.unionᵢ_sub_right_image <- ✅ Set.unionᵢ_div_right_image
❌ nsmul_neg <- ✅ pow_lt_one'
❌ LatticeOrderedCommGroup.pos_add_neg <- ✅ LatticeOrderedCommGroup.pos_mul_neg
❌ AddMonoidHom.compHom' <- ✅ MonoidHom.compHom'
❌ LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub <- ✅ LatticeOrderedCommGroup.inf_sq_eq_mul_div_abs_div
❌ Function.Injective.cancelMonoid -> ✅ Function.Injective.addCancelMonoid
❌ neg_le_iff_add_nonneg' <- ✅ inv_le_iff_one_le_mul'
❌ Multiset.sum_map_sub <- ✅ Multiset.prod_map_div
❌ Right.pow_neg <- ✅ Right.pow_lt_one_of_lt
❌ sub_lt_comm <- ✅ div_lt_comm
❌ Set.empty_add <- ✅ Set.empty_mul
❌ min_add_max <- ✅ min_mul_max
❌ FreeAddMonoid.of <- ✅ FreeMonoid.of
❌ AddSubmonoid.closure <- ✅ Submonoid.closure
❌ FreeAddMonoid.casesOn <- ✅ FreeMonoid.casesOn
❌ AddMonoidHom.coe_ofClosureMEqTopRight <- ✅ MonoidHom.coe_ofClosureMEqTopRight
❌ FreeAddMonoid.hom_map_lift <- ✅ FreeMonoid.hom_map_lift
❌ Set.vadd_union <- ✅ Set.smul_union
❌ smul_neg_iff <- ✅ pow_lt_one_iff
❌ LatticeOrderedCommGroup.abs_nonneg <- ✅ LatticeOrderedCommGroup.one_le_abs
❌ List.sum_add_sum_eq_sum_zipWith_of_length_eq <- ✅ List.prod_mul_prod_eq_prod_zipWith_of_length_eq
❌ sub_lt_sub_iff_left <- ✅ div_lt_div_iff_left
❌ Set.unionᵢ_add <- ✅ Set.unionᵢ_mul
❌ AddSubsemigroup.mem_supᵢ_of_mem <- ✅ Subsemigroup.mem_supᵢ_of_mem
❌ IsAddUnit.vadd_left_cancel <- ✅ IsUnit.smul_left_cancel
❌ Pi.orderedAddCommGroup <- ✅ Pi.orderedCommGroup
❌ Right.pow_nonpos <- ✅ Right.pow_le_one_of_le
❌ le_of_forall_pos_lt_add' <- ✅ le_of_forall_one_lt_lt_mul'
❌ add_eq_zero_iff <- ✅ mul_eq_one_iff
❌ neg_add_lt_iff_lt_add' <- ✅ inv_mul_lt_iff_lt_mul'
❌ Sum.vadd_swap <- ✅ Sum.smul_swap
❌ neg_add_neg_iff_lt <- ✅ inv_mul_lt_one_iff_lt
❌ Right.self_lt_neg <- ✅ Right.self_lt_inv
❌ LatticeOrderedCommGroup.neg_of_neg_nonpos <- ✅ LatticeOrderedCommGroup.neg_of_inv_le_one
❌ AddUnits.mk_val <- ✅ Units.mk_val
❌ nsmul_nonneg_iff <- ✅ one_le_pow_iff
❌ Set.vadd_inter_subset <- ✅ Set.smul_inter_subset
❌ Multiset.le_sum_nonempty_of_subadditive_on_pred <- ✅ Multiset.le_prod_nonempty_of_submultiplicative_on_pred
❌ List.sum_nil <- ✅ List.prod_nil
❌ IsAddGroupHom.map_sub <- ✅ IsGroupHom.map_div
❌ Multiset.sum_hom <- ✅ Multiset.prod_hom
❌ FreeAddMonoid.lift_symm_apply <- ✅ FreeMonoid.lift_symm_apply
❌ nsmul_strictMono_right <- ✅ pow_strictMono_left
❌ List.sum_nonneg <- ✅ List.one_le_prod_of_one_le
❌ AddSemiconjBy.map <- ✅ SemiconjBy.map
❌ Set.unionᵢ_add_right_image <- ✅ Set.unionᵢ_mul_right_image
❌ LinearOrderedAddCommGroup.to_noMinOrder <- ✅ LinearOrderedCommGroup.to_noMinOrder
❌ vadd_zero_add <- ✅ smul_one_mul
❌ Set.subset_set_vadd_iff <- ✅ Set.subset_set_smul_iff
❌ Multiset.sum_eq_zero_iff <- ✅ Multiset.prod_eq_one_iff
❌ Set.unionᵢ_sub <- ✅ Set.unionᵢ_div
❌ Multiset.sum_map_eq_smul_single <- ✅ Multiset.prod_map_eq_pow_single
❌ FreeAddMonoid.recOn <- ✅ FreeMonoid.recOn
❌ LatticeOrderedCommGroup.abs_abs <- ✅ LatticeOrderedCommGroup.mabs_mabs
❌ AddCommSemigroup.to_isCommutative <- ✅ CommSemigroup.to_isCommutative
❌ Add.toVAdd <- ✅ Mul.toSMul
❌ AddSubmonoid.closure_empty <- ✅ Submonoid.closure_empty
❌ le_add_left <- ✅ le_mul_left
❌ FreeAddMonoid.map_id <- ✅ FreeMonoid.map_id
❌ Multiset.sum_add <- ✅ Multiset.prod_add
❌ AddOpposite.op_sub <- ✅ MulOpposite.op_div
❌ Set.vadd_set_nonempty <- ✅ Set.smul_set_nonempty
❌ AddCon.quotientKerEquivRange <- ✅ Con.quotientKerEquivRange
❌ Set.neg <- ✅ Set.inv
❌ AddCon.comapQuotientEquiv <- ✅ Con.comapQuotientEquiv
❌ LatticeOrderedCommGroup.le_iff_pos_le_neg_ge <- ✅ LatticeOrderedCommGroup.m_le_iff_pos_le_neg_ge
❌ Set.unionᵢ_vadd_left_image <- ✅ Set.unionᵢ_smul_left_image
❌ AddSubsemigroup.mem_sup_right <- ✅ Subsemigroup.mem_sup_right
❌ AddSemiconjBy.add_right <- ✅ SemiconjBy.mul_right
❌ AddMonoidHom.compr₂ <- ✅ MonoidHom.compr₂
❌ smul_mem <- ✅ pow_mem
❌ Set.image_add_left <- ✅ Set.image_mul_left
❌ Set.union_sub <- ✅ Set.union_div
❌ sub_le_iff_le_add' <- ✅ div_le_iff_le_mul'
❌ List.sum_eq_foldr <- ✅ List.prod_eq_foldr
❌ OneHom.map_one' -> ✅ ZeroHom.map_zero'
❌ vadd_univ_pi <- ✅ smul_univ_pi
❌ min_sub_sub_right <- ✅ min_div_div_right'
❌ Set.subset_add_right <- ✅ Set.subset_mul_right
❌ Part.some_add_some <- ✅ Part.some_mul_some
❌ LatticeOrderedCommGroup.neg_abs <- ✅ LatticeOrderedCommGroup.m_neg_abs
❌ LatticeOrderedCommGroup.neg_le_abs <- ✅ LatticeOrderedCommGroup.inv_le_abs
❌ comp_vadd_left <- ✅ comp_smul_left
❌ AddCon.lift_mk' <- ✅ Con.lift_mk'
❌ Function.Injective.orderedAddCommMonoid <- ✅ Function.Injective.orderedCommMonoid
❌ List.sum_hom <- ✅ List.prod_hom
❌ AddSubmonoid.subsingleton_iff <- ✅ Submonoid.subsingleton_iff
❌ AddCon.lift_coe <- ✅ Con.lift_coe
❌ Set.neg_subset_neg <- ✅ Set.inv_subset_inv
❌ Set.interᵢ_add_subset <- ✅ Set.interᵢ_mul_subset
❌ AddCon.lift_apply_mk' <- ✅ Con.lift_apply_mk'
❌ Set.addCommSemigroup <- ✅ Set.commSemigroup
❌ Set.add_nonempty <- ✅ Set.mul_nonempty
❌ WithBot.coe_zero <- ✅ WithBot.coe_one
❌ Multiset.sum_erase <- ✅ Multiset.prod_erase
❌ WithTop.zero_eq_coe <- ✅ WithTop.one_eq_coe
❌ LatticeOrderedCommGroup.abs_abs_sub_abs_le <- ✅ LatticeOrderedCommGroup.abs_abs_div_abs_le
❌ AddCon.Quotient.inhabited <- ✅ Con.Quotient.inhabited
❌ Set.add_subset_add_left <- ✅ Set.mul_subset_mul_left
❌ AddSubmonoid.closure_induction <- ✅ Submonoid.closure_induction
❌ add_pos_iff <- ✅ one_lt_mul_iff
❌ AddMonoid.toAddAction <- ✅ Monoid.toMulAction
❌ Set.unionᵢ₂_vadd <- ✅ Set.unionᵢ₂_smul
❌ Part.some_sub_some <- ✅ Part.some_div_some
❌ OrderedAddCommGroup.to_covariantClass_left_le <- ✅ OrderedCommGroup.to_covariantClass_left_le
❌ add_inf <- ✅ mul_inf
❌ AddSubmonoid.coe_copy <- ✅ Submonoid.coe_copy
❌ AddCommute.map <- ✅ Commute.map
❌ Left.pow_nonneg <- ✅ Left.one_le_pow_of_le
❌ OrderedAddCommGroup.to_contravariantClass_right_le <- ✅ OrderedCommGroup.to_contravariantClass_right_le
❌ AddLeftCancelMonoid.toAddMonoid_injective <- ✅ LeftCancelMonoid.toMonoid_injective
❌ add_neg_nonpos_iff_le <- ✅ mul_inv_le_one_iff_le
❌ Set.nonempty_neg <- ✅ Set.nonempty_inv
❌ add_csupᵢ_le <- ✅ mul_csupᵢ_le
❌ Con.instPowQuotientToMulToMulOneClassNat -> ✅ AddCon.Quotient.nsmul
❌ Set.add_interᵢ_subset <- ✅ Set.mul_interᵢ_subset
❌ Set.Nonempty.of_vadd_left <- ✅ Set.Nonempty.of_smul_left
❌ le_map_add_map_sub <- ✅ le_map_mul_map_div
❌ AddCon.mk'_ker <- ✅ Con.mk'_ker
❌ AddCon.hasNeg <- ✅ Con.hasInv
❌ Set.neg_subset <- ✅ Set.inv_subset
❌ min_add_add_right <- ✅ min_mul_mul_right
❌ Set.neg_univ <- ✅ Set.inv_univ
❌ Set.zero_mem_sub_iff <- ✅ Set.one_mem_div_iff
❌ Set.vadd_set_eq_empty <- ✅ Set.smul_set_eq_empty
❌ Set.preimage_add_left_singleton <- ✅ Set.preimage_mul_left_singleton
❌ AddMonoidHom.map_zsmul' <- ✅ MonoidHom.map_zpow'
❌ Set.vadd_singleton <- ✅ Set.smul_singleton
❌ Multiset.sum_le_sum_map <- ✅ Multiset.prod_le_prod_map
❌ LatticeOrderedCommGroup.neg_le_neg <- ✅ LatticeOrderedCommGroup.inv_le_neg
❌ Function.Injective.linearOrderedAddCommGroup <- ✅ Function.Injective.linearOrderedCommGroup
❌ Set.vadd_subset_vadd <- ✅ Set.smul_subset_smul
❌ nsmul_pos_iff <- ✅ one_lt_pow_iff
❌ Set.neg_singleton <- ✅ Set.inv_singleton
❌ nonpos_iff_eq_zero <- ✅ le_one_iff_eq_one
❌ ite_vadd <- ✅ ite_smul
❌ Set.sub_subset_iff <- ✅ Set.div_subset_iff
❌ neg_nonneg_of_nonpos <- ✅ one_le_inv_of_le_one
❌ add_vadd_comm <- ✅ mul_smul_comm
❌ Set.preimage_add_right_zero' <- ✅ Set.preimage_mul_right_one'
❌ sub_neg <- ✅ div_lt_one'
❌ AddOpposite.unop_injective <- ✅ MulOpposite.unop_injective
❌ AddSubmonoid.closure_union <- ✅ Submonoid.closure_union
❌ AddCon.lift_range <- ✅ Con.lift_range
❌ Set.addActionSet <- ✅ Set.mulActionSet
❌ AddSubsemigroup.equivMapOfInjective <- ✅ Subsemigroup.equivMapOfInjective
❌ LatticeOrderedCommGroup.pos_of_nonpos <- ✅ LatticeOrderedCommGroup.pos_of_le_one
❌ Set.neg_insert <- ✅ Set.inv_insert
❌ AddSubmonoid.gi <- ✅ Submonoid.gi
❌ Multiset.sum_map_sum_map <- ✅ Multiset.prod_map_prod_map
❌ instVAddLex' <- ✅ instSMulLex'
❌ Set.univ_add_of_zero_mem <- ✅ Set.univ_mul_of_one_mem
❌ Set.nsmul_subset_nsmul <- ✅ Set.pow_subset_pow
❌ Set.image_sub <- ✅ Set.image_div
❌ VAddAssocClass.op_left <- ✅ IsScalarTower.op_left
❌ AddCon.quotientQuotientEquivQuotient <- ✅ Con.quotientQuotientEquivQuotient
❌ AddMonoidHom.ext_iff₂ <- ✅ MonoidHom.ext_iff₂
❌ Set.sub <- ✅ Set.div
❌ AddSubmonoid.mem_infₛ <- ✅ Submonoid.mem_infₛ
❌ AddCon.map_apply <- ✅ Con.map_apply
❌ neg_lt_sub_iff_lt_add <- ✅ inv_lt_div_iff_lt_mul
❌ smul_nonpos_iff <- ✅ pow_le_one_iff
❌ Set.add_empty <- ✅ Set.mul_empty
❌ WithZero.neg <- ✅ WithOne.inv
❌ sub_le_sub_flip <- ✅ div_le_div_flip
❌ Set.vadd_subset_vadd_right <- ✅ Set.smul_subset_smul_right
❌ AddCon.kerLift_injective <- ✅ Con.kerLift_injective
❌ FreeAddMonoid.vadd_def <- ✅ FreeMonoid.smul_def
❌ AddSubsemigroup.supᵢ_induction' <- ✅ Subsemigroup.supᵢ_induction'
❌ Set.neg_mem_Icc_iff <- ✅ Set.inv_mem_Icc_iff
❌ Set.unionᵢ_vadd_set <- ✅ Set.unionᵢ_smul_set
❌ Set.unionᵢ₂_add <- ✅ Set.unionᵢ₂_mul
❌ Set.vadd_mem_vadd_set_iff <- ✅ Set.smul_mem_smul_set_iff
❌ Part.right_dom_of_add_dom <- ✅ Part.right_dom_of_mul_dom
❌ AddCon.addAction <- ✅ Con.mulAction
❌ le_self_add <- ✅ le_self_mul
❌ Set.mem_vadd_set_iff_neg_vadd_mem <- ✅ Set.mem_smul_set_iff_inv_smul_mem
❌ FreeAddMonoid.lift_apply <- ✅ FreeMonoid.lift_apply
❌ Multiset.le_sum_of_subadditive_on_pred <- ✅ Multiset.le_prod_of_submultiplicative_on_pred
❌ neg_le_neg <- ✅ inv_le_inv'
❌ List.Sublist.sum_le_sum <- ✅ List.Sublist.prod_le_prod'
❌ AddSubmonoid.coe_infₛ <- ✅ Submonoid.coe_infₛ
❌ AddMonoidHom.map_multiset_sum <- ✅ MonoidHom.map_multiset_prod
❌ vadd_eq_add <- ✅ smul_eq_mul
❌ IsAddGroupHom.map_neg <- ✅ IsGroupHom.map_inv
❌ LinearOrderedAddCommGroup.to_noMaxOrder <- ✅ LinearOrderedCommGroup.to_noMaxOrder
❌ Part.sub_mem_sub <- ✅ Part.div_mem_div
❌ AddSubmonoid.closure_induction₂ <- ✅ Submonoid.closure_induction₂
❌ neg_lt_sub_iff_lt_add' <- ✅ inv_lt_div_iff_lt_mul'
❌ vadd_eq_iff_eq_neg_vadd <- ✅ smul_eq_iff_eq_inv_smul
❌ ZeroHom.withTopMap <- ✅ OneHom.withTopMap
❌ cmp_sub_zero <- ✅ cmp_div_one'
❌ IsAddGroupHom.add <- ✅ IsGroupHom.mul
❌ AddUnits.val_lt_val <- ✅ Units.val_lt_val
❌ OrderEmbedding.addLeft <- ✅ OrderEmbedding.mulLeft
❌ Right.neg_lt_self <- ✅ Right.inv_lt_self
❌ sub_le_sub_iff_left <- ✅ div_le_div_iff_left
❌ Left.neg_lt_self <- ✅ Left.inv_lt_self
❌ List.sum_hom₂ <- ✅ List.prod_hom₂
❌ sub_le_iff_le_add <- ✅ div_le_iff_le_mul
❌ le_of_forall_pos_sub_le <- ✅ le_of_forall_one_lt_div_le
❌ Set.add <- ✅ Set.mul
❌ Multiset.le_sum_of_subadditive <- ✅ Multiset.le_prod_of_submultiplicative
❌ AddCancelCommMonoid.ext <- ✅ CancelCommMonoid.ext
❌ Set.add_univ_of_zero_mem <- ✅ Set.mul_univ_of_one_mem
❌ AddAction.toFun <- ✅ MulAction.toFun
❌ Set.pairwiseDisjoint_vadd_iff <- ✅ Set.pairwiseDisjoint_smul_iff
❌ zero_le <- ✅ one_le
❌ LatticeOrderedCommGroup.abs_add_le <- ✅ LatticeOrderedCommGroup.mabs_mul_le
❌ Set.vaddCommClass_set'' <- ✅ Set.smulCommClass_set''
❌ Set.Nonempty.of_vadd_right <- ✅ Set.Nonempty.of_smul_right
❌ FreeAddMonoid.map_comp <- ✅ FreeMonoid.map_comp
❌ LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice <- ✅ LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice
❌ Set.vadd_set_Union <- ✅ Set.smul_set_Union
❌ AddSubmonoid.coe_set_mk <- ✅ Submonoid.coe_set_mk
❌ AddMonoidHom.flip <- ✅ MonoidHom.flip
❌ AddCon.lift <- ✅ Con.lift
❌ Set.empty_vadd <- ✅ Set.empty_smul
❌ AddSubmonoid.mem_inf <- ✅ Submonoid.mem_inf
❌ AddSubmonoid.disjoint_def' <- ✅ Submonoid.disjoint_def'
❌ Set.unionᵢ_neg <- ✅ Set.unionᵢ_inv
❌ LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub <- ✅ LatticeOrderedCommGroup.sup_sq_eq_mul_mul_abs_div
❌ FreeAddMonoid.ofList_comp_toList <- ✅ FreeMonoid.ofList_comp_toList
❌ LatticeOrderedCommGroup.abs_inf_sub_inf_le_abs <- ✅ LatticeOrderedCommGroup.mabs_inf_div_inf_le_mabs
❌ Set.vadd_unionᵢ₂ <- ✅ Set.smul_unionᵢ₂
❌ Left.nonneg_neg_iff <- ✅ Left.one_le_inv_iff
❌ List.sum_drop_succ <- ✅ List.prod_drop_succ
❌ AddSubmonoid.closure_induction' <- ✅ Submonoid.closure_induction'
❌ LatticeOrderedCommGroup.pos_inf_neg_eq_zero <- ✅ LatticeOrderedCommGroup.pos_inf_neg_eq_one
❌ Set.add_interᵢ₂_subset <- ✅ Set.mul_interᵢ₂_subset
❌ le_iff_exists_add <- ✅ le_iff_exists_mul
❌ Option.vadd_none <- ✅ Option.smul_none
❌ AddAction.exists_vadd_eq <- ✅ MulAction.exists_smul_eq
❌ Multiset.coe_sum <- ✅ Multiset.coe_prod
❌ AddMonoidHom.compr₂_apply <- ✅ MonoidHom.compr₂_apply
❌ Multiset.sum_pair <- ✅ Multiset.prod_pair
❌ AddEquiv.coe_toAddHom <- ✅ MulEquiv.coe_toMulHom
❌ Set.isAddUnit_iff_singleton <- ✅ Set.isUnit_iff_singleton
❌ Set.neg_preimage <- ✅ Set.inv_preimage
❌ List.sum_cons <- ✅ List.prod_cons
❌ Multiset.sum_eq_zero <- ✅ Multiset.prod_eq_one
❌ neg_le_sub_iff_le_add <- ✅ inv_le_div_iff_le_mul
❌ Fintype.decidableEqAddMonoidHomFintype <- ✅ Fintype.decidableEqMonoidHomFintype
❌ AddMonoidHom.flip_apply <- ✅ MonoidHom.flip_apply
❌ lt_neg_iff_add_neg <- ✅ lt_inv_iff_mul_lt_one
❌ AddSubmonoid.disjoint_def <- ✅ Submonoid.disjoint_def
❌ min_neg_neg <- ✅ min_inv_inv'
❌ lt_neg_add_iff_add_lt <- ✅ lt_inv_mul_iff_mul_lt
❌ Set.sub_interᵢ_subset <- ✅ Set.div_interᵢ_subset
❌ Set.image_neg <- ✅ Set.image_inv
❌ LatticeOrderedCommGroup.le_abs <- ✅ LatticeOrderedCommGroup.le_mabs
❌ Multiset.le_sum_nonempty_of_subadditive <- ✅ Multiset.le_prod_nonempty_of_submultiplicative
❌ AddSubmonoid.subset_closure <- ✅ Submonoid.subset_closure
❌ Set.zero_mem_zero <- ✅ Set.one_mem_one
❌ zero_vadd_eq_id <- ✅ one_smul_eq_id
❌ Set.vaddSet <- ✅ Set.smulSet
❌ FreeAddMonoid.map_of <- ✅ FreeMonoid.map_of
❌ AddCon.map <- ✅ Con.map
❌ AddRightCancelSemigroup.toIsRightCancelAdd <- ✅ RightCancelSemigroup.toIsRightCancelMul
❌ add_neg_le_neg_add_iff <- ✅ mul_inv_le_inv_mul_iff
❌ Function.extend_vadd <- ✅ Function.extend_smul
❌ Part.sub_get_eq <- ✅ Part.div_get_eq
❌ Antitone.neg <- ✅ Antitone.inv
❌ AddSubmonoid.Simps.coe <- ✅ Submonoid.Simps.coe
❌ add_neg_lt_neg_add_iff <- ✅ mul_inv_lt_inv_mul_iff
❌ Set.singleton_add <- ✅ Set.singleton_mul
❌ List.sum_add_sum_eq_sum_zipWith_add_sum_drop <- ✅ List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop
❌ Set.vadd_set_symm_diff <- ✅ Set.smul_set_symm_diff
❌ AddCon.mrange_mk' <- ✅ Con.mrange_mk'
❌ Left.pow_nonpos <- ✅ Left.pow_le_one_of_le
❌ LatticeOrderedCommGroup.neg_part_def <- ✅ LatticeOrderedCommGroup.m_neg_part_def
❌ List.sum_replicate <- ✅ List.prod_replicate
❌ Set.add_union <- ✅ Set.mul_union
❌ neg_add_le_iff_le_add <- ✅ inv_mul_le_iff_le_mul
❌ Multiset.sum_le_card_nsmul <- ✅ Multiset.prod_le_pow_card
❌ AddMonoidHom.eqLocusM <- ✅ MonoidHom.eqLocusM
❌ AddSubmonoid.mem_infᵢ <- ✅ Submonoid.mem_infᵢ
❌ Set.subset_zero_iff_eq <- ✅ Set.subset_one_iff_eq
❌ List.sum_le_card_nsmul <- ✅ List.prod_le_pow_card
❌ Multiset.single_le_sum <- ✅ Multiset.single_le_prod
❌ AddAction.injective <- ✅ MulAction.injective
❌ FreeAddMonoid.ofList_map <- ✅ FreeMonoid.ofList_map
❌ Set.Nonempty.of_add_right <- ✅ Set.Nonempty.of_mul_right
❌ AddEquiv.withZeroCongr_refl <- ✅ MulEquiv.withOneCongr_refl
❌ AddCon.hasSub <- ✅ Con.hasDiv
❌ LatticeOrderedCommGroup.pos_eq_zero_iff <- ✅ LatticeOrderedCommGroup.pos_eq_one_iff
❌ Set.image_op_add <- ✅ Set.image_op_mul
❌ FreeAddMonoid.map <- ✅ FreeMonoid.map
❌ Set.add_subset_add <- ✅ Set.mul_subset_mul
❌ neg_lt_neg_iff <- ✅ inv_lt_inv_iff
❌ List.sum_pos <- ✅ List.one_lt_prod_of_one_lt
❌ Sigma.vadd_def <- ✅ Sigma.smul_def
❌ FreeAddMonoid.toList_zero <- ✅ FreeMonoid.toList_one
❌ List.single_le_sum <- ✅ List.single_le_prod
❌ Set.unionᵢ_neg_vadd <- ✅ Set.unionᵢ_inv_smul
❌ le_sub_comm <- ✅ le_div_comm
❌ FreeAddMonoid.recOn_zero <- ✅ FreeMonoid.recOn_one
❌ Multiset.sum_hom₂ <- ✅ Multiset.prod_hom₂
❌ exists_zero_lt <- ✅ exists_one_lt'
❌ inf_add_sup <- ✅ inf_mul_sup
❌ IsAddUnit.set <- ✅ IsUnit.set
❌ instVAddLex <- ✅ instSMulLex
❌ LatticeOrderedCommGroup.pos_sub_neg <- ✅ LatticeOrderedCommGroup.pos_div_neg
❌ LatticeOrderedCommGroup.neg_eq_pos_neg <- ✅ LatticeOrderedCommGroup.neg_eq_pos_inv
❌ FreeAddMonoid.toList_comp_ofList <- ✅ FreeMonoid.toList_comp_ofList
❌ LatticeOrderedCommGroup.neg_nonpos_iff <- ✅ LatticeOrderedCommGroup.neg_le_one_iff
❌ AddCon.induction_on_addUnits <- ✅ Con.induction_on_units
❌ List.sum_hom_rel <- ✅ List.prod_hom_rel
❌ le_neg_add_iff_le <- ✅ le_inv_mul_iff_le
❌ Multiset.sum_eq_foldr <- ✅ Multiset.prod_eq_foldr
❌ Set.subset_add_left <- ✅ Set.subset_mul_left
❌ List.length_pos_of_sum_neg <- ✅ List.length_pos_of_prod_lt_one
❌ AddAction.compHom <- ✅ MulAction.compHom
❌ FreeAddMonoid.casesOn_of_add <- ✅ FreeMonoid.casesOn_of_mul
❌ AddCon.addSemigroup <- ✅ Con.semigroup
❌ le_iff_forall_pos_le_add <- ✅ le_iff_forall_one_lt_le_mul
❌ AddCon.mk' <- ✅ Con.mk'
❌ List.alternatingSum_cons <- ✅ List.alternatingProd_cons
❌ le_of_forall_pos_lt_add <- ✅ le_of_forall_one_lt_lt_mul
❌ AddAction.Regular.isPretransitive <- ✅ MulAction.Regular.isPretransitive
❌ Function.const_neg <- ✅ Function.const_lt_one
❌ AddLeftCancelMonoid.ext <- ✅ LeftCancelMonoid.ext
❌ eq_zero_of_neg_eq <- ✅ eq_one_of_inv_eq'
❌ Multiset.sum_map_zero <- ✅ Multiset.prod_map_one
❌ Set.add_mem_add <- ✅ Set.mul_mem_mul
❌ AddSubmonoid.closure_le <- ✅ Submonoid.closure_le
❌ LatticeOrderedCommGroup.neg_of_nonpos <- ✅ LatticeOrderedCommGroup.neg_of_le_one
❌ Left.pow_neg <- ✅ Left.pow_lt_one_of_lt
❌ Set.singletonAddMonoidHom <- ✅ Set.singletonMonoidHom
❌ AddUnits.val_mkOfAddEqZero <- ✅ Units.val_mkOfMulEqOne
❌ List.sum_map_add <- ✅ List.prod_map_mul
❌ AddOpposite.unop_sub <- ✅ MulOpposite.unop_div
❌ csupᵢ_add_csupᵢ_le <- ✅ csupᵢ_mul_csupᵢ_le
❌ MulOpposite.op_inv -> ✅ AddOpposite.op_neg
❌ AddCon.kerLift <- ✅ Con.kerLift
❌ AddMonoidHom.eqLocusM_same <- ✅ MonoidHom.eqLocusM_same
❌ le_sub_iff_add_le <- ✅ le_div_iff_mul_le
❌ Set.mem_add <- ✅ Set.mem_mul
❌ Set.neg_mem_Ico_iff <- ✅ Set.inv_mem_Ico_iff
❌ Set.singleton_zero <- ✅ Set.singleton_one
❌ Set.singleton_add_singleton <- ✅ Set.singleton_mul_singleton
❌ List.Perm.sum_eq' <- ✅ List.Perm.prod_eq'
❌ List.alternatingSum_reverse <- ✅ List.alternatingProd_reverse
❌ SubNegMonoid.ext <- ✅ DivInvMonoid.ext
❌ FreeAddMonoid.hom_eq <- ✅ FreeMonoid.hom_eq
❌ AddMonoidHom.eq_of_eqOn_topM <- ✅ MonoidHom.eq_of_eqOn_topM
❌ Multiset.sum_eq_foldl <- ✅ Multiset.prod_eq_foldl
❌ Set.preimage_add_left_zero' <- ✅ Set.preimage_mul_left_one'
❌ Pi.Lex.orderedAddCommGroup <- ✅ Pi.Lex.orderedCommGroup
❌ vadd_left_cancel_iff <- ✅ smul_left_cancel_iff
❌ Set.interᵢ₂_sub_subset <- ✅ Set.interᵢ₂_div_subset
❌ Multiset.sum_map_neg <- ✅ Multiset.prod_map_inv
❌ Set.set_vadd_subset_iff <- ✅ Set.set_smul_subset_iff
❌ List.alternatingSum_singleton <- ✅ List.alternatingProd_singleton
❌ neg_le_iff_add_nonneg <- ✅ inv_le_iff_one_le_mul
❌ WithTop.map_zero <- ✅ WithTop.map_one
❌ WithTop.top_ne_zero <- ✅ WithTop.top_ne_one
❌ List.sum_map_erase <- ✅ List.prod_map_erase
❌ Set.vadd_mem_vadd_set <- ✅ Set.smul_mem_smul_set
❌ LatticeOrderedCommGroup.Birkhoff_inequalities <- ✅ LatticeOrderedCommGroup.m_Birkhoff_inequalities
❌ Set.vadd_set_unionᵢ₂ <- ✅ Set.smul_set_unionᵢ₂
❌ Set.vadd_set_subset_iff <- ✅ Set.smul_set_subset_iff
❌ AddGroup.toSubNegAddMonoid_injective <- ✅ Group.toDivInvMonoid_injective
❌ AddAction.surjective <- ✅ MulAction.surjective
❌ le_map_add_map_sub <- ✅ le_map_add_map_div
❌ bot_eq_zero <- ✅ bot_eq_one
❌ le_add_cinfᵢ <- ✅ le_mul_cinfᵢ
❌ LatticeOrderedCommGroup.pos_abs <- ✅ LatticeOrderedCommGroup.m_pos_abs
❌ max_sub_sub_right <- ✅ max_div_div_right'
❌ Left.neg_pos_iff <- ✅ Left.one_lt_inv_iff
❌ StrictAntiOn.neg <- ✅ StrictAntiOn.inv
❌ AddSemiconjBy.transitive <- ✅ SemiconjBy.transitive
❌ Option.vadd_def <- ✅ Option.smul_def
❌ Set.Nonempty.of_add_left <- ✅ Set.Nonempty.of_mul_left
❌ Set.interᵢ_sub_subset <- ✅ Set.interᵢ_div_subset
❌ List.sum_neg <- ✅ List.prod_inv
❌ Function.Surjective.addActionLeft <- ✅ Function.Surjective.mulActionLeft
❌ Multiset.sum_hom' <- ✅ Multiset.prod_hom'
❌ WithTop.zero <- ✅ WithTop.one
❌ eq_neg_vadd_iff <- ✅ eq_inv_smul_iff
❌ AddSubsemigroup.coe_supᵢ_of_directed <- ✅ Subsemigroup.coe_supᵢ_of_directed
❌ Set.add_unionᵢ <- ✅ Set.mul_unionᵢ
❌ sub_lt_iff_lt_add <- ✅ div_lt_iff_lt_mul
❌ AddMonoidHom.compl₂_apply <- ✅ MonoidHom.compl₂_apply
❌ vadd_pi_subset <- ✅ smul_pi_subset
❌ Set.mem_neg <- ✅ Set.mem_inv
❌ Set.sub_nonempty <- ✅ Set.div_nonempty
❌ pos_iff_ne_zero <- ✅ one_lt_iff_ne_one
❌ lt_iff_exists_add <- ✅ lt_iff_exists_mul
❌ AddCon.zsmul <- ✅ Con.zpow