awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F L
inst_4 : Algebra F K
hA : ∀ (x : K), Splits (map (algebraMap F L) (minpoly F x))
inst_5 : Algebra.IsAlgebraic F K
x : K
a : L
h :
  Membership.mem (γ := Set L) (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) a ↔
    Eq.{u_3 + 1} (α := L) ((aeval a : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
⊢ Membership.mem (γ := Set L) (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) a ↔ a ∈ rootSet (minpoly F x) L

Tactic:
rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x))]

Premises used: Algebra.IsIntegral.isIntegral, Polynomial.mem_rootSet_of_ne, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F L
inst_4 : Algebra F K
hA : ∀ (x : K), Splits (map (algebraMap F L) (minpoly F x))
inst_5 : Algebra.IsAlgebraic F K
x : K
a : L
⊢ Membership.mem (γ := Set L) (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) a ↔
    Eq.{u_3 + 1} (α := L) ((aeval a : (a : F[X]) → L) (minpoly F x) : L) (0 : L)

Tactic:
⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦ IntermediateField.exists_algHom_of_splits_of_aeval
    (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, hA x⟩) ha⟩

Premises used: Algebra.IsIntegral.isIntegral, minpoly, And.intro, Iff.intro, _private.0.Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits.match_1, IntermediateField.exists_algHom_of_splits_of_aeval, Polynomial.aeval, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F L
inst_4 : Algebra F K
hA : ∀ (x : K), Splits (map (algebraMap F L) (minpoly F x))
inst_5 : Algebra.IsAlgebraic F K
x : K
a : L
h :
  Membership.mem (γ := Set L) (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) a →
    ∀ (ψ : K →ₐ[F] L) (hψ : (fun (ψ : K →ₐ[F] L) ↦ ((ψ : (a : K) → L) x : L)) ψ = a),
      Eq.{u_3 + 1} (α := L) ((aeval a : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
⊢ Membership.mem (γ := Set L) (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) a ↔
    Eq.{u_3 + 1} (α := L) ((aeval a : (a : F[X]) → L) (minpoly F x) : L) (0 : L)

Tactic:
refine ⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦ IntermediateField.exists_algHom_of_splits_of_aeval
    (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, hA x⟩) ha⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F L
inst_4 : Algebra F K
hA : ∀ (x : K), Splits (map (algebraMap F L) (minpoly F x))
inst_5 : Algebra.IsAlgebraic F K
x : K
a : L
h_1 : Membership.mem (γ := Set L) (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) a
ψ : K →ₐ[F] L
hψ : (fun (ψ : K →ₐ[F] L) ↦ ((ψ : (a : K) → L) x : L)) ψ = a
h :
  Eq.{u_3 + 1} (α := L)
    ((aeval ((fun (ψ : K →ₐ[F] L) ↦ ((ψ : (a : K) → L) x : L)) ψ) : (a : F[X]) → L) (minpoly F x) : L) (0 : L)
h₁ : Eq.{u_3 + 1} (α := L) ((ψ : (a : K) → L) ((aeval x : (a : F[X]) → K) (minpoly F x) : K) : L) (0 : L)
h₂ : Eq.{u_3 + 1} (α := L) ((ψ : (a : K) → L) 0 : L) (0 : L)
h₃ h₄ : Eq.{u_3 + 1} (α := L) 0 0
⊢ Eq.{u_3 + 1} (α := L) ((aeval a : (a : F[X]) → L) (minpoly F x) : L) (0 : L)

Tactic:
rw [← hψ, Polynomial.aeval_algHom_apply ψ x, minpoly.aeval, map_zero]

Premises used: map_zero, minpoly.aeval, Polynomial.aeval_algHom_apply
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
inst_3 : Fintype R
p : R[X]
hp : 0 < p.degree
a : R
h : Membership.mem (γ := Finset R) (image (fun (x : R) ↦ eval x p) univ) a
⊢ {a_1 : R | eval a_1 p = a} = (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).roots.toFinset

Tactic:
simp [Finset.ext_iff, ← mem_roots_sub_C hp]

Premises used: Finset.ext_iff, Polynomial.mem_roots_sub_C
-- Module: Mathlib.FieldTheory.Finite.Basic
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
hd : Disjoint.{u_2} (α := Finset R) (image (fun (x : R) ↦ eval x f) univ) (image (fun (x : R) ↦ eval x (-g)) univ)
rw : LT.lt (α := WithBot ℕ) 0 2
⊢ 0 < f.degree

Tactic:
rw [hf2]
-- Module: Mathlib.FieldTheory.Finite.Basic
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
hd : Disjoint.{u_2} (α := Finset R) (image (fun (x : R) ↦ eval x f) univ) (image (fun (x : R) ↦ eval x (-g)) univ)
⊢ LT.lt (α := WithBot ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.FieldTheory.Finite.Basic
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
hd : Disjoint.{u_2} (α := Finset R) (image (fun (x : R) ↦ eval x f) univ) (image (fun (x : R) ↦ eval x (-g)) univ)
⊢ ¬Fintype.card R % 2 = f.natDegree * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x f) univ) % 2

Tactic:
simp [natDegree_eq_of_degree_eq_some hf2, hR]

Premises used: Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.FieldTheory.Finite.Basic
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
hd : Disjoint.{u_2} (α := Finset R) (image (fun (x : R) ↦ eval x f) univ) (image (fun (x : R) ↦ eval x (-g)) univ)
rw : LT.lt (α := WithBot ℕ) 0 2
⊢ 0 < (-g).degree

Tactic:
rw [degree_neg, hg2]

Premises used: Polynomial.degree_neg
-- Module: Mathlib.FieldTheory.Finite.Basic
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
hd : Disjoint.{u_2} (α := Finset R) (image (fun (x : R) ↦ eval x f) univ) (image (fun (x : R) ↦ eval x (-g)) univ)
rw :
  f.natDegree * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x f) univ) +
      (-g).natDegree * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x (-g)) univ) =
    2 *
      (card.{u_2} (α := R) (image (fun (x : R) ↦ eval x f) univ) +
        card.{u_2} (α := R) (image (fun (x : R) ↦ eval x (-g)) univ))
