-- Mathlib/FieldTheory/Finite/Basic.lean
theorem sum_subgroup_units_eq_zero [Ring K] [NoZeroDivisors K]
    {G : Subgroup Kˣ} [Fintype G] (hg : G ≠ ⊥) :
    ∑ x : G, (x.val : K) = 0

Proof state:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : ∃ a, a ≠ 1
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
rcases hg with ⟨a, ha⟩

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : G ≠ ⊥
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
rw [Subgroup.ne_bot_iff_exists_ne_one] at hg

Result:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : ∃ a, a ≠ 1
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
⊢ map a_mul_emb univ = univ

Tactic:
simp

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
have hzero : (((a : Kˣ) : K) - 1) = 0 ∨ ∑ x : ↥G, ((x : Kˣ) : K) = 0 := by
  rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ a = 1

Tactic:
ext

Result:
case intro.a.a
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ ↑↑a = ↑↑1

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
have h_unchanged : Finset.univ.map a_mul_emb = Finset.univ := by simp

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
apply Or.resolve_left hzero

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
⊢ ¬↑↑a - 1 = 0

Proof state:
case intro.a.a
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ ↑↑a = ↑↑1

Tactic:
rwa [← sub_eq_zero]

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x ∈ map a_mul_emb univ, ↑↑x = ∑ x : ↥G, ↑↑(a_mul_emb x)
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
simp only [h_unchanged, mulLeftEmbedding_apply, Subgroup.coe_mul, Units.val_mul, ← mul_sum,
  a_mul_emb] at h_sum_map

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
⊢ ¬↑↑a - 1 = 0

Tactic:
contrapose! ha

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0
ha : ↑↑a - 1 = 0
⊢ a = 1

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
have h_sum_map := Finset.univ.sum_map a_mul_emb fun x => ((x : Kˣ) : K)

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x ∈ map a_mul_emb univ, ↑↑x = ∑ x : ↥G, ↑↑(a_mul_emb x)
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
⊢ ∑ x : ↥G, ↑↑x = 0

Tactic:
let a_mul_emb : G ↪ G := mulLeftEmbedding a

Result:
case intro
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
⊢ ∑ x : ↥G, ↑↑x = 0

Proof state:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x
⊢ ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0

Tactic:
rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]

Result:
no goals