[GOAL]
α : Type u
inst✝ : AddZeroClass α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddMonoid α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddMonoidWithOne α
src✝² : AddMonoid αᵐᵒᵖ := addMonoid α
src✝¹ : One αᵐᵒᵖ := one α
src✝ : NatCast αᵐᵒᵖ := natCast α
⊢ op ↑0 = 0
[PROOFSTEP]
rw [Nat.cast_zero, op_zero]
[GOAL]
α : Type u
inst✝ : AddMonoidWithOne α
src✝² : AddMonoid αᵐᵒᵖ := addMonoid α
src✝¹ : One αᵐᵒᵖ := one α
src✝ : NatCast αᵐᵒᵖ := natCast α
⊢ ∀ (n : ℕ), op ↑(n + 1) = op ↑n + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : SubNegMonoid α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddGroup α
⊢ unop 0 = 0
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddGroupWithOne α
src✝¹ : AddMonoidWithOne αᵐᵒᵖ := addMonoidWithOne α
src✝ : AddGroup αᵐᵒᵖ := addGroup α
n : ℕ
⊢ op ↑↑n = op ↑n
[PROOFSTEP]
rw [Int.cast_ofNat]
[GOAL]
α : Type u
inst✝ : AddGroupWithOne α
src✝¹ : AddMonoidWithOne αᵐᵒᵖ := addMonoidWithOne α
src✝ : AddGroup αᵐᵒᵖ := addGroup α
n : ℕ
⊢ op ↑(Int.negSucc n) = op (-unop (op ↑(n + 1)))
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
src✝¹ : Monoid αᵐᵒᵖ := monoid α
src✝ : Inv αᵐᵒᵖ := inv α
n : ℕ
x : αᵐᵒᵖ
⊢ unop ((fun n x => op (unop x ^ n)) (Int.ofNat (Nat.succ n)) x) =
    unop (x * (fun n x => op (unop x ^ n)) (Int.ofNat n) x)
[PROOFSTEP]
simp only [Int.ofNat_eq_coe]
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
src✝¹ : Monoid αᵐᵒᵖ := monoid α
src✝ : Inv αᵐᵒᵖ := inv α
n : ℕ
x : αᵐᵒᵖ
⊢ unop (op (unop x ^ ↑(Nat.succ n))) = unop (x * op (unop x ^ ↑n))
[PROOFSTEP]
rw [unop_op, zpow_ofNat, pow_succ', unop_mul, unop_op, zpow_ofNat]
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
x y : α
⊢ op (x / y) = (op y)⁻¹ * op x
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : α
⊢ SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y
[PROOFSTEP]
simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
[PROOFSTEP]
conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y
[PROOFSTEP]
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y
[PROOFSTEP]
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : Mul α
a x y : αᵐᵒᵖ
| SemiconjBy a x y
[PROOFSTEP]
rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
[GOAL]
α : Type u
inst✝ : MulOneClass α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : Monoid α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : CommMonoid α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : DivInvMonoid α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : Group α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : CommGroup α
⊢ unop 1 = 1
[PROOFSTEP]
exact rfl
[GOAL]
α : Type u
inst✝ : AddCommMonoidWithOne α
src✝² : AddCommMonoid αᵃᵒᵖ := addCommMonoid α
src✝¹ : One αᵃᵒᵖ := one
src✝ : NatCast αᵃᵒᵖ := natCast α
⊢ op ↑0 = 0
[PROOFSTEP]
rw [Nat.cast_zero, op_zero]
[GOAL]
α : Type u
inst✝ : AddCommMonoidWithOne α
src✝² : AddCommMonoid αᵃᵒᵖ := addCommMonoid α
src✝¹ : One αᵃᵒᵖ := one
src✝ : NatCast αᵃᵒᵖ := natCast α
⊢ ∀ (n : ℕ), op ↑(n + 1) = op ↑n + 1
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
hf : ∀ (x y : M), Commute (↑f x) (↑f y)
x y : M
⊢ (op ∘ ↑f) (x * y) = (op ∘ ↑f) x * (op ∘ ↑f) y
[PROOFSTEP]
simp [(hf x y).eq]
[GOAL]
α : Type u
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
hf : ∀ (x y : M), Commute (↑f x) (↑f y)
x y : M
⊢ OneHom.toFun { toFun := op ∘ ↑f, map_one' := (_ : op (↑f 1) = op 1) } (x * y) =
    OneHom.toFun { toFun := op ∘ ↑f, map_one' := (_ : op (↑f 1) = op 1) } x *
      OneHom.toFun { toFun := op ∘ ↑f, map_one' := (_ : op (↑f 1) = op 1) } y
[PROOFSTEP]
simp [(hf x y).eq]
[GOAL]
α : Type u
M : Type ?u.46725
inst✝ : Monoid M
x : Mᵐᵒᵖˣ
⊢ ↑((fun X =>
          MulOpposite.rec'
            (fun u =>
              { val := op ↑u, inv := op ↑u⁻¹, val_inv := (_ : op ↑u * op ↑u⁻¹ = 1),
                inv_val := (_ : op ↑u⁻¹ * op ↑u = 1) })
            X)
        ((fun u =>
            op
              { val := unop ↑u, inv := unop ↑u⁻¹, val_inv := (_ : unop ↑u * unop ↑u⁻¹ = 1),
                inv_val := (_ : unop ↑u⁻¹ * unop ↑u = 1) })
          x)) =
    ↑x
[PROOFSTEP]
simp
[GOAL]
α : Type u
M : Type ?u.46725
inst✝ : Monoid M
x : Mˣᵐᵒᵖ
⊢ ↑(unop
        ((fun u =>
            op
              { val := unop ↑u, inv := unop ↑u⁻¹, val_inv := (_ : unop ↑u * unop ↑u⁻¹ = 1),
                inv_val := (_ : unop ↑u⁻¹ * unop ↑u = 1) })
          ((fun X =>
              MulOpposite.rec'
                (fun u =>
                  { val := op ↑u, inv := op ↑u⁻¹, val_inv := (_ : op ↑u * op ↑u⁻¹ = 1),
                    inv_val := (_ : op ↑u⁻¹ * op ↑u = 1) })
                X)
            x))) =
    ↑(unop x)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
α : Type ?u.65550
β : Type ?u.65553
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : α
⊢ (unop ∘ ↑(symm f) ∘ MulOpposite.op) ((unop ∘ ↑f ∘ MulOpposite.op) x) = x
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
α : Type ?u.65550
β : Type ?u.65553
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : β
⊢ (unop ∘ ↑f ∘ MulOpposite.op) ((unop ∘ ↑(symm f) ∘ MulOpposite.op) x) = x
[PROOFSTEP]
simp
