[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a✝ b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (0 * a) = f 0
[PROOFSTEP]
simp only [mul, zero, zero_mul]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a✝ b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (a * 0) = f 0
[PROOFSTEP]
simp only [mul, zero, mul_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ 0 * f x = 0
[PROOFSTEP]
simp only [← zero, ← mul, zero_mul]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ f x * 0 = 0
[PROOFSTEP]
simp only [← zero, ← mul, mul_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a✝ b✝ : M₀
H : a✝ * b✝ = 0
⊢ f (?m.2223 H) * f (?m.2224 H) = 0
[PROOFSTEP]
rw [← mul, H, zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a✝ b✝ : M₀
H✝ : a✝ * b✝ = 0
this : f a✝ * f b✝ = 0
H : f a✝ = 0
⊢ f a✝ = f 0
[PROOFSTEP]
rwa [zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a✝ b✝ : M₀
H✝ : a✝ * b✝ = 0
this : f a✝ * f b✝ = 0
H : f b✝ = 0
⊢ f b✝ = f 0
[PROOFSTEP]
rwa [zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
⊢ b✝ = c✝
[PROOFSTEP]
have := congr_arg f He
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f (a✝ * b✝) = f (a✝ * c✝)
⊢ b✝ = c✝
[PROOFSTEP]
rw [mul, mul] at this 
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f a✝ * f b✝ = f a✝ * f c✝
⊢ b✝ = c✝
[PROOFSTEP]
exact hf (mul_left_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f a✝ * f b✝ = f a✝ * f c✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0
[PROOFSTEP]
rw [Hfa, zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
⊢ a✝ = c✝
[PROOFSTEP]
have := congr_arg f He
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f (a✝ * b✝) = f (c✝ * b✝)
⊢ a✝ = c✝
[PROOFSTEP]
rw [mul, mul] at this 
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f a✝ * f b✝ = f c✝ * f b✝
⊢ a✝ = c✝
[PROOFSTEP]
exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f a✝ * f b✝ = f c✝ * f b✝
Hfa : f b✝ = 0
⊢ f b✝ = f 0
[PROOFSTEP]
rw [Hfa, zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : CancelMonoidWithZero M₀
a b c : M₀
inst✝³ : Zero M₀'
inst✝² : Mul M₀'
inst✝¹ : One M₀'
inst✝ : Pow M₀' ℕ
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : M₀'), f (x * y) = f x * f y
npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : Monoid M₀' := Injective.monoid f hf one mul npow
src✝ : MulZeroClass M₀' := Injective.mulZeroClass f hf zero mul
a✝ b✝ c✝ : M₀'
hx : a✝ ≠ 0
H : a✝ * b✝ = a✝ * c✝
⊢ f a✝ * f b✝ = f a✝ * f c✝
[PROOFSTEP]
erw [← mul, ← mul, H]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : CancelMonoidWithZero M₀
a b c : M₀
inst✝³ : Zero M₀'
inst✝² : Mul M₀'
inst✝¹ : One M₀'
inst✝ : Pow M₀' ℕ
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : M₀'), f (x * y) = f x * f y
npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : Monoid M₀' := Injective.monoid f hf one mul npow
src✝ : MulZeroClass M₀' := Injective.mulZeroClass f hf zero mul
a✝ b✝ c✝ : M₀'
hx : b✝ ≠ 0
H : a✝ * b✝ = c✝ * b✝
⊢ f a✝ * f b✝ = f c✝ * f b✝
[PROOFSTEP]
erw [← mul, ← mul, H]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
src✝² : MonoidWithZero G₀' := Injective.monoidWithZero f hf zero one mul npow
src✝¹ : DivInvMonoid G₀' := Injective.divInvMonoid f hf one mul inv div npow zpow
src✝ : Nontrivial G₀' := pullback_nonzero f zero one
⊢ f 0⁻¹ = f 0
[PROOFSTEP]
erw [inv, zero, inv_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x✝ : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
src✝² : MonoidWithZero G₀' := Injective.monoidWithZero f hf zero one mul npow
src✝¹ : DivInvMonoid G₀' := Injective.divInvMonoid f hf one mul inv div npow zpow
src✝ : Nontrivial G₀' := pullback_nonzero f zero one
x : G₀'
hx : x ≠ 0
⊢ f (x * x⁻¹) = f 1
[PROOFSTEP]
erw [one, mul, inv, mul_inv_cancel ((hf.ne_iff' zero).2 hx)]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
src✝¹ : MonoidWithZero G₀' := Surjective.monoidWithZero f hf zero one mul npow
src✝ : DivInvMonoid G₀' := Surjective.divInvMonoid f hf one mul inv div npow zpow
⊢ 0⁻¹ = 0
[PROOFSTEP]
erw [← zero, ← inv, inv_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x✝ : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
src✝¹ : MonoidWithZero G₀' := Surjective.monoidWithZero f hf zero one mul npow
src✝ : DivInvMonoid G₀' := Surjective.divInvMonoid f hf one mul inv div npow zpow
x : G₀
hx : f x ≠ 0
⊢ f x * (f x)⁻¹ = 1
[PROOFSTEP]
erw [← inv, ← mul, mul_inv_cancel (mt (congr_arg f) <| fun h ↦ hx (h.trans zero)), one]