⊢ f.natDegree * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x f) univ) +
      (-g).natDegree * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x (-g)) univ) =
    2 * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x f) univ ∪ image (fun (x : R) ↦ eval x (-g)) univ)

Tactic:
rw [card_union_of_disjoint hd]

Premises used: Finset.card_union_of_disjoint
-- Module: Mathlib.FieldTheory.Finite.Basic
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
hd : Disjoint.{u_2} (α := Finset R) (image (fun (x : R) ↦ eval x f) univ) (image (fun (x : R) ↦ eval x (-g)) univ)
⊢ f.natDegree * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x f) univ) +
      (-g).natDegree * card.{u_2} (α := R) (image (fun (x : R) ↦ eval x (-g)) univ) =
    2 *
      (card.{u_2} (α := R) (image (fun (x : R) ↦ eval x f) univ) +
        card.{u_2} (α := R) (image (fun (x : R) ↦ eval x (-g)) univ))

Tactic:
simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, mul_add
-- Module: Mathlib.FieldTheory.Finite.Basic
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⦄,
      (∃ (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

Premises used: Finset.mem_image, Finset.disjoint_left
-- Module: Mathlib.FieldTheory.Finite.Basic
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),
    (∃ (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

Premises used: Not
-- Module: Mathlib.FieldTheory.Finite.Basic
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
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
⊢ ∃ (a : R) (b : R), eval a f + eval b g = 0

Tactic:
rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
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
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ eval a f + eval b g = 0

Tactic:
rw [ha, ← hb, eval_neg, neg_add_cancel]

Premises used: neg_add_cancel, Polynomial.eval_neg
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ ∃ (a : R) (b : R), eval a f + eval b g = 0

Tactic:
exact ⟨a, b, by rw [ha, ← hb, eval_neg, neg_add_cancel]⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) a),
    a * (fun (x : Kˣ) (x_1 : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) x) ↦ x⁻¹) a ha = 1

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) a),
    a ≠ 1 → (fun (x : Kˣ) (x_1 : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) x) ↦ x⁻¹) a ha ≠ a

Tactic:
simp +contextual [Units.inv_eq_self_iff]

Premises used: Units.inv_eq_self_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) a),
    Membership.mem (γ := Finset Kˣ) (erase univ (-1))
      ((fun (x : Kˣ) (x_1 : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) x) ↦ x⁻¹) a ha)

Tactic:
simp [@inv_eq_iff_eq_inv _ _ a]

Premises used: inv_eq_iff_eq_inv
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) a),
    (fun (x : Kˣ) (x_1 : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) x) ↦ x⁻¹)
        ((fun (x : Kˣ) (x_1 : Membership.mem (γ := Finset Kˣ) (erase univ (-1)) x) ↦ x⁻¹) a ha) ⋯ =
      a

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
⊢ 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)
-- Module: Mathlib.FieldTheory.Finite.Basic
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := Kˣ) (-1) (-1)
⊢ Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, x) (-1)

