awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this_1 : DecidableEq R := Classical.decEq R
this : ¬Disjoint.{u_2} (α := Finset R) (image (fun (x : R) ↦ eval x f) univ) (image (fun (x : R) ↦ eval x (-g)) univ)
⊢ ∃ (a : R) (b : R), eval a f + eval b g = 0
have this₁ : ¬∀ ⦃a : R⦄,
    (∃ (a_1 : R), Membership.mem (γ := Finset R) univ a_1 ∧ eval a_1 f = a) →
      ¬∃ (a_2 : R), Membership.mem (γ := Finset R) univ a_2 ∧ eval a_2 (-g) = a
Tactic: simp only [disjoint_left, mem_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this_1 : DecidableEq R := Classical.decEq R
this :
  ¬∀ ⦃a : R⦄,
      (∃ (a_1 : R), Membership.mem (γ := Finset R) univ a_1 ∧ eval a_1 f = a) →
        ¬∃ (a_2 : R), Membership.mem (γ := Finset R) univ a_2 ∧ eval a_2 (-g) = a
⊢ ∃ (a : R) (b : R), eval a f + eval b g = 0
have this₁ : ∃ (a : R),
  (∃ (a_1 : R), Membership.mem (γ := Finset R) univ a_1 ∧ eval a_1 f = a) ∧
    ∃ (a_1 : R), Membership.mem (γ := Finset R) univ a_1 ∧ eval a_1 (-g) = a
Tactic: push Not at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this_1 : DecidableEq R := Classical.decEq R
this :
  ∃ (a : R),
    (∃ (a_1 : R), Membership.mem (γ := Finset R) univ a_1 ∧ eval a_1 f = a) ∧
      ∃ (a_1 : R), Membership.mem (γ := Finset R) univ a_1 ∧ eval a_1 (-g) = a
⊢ ∃ (a : R) (b : R), eval a f + eval b g = 0
have rcases : ∀ (x a : R),
  Membership.mem (γ := Finset R) univ a →
    ∀ (ha : eval a f = x) (b : R),
      Membership.mem (γ := Finset R) univ b → ∀ (hb : eval b (-g) = x), ∃ (a : R) (b : R), eval a f + eval b g = 0
Tactic: rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left : Membership.mem (γ := Finset R) univ a
ha : eval a f = x
b : R
left_1 : Membership.mem (γ := Finset R) univ b
hb : eval b (-g) = x
⊢ eval a f + eval b g = 0
have rw : x + eval b g = 0
Tactic: rw [ha, ← hb, eval_neg, neg_add_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left : Membership.mem (γ := Finset R) univ a
ha : eval a f = x
b : R
left_1 : Membership.mem (γ := Finset R) univ b
hb : eval b (-g) = x
rw : x + eval b g = 0
⊢ eval a f + eval b g = 0
have rw₁ : eval b (-g) + eval b g = 0
Tactic: rw [ha, ← hb, eval_neg, neg_add_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left : Membership.mem (γ := Finset R) univ a
ha : eval a f = x
b : R
left_1 : Membership.mem (γ := Finset R) univ b
hb : eval b (-g) = x
rw : x + eval b g = 0
rw₁ : eval b (-g) + eval b g = 0
⊢ eval a f + eval b g = 0
have rw₂ : -eval b g + eval b g = 0
Tactic: rw [ha, ← hb, eval_neg, neg_add_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Fintype R
f g : R[X]
hf2 : f.degree = 2
hg2 : g.degree = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left : Membership.mem (γ := Finset R) univ a
ha : eval a f = x
b : R
left_1 : Membership.mem (γ := Finset R) univ b
hb : eval b (-g) = x
rw : x + eval b g = 0
rw₁ : eval b (-g) + eval b g = 0
rw₂ : -eval b g + eval b g = 0
⊢ eval a f + eval b g = 0
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [ha, ← hb, eval_neg, neg_add_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
⊢ Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)
have this : Eq.{u_1 + 1} (α := Kˣ) (∏ x ∈ erase univ (-1), x) 1
Tactic: have : (∏ x ∈ (@univ Kˣ _).erase (-1), x) = 1 :=
      prod_involution (fun x _ => x⁻¹) (by simp)
        (fun a => by simp +contextual [Units.inv_eq_self_iff])
        (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
this : Eq.{u_1 + 1} (α := Kˣ) (∏ x ∈ erase univ (-1), x) 1
⊢ Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)
have rw : Eq (α := Kˣ) (∏ x ∈ insert (-1) (erase univ (-1)), x) (-1)
Tactic: rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
this : Eq.{u_1 + 1} (α := Kˣ) (∏ x ∈ erase univ (-1), x) 1
rw : Eq (α := Kˣ) (∏ x ∈ insert (-1) (erase univ (-1)), x) (-1)
⊢ Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)
have rw₁ : HMul.hMul (α := Kˣ) (-1) (∏ x ∈ erase univ (-1), x) = -1
Tactic: rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
this : Eq.{u_1 + 1} (α := Kˣ) (∏ x ∈ erase univ (-1), x) 1
rw : Eq (α := Kˣ) (∏ x ∈ insert (-1) (erase univ (-1)), x) (-1)
rw₁ : HMul.hMul (α := Kˣ) (-1) (∏ x ∈ erase univ (-1), x) = -1
⊢ Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)
have rw₂ : HMul.hMul (α := Kˣ) (-1) 1 = -1
Tactic: rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
this : Eq.{u_1 + 1} (α := Kˣ) (∏ x ∈ erase univ (-1), x) 1
rw : Eq (α := Kˣ) (∏ x ∈ insert (-1) (erase univ (-1)), x) (-1)
rw₁ : HMul.hMul (α := Kˣ) (-1) (∏ x ∈ erase univ (-1), x) = -1
rw₂ : HMul.hMul (α := Kˣ) (-1) 1 = -1
⊢ Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)
have rw₃ : Eq.{u_1 + 1} (α := Kˣ) (-1) (-1)
Tactic: rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
⊢ Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)
have have : ∀ (this : Eq.{u_1 + 1} (α := Kˣ) (∏ x ∈ erase univ (-1), x) 1), Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)
Tactic: classical
    have : (∏ x ∈ (@univ Kˣ _).erase (-1), x) = 1 :=
      prod_involution (fun x _ => x⁻¹) (by simp)
        (fun a => by simp +contextual [Units.inv_eq_self_iff])
        (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
    rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
⊢ False
have have : ∀ (p : ℕ) (char_p : CharP K p), False
Tactic: have ⟨p, char_p⟩ := CharP.exists K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
⊢ False
have hd : p ∣ n
Tactic: have hd : p ∣ n := (CharP.cast_eq_zero_iff K p n).mp nzero
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
⊢ False
have fact_pprime : Fact (Nat.Prime p)
Tactic: have fact_pprime := Fact.mk pprime
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
⊢ False
have inl : ∀ (x : ↥G) (hx : orderOf x = p), False
Tactic: have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
⊢ orderOf u = p
have rwa : orderOf (↑x : Kˣ) = p
Tactic: rwa [orderOf_units, Subgroup.orderOf_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
⊢ False
have hu : orderOf u = p
Tactic: have hu : orderOf u = p := by rwa [orderOf_units, Subgroup.orderOf_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
⊢ u = 1
have rw : u - 1 = 0
Tactic: rw [← sub_left_inj, sub_self 1]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
⊢ u - 1 = 0
have apply : (u - 1) ^ p = 0
Tactic: apply eq_zero_of_pow_eq_zero (n := p)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
⊢ (u - 1) ^ p = 0
have h : Commute u 1
Tactic: rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
⊢ False
have h : u = 1
Tactic: have h : u = 1 := by
      rw [← sub_left_inj, sub_self 1]
      apply eq_zero_of_pow_eq_zero (n := p)
      rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
      exact Commute.one_right u
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
h : u = 1
⊢ False
have inl : 1 = p
Tactic: apply pprime.one_lt.ne
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
h : u = 1
⊢ 1 = p
have inl : 1 = orderOf u
Tactic: rw [← hu, h, orderOf_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
h : u = 1
inl : 1 = orderOf u
⊢ 1 = p
have inl₁ : 1 = orderOf.{u_1} (G := K) 1
Tactic: rw [← hu, h, orderOf_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := (↑(↑x : Kˣ) : K)
hu : orderOf u = p
h : u = 1
inl : 1 = orderOf u
inl₁ : 1 = orderOf.{u_1} (G := K) 1
⊢ 1 = p
have inl₂ : Eq (α := ℕ) 1 1
Tactic: rw [← hu, h, orderOf_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
inst_2 : Nontrivial K
G : Subgroup Kˣ
inst_3 : Fintype ↥G
n : ℕ := Fintype.card.{u_1} ↥G
nzero : Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} ↥G) : K) 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
⊢ False
have x : Nat.Prime p ∨ p = 0
Tactic: cases CharP.char_is_prime_or_zero K p with
  | inr pzero =>
    exact (Fintype.card_pos).ne' <| Nat.eq_zero_of_zero_dvd <| pzero ▸ hd
  | inl pprime =>
    have fact_pprime := Fact.mk pprime
    -- G has an element x of order p by Cauchy's theorem
    have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
    -- F has an element u (= ↑↑x) of order p
    let u := ((x : Kˣ) : K)
    have hu : orderOf u = p := by rwa [orderOf_units, Subgroup.orderOf_coe]
    -- u ^ p = 1 implies (u - 1) ^ p = 0 and hence u = 1 ...
    have h : u = 1 := by
      rw [← sub_left_inj, sub_self 1]
      apply eq_zero_of_pow_eq_zero (n := p)
      rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
      exact Commute.one_right u
    -- ... meaning x didn't have order p after all, contradiction
    apply pprime.one_lt.ne
    rw [← hu, h, orderOf_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
hg : G ≠ ⊥
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have hg₁ : ∃ (a : ↥G), a ≠ 1
Tactic: rw [Subgroup.ne_bot_iff_exists_ne_one] at hg
Cleared hypotheses: hg
-- 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
hg : ∃ (a : ↥G), a ≠ 1
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have rcases : ∀ (a : ↥G) (ha : a ≠ 1), Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
Tactic: rcases hg with ⟨a, ha⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have h_unchanged : map a_mul_emb univ = univ
Tactic: have h_unchanged : Finset.univ.map a_mul_emb = Finset.univ := by simp
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have 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))
Tactic: have h_sum_map := Finset.univ.sum_map a_mul_emb fun x => ((x : Kˣ) : K)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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))
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have h_sum_map₁ : ∑ 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
Cleared hypotheses: h_sum_map
-- 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
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
have rw : ((↑(↑a : Kˣ) : K) - 1) * ∑ x : ↥G, (↑(↑x : Kˣ) : K) = 0
Tactic: rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
-- 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
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
⊢ (↑(↑a : Kˣ) : K) - 1 = 0 ∨ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have rw₁ : (↑(↑a : Kˣ) : K) * ∑ x : ↥G, (↑(↑x : Kˣ) : K) - HMul.hMul (α := K) 1 (∑ x : ↥G, (↑(↑x : Kˣ) : K)) = 0
Tactic: rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
-- 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
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
⊢ (↑(↑a : Kˣ) : K) - 1 = 0 ∨ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have rw₂ : ∑ x : ↥G, (↑(↑x : Kˣ) : K) - HMul.hMul (α := K) 1 (∑ x : ↥G, (↑(↑x : Kˣ) : K)) = 0
Tactic: rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
-- 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
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
⊢ (↑(↑a : Kˣ) : K) - 1 = 0 ∨ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have rw₃ : HSub.hSub (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) = 0
Tactic: rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
-- 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
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
⊢ (↑(↑a : Kˣ) : K) - 1 = 0 ∨ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have rw₄ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [← mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have hzero : (↑(↑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]
-- 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
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
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
have apply : ¬(↑(↑a : Kˣ) : K) - 1 = 0
Tactic: apply Or.resolve_left hzero
-- 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
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
⊢ ¬(↑(↑a : Kˣ) : K) - 1 = 0
have contrapose : ∀ (ha : (↑(↑a : Kˣ) : K) - 1 = 0), a = 1
Tactic: contrapose ha
Cleared hypotheses: ha
-- 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 = 1
have a₁ : (↑(↑a : Kˣ) : K) = (↑(↑1 : Kˣ) : K)
Tactic: ext