-- Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean
lemma isLocalHom_of_exists_map_ne_one [FunLike F G₀ M] [MonoidHomClass F G₀ M] {f : F}
    (hf : ∃ x : G₀, f x ≠ 1) : IsLocalHom f where
  map_nonunit a h

Proof state:
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h : IsUnit (f a)
⊢ IsUnit a

Tactic:
rcases eq_or_ne a 0 with (rfl | h)

Result:
case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
h : IsUnit (f 0)
⊢ IsUnit 0

case inr
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h✝ : IsUnit (f a)
h : a ≠ 0
⊢ IsUnit a

Proof state:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
⊢ IsUnit 0

Tactic:
refine (ht ?_).elim

Result:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
⊢ f t = 1

Proof state:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
⊢ f t = 1

Tactic:
have := map_mul f t 0

Result:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : f (t * 0) = f t * f 0
⊢ f t = 1

Proof state:
case inr
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
a : G₀
h✝ : IsUnit (f a)
h : a ≠ 0
⊢ IsUnit a

Tactic:
exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩

Result:
no goals

Proof state:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : 1 * f 0 = f t * f 0
⊢ f t = 1

Tactic:
exact (h.mul_right_cancel this).symm

Result:
no goals

Proof state:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : f (t * 0) = f t * f 0
⊢ f t = 1

Tactic:
rw [← one_mul (f (t * 0)), mul_zero] at this

Result:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : 1 * f 0 = f t * f 0
⊢ f t = 1

Proof state:
case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
hf : ∃ x, f x ≠ 1
h : IsUnit (f 0)
⊢ IsUnit 0

Tactic:
obtain ⟨t, ht⟩ := hf

Result:
case inl.intro
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
⊢ IsUnit 0