awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : 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 : Kˣ) : K) = (↑(↑a : Kˣ) : K) * ∑ x : ↥G, (↑(↑x : Kˣ) : K)
hzero : (↑(↑a : Kˣ) : K) - 1 = 0 ∨ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
ha : (↑(↑a : Kˣ) : K) - 1 = 0
⊢ (↑(↑a : Kˣ) : K) = (↑(↑1 : Kˣ) : K)
have a₁ : (↑(↑a : Kˣ) : K) - (↑(↑1 : Kˣ) : K) = 0
Tactic: rwa [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
inst_3 : Decidable (G = ⊥)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)
have pos : ∀ (G_bot : G = ⊥), Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)
Tactic: by_cases G_bot : G = ⊥
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
inst_3 : Decidable (G = ⊥)
pos : ∀ (G_bot : G = ⊥), Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)
have neg : ∀ (G_bot : ¬G = ⊥), Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)
Tactic: by_cases G_bot : G = ⊥
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
inst_3 : Decidable (G = ⊥)
G_bot : G = ⊥
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)
have pos : ∀ [inst_4 : Fintype ↥⊥] [inst_5 : Decidable (Eq.{u_1 + 1} (α := Subgroup Kˣ) ⊥ ⊥)],
  Eq.{u_1 + 1} (α := K) (∑ x : ↥⊥, (↑(↑x : Kˣ) : K)) (if Eq.{u_1 + 1} (α := Subgroup Kˣ) ⊥ ⊥ then 1 else 0)
Tactic: subst G_bot
Cleared hypotheses: G, inst_2, inst_3, G_bot
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Fintype ↥⊥
inst_3 : Decidable (Eq.{u_1 + 1} (α := Subgroup Kˣ) ⊥ ⊥)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥⊥, (↑(↑x : Kˣ) : K)) (if Eq.{u_1 + 1} (α := Subgroup Kˣ) ⊥ ⊥ then 1 else 0)
have pos : Eq.{u_1 + 1} (α := ↥⊥) default 1
Tactic: simp only [univ_unique, sum_singleton, ↓reduceIte, Units.val_eq_one, OneMemClass.coe_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
inst_3 : Decidable (G = ⊥)
G_bot : ¬G = ⊥
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)
have neg : Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
Tactic: simp only [G_bot, ite_false]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Fintype.card.{u_1} ↥G
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K) ^ k) 0
have k_lt_card_G₁ : k < Nat.card.{u_1} ↥G
Tactic: rw [← Nat.card_eq_fintype_card] at k_lt_card_G
Cleared hypotheses: k_lt_card_G
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K) ^ k) 0
have a : Nontrivial K
Tactic: nontriviality K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K) ^ k) 0
have this : IsDomain K
Tactic: have := NoZeroDivisors.to_isDomain K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K) ^ k) 0
have rcases : ∀ (a : ↥G) (ha : a ^ k ≠ 1), Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K) ^ k) 0
Tactic: rcases (exists_pow_ne_one_of_isCyclic k_pos k_lt_card_G) with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
have simp_rw : Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
  (Multiset.map (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k) (val univ))
Tactic: simp_rw [← mul_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ Eq.{u_1 + 1} (α := (x : ↥G) → K) (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k)
    ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a)
have h : ∀ (x : ↥G), ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k = ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k) (val univ))
have as_comp : Eq.{u_1 + 1} (α := (x : ↥G) → K) (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k)
  ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a)
Tactic: have as_comp :
      (fun x : ↥G => (((x : Kˣ) : K) * ((a : Kˣ) : K)) ^ k)
        = (fun x : ↥G => ((x : Kˣ) : K) ^ k) ∘ fun x : ↥G => x * a := by
      funext x
      simp only [Function.comp_apply, Subgroup.coe_mul, Units.val_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
as_comp :
  Eq.{u_1 + 1} (α := (x : ↥G) → K) (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k)
    ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a)
⊢ Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k) (val univ))
have rw : Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
  (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ)))
Tactic: rw [as_comp, ← Multiset.map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
as_comp :
  Eq.{u_1 + 1} (α := (x : ↥G) → K) (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k)
    ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a)
⊢ Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ)))
have e_s : Eq.{u_1 + 1} (α := Multiset ↥G) (val univ) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ))
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
as_comp :
  Eq.{u_1 + 1} (α := (x : ↥G) → K) (fun (x : ↥G) ↦ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k)
    ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a)
⊢ Eq.{u_1 + 1} (α := Multiset ↥G) (val univ) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ))
have e_s : Eq.{u_1 + 1} (α := Multiset ↥G) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ)) (val univ)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))) 0
have h_multiset_map : Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
  (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
Tactic: have h_multiset_map :
    Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k) =
      Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) := by
    simp_rw [← mul_pow]
    have as_comp :
      (fun x : ↥G => (((x : Kˣ) : K) * ((a : Kˣ) : K)) ^ k)
        = (fun x : ↥G => ((x : Kˣ) : K) ^ k) ∘ fun x : ↥G => x * a := by
      funext x
      simp only [Function.comp_apply, Subgroup.coe_mul, Units.val_mul]
    rw [as_comp, ← Multiset.map_map]
    congr
    rw [eq_comm]
    exact Multiset.map_univ_val_equiv (Equiv.mulRight a)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)))
    (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ)))
have rw : Eq.{u_1 + 1} (α := K)
  (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ)))
  (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ)))
Tactic: rw [h_multiset_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))) 0
have h_multiset_map_sum : Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)))
  (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ)))
Tactic: have h_multiset_map_sum : (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k) Finset.univ.val).sum =
    (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) Finset.univ.val).sum := by
    rw [h_multiset_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)))
    (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ)))
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))) 0
have h_multiset_map_sum₁ : Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
Tactic: rw [Multiset.sum_map_mul_right] at h_multiset_map_sum
Cleared hypotheses: h_multiset_map_sum
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
⊢ ((↑(↑a : Kˣ) : K) ^ k - 1) * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) = 0
have rw : (↑(↑a : Kˣ) : K) ^ k * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) -
    HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
  0
Tactic: rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
rw :
  (↑(↑a : Kˣ) : K) ^ k * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
⊢ ((↑(↑a : Kˣ) : K) ^ k - 1) * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) = 0
have rw₁ : Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k -
    HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
  0
Tactic: rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
rw :
  (↑(↑a : Kˣ) : K) ^ k * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
rw₁ :
  Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
⊢ ((↑(↑a : Kˣ) : K) ^ k - 1) * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) = 0
have rw₂ : Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) -
    HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
  0
Tactic: rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
rw :
  (↑(↑a : Kˣ) : K) ^ k * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
rw₁ :
  Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
rw₂ :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
⊢ ((↑(↑a : Kˣ) : K) ^ k - 1) * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) = 0
have rw₃ : HSub.hSub (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)))
    (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
  0
Tactic: rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
rw :
  (↑(↑a : Kˣ) : K) ^ k * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
rw₁ :
  Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
rw₂ :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) -
      HMul.hMul (α := K) 1 (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
rw₃ :
  HSub.hSub (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)))
      (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) =
    0
⊢ ((↑(↑a : Kˣ) : K) ^ k - 1) * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) = 0
have rw₄ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))) 0
have hzero : ((↑(↑a : Kˣ) : K) ^ k - 1) * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) = 0
Tactic: have hzero : (((a : Kˣ) : K) ^ k - 1 : K)
                  * (Multiset.map (fun i : G => (i.val : K) ^ k) Finset.univ.val).sum = 0 := by
    rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
hzero : ((↑(↑a : Kˣ) : K) ^ k - 1) * Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ)) = 0
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))) 0
have hzero₁ : (↑(↑a : Kˣ) : K) ^ k - 1 = 0 ∨
  Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) 0
Tactic: rw [mul_eq_zero] at hzero
Cleared hypotheses: hzero
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
hzero :
  (↑(↑a : Kˣ) : K) ^ k - 1 = 0 ∨
    Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) 0
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))) 0
have refine : ∀ (h : (↑(↑a : Kˣ) : K) ^ k - 1 = 0), a ^ k = 1
Tactic: refine hzero.resolve_left fun h => ha ?_