-- Mathlib/GroupTheory/FiniteAbelian/Duality.lean
private
lemma exists_apply_ne_one_aux
    (H : ∀ n : ℕ, n ∣ Monoid.exponent G → ∀ a : ZMod n, a ≠ 0 →
      ∃ φ : Multiplicative (ZMod n) →* M, φ (.ofAdd a) ≠ 1)
    {a : G} (ha : a ≠ 1) :
    ∃ φ : G →* M, φ a ≠ 1

Proof state:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
⊢ ∃ i, e a i ≠ 1

Tactic:
contrapose! ha

Result:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
ha : ∀ (i : ι), e a i = 1
⊢ a = 1

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi✝ : e a i ≠ 1
hi : Multiplicative.toAdd (e a i) ≠ 0
⊢ ∃ φ, φ a ≠ 1

Tactic:
obtain ⟨φi, hφi⟩ := H (n i) (dvd_exponent e i) ((e a i).toAdd) hi

Result:
case intro.intro.intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi✝ : e a i ≠ 1
hi : Multiplicative.toAdd (e a i) ≠ 0
φi : Multiplicative (ZMod (n i)) →* M
hφi : φi (Multiplicative.ofAdd (Multiplicative.toAdd (e a i))) ≠ 1
⊢ ∃ φ, φ a ≠ 1

Proof state:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
⊢ ∃ φ, φ a ≠ 1

Tactic:
let e := h.some

Result:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
⊢ ∃ φ, φ a ≠ 1

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi✝ : e a i ≠ 1
hi : Multiplicative.toAdd (e a i) ≠ 0
φi : Multiplicative (ZMod (n i)) →* M
hφi : φi (Multiplicative.ofAdd (Multiplicative.toAdd (e a i))) ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
use (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i)).comp e

Result:
case h
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi✝ : e a i ≠ 1
hi : Multiplicative.toAdd (e a i) ≠ 0
φi : Multiplicative (ZMod (n i)) →* M
hφi : φi (Multiplicative.ofAdd (Multiplicative.toAdd (e a i))) ≠ 1
⊢ ((φi.comp (Pi.evalMonoidHom (fun i => Multiplicative (ZMod (n i))) i)).comp ↑e) a ≠ 1

Proof state:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
obtain ⟨ι, _, n, _, h⟩ := CommGroup.equiv_prod_multiplicative_zmod_of_finite G

Result:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
⊢ ∃ φ, φ a ≠ 1

Proof state:
case intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
⊢ ∃ φ, φ a ≠ 1

Tactic:
obtain ⟨i, hi⟩ : ∃ i : ι, e a i ≠ 1 := by
  contrapose! ha
  exact (MulEquiv.map_eq_one_iff e).mp <| funext ha

Result:
case intro.intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi : e a i ≠ 1
⊢ ∃ φ, φ a ≠ 1

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi : e a i ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
have hi : (e a i).toAdd ≠ 0 := by
  simp only [ne_eq, toAdd_eq_zero, hi, not_false_eq_true]

Result:
case intro.intro.intro.intro.intro
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi✝ : e a i ≠ 1
hi : Multiplicative.toAdd (e a i) ≠ 0
⊢ ∃ φ, φ a ≠ 1

Proof state:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
i : ι
hi : e a i ≠ 1
⊢ Multiplicative.toAdd (e a i) ≠ 0

Tactic:
simp only [ne_eq, toAdd_eq_zero, hi, not_false_eq_true]

Result:
no goals