case pos
α : Type ?u.17885
M₀ : Type ?u.17888
G₀ : Type u_2
M₀' : Type ?u.17894
G₀' : Type u_1
F : Type u_3
F' : Type ?u.17903
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)⁻¹

case neg
α : Type ?u.17885
M₀ : Type ?u.17888
G₀ : Type u_2
M₀' : Type ?u.17894
G₀' : Type u_1
F : Type u_3
F' : Type ?u.17903
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)⁻¹
α : Type ?u.17885
M₀ : Type ?u.17888
G₀ : Type u_2
M₀' : Type ?u.17894
G₀' : Type u_1
F : Type u_3
F' : Type ?u.17903
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
⊢ ↑f a⁻¹ = (↑f a)⁻¹
by_cases h : a = 0
no goals
case pos
α : Type ?u.17885
M₀ : Type ?u.17888
G₀ : Type u_2
M₀' : Type ?u.17894
G₀' : Type u_1
F : Type u_3
F' : Type ?u.17903
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)⁻¹
simp [h, map_zero f]
case neg.h
α : Type ?u.17885
M₀ : Type ?u.17888
G₀ : Type u_2
M₀' : Type ?u.17894
G₀' : Type u_1
F : Type u_3
F' : Type ?u.17903
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
case neg
α : Type ?u.17885
M₀ : Type ?u.17888
G₀ : Type u_2
M₀' : Type ?u.17894
G₀' : Type u_1
F : Type u_3
F' : Type ?u.17903
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)⁻¹
apply eq_inv_of_mul_eq_one_left
no goals
case neg.h
α : Type ?u.17885
M₀ : Type ?u.17888
G₀ : Type u_2
M₀' : Type ?u.17894
G₀' : Type u_1
F : Type u_3
F' : Type ?u.17903
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
rw [← map_mul, inv_mul_cancel h, map_one]