[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a b c : RingAut R), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ b✝ c✝ : RingAut R
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a : RingAut R), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
⊢ 1 * a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a : RingAut R), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
⊢ a✝ * 1 = a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (a : RingAut R), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
a✝ : RingAut R
x✝ : R
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
apply Equiv.left_inv
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingAut R →* AddAut R
[PROOFSTEP]
refine' { toFun := RingEquiv.toAddEquiv .. }
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toAddEquiv 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toAddEquiv 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (x y : RingAut R),
    OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
        (x * y) =
      OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
          x *
        OneHom.toFun
          { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
x✝ y✝ : RingAut R
⊢ OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
      (x✝ * y✝) =
    OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
        x✝ *
      OneHom.toFun { toFun := RingEquiv.toAddEquiv, map_one' := (_ : RingEquiv.toAddEquiv 1 = RingEquiv.toAddEquiv 1) }
        y✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingAut R →* MulAut R
[PROOFSTEP]
refine' { toFun := RingEquiv.toMulEquiv .. }
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toMulEquiv 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingEquiv.toMulEquiv 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (x y : RingAut R),
    OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
        (x * y) =
      OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
          x *
        OneHom.toFun
          { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
x✝ y✝ : RingAut R
⊢ OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
      (x✝ * y✝) =
    OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
        x✝ *
      OneHom.toFun { toFun := RingEquiv.toMulEquiv, map_one' := (_ : RingEquiv.toMulEquiv 1 = RingEquiv.toMulEquiv 1) }
        y✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ RingAut R →* Equiv.Perm R
[PROOFSTEP]
refine' { toFun := RingEquiv.toEquiv .. }
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ 1.toEquiv = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ 1.toEquiv = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
⊢ ∀ (x y : RingAut R),
    OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } (x * y) =
      OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } x *
        OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
x✝ y✝ : RingAut R
⊢ OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } (x✝ * y✝) =
    OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } x✝ *
      OneHom.toFun { toFun := RingEquiv.toEquiv, map_one' := (_ : 1.toEquiv = 1.toEquiv) } y✝
[PROOFSTEP]
rfl


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => b⁻¹ * a) ((fun b => a / b) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => a / b) ((fun b => b⁻¹ * a) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => b * a) ((fun b => b / a) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => b / a) ((fun b => b * a) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]


