[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
hc : c ≠ 0
⊢ a / c / (b / c) = a / b
[PROOFSTEP]
rw [div_div_eq_mul_div, div_mul_cancel _ hc]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
hc : c ≠ 0
⊢ a / c * (c / b) = a / b
[PROOFSTEP]
rw [← mul_div_assoc, div_mul_cancel _ hc]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ c a b : G₀
h : b = 0 → a = 0
hb : b = 0
⊢ a / b * b = a
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ c a b : G₀
h : b = 0 → a = 0
hb : b = 0
⊢ a * b / b = a
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c d a b : G₀
h : a = 0 → b = 0
⊢ a * b / a = b
[PROOFSTEP]
rw [mul_comm, mul_div_cancel_of_imp h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c d a b : G₀
h : b = 0 → a = 0
⊢ b * (a / b) = a
[PROOFSTEP]
rw [mul_comm, div_mul_cancel_of_imp h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c✝ d✝ a b c d : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ a * d = c * b
[PROOFSTEP]
rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel _ hd]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a b✝ c d b : G₀
h : a ≠ 0
⊢ 1 / (a * b) * a = 1 / b
[PROOFSTEP]
rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c d a b : G₀
hc : c ≠ 0
⊢ c / a / (c / b) = b / a
[PROOFSTEP]
rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : GroupWithZero G₀
inst✝³ : Nontrivial M₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f✝ : F
a : G₀
f g : F'
h : ↑f a = ↑g a
⊢ ↑f a⁻¹ = ↑g a⁻¹
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : GroupWithZero G₀
inst✝³ : Nontrivial M₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f✝ : F
f g : F'
h : ↑f 0 = ↑g 0
⊢ ↑f 0⁻¹ = ↑g 0⁻¹
[PROOFSTEP]
rw [inv_zero, map_zero, map_zero]
[GOAL]
case inr
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : GroupWithZero G₀
inst✝³ : Nontrivial M₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f✝ : F
a : G₀
f g : F'
h : ↑f a = ↑g a
ha : a ≠ 0
⊢ ↑f a⁻¹ = ↑g a⁻¹
[PROOFSTEP]
exact (IsUnit.mk0 a ha).eq_on_inv f g h
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
⊢ ↑f a⁻¹ = (↑f a)⁻¹
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
h : a = 0
⊢ ↑f a⁻¹ = (↑f a)⁻¹
[PROOFSTEP]
simp [h, map_zero f]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
h : ¬a = 0
⊢ ↑f a⁻¹ = (↑f a)⁻¹
[PROOFSTEP]
apply eq_inv_of_mul_eq_one_left
[GOAL]
case neg.h
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
h : ¬a = 0
⊢ ↑f a⁻¹ * ↑f a = 1
[PROOFSTEP]
rw [← map_mul, inv_mul_cancel h, map_one]
