-- Mathlib/NumberTheory/MulChar/Duality.lean
theorem exists_apply_ne_one_of_hasEnoughRootsOfUnity [Nontrivial R] {a : M} (ha : a ≠ 1) :
    ∃ χ : MulChar M R, χ a ≠ 1

Proof state:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ φ, φ hu.unit ≠ 1

Tactic:
refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_

Result:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ hu.unit ≠ 1

Proof state:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
hu : IsUnit a
ha : hu.unit = 1
⊢ a = 1

Tactic:
rw [← hu.unit_spec, ha, Units.val_eq_one]

Result:
no goals

Proof state:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ χ, χ a ≠ 1

Tactic:
refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_

Result:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ φ, φ hu.unit ≠ 1

Proof state:
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
⊢ ∃ χ, χ a ≠ 1

Tactic:
by_cases hu : IsUnit a

Result:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ χ, χ a ≠ 1

case neg
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ ∃ χ, χ a ≠ 1

Proof state:
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ 1 a ≠ 1

Tactic:
simpa only [map_nonunit _ hu] using zero_ne_one

Result:
no goals

Proof state:
case neg
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ ∃ χ, χ a ≠ 1

Tactic:
exact ⟨1, by simpa only [map_nonunit _ hu] using zero_ne_one⟩

Result:
no goals

Proof state:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ hu.unit ≠ 1

Tactic:
contrapose! ha

Result:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
hu : IsUnit a
ha : hu.unit = 1
⊢ a = 1