[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a + b) * (a - b)
[PROOFSTEP]
rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a - b) * (a + b)
[PROOFSTEP]
rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b
[PROOFSTEP]
rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero, add_eq_zero_iff_eq_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)
[PROOFSTEP]
rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : NonAssocRing R
inst✝ : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a = 1 ∨ a = -1
[PROOFSTEP]
rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1
[PROOFSTEP]
rw [inv_eq_iff_mul_eq_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1
[PROOFSTEP]
simp only [ext_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
[PROOFSTEP]
exact mul_self_eq_one_iff


[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.27
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Distrib S
f : R → S
hf : Injective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f (x * (y + z)) = f (x * y + x * z)
[PROOFSTEP]
simp only [*, left_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.27
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Distrib S
f : R → S
hf : Injective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f ((x + y) * z) = f (x * z + y * z)
[PROOFSTEP]
simp only [*, right_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.1511
inst✝² : Distrib R
inst✝¹ : Add S
inst✝ : Mul S
f : R → S
hf : Surjective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f x * (f y + f z) = f x * f y + f x * f z
[PROOFSTEP]
simp only [← add, ← mul, left_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.1511
inst✝² : Distrib R
inst✝¹ : Add S
inst✝ : Mul S
f : R → S
hf : Surjective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ (f x + f y) * f z = f x * f z + f y * f z
[PROOFSTEP]
simp only [← add, ← mul, right_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : β → α
hf : Injective f
neg : ∀ (a : β), f (-a) = -f a
mul : ∀ (a b : β), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Injective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : β
⊢ f (-x * y) = f (-(x * y))
[PROOFSTEP]
erw [neg, mul, neg, neg_mul, mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : β → α
hf : Injective f
neg : ∀ (a : β), f (-a) = -f a
mul : ∀ (a b : β), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Injective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : β
⊢ f (x * -y) = f (-(x * y))
[PROOFSTEP]
erw [neg, mul, neg, mul_neg, mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : α → β
hf : Surjective f
neg : ∀ (a : α), f (-a) = -f a
mul : ∀ (a b : α), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Surjective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : α
⊢ -f x * f y = -(f x * f y)
[PROOFSTEP]
erw [← neg, ← mul, neg_mul, neg, mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : α → β
hf : Surjective f
neg : ∀ (a : α), f (-a) = -f a
mul : ∀ (a b : α), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Surjective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : α
⊢ f x * -f y = -(f x * f y)
[PROOFSTEP]
erw [← neg, ← mul, mul_neg, neg, mul]


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
g : N → M
h₁ : Function.LeftInverse g ↑f
⊢ g 1 = 1
[PROOFSTEP]
rw [← f.map_one, h₁]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : Function.LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
x y : N
⊢ g (x * y) = g (↑f (g x) * ↑f (g y))
[PROOFSTEP]
rw [h₂ x, h₂ y]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : Function.LeftInverse g ↑f
h₂ : Function.RightInverse g ↑f
x y : N
⊢ g (↑f (g x) * ↑f (g y)) = g (↑f (g x * g y))
[PROOFSTEP]
rw [f.map_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulEquivClass F M N
src✝ : MulHomClass F M N := instMulHomClass F
e : F
⊢ ↑e 1 * ↑e (EquivLike.inv e 1) = ↑e (EquivLike.inv e 1)
[PROOFSTEP]
rw [← map_mul, one_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
e : F
⊢ ↑e 0 = ↑e 0 * ↑e (EquivLike.inv e 0)
[PROOFSTEP]
rw [← map_mul, zero_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
e : F
⊢ ↑e 0 * ↑e (EquivLike.inv e 0) = 0
[PROOFSTEP]
simp
  -- See note [lower instance priority]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
f g : M ≃* N
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
g : M ≃* N
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
h₁ : (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = (fun f => f.invFun) g
⊢ { toEquiv := toEquiv✝, map_mul' := map_mul'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
toEquiv✝¹ : M ≃ N
map_mul'✝¹ : ∀ (x y : M), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
⊢ { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } = { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEquiv
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝¹ : Mul M
inst✝ : Mul N
toEquiv✝¹ : M ≃ N
map_mul'✝¹ : ∀ (x y : M), Equiv.toFun toEquiv✝¹ (x * y) = Equiv.toFun toEquiv✝¹ x * Equiv.toFun toEquiv✝¹ y
toEquiv✝ : M ≃ N
map_mul'✝ : ∀ (x y : M), Equiv.toFun toEquiv✝ (x * y) = Equiv.toFun toEquiv✝ x * Equiv.toFun toEquiv✝ y
h₁ :
  (fun f => f.toFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.toFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
h₂ :
  (fun f => f.invFun) { toEquiv := toEquiv✝¹, map_mul' := map_mul'✝¹ } =
    (fun f => f.invFun) { toEquiv := toEquiv✝, map_mul' := map_mul'✝ }
⊢ toEquiv✝¹ = toEquiv✝
[PROOFSTEP]
apply Equiv.coe_fn_injective h₁
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : Mul P
inst✝ : Mul Q
h1 : M ≃* N
h2 : N ≃* P
src✝ : M ≃ P := h1.trans h2.toEquiv
x y : M
⊢ ↑h2 (↑h1 (x * y)) = ↑h2 (↑h1 x) * ↑h2 (↑h1 y)
[PROOFSTEP]
rw [h1.map_mul, h2.map_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
⊢ (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h : M → P
x✝ : M
⊢ (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) x✝ = h x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
⊢ (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
k : N → Q
x✝ : N
⊢ (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) x✝ = k x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
⊢ Equiv.toFun
      { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
        left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
        right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
      (h * k) =
    Equiv.toFun
        { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
          left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
          right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
        h *
      Equiv.toFun
        { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
          left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
          right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
        k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁵ : Mul M✝
inst✝⁴ : Mul N✝
inst✝³ : Mul P✝
inst✝² : Mul Q✝
M : Type u_12
N : Type u_13
P : Type u_14
Q : Type u_15
inst✝¹ : Mul P
inst✝ : Mul Q
f : M ≃ N
g : P ≃* Q
h k : M → P
x✝ : N
⊢ Equiv.toFun
      { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
        left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
        right_inv := (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
      (h * k) x✝ =
    (Equiv.toFun
          { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
            left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
            right_inv :=
              (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
          h *
        Equiv.toFun
          { toFun := fun h n => ↑g (h (↑f.symm n)), invFun := fun k m => ↑(symm g) (k (↑f m)),
            left_inv := (_ : ∀ (h : M → P), (fun k m => ↑(symm g) (k (↑f m))) ((fun h n => ↑g (h (↑f.symm n))) h) = h),
            right_inv :=
              (_ : ∀ (k : N → Q), (fun h n => ↑g (h (↑f.symm n))) ((fun k m => ↑(symm g) (k (↑f m))) k) = k) }
          k)
      x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h : M →* P
⊢ (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
      ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
    h
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h : M →* P
x✝ : M
⊢ ↑((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
          ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h))
      x✝ =
    ↑h x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
k : N →* Q
⊢ (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
      ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
    k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
k : N →* Q
x✝ : N
⊢ ↑((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
          ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k))
      x✝ =
    ↑k x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h k : M →* P
⊢ Equiv.toFun
      { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
        invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
        left_inv :=
          (_ :
            ∀ (h : M →* P),
              (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                  ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                h),
        right_inv :=
          (_ :
            ∀ (k : N →* Q),
              (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                  ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                k) }
      (h * k) =
    Equiv.toFun
        { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
          invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
          left_inv :=
            (_ :
              ∀ (h : M →* P),
                (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                    ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                  h),
          right_inv :=
            (_ :
              ∀ (k : N →* Q),
                (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                    ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                  k) }
        h *
      Equiv.toFun
        { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
          invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
          left_inv :=
            (_ :
              ∀ (h : M →* P),
                (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                    ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                  h),
          right_inv :=
            (_ :
              ∀ (k : N →* Q),
                (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                    ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                  k) }
        k
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M✝ : Type u_6
N✝ : Type u_7
P✝ : Type u_8
Q✝ : Type u_9
G : Type u_10
H : Type u_11
inst✝⁷ : Mul M✝
inst✝⁶ : Mul N✝
inst✝⁵ : Mul P✝
inst✝⁴ : Mul Q✝
M : Type ?u.66798
N : Type ?u.66801
P : Type ?u.66804
Q : Type ?u.66807
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
inst✝ : CommMonoid Q
f : M ≃* N
g : P ≃* Q
h k : M →* P
x✝ : N
⊢ ↑(Equiv.toFun
          { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
            invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
            left_inv :=
              (_ :
                ∀ (h : M →* P),
                  (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                      ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                    h),
            right_inv :=
              (_ :
                ∀ (k : N →* Q),
                  (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                      ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                    k) }
          (h * k))
      x✝ =
    ↑(Equiv.toFun
            { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
              invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
              left_inv :=
                (_ :
                  ∀ (h : M →* P),
                    (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                        ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                      h),
              right_inv :=
                (_ :
                  ∀ (k : N →* Q),
                    (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                        ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                      k) }
            h *
          Equiv.toFun
            { toFun := fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))),
              invFun := fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)),
              left_inv :=
                (_ :
                  ∀ (h : M →* P),
                    (fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f)))
                        ((fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f)))) h) =
                      h),
              right_inv :=
                (_ :
                  ∀ (k : N →* Q),
                    (fun h => MonoidHom.comp (toMonoidHom g) (MonoidHom.comp h (toMonoidHom (symm f))))
                        ((fun k => MonoidHom.comp (toMonoidHom (symm g)) (MonoidHom.comp k (toMonoidHom f))) k) =
                      k) }
            k)
      x✝
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
⊢ IsLeftRegular k
[PROOFSTEP]
refine' fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ _)
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * (x - y) = 0
[PROOFSTEP]
rw [mul_sub, sub_eq_zero, h']
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
⊢ IsRightRegular k
[PROOFSTEP]
refine' fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ _)
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ (x - y) * k = 0
[PROOFSTEP]
rw [sub_mul, sub_eq_zero, h']
[GOAL]
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
k : α
h : IsRegular k
⊢ k ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
h : IsRegular 0
⊢ False
[PROOFSTEP]
exact not_not.mpr h.left not_isLeftRegular_zero
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
⊢ MonoidWithZero α
[PROOFSTEP]
infer_instance


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
f g : α →ₙ+* β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
g : α →ₙ+* β
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h : (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = (fun f => f.toFun) g
⊢ { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : MulHom.toFun toMulHom✝¹ 0 = 0
map_add'✝¹ : ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h :
  (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMulHom
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : MulHom.toFun toMulHom✝¹ 0 = 0
map_add'✝¹ : ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h :
  (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMulHom✝¹ = toMulHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toMulHom.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
toMulHom✝¹ : α →ₙ* β
map_zero'✝¹ : MulHom.toFun toMulHom✝¹ 0 = 0
map_add'✝¹ : ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y
toMulHom✝ : α →ₙ* β
map_zero'✝ : MulHom.toFun toMulHom✝ 0 = 0
map_add'✝ : ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y
h :
  (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ↑toMulHom✝¹ = ↑toMulHom✝
[PROOFSTEP]
exact h
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ α →ₙ+* α
[PROOFSTEP]
refine' { toFun := id .. }
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ ∀ (x y : α), id (x * y) = id x * id y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ ∀ (x y : α),
    MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } (x + y) =
      MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } x +
        MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
x✝ y✝ : α
⊢ id (x✝ * y✝) = id x✝ * id y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α✝
inst✝¹ : NonUnitalNonAssocSemiring β
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
x✝ y✝ : α
⊢ MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } (x✝ + y✝) =
    MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } x✝ +
      MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id (x * y)) } y✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g✝ : β →ₙ+* γ
f : α →ₙ+* β
g : β →ₙ+* γ
⊢ comp g 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g✝ : β →ₙ+* γ
f : α →ₙ+* β
g : β →ₙ+* γ
x✝ : α
⊢ ↑(comp g 0) x✝ = ↑0 x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f✝ f : α →ₙ+* β
⊢ comp 0 f = 0
[PROOFSTEP]
ext
[GOAL]
case a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f✝ f : α →ₙ+* β
x✝ : α
⊢ ↑(comp 0 f) x✝ = ↑0 x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g✝ : β →ₙ+* γ
f : α →ₙ+* β
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
x : α
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonAssocSemiring α
inst✝¹ : NonAssocSemiring β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ ↑f (bit1 a) = bit1 (↑f a)
[PROOFSTEP]
simp [bit1]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f g : α →+* β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
g : α →+* β
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } =
    (fun f => f.toFun) g
⊢ { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMonoidHom
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
apply FunLike.coe_injective'
[GOAL]
case mk.mk.e_toMonoidHom.a
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
toMonoidHom✝¹ : α →* β
map_zero'✝¹ : OneHom.toFun (↑toMonoidHom✝¹) 0 = 0
map_add'✝¹ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y
toMonoidHom✝ : α →* β
map_zero'✝ : OneHom.toFun (↑toMonoidHom✝) 0 = 0
map_add'✝ :
  ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y
h :
  (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =
    (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
⊢ ↑toMonoidHom✝¹ = ↑toMonoidHom✝
[PROOFSTEP]
exact h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ ↑(toMonoidWithZeroHom f) = ↑f
[PROOFSTEP]
rfl
[GOAL]
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ ↑f (if p then 0 else 1) = if p then 0 else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f (if p then 0 else 1) = 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f (if p then 0 else 1) = 1
[PROOFSTEP]
simp [h]
[GOAL]
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ ↑f (if p then 1 else 0) = if p then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ ↑f (if p then 1 else 0) = 1
[PROOFSTEP]
simp [h]
[GOAL]
case neg
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f✝ : α →+* β
x y : α
F : Type u_5
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ ↑f (if p then 1 else 0) = 0
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
x y : α
⊢ 0 = 1 ↔ ↑f 1 = 0
[PROOFSTEP]
rw [map_one, eq_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
f : α →+* β
x✝ y : α
h : ↑f 1 = 0
x : α
⊢ ↑f x = 0
[PROOFSTEP]
rw [← mul_one x, map_mul, h, mul_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝³ : NonAssocSemiring α
x✝² : NonAssocSemiring β
f : α →+* β
x✝¹ y✝ : α
h : ∀ (x : α), ↑f x = 0
y : β
x✝ : y ∈ Set.range ↑f
x : α
hx : ↑f x = y
⊢ y ∈ {0}
[PROOFSTEP]
simp [← hx, h x]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
x y✝ : α
h : ∀ (x : α), ↑f x = 0
y : β
hy : y ∈ {0}
⊢ ↑f 0 = y
[PROOFSTEP]
simpa using hy.symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
x y : α
inst✝ : Nontrivial β
h : 1 = 0
⊢ ↑f 1 = 0
[PROOFSTEP]
rw [h, map_zero]
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ α →+* α
[PROOFSTEP]
refine' { toFun := _root_.id .. }
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ _root_.id 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ ∀ (x y : α),
    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
        OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y
[PROOFSTEP]
intros
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
          map_mul' :=
            (_ :
              ∀ (x y : α),
                OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                  OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
      0 =
    0
[PROOFSTEP]
intros
[GOAL]
case refine'_4
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ ∀ (x y : α),
    OneHom.toFun
        (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
              map_mul' :=
                (_ :
                  ∀ (x y : α),
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                        OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := _root_.id, map_one' := ?refine'_1 },
              map_mul' :=
                (_ :
                  ∀ (x y : α),
                    OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } (x * y) =
                      OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } x *
                        OneHom.toFun { toFun := _root_.id, map_one' := ?refine'_1 } y) })
          y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ _root_.id 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α✝
x✝¹ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
x✝ y✝ : α
⊢ OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x✝ * y✝) =
    OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } x✝ *
      OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝¹ : NonAssocSemiring α✝
x✝ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
          map_mul' :=
            (_ :
              ∀ (x y : α),
                OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
      0 =
    0
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α✝
x✝¹ : NonAssocSemiring β
α : Type u_5
inst✝ : NonAssocSemiring α
x✝ y✝ : α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
          map_mul' :=
            (_ :
              ∀ (x y : α),
                OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
      (x✝ + y✝) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                    OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
        x✝ +
      OneHom.toFun
        (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) },
            map_mul' :=
              (_ :
                ∀ (x y : α),
                  OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y) =
                    OneHom.toFun { toFun := _root_.id, map_one' := (_ : _root_.id 1 = _root_.id 1) } (x * y)) })
        y✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f : α →+* β
src✝ : α →ₙ+* γ := NonUnitalRingHom.comp (toNonUnitalRingHom g) (toNonUnitalRingHom f)
⊢ (↑g ∘ ↑f) 1 = 1
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
x : α
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
⊢ IsDomain β
[PROOFSTEP]
haveI := pullback_nonzero f f.map_zero f.map_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this : Nontrivial β
⊢ IsDomain β
[PROOFSTEP]
haveI := IsRightCancelMulZero.to_noZeroDivisors α
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝ : Nontrivial β
this : NoZeroDivisors α
⊢ IsDomain β
[PROOFSTEP]
haveI := hf.noZeroDivisors f f.map_zero f.map_mul
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Ring α
inst✝¹ : IsDomain α
inst✝ : Ring β
f : β →+* α
hf : Injective ↑f
this✝¹ : Nontrivial β
this✝ : NoZeroDivisors α
this : NoZeroDivisors β
⊢ IsDomain β
[PROOFSTEP]
exact NoZeroDivisors.to_isDomain β
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
have hxy := h (x + y)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy : ↑f ((x + y) * (x + y)) = ↑f (x + y) * ↑f (x + y)
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul, mul_add, mul_add, ←
  sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub, ← sub_sub, mul_comm y x, mul_comm (f y) (f x)] at
  hxy
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy✝ : ↑f x * ↑f x + ↑f (y * x) + (↑f (x * y) + ↑f y * ↑f y) = ↑f x * ↑f x + ↑f x * ↑f y + (↑f y * ↑f x + ↑f y * ↑f y)
hxy : ↑f (x * y) + ↑f y * ↑f y + (↑f x * ↑f x + ↑f (x * y)) - ↑f x * ↑f x - ↑f x * ↑f y - ↑f x * ↑f y - ↑f y * ↑f y = 0
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
simp only [add_assoc, add_sub_assoc, add_sub_cancel'_right] at hxy
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy✝ : ↑f x * ↑f x + ↑f (y * x) + (↑f (x * y) + ↑f y * ↑f y) = ↑f x * ↑f x + ↑f x * ↑f y + (↑f y * ↑f x + ↑f y * ↑f y)
hxy : ↑f (x * y) + (↑f (x * y) - ↑f x * ↑f y - ↑f x * ↑f y) = 0
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero (M₀ := α), sub_eq_zero,
  or_iff_not_imp_left] at hxy
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x y : β
hxy✝ : ↑f x * ↑f x + ↑f (y * x) + (↑f (x * y) + ↑f y * ↑f y) = ↑f x * ↑f x + ↑f x * ↑f y + (↑f y * ↑f x + ↑f y * ↑f y)
hxy : ¬2 = 0 → ↑f (x * y) = ↑f x * ↑f y
⊢ OneHom.toFun { toFun := f.toFun, map_one' := h_one } (x * y) =
    OneHom.toFun { toFun := f.toFun, map_one' := h_one } x * OneHom.toFun { toFun := f.toFun, map_one' := h_one } y
[PROOFSTEP]
exact hxy h_two
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
⊢ ↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) = f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), ↑f (x * x) = ↑f x * ↑f x
h_two : 2 ≠ 0
h_one : ↑f 1 = 1
x✝ : β
⊢ ↑↑(mkRingHomOfMulSelfOfTwoNeZero f h h_two h_one) x✝ = ↑f x✝
[PROOFSTEP]
rfl


[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p q : S
h : Commute p q
h₁ : IsIdempotentElem p
h₂ : IsIdempotentElem q
⊢ IsIdempotentElem (p * q)
[PROOFSTEP]
rw [IsIdempotentElem, mul_assoc, ← mul_assoc q, ← h.eq, mul_assoc p, h₂.eq, ← mul_assoc, h₁.eq]
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : R
h : IsIdempotentElem p
⊢ IsIdempotentElem (1 - p)
[PROOFSTEP]
rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : N
n✝ : ℕ
h : IsIdempotentElem p
n : ℕ
x✝ : IsIdempotentElem (p ^ n)
⊢ p ^ Nat.succ n * p ^ Nat.succ n = p ^ Nat.succ n
[PROOFSTEP]
conv_rhs =>
  rw [← h.eq]
    --Porting note: was `nth_rw 3 [← h.eq]`
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : N
n✝ : ℕ
h : IsIdempotentElem p
n : ℕ
x✝ : IsIdempotentElem (p ^ n)
| p ^ Nat.succ n
[PROOFSTEP]
rw [← h.eq]
    --Porting note: was `nth_rw 3 [← h.eq]`
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : N
n✝ : ℕ
h : IsIdempotentElem p
n : ℕ
x✝ : IsIdempotentElem (p ^ n)
| p ^ Nat.succ n
[PROOFSTEP]
rw [← h.eq]
    --Porting note: was `nth_rw 3 [← h.eq]`
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : N
n✝ : ℕ
h : IsIdempotentElem p
n : ℕ
x✝ : IsIdempotentElem (p ^ n)
| p ^ Nat.succ n
[PROOFSTEP]
rw [← h.eq]
  --Porting note: was `nth_rw 3 [← h.eq]`
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : N
n✝ : ℕ
h : IsIdempotentElem p
n : ℕ
x✝ : IsIdempotentElem (p ^ n)
⊢ p ^ Nat.succ n * p ^ Nat.succ n = (p * p) ^ Nat.succ n
[PROOFSTEP]
rw [← sq, ← sq, ← pow_mul, ← pow_mul']
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : N
n✝ : ℕ
h : IsIdempotentElem p
n : ℕ
ih : p ^ (n + 1) = p
⊢ p ^ (Nat.succ n + 1) = p
[PROOFSTEP]
rw [pow_succ, ih, h.eq]
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : G₀
⊢ IsIdempotentElem p ↔ p = 0 ∨ p = 1
[PROOFSTEP]
refine'
  Iff.intro (fun h => or_iff_not_imp_left.mpr fun hp => _) fun h =>
    h.elim (fun hp => hp.symm ▸ zero) fun hp => hp.symm ▸ one
[GOAL]
M : Type u_1
N : Type u_2
S : Type u_3
M₀ : Type u_4
M₁ : Type u_5
R : Type u_6
G : Type u_7
G₀ : Type u_8
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : G₀
h : IsIdempotentElem p
hp : ¬p = 0
⊢ p = 1
[PROOFSTEP]
exact mul_left_cancel₀ hp (h.trans (mul_one p).symm)


[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
a b c d : R
⊢ (a + b + c) * d = a * d + b * d + c * d
[PROOFSTEP]
simp [right_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (a + 1) * b = a * b + b
[PROOFSTEP]
rw [add_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (b + 1) = a * b + a
[PROOFSTEP]
rw [mul_add, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (1 + a) * b = b + a * b
[PROOFSTEP]
rw [add_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (1 + b) = a + a * b
[PROOFSTEP]
rw [mul_add, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocSemiring α
n : α
⊢ 1 * n + 1 * n = n + n
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocSemiring α
n : α
⊢ n * 1 + n * 1 = n + n
[PROOFSTEP]
rw [mul_one]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
⊢ (a * if P then b else c) = if P then a * b else a * c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : P
⊢ a * b = a * b
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : ¬P
⊢ a * c = a * c
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
⊢ (if P then a else b) * c = if P then a * c else b * c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : P
⊢ a * c = a * c
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : ¬P
⊢ b * c = b * c
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (a * if P then 1 else 0) = if P then a else 0
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (if P then 1 else 0) * a = if P then a else 0
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a * b else 0) = (if P then a else 0) * b
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : P
⊢ (if P then a * b else 0) = (if P then a else 0) * b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : ¬P
⊢ (if P then a * b else 0) = (if P then a else 0) * b
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a * b else 0) = a * if P then b else 0
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : P
⊢ (if P then a * b else 0) = a * if P then b else 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : ¬P
⊢ (if P then a * b else 0) = a * if P then b else 0
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝² : MulZeroClass α
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b : α
⊢ (if P ∧ Q then a * b else 0) = (if P then a else 0) * if Q then b else 0
[PROOFSTEP]
simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommSemiring α
a✝ b✝ c a b : α
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b
[PROOFSTEP]
simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * -b = a * b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * b = a * -b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -a = -1 * a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ a * -1 = -a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -1 * a = -a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
src✝¹ : Zero α := inferInstanceAs (Zero α)
src✝ : InvolutiveNeg α := inferInstanceAs (InvolutiveNeg α)
⊢ -0 = 0
[PROOFSTEP]
rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ -a * b + a * b = 0
[PROOFSTEP]
rw [← right_distrib, add_left_neg, zero_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * -b + a * b = 0
[PROOFSTEP]
rw [← left_distrib, add_left_neg, mul_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b - c) = a * b - a * c
[PROOFSTEP]
simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ (a - b) * c = a * c - b * c
[PROOFSTEP]
simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
⊢ a * e + c = b * e + d ↔ a * e + c = d + b * e
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = d + b * e
⊢ a * e + c - b * e = d
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = d + b * e
⊢ d + b * e - b * e = d
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c - b * e = d
⊢ a * e + c = d + b * e
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c - b * e = d
⊢ a * e + c = a * e + c - b * e + b * e
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
⊢ a * e + c - b * e = d ↔ (a - b) * e + c = d
[PROOFSTEP]
simp [sub_mul, sub_add_eq_add_sub]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = b * e + d
⊢ (a - b) * e + c = a * e + c - b * e
[PROOFSTEP]
simp [sub_mul, sub_add_eq_add_sub]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = b * e + d
⊢ a * e + c - b * e = d
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = b * e + d
⊢ b * e + d - b * e = d
[PROOFSTEP]
simp [@add_sub_cancel α]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ (a - 1) * b = a * b - b
[PROOFSTEP]
rw [sub_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ a * (b - 1) = a * b - a
[PROOFSTEP]
rw [mul_sub, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ (1 - a) * b = b - a * b
[PROOFSTEP]
rw [sub_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ a * (1 - b) = a - a * b
[PROOFSTEP]
rw [mul_sub, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ 0 * a + 0 * a = 0 * a + 0
[PROOFSTEP]
rw [← add_mul, zero_add, add_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ a * 0 + a * 0 = a * 0 + 0
[PROOFSTEP]
rw [← mul_add, add_zero, add_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ 0 * a + 0 * a = 0 * a + 0
[PROOFSTEP]
rw [← add_mul, zero_add, add_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ a * 0 + a * 0 = a * 0 + 0
[PROOFSTEP]
rw [← mul_add, add_zero, add_zero]


[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a b : α
u : αˣ
⊢ -↑u * -↑u⁻¹ = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a b : α
u : αˣ
⊢ -↑u⁻¹ * -↑u = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a✝ b a : α
u : αˣ
⊢ -(a /ₚ u) = -a /ₚ u
[PROOFSTEP]
simp only [divp, neg_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u + b /ₚ u = (a + b) /ₚ u
[PROOFSTEP]
simp only [divp, add_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a + b /ₚ u = (a * ↑u + b) /ₚ u
[PROOFSTEP]
simp only [divp, add_mul, Units.mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a - b /ₚ u = (a * ↑u - b) /ₚ u
[PROOFSTEP]
simp only [divp, sub_mul, Units.mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u + b = (a + b * ↑u) /ₚ u
[PROOFSTEP]
simp only [divp, add_mul, Units.mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u - b = (a - b * ↑u) /ₚ u
[PROOFSTEP]
simp only [divp, sub_mul, sub_right_inj]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ b = b * ↑u * ↑u⁻¹
[PROOFSTEP]
rw [mul_assoc, Units.mul_inv, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)
[PROOFSTEP]
simp only [divp, add_mul, mul_inv_rev, val_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)
[PROOFSTEP]
rw [mul_comm (↑u₁ * b), mul_comm b]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one, mul_one]
  -- porting note: `assoc_rw` not ported: `assoc_rw [mul_inv, mul_inv, mul_one, mul_one]`
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)
[PROOFSTEP]
simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a * (1 + ↑a⁻¹ * b)
[PROOFSTEP]
rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]


[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ ↑σ' (↑σ x) = x
[PROOFSTEP]
rw [← RingHom.comp_apply, comp_eq]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ ↑(RingHom.id R₁) x = x
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ ↑σ (↑σ' x) = x
[PROOFSTEP]
rw [← RingHom.comp_apply, comp_eq₂]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ ↑(RingHom.id R₂) x = x
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁴ : Semiring R₁
inst✝³ : Semiring R₂
inst✝² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝¹ : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst✝ : RingHomInvPair σ₁₂ σ₂₁
⊢ RingHom.comp σ₂₁ σ₁₂ = RingHom.id R₁
[PROOFSTEP]
simp only [comp_eq]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁴ : Semiring R₁
inst✝³ : Semiring R₂
inst✝² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝¹ : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst✝ : RingHomInvPair σ₁₂ σ₂₁
⊢ RingHom.comp σ₁₂ σ₂₁ = RingHom.id R₂
[PROOFSTEP]
simp only [comp_eq₂]
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ RingHom.comp σ₁₂ (RingHom.id R₁) = σ₁₂
[PROOFSTEP]
ext
[GOAL]
case a
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
x✝ : R₁
⊢ ↑(RingHom.comp σ₁₂ (RingHom.id R₁)) x✝ = ↑σ₁₂ x✝
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ RingHom.comp (RingHom.id R₂) σ₁₂ = σ₁₂
[PROOFSTEP]
ext
[GOAL]
case a
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
x✝ : R₁
⊢ ↑(RingHom.comp (RingHom.id R₂) σ₁₂) x✝ = ↑σ₁₂ x✝
[PROOFSTEP]
simp
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
⊢ Function.Surjective ↑σ₁₃
[PROOFSTEP]
have := σ₂₃.surjective.comp σ₁₂.surjective
[GOAL]
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective (↑σ₂₃ ∘ ↑σ₁₂)
⊢ Function.Surjective ↑σ₁₃
[PROOFSTEP]
rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this


[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
⊢ ∀ (a b : R), a + b = b + a
[PROOFSTEP]
intro a b
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
⊢ a + b = b + a
[PROOFSTEP]
have h₁ : (1 + 1 : R) * (a + b) = a + (a + b) + b :=
  by
  rw [left_distrib]
  simp only [right_distrib, one_mul, add_assoc]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
⊢ (1 + 1) * (a + b) = a + (a + b) + b
[PROOFSTEP]
rw [left_distrib]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
⊢ (1 + 1) * a + (1 + 1) * b = a + (a + b) + b
[PROOFSTEP]
simp only [right_distrib, one_mul, add_assoc]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
h₁ : (1 + 1) * (a + b) = a + (a + b) + b
⊢ a + b = b + a
[PROOFSTEP]
have h₂ : (1 + 1 : R) * (a + b) = a + (b + a) + b :=
  by
  rw [right_distrib]
  simp only [left_distrib, one_mul, add_assoc]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
h₁ : (1 + 1) * (a + b) = a + (a + b) + b
⊢ (1 + 1) * (a + b) = a + (b + a) + b
[PROOFSTEP]
rw [right_distrib]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
h₁ : (1 + 1) * (a + b) = a + (a + b) + b
⊢ 1 * (a + b) + 1 * (a + b) = a + (b + a) + b
[PROOFSTEP]
simp only [left_distrib, one_mul, add_assoc]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
h₁ : (1 + 1) * (a + b) = a + (a + b) + b
h₂ : (1 + 1) * (a + b) = a + (b + a) + b
⊢ a + b = b + a
[PROOFSTEP]
have := h₁.symm.trans h₂
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
a b : R
h₁ : (1 + 1) * (a + b) = a + (a + b) + b
h₂ : (1 + 1) * (a + b) = a + (b + a) + b
this : a + (a + b) + b = a + (b + a) + b
⊢ a + b = b + a
[PROOFSTEP]
rwa [add_left_inj, add_right_inj] at this
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = 0
[PROOFSTEP]
have : 0 * a = 0 * a + 0 * a :=
  calc
    0 * a = (0 + 0) * a := by rw [zero_add]
    _ = 0 * a + 0 * a := by rw [right_distrib]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = (0 + 0) * a
[PROOFSTEP]
rw [zero_add]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ (0 + 0) * a = 0 * a + 0 * a
[PROOFSTEP]
rw [right_distrib]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0 * a + 0 * a
⊢ 0 * a = 0
[PROOFSTEP]
rwa [self_eq_add_right] at this
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = 0
[PROOFSTEP]
have : a * 0 = a * 0 + a * 0 :=
  calc
    a * 0 = a * (0 + 0) := by rw [zero_add]
    _ = a * 0 + a * 0 := by rw [left_distrib]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = a * (0 + 0)
[PROOFSTEP]
rw [zero_add]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * (0 + 0) = a * 0 + a * 0
[PROOFSTEP]
rw [left_distrib]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add add_left_neg
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = a * 0 + a * 0
⊢ a * 0 = 0
[PROOFSTEP]
rwa [self_eq_add_right] at this
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
a : R
⊢ a * 1 = a
[PROOFSTEP]
rw [mul_comm, one_mul]
[GOAL]
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
add_left_neg : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
rw [mul_comm, left_distrib, mul_comm, mul_comm b c]