Tactic:
rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]

Premises used: Finset.mem_univ, Finset.prod_insert, Finset.notMem_erase, mul_one, OfNat.ofNat, Finset.insert_erase, Neg.neg
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Fintype Kˣ
have have₁ have₂ :
  ∀ (this : Eq.{u_1 + 1} (α := Kˣ) (∏ x ∈ erase univ (-1), x) 1), Eq.{u_1 + 1} (α := Kˣ) (∏ x : Kˣ, 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]

Premises used: Finset.prod_insert, Finset.notMem_erase, mul_one
-- Module: Mathlib.FieldTheory.Finite.Basic
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
have : ∀ (p : ℕ) (char_p : CharP K p), False
⊢ False

Tactic:
have ⟨p, char_p⟩ := CharP.exists K
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ p ∣ n

Tactic:
have hd : p ∣ n := (CharP.cast_eq_zero_iff K p n).mp nzero
-- Module: Mathlib.FieldTheory.Finite.Basic
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
pzero : p = 0
⊢ False

Tactic:
(Fintype.card_pos).ne' <| Nat.eq_zero_of_zero_dvd <| pzero ▸ hd

Premises used: LT.lt.ne', Fintype.card_pos, Nat.eq_zero_of_zero_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
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
pzero : p = 0
⊢ False

Tactic:
exact (Fintype.card_pos).ne' <| Nat.eq_zero_of_zero_dvd <| pzero ▸ hd

Premises used: LT.lt.ne', Fintype.card_pos, Nat.eq_zero_of_zero_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
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 (Nat.Prime p)

Tactic:
have fact_pprime := Fact.mk pprime
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
inl : ∀ (x : ↥G) (hx : orderOf x = p), False
⊢ False

Tactic:
have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
rwa : orderOf (↑x : Kˣ) = p
rwa₁ rwa₂ rwa₃ rwa₄ : orderOf x = p
⊢ orderOf u = p

Tactic:
rwa [orderOf_units, Subgroup.orderOf_coe]

Premises used: orderOf_units, Subgroup.orderOf_coe
-- Module: Mathlib.FieldTheory.Finite.Basic
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

Tactic:
have hu : orderOf u = p := by rwa [orderOf_units, Subgroup.orderOf_coe]
-- Module: Mathlib.FieldTheory.Finite.Basic
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
rw : u - 1 = 0
⊢ u = 1

Tactic:
rw [← sub_left_inj, sub_self 1]

Premises used: sub_self, sub_left_inj, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.Basic
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
apply : (u - 1) ^ p = 0
⊢ u - 1 = 0

Tactic:
apply eq_zero_of_pow_eq_zero (n := p)

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : Commute u 1
⊢ (u - 1) ^ p = 0

Tactic:
rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]

Premises used: one_pow, sub_self, pow_orderOf_eq_one, sub_pow_char_of_commute
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ Commute u 1

Tactic:
Commute.one_right u

Premises used: Commute.one_right
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ Commute u 1

Tactic:
exact Commute.one_right u

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

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
-- Module: Mathlib.FieldTheory.Finite.Basic
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 = p
⊢ False

Tactic:
apply pprime.one_lt.ne

Premises used: Nat.Prime.one_lt, LT.lt.ne
-- Module: Mathlib.FieldTheory.Finite.Basic
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
inl₂ inl₃ : Eq (α := ℕ) 1 1
⊢ 1 = p

Tactic:
rw [← hu, h, orderOf_one]

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

Premises used: orderOf_one, LT.lt.ne', CharP.char_is_prime_or_zero, Fintype.card_pos, Nat.eq_zero_of_zero_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
hg : G ≠ ⊥
⊢ ∃ (a : ↥G), a ≠ 1

Tactic:
rw [Subgroup.ne_bot_iff_exists_ne_one] at hg

Premises used: Subgroup.ne_bot_iff_exists_ne_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Ring K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
hg : ∃ (a : ↥G), a ≠ 1
rcases : ∀ (a : ↥G) (ha : a ≠ 1), Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : ↥G, (↑(↑x : Kˣ) : K)) 0

Tactic:
rcases hg with ⟨a, 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
ha : a ≠ 1
a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a
⊢ map a_mul_emb univ = univ

Tactic:
simp