awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
⊢ map a_mul_emb univ = univ

Tactic:
have h_unchanged : Finset.univ.map a_mul_emb = Finset.univ := by simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
a : ↥G
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
h_unchanged : map a_mul_emb univ = univ
⊢ Eq (α := K) (∑ x ∈ map a_mul_emb univ, (↑(↑x : Kˣ) : K)) (∑ x : ↥G, (↑(↑((a_mul_emb : (a : ↥G) → ↥G) x) : Kˣ) : K))

Tactic:
have h_sum_map := Finset.univ.sum_map a_mul_emb fun x => ((x : Kˣ) : K)
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : 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 :
  Eq (α := K) (∑ x ∈ map a_mul_emb univ, (↑(↑x : Kˣ) : K)) (∑ x : ↥G, (↑(↑((a_mul_emb : (a : ↥G) → ↥G) x) : Kˣ) : K))
⊢ ∑ x : ↥G, (↑(↑x : Kˣ) : K) = (↑(↑a : Kˣ) : K) * ∑ x : ↥G, (↑(↑x : Kˣ) : K)

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

Premises used: Finset.mul_sum, Subgroup.coe_mul, mulLeftEmbedding_apply, Units.val_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : 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 : Kˣ) : K) = (↑(↑a : Kˣ) : K) * ∑ x : ↥G, (↑(↑x : Kˣ) : K)
rw : ((↑(↑a : Kˣ) : K) - 1) * ∑ x : ↥G, (↑(↑x : Kˣ) : K) = 0
rw₁ : (↑(↑a : Kˣ) : K) * ∑ x : ↥G, (↑(↑x : Kˣ) : K) - HMul.hMul (α := K) 1 (∑ x : ↥G, (↑(↑x : Kˣ) : K)) = 0
rw₂ : ∑ x : ↥G, (↑(↑x : Kˣ) : K) - HMul.hMul (α := K) 1 (∑ x : ↥G, (↑(↑x : Kˣ) : K)) = 0
rw₃ : HSub.hSub (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) = 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := K) 0 0
⊢ (↑(↑a : Kˣ) : K) - 1 = 0 ∨ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0

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

Premises used: sub_self, mul_eq_zero, sub_mul, one_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : 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 : Kˣ) : K) = (↑(↑a : Kˣ) : K) * ∑ x : ↥G, (↑(↑x : Kˣ) : K)
⊢ (↑(↑a : Kˣ) : K) - 1 = 0 ∨ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 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]
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : 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 : 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
apply : ¬(↑(↑a : Kˣ) : K) - 1 = 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0

Tactic:
apply Or.resolve_left hzero

Premises used: Or.resolve_left
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : 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 : 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
contrapose : ∀ (ha : (↑(↑a : Kˣ) : K) - 1 = 0), a = 1
⊢ ¬(↑(↑a : Kˣ) : K) - 1 = 0

Tactic:
contrapose ha
-- Module: Mathlib.FieldTheory.Finite.Basic
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₁ : (↑(↑a : Kˣ) : K) = (↑(↑1 : Kˣ) : K)
⊢ a = 1

Tactic:
ext
-- Module: Mathlib.FieldTheory.Finite.Basic
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₁ a₂ a₃ a₄ : (↑(↑a : Kˣ) : K) - (↑(↑1 : Kˣ) : K) = 0
⊢ (↑(↑a : Kˣ) : K) = (↑(↑1 : Kˣ) : K)

Tactic:
rwa [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
neg : ∀ (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)

Tactic:
by_cases G_bot : G = ⊥
-- Module: Mathlib.FieldTheory.Finite.Basic
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 = ⊥
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)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)

Tactic:
subst G_bot
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Fintype ↥⊥
inst_3 : Decidable (Eq.{u_1 + 1} (α := Subgroup Kˣ) ⊥ ⊥)
pos : Eq.{u_1 + 1} (α := ↥⊥) default 1
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥⊥, (↑(↑x : Kˣ) : K)) (if Eq.{u_1 + 1} (α := Subgroup Kˣ) ⊥ ⊥ then 1 else 0)

Tactic:
simp only [univ_unique, sum_singleton, ↓reduceIte, Units.val_eq_one, OneMemClass.coe_eq_one]

Premises used: Finset.univ_unique, OneMemClass.coe_eq_one, Finset.sum_singleton, reduceIte, Units.val_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
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} (α := ↥⊥)
    (Subtype.mk (p := fun (x : Kˣ) ↦ Membership.mem (γ := Set Kˣ) {1} x) 1 ⋯ :
      { x : Kˣ // Membership.mem (γ := Set Kˣ) {1} x })
    (1 : ↥⊥)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
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 = ⊥
neg : Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (if G = ⊥ then 1 else 0)

Tactic:
simp only [G_bot, ite_false]

Premises used: ite_false
-- Module: Mathlib.FieldTheory.Finite.Basic
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)) 0

Tactic:
sum_subgroup_units_eq_zero G_bot

Premises used: FiniteField.sum_subgroup_units_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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)) 0

Tactic:
exact sum_subgroup_units_eq_zero G_bot

Premises used: FiniteField.sum_subgroup_units_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ k < Nat.card.{u_1} ↥G

Tactic:
rw [← Nat.card_eq_fintype_card] at k_lt_card_G

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ Nontrivial K

Tactic:
nontriviality K
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ IsDomain K

Tactic:
have := NoZeroDivisors.to_isDomain K
-- Module: Mathlib.FieldTheory.Finite.Basic
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
rcases : ∀ (a : ↥G) (ha : a ^ k ≠ 1), Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K) ^ k) 0
⊢ 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⟩

Premises used: exists_pow_ne_one_of_isCyclic
-- Module: Mathlib.FieldTheory.Finite.Basic
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
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))
⊢ 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:
simp_rw [← mul_pow]

Premises used: mul_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
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_1 : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h :
  ∀ (x : ↥G),
    ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k = ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a) x
⊢ 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:
funext x
-- Module: Mathlib.FieldTheory.Finite.Basic
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
x : ↥G
⊢ ((↑(↑x : Kˣ) : K) * (↑(↑a : Kˣ) : K)) ^ k = ((fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) ∘ fun (x : ↥G) ↦ x * a) x

Tactic:
simp only [Function.comp_apply, Subgroup.coe_mul, Units.val_mul]

Premises used: Subgroup.coe_mul, Function.comp_apply, Units.val_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
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)

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]
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
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)))
⊢ 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:
rw [as_comp, ← Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
e_s : Eq.{u_1 + 1} (α := Multiset ↥G) (val univ) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ))
⊢ 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:
congr
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
e_s : Eq.{u_1 + 1} (α := Multiset ↥G) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ)) (val univ)
⊢ Eq.{u_1 + 1} (α := Multiset ↥G) (val univ) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ))

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.FieldTheory.Finite.Basic
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) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ)) (val univ)

Tactic:
Multiset.map_univ_val_equiv (Equiv.mulRight a)

Premises used: Set.Mem, Multiset.map_univ_val_equiv, Equiv.mulRight
-- Module: Mathlib.FieldTheory.Finite.Basic
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) (Multiset.map (fun (x : ↥G) ↦ x * a) (val univ)) (val univ)

Tactic:
exact Multiset.map_univ_val_equiv (Equiv.mulRight a)

Premises used: Multiset.map_univ_val_equiv, Equiv.mulRight
-- Module: Mathlib.FieldTheory.Finite.Basic
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))

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)
-- Module: Mathlib.FieldTheory.Finite.Basic
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))
rw 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)))
⊢ 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:
rw [h_multiset_map]
-- Module: Mathlib.FieldTheory.Finite.Basic
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)))

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]
-- Module: Mathlib.FieldTheory.Finite.Basic
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)))
⊢ 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

Premises used: Multiset.sum_map_mul_right
-- Module: Mathlib.FieldTheory.Finite.Basic
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
rw₄ rw₅ : Eq.{u_1 + 1} (α := K) 0 0
⊢ ((↑(↑a : Kˣ) : K) ^ 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]

Premises used: sub_self, sub_mul, mul_comm, one_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
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

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]
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ (↑(↑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

Premises used: mul_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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

Tactic:
hzero.resolve_left fun h => ha ?_

Premises used: Or.resolve_left