feat: Missing opposite instances (#2940)

Match leanprover-community/mathlib#18602



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/Field/Opposite.lean

@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
 ! This file was ported from Lean 3 source module algebra.field.opposite
-! leanprover-community/mathlib commit aba57d4d3dae35460225919dcd82fe91355162f9
+! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Ring.Opposite
+import Mathlib.Data.Int.Cast.Lemmas
 
 /-!
 # Field structure on the multiplicative/additive opposite
@@ -19,11 +20,34 @@ namespace MulOpposite
 
 variable (α : Type _)
 
+@[to_additive]
+instance ratCast [RatCast α] : RatCast αᵐᵒᵖ :=
+  ⟨fun n => op n⟩
+
+variable {α}
+
+@[to_additive (attr := simp, norm_cast)]
+theorem op_ratCast [RatCast α] (q : ℚ) : op (q : α) = q :=
+  rfl
+#align mul_opposite.op_rat_cast MulOpposite.op_ratCast
+#align add_opposite.op_rat_cast AddOpposite.op_ratCast
+
+@[to_additive (attr := simp, norm_cast)]
+theorem unop_ratCast [RatCast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q :=
+  rfl
+#align mul_opposite.unop_rat_cast MulOpposite.unop_ratCast
+#align add_opposite.unop_rat_cast AddOpposite.unop_ratCast
+
+variable (α)
+
 instance divisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ :=
   { MulOpposite.groupWithZero α, MulOpposite.semiring α with }
 
 instance divisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ :=
-  { MulOpposite.groupWithZero α, MulOpposite.ring α with }
+  { MulOpposite.divisionSemiring α, MulOpposite.ring α, MulOpposite.ratCast α with
+    ratCast_mk := fun a b hb h => unop_injective $ by
+      rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast,
+        Int.commute_cast, div_eq_mul_inv] }
 
 instance semifield [Semifield α] : Semifield αᵐᵒᵖ :=
   { MulOpposite.divisionSemiring α, MulOpposite.commSemiring α with }
@@ -39,7 +63,11 @@ instance divisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ :
   { AddOpposite.groupWithZero α, AddOpposite.semiring α with }
 
 instance divisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ :=
-  { AddOpposite.groupWithZero α, AddOpposite.ring α with }
+  { -- porting note: added `ratCast` override
+    AddOpposite.groupWithZero α, AddOpposite.ring α, AddOpposite.ratCast α with
+    ratCast_mk := fun a b hb h => unop_injective $ by
+      rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast,
+        div_eq_mul_inv] }
 
 instance semifield [Semifield α] : Semifield αᵃᵒᵖ :=
   { AddOpposite.divisionSemiring, AddOpposite.commSemiring α with }

Mathlib/Algebra/Group/Opposite.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
 ! This file was ported from Lean 3 source module algebra.group.opposite
-! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
+! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -29,6 +29,13 @@ namespace MulOpposite
 ### Additive structures on `αᵐᵒᵖ`
 -/
 
+@[to_additive]
+instance natCast [NatCast α] : NatCast αᵐᵒᵖ :=
+  ⟨fun n => op n⟩
+
+@[to_additive]
+instance intCast [IntCast α] : IntCast αᵐᵒᵖ :=
+  ⟨fun n => op n⟩
 
 instance addSemigroup [AddSemigroup α] : AddSemigroup αᵐᵒᵖ :=
   unop_injective.addSemigroup _ fun _ _ => rfl
@@ -48,14 +55,16 @@ instance addZeroClass [AddZeroClass α] : AddZeroClass αᵐᵒᵖ :=
 instance addMonoid [AddMonoid α] : AddMonoid αᵐᵒᵖ :=
   unop_injective.addMonoid _ (by exact rfl) (fun _ _ => rfl) fun _ _ => rfl
 
+instance addCommMonoid [AddCommMonoid α] : AddCommMonoid αᵐᵒᵖ :=
+  unop_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl
+
 instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne αᵐᵒᵖ :=
-  { MulOpposite.addMonoid α, MulOpposite.one α with
-    natCast := fun n => op n,
-    natCast_zero := show op ((0 : ℕ) : α) = 0 by simp,
-    natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ((n : ℕ) : α) + 1 by simp }
+  { MulOpposite.addMonoid α, MulOpposite.one α, MulOpposite.natCast _ with
+    natCast_zero := show op ((0 : ℕ) : α) = 0 by rw [Nat.cast_zero, op_zero]
+    natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ↑(n : ℕ) + 1 by simp }
 
-instance addCommMonoid [AddCommMonoid α] : AddCommMonoid αᵐᵒᵖ :=
-  unop_injective.addCommMonoid _ (by exact rfl) (fun _ _ => rfl) fun _ _ => rfl
+instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵐᵒᵖ :=
+  { MulOpposite.addMonoidWithOne α, MulOpposite.addCommMonoid α with }
 
 instance subNegMonoid [SubNegMonoid α] : SubNegMonoid αᵐᵒᵖ :=
   unop_injective.subNegMonoid _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
@@ -65,16 +74,19 @@ instance addGroup [AddGroup α] : AddGroup αᵐᵒᵖ :=
   unop_injective.addGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
   (fun _ _ => rfl) fun _ _ => rfl
 
+instance addCommGroup [AddCommGroup α] : AddCommGroup αᵐᵒᵖ :=
+  unop_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl) fun _ _ => rfl
+
 instance addGroupWithOne [AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ :=
   { MulOpposite.addMonoidWithOne α, MulOpposite.addGroup α with
     intCast := fun n => op n,
     intCast_ofNat := fun n => show op ((n : ℤ) : α) = op (n : α) by rw [Int.cast_ofNat],
     intCast_negSucc := fun n =>
       show op _ = op (-unop (op ((n + 1 : ℕ) : α))) by simp }
 
-instance addCommGroup [AddCommGroup α] : AddCommGroup αᵐᵒᵖ :=
-  unop_injective.addCommGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
+instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵐᵒᵖ :=
+  { MulOpposite.addGroupWithOne α, MulOpposite.addCommGroup α with }
 
 /-!
 ### Multiplicative structures on `αᵐᵒᵖ`
@@ -166,6 +178,29 @@ instance commGroup [CommGroup α] : CommGroup αᵐᵒᵖ :=
   { MulOpposite.group α, MulOpposite.commMonoid α with }
 
 variable {α}
+@[to_additive (attr := simp, norm_cast)]
+theorem op_natCast [NatCast α] (n : ℕ) : op (n : α) = n :=
+  rfl
+#align mul_opposite.op_nat_cast MulOpposite.op_natCast
+#align add_opposite.op_nat_cast AddOpposite.op_natCast
+
+@[to_additive (attr := simp, norm_cast)]
+theorem op_intCast [IntCast α] (n : ℤ) : op (n : α) = n :=
+  rfl
+#align mul_opposite.op_int_cast MulOpposite.op_intCast
+#align add_opposite.op_int_cast AddOpposite.op_intCast
+
+@[to_additive (attr := simp, norm_cast)]
+theorem unop_natCast [NatCast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n :=
+  rfl
+#align mul_opposite.unop_nat_cast MulOpposite.unop_natCast
+#align add_opposite.unop_nat_cast AddOpposite.unop_natCast
+
+@[to_additive (attr := simp, norm_cast)]
+theorem unop_intCast [IntCast α] (n : ℤ) : unop (n : αᵐᵒᵖ) = n :=
+  rfl
+#align mul_opposite.unop_int_cast MulOpposite.unop_intCast
+#align add_opposite.unop_int_cast AddOpposite.unop_intCast
 
 @[to_additive (attr := simp)]
 theorem unop_div [DivInvMonoid α] (x y : αᵐᵒᵖ) : unop (x / y) = (unop y)⁻¹ * unop x :=
@@ -300,6 +335,17 @@ instance commGroup [CommGroup α] : CommGroup αᵃᵒᵖ :=
   unop_injective.commGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
     (fun _ _ => rfl) fun _ _ => rfl
 
+-- NOTE: `addMonoidWithOne α → addMonoidWithOne αᵃᵒᵖ` does not hold
+instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵃᵒᵖ :=
+  { AddOpposite.addCommMonoid α, AddOpposite.one, AddOpposite.natCast α with
+    natCast_zero := show op ((0 : ℕ) : α) = 0 by rw [Nat.cast_zero, op_zero]
+    natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ↑(n : ℕ) + 1 by simp [add_comm] }
+
+instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵃᵒᵖ :=
+  { AddOpposite.addCommMonoidWithOne α, AddOpposite.addCommGroup α, AddOpposite.intCast α with
+    intCast_ofNat := λ _ ↦ congr_arg op $ Int.cast_ofNat _
+    intCast_negSucc := λ _ ↦ congr_arg op $ Int.cast_negSucc _ }
+
 variable {α}
 
 /-- The function `AddOpposite.op` is a multiplicative equivalence. -/

Mathlib/Algebra/Ring/Defs.lean

@@ -333,7 +333,7 @@ class NonUnitalRing (α : Type _) extends NonUnitalNonAssocRing α, NonUnitalSem
 
 /-- A unital but not-necessarily-associative ring. -/
 class NonAssocRing (α : Type _) extends NonUnitalNonAssocRing α, NonAssocSemiring α,
-    AddGroupWithOne α
+    AddCommGroupWithOne α
 #align non_assoc_ring NonAssocRing
 
 class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R

Mathlib/Algebra/Ring/Opposite.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
 ! This file was ported from Lean 3 source module algebra.ring.opposite
-! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
+! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -130,8 +130,8 @@ instance nonUnitalSemiring [NonUnitalSemiring α] : NonUnitalSemiring αᵃᵒ
   { AddOpposite.semigroupWithZero α, AddOpposite.nonUnitalNonAssocSemiring α with }
 
 instance nonAssocSemiring [NonAssocSemiring α] : NonAssocSemiring αᵃᵒᵖ :=
-  { AddOpposite.mulZeroOneClass α,
-    AddOpposite.nonUnitalNonAssocSemiring α with }
+  { AddOpposite.mulZeroOneClass α, AddOpposite.nonUnitalNonAssocSemiring α,
+    AddOpposite.addCommMonoidWithOne _ with }
 
 instance semiring [Semiring α] : Semiring αᵃᵒᵖ :=
   { AddOpposite.nonUnitalSemiring α, AddOpposite.nonAssocSemiring α,
@@ -149,11 +149,13 @@ instance nonUnitalNonAssocRing [NonUnitalNonAssocRing α] : NonUnitalNonAssocRin
 instance nonUnitalRing [NonUnitalRing α] : NonUnitalRing αᵃᵒᵖ :=
   { AddOpposite.addCommGroup α, AddOpposite.semigroupWithZero α, AddOpposite.distrib α with }
 
+-- porting note: added missing `addCommGroupWithOne` inheritance
 instance nonAssocRing [NonAssocRing α] : NonAssocRing αᵃᵒᵖ :=
-  { AddOpposite.addCommGroup α, AddOpposite.mulZeroOneClass α, AddOpposite.distrib α with }
+  { AddOpposite.addCommGroupWithOne α, AddOpposite.mulZeroOneClass α, AddOpposite.distrib α with }
 
+-- porting note: added missing `addCommGroupWithOne` inheritance
 instance ring [Ring α] : Ring αᵃᵒᵖ :=
-  { AddOpposite.addCommGroup α, AddOpposite.monoid α, AddOpposite.semiring α with }
+  { AddOpposite.addCommGroupWithOne α, AddOpposite.monoid α, AddOpposite.semiring α with }
 
 instance nonUnitalCommRing [NonUnitalCommRing α] : NonUnitalCommRing αᵃᵒᵖ :=
   { AddOpposite.nonUnitalRing α, AddOpposite.nonUnitalCommSemiring α with }

Mathlib/Data/Int/Cast/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 
 ! This file was ported from Lean 3 source module data.int.cast.defs
-! leanprover-community/mathlib commit 99e8971dc62f1f7ecf693d75e75fbbabd55849de
+! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -60,9 +60,11 @@ class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGro
 #align add_group_with_one.int_cast_neg_succ_of_nat AddGroupWithOne.intCast_negSucc
 
 /-- An `AddCommGroupWithOne` is an `AddGroupWithOne` satisfying `a + b = b + a`. -/
-class AddCommGroupWithOne (R : Type u) extends AddCommGroup R, AddGroupWithOne R
+class AddCommGroupWithOne (R : Type u)
+  extends AddCommGroup R, AddGroupWithOne R, AddCommMonoidWithOne R
 #align add_comm_group_with_one AddCommGroupWithOne
 #align add_comm_group_with_one.to_add_comm_group AddCommGroupWithOne.toAddCommGroup
 #align add_comm_group_with_one.to_add_group_with_one AddCommGroupWithOne.toAddGroupWithOne
+#align add_comm_group_with_one.to_add_comm_monoid_with_one AddCommGroupWithOne.toAddCommMonoidWithOne
 
 open Nat

Mathlib/Data/Int/Cast/Lemmas.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 Ported by: Scott Morrison
 
 ! This file was ported from Lean 3 source module data.int.cast.lemmas
-! leanprover-community/mathlib commit 7a89b1aed52bcacbcc4a8ad515e72c5c07268940
+! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -368,22 +368,6 @@ theorem Sum.elim_intCast_intCast {α β γ : Type _} [IntCast γ] (n : ℤ) :
   @Sum.elim_lam_const_lam_const α β γ n
 #align sum.elim_int_cast_int_cast Sum.elim_intCast_intCast
 
-namespace MulOpposite
-
-variable [AddGroupWithOne α]
-
-@[simp, norm_cast]
-theorem op_intCast (z : ℤ) : op (z : α) = z :=
-  rfl
-#align mul_opposite.op_int_cast MulOpposite.op_intCast
-
-@[simp, norm_cast]
-theorem unop_intCast (n : ℤ) : unop (n : αᵐᵒᵖ) = n :=
-  rfl
-#align mul_opposite.unop_int_cast MulOpposite.unop_intCast
-
-end MulOpposite
-
 /-! ### Order dual -/
 
 

Mathlib/Data/Nat/Cast/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.cast.basic
-! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
+! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -297,22 +297,6 @@ instance Nat.uniqueRingHom {R : Type _} [NonAssocSemiring R] : Unique (ℕ →+*
   default := Nat.castRingHom R
   uniq := RingHom.eq_natCast'
 
-namespace MulOpposite
-
-variable [AddMonoidWithOne α]
-
-@[simp, norm_cast]
-theorem op_natCast (n : ℕ) : op (n : α) = n :=
-  rfl
-#align mul_opposite.op_nat_cast MulOpposite.op_natCast
-
-@[simp, norm_cast]
-theorem unop_natCast (n : ℕ) : unop (n : αᵐᵒᵖ) = n :=
-  rfl
-#align mul_opposite.unop_nat_cast MulOpposite.unop_natCast
-
-end MulOpposite
-
 namespace Pi
 
 variable {π : α → Type _} [∀ a, NatCast (π a)]

Mathlib/Data/Rat/Cast.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.rat.cast
-! leanprover-community/mathlib commit 422e70f7ce183d2900c586a8cda8381e788a0c62
+! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -499,24 +499,6 @@ instance Rat.subsingleton_ringHom {R : Type _} [Semiring R] : Subsingleton (ℚ
   ⟨RingHom.ext_rat⟩
 #align rat.subsingleton_ring_hom Rat.subsingleton_ringHom
 
-namespace MulOpposite
-
-variable [DivisionRing α]
-
-@[simp, norm_cast]
-theorem op_ratCast (r : ℚ) : op (r : α) = (↑r : αᵐᵒᵖ) := by
-  rw [cast_def, div_eq_mul_inv, op_mul, op_inv, op_natCast, op_intCast,
-    (Commute.cast_int_right _ r.num).eq, cast_def, div_eq_mul_inv]
-#align mul_opposite.op_rat_cast MulOpposite.op_ratCast
-
-@[simp, norm_cast]
-theorem unop_ratCast (r : ℚ) : unop (r : αᵐᵒᵖ) = r := by
-  rw [cast_def, div_eq_mul_inv, unop_mul, unop_inv, unop_natCast, unop_intCast,
-    (Commute.cast_int_right _ r.num).eq, cast_def, div_eq_mul_inv]
-#align mul_opposite.unop_rat_cast MulOpposite.unop_ratCast
-
-end MulOpposite
-
 section SMul
 
 namespace Rat