case inl
α : Type ?u.15847
M₀ : Type ?u.15850
G₀ : Type u_3
M₀' : Type u_1
G₀' : Type ?u.15859
F : Type ?u.15862
F' : Type u_2
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⁻¹

case inr
α : Type ?u.15847
M₀ : Type ?u.15850
G₀ : Type u_3
M₀' : Type u_1
G₀' : Type ?u.15859
F : Type ?u.15862
F' : Type u_2
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⁻¹
α : Type ?u.15847
M₀ : Type ?u.15850
G₀ : Type u_3
M₀' : Type u_1
G₀' : Type ?u.15859
F : Type ?u.15862
F' : Type u_2
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⁻¹
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case inl
α : Type ?u.15847
M₀ : Type ?u.15850
G₀ : Type u_3
M₀' : Type u_1
G₀' : Type ?u.15859
F : Type ?u.15862
F' : Type u_2
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⁻¹
rw [inv_zero, map_zero, map_zero]
no goals
case inr
α : Type ?u.15847
M₀ : Type ?u.15850
G₀ : Type u_3
M₀' : Type u_1
G₀' : Type ?u.15859
F : Type ?u.15862
F' : Type u_2
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⁻¹
exact (IsUnit.mk0 a ha).eq_on_inv f g h