awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
obtain : ∀ (K : Type) (w : Field K), CharP K p → ∀ (H : Infinite K), dickson 1 1 p = HPow.hPow (α := (ZMod p)[X]) X p
⊢ dickson 1 1 p = HPow.hPow (α := (ZMod p)[X]) X p

Tactic:
obtain ⟨K, _, _, H⟩ : ∃ (K : Type) (_ : Field K), ∃ _ : CharP K p, Infinite K := by
    let K := FractionRing (Polynomial (ZMod p))
    let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C
    have : CharP K p := by
      rw [← f.charP_iff_charP]
      infer_instance
    haveI : Infinite K :=
      Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
        (IsFractionRing.injective _ _)
    refine ⟨K, ?_, ?_, ?_⟩ <;> infer_instance
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
a : Eq (α := K[X]) (map (ZMod.castHom ⋯ K) (dickson 1 1 p)) (map (ZMod.castHom ⋯ K) (HPow.hPow (α := (ZMod p)[X]) X p))
⊢ dickson 1 1 p = HPow.hPow (α := (ZMod p)[X]) X p

Tactic:
apply map_injective (ZMod.castHom (dvd_refl p) K) (RingHom.injective _)

Premises used: Polynomial.map_injective, RingHom.injective, dvd_refl, ZMod.castHom
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
a : dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p = HPow.hPow (α := K[X]) X p
⊢ Eq (α := K[X]) (map (ZMod.castHom ⋯ K) (dickson 1 1 p)) (map (ZMod.castHom ⋯ K) (HPow.hPow (α := (ZMod p)[X]) X p))

Tactic:
rw [map_dickson, Polynomial.map_pow, map_X]

Premises used: Polynomial.map_dickson, Polynomial.map_pow, Polynomial.map_X
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
a :
  Set.Infinite (α := K)
    {x : K | eval x (dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
⊢ dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p = HPow.hPow (α := K[X]) X p

Tactic:
apply eq_of_infinite_eval_eq

Premises used: Polynomial.eq_of_infinite_eval_eq
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
a :
  Subset (α := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
    {x : K | eval x (dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
a₁ : Set.Infinite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Infinite (α := K)
    {x : K | eval x (dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}

Tactic:
apply @Set.Infinite.mono _ { x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0 }

Premises used: Set.Infinite.mono
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
x : K
hx : x ≠ 0
⊢ Membership.mem (γ := Set K)
    {x : K | eval x (dickson 1 ((ZMod.castHom ⋯ K : (a : ZMod p) → K) 1) p) = eval x (HPow.hPow (α := K[X]) X p)}
    (x + x⁻¹)

Tactic:
simp only [eval_X, eval_pow, Set.mem_setOf_eq, ZMod.cast_one', add_pow_char,
      dickson_one_one_eval_add_inv _ _ (mul_inv_cancel₀ hx), ZMod.castHom_apply]

Premises used: mul_inv_cancel₀, Polynomial.eval_X, Polynomial.eval_pow, add_pow_char, ZMod.castHom_apply, ZMod.cast_one', Set.mem_setOf_eq, Polynomial.dickson_one_one_eval_add_inv
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Infinite (α := K) Set.univ

Tactic:
rw [← Set.infinite_univ_iff] at H

Premises used: Set.infinite_univ_iff
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Infinite K
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
H₁ : Set.Infinite (α := K) Set.univ
⊢ Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}

Tactic:
rw [← Set.infinite_univ_iff] at H

Premises used: Set.infinite_univ_iff
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
a : Set.Finite (α := K) Set.univ
⊢ False

Tactic:
apply H
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
this :
  Eq (α := Set K) Set.univ
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})
rw :
  Set.Finite (α := K)
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})
⊢ Set.Finite (α := K) Set.univ

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite (α := K)
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})

Tactic:
h.biUnion fun x _ => ?_

Premises used: Set.Finite.biUnion
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
refine :
  ∀ (x : K),
    Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x →
      Set.Finite (α := K) {y : K | x = y + y⁻¹ ∨ y = 0}
⊢ Set.Finite (α := K)
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})

Tactic:
refine h.biUnion fun x _ => ?_

Premises used: Set.Finite.biUnion
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H_1 : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
H : φ = 0
rw : Eq (α := K) (eval 0 0) 0
rw₁ rw₂ : Eq (α := K) 0 0
⊢ eval 0 φ = 0

Tactic:
rw [H, eval_zero]

Premises used: Polynomial.eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H_1 : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
H : φ = 0
⊢ eval 0 φ = 0

Tactic:
have : φ.eval 0 = 0 := by rw [H, eval_zero]
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H_1 : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
H : φ = 0
this : eval 0 φ = 0
⊢ False

Tactic:
simpa [φ, eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul,
          mul_zero, sq, zero_add, one_ne_zero]

Premises used: sub_zero, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_mul, sq, zero_add, MulZeroClass.mul_zero, Polynomial.eval_add, Polynomial.eval_one, one_ne_zero, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
⊢ φ ≠ 0

Tactic:
have hφ : φ ≠ 0 := by
        intro H
        have : φ.eval 0 = 0 := by rw [H, eval_zero]
        simpa [φ, eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul,
          mul_zero, sq, zero_add, one_ne_zero]
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
⊢ (↑(φ.roots ∪ {0}).toFinset : Set K).Finite

Tactic:
(φ.roots ∪ {0}).toFinset.finite_toSet

Premises used: Multiset.toFinset, Polynomial.roots, Finset.finite_toSet, Union.union, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
h₁ : {y : K | x = y + y⁻¹ ∨ y = 0} = (↑(φ.roots ∪ {0}).toFinset : Set K)
⊢ Set.Finite (α := K) {y : K | x = y + y⁻¹ ∨ y = 0}

Tactic:
convert! (φ.roots ∪ {0}).toFinset.finite_toSet using 1

Premises used: Multiset.toFinset, Polynomial.roots, Finset.finite_toSet, Union.union, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
h₁ : ∀ (y : K), Membership.mem (γ := Set K) {y : K | x = y + y⁻¹ ∨ y = 0} y ↔ y ∈ (↑(φ.roots ∪ {0}).toFinset : Set K)
⊢ {y : K | x = y + y⁻¹ ∨ y = 0} = (↑(φ.roots ∪ {0}).toFinset : Set K)

Tactic:
ext1 y
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
y : K
h₁ : x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0
⊢ Membership.mem (γ := Set K) {y : K | x = y + y⁻¹ ∨ y = 0} y ↔ y ∈ (↑(φ.roots ∪ {0}).toFinset : Set K)

Tactic:
simp only [φ, Multiset.mem_toFinset, Set.mem_setOf_eq, Finset.mem_coe, Multiset.mem_union,
          mem_roots hφ, IsRoot, eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one,
          Multiset.mem_singleton]

Premises used: Multiset.mem_union, Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.IsRoot, Polynomial.eval_mul, Set.mem_setOf_eq, Multiset.mem_singleton, Polynomial.mem_roots, Polynomial.eval_add, Polynomial.eval_one, Polynomial.eval_sub, Finset.mem_coe, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
y : K
pos : ∀ (hy : y = 0), x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0
neg : ∀ (hy : ¬y = 0), x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
y : K
hy : y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0

Tactic:
simp only [hy, or_true]

Premises used: or_true
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
apply : x = y + y⁻¹ ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0

Tactic:
apply or_congr _ Iff.rfl

Premises used: or_congr, Iff.rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
rw : y * y + 1 - x * y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0
⊢ x = y + y⁻¹ ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0

Tactic:
rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel₀ hy]

Premises used: add_mul, sub_eq_zero, eq_comm, mul_left_inj', inv_mul_cancel₀
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
a : y * y + 1 - x * y = HPow.hPow (β := ℕ) y 2 - x * y + 1
⊢ y * y + 1 - x * y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0

Tactic:
apply eq_iff_eq_cancel_right.mpr

Premises used: Iff.mpr, eq_iff_eq_cancel_right
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ y * y + 1 - x * y = HPow.hPow (β := ℕ) y 2 - x * y + 1

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
h_1 : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x
φ : K[X] := HPow.hPow (α := K[X]) (β := ℕ) X 2 - HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) x : K[X]) X + 1
hφ : φ ≠ 0
h₁ : {y : K | x = y + y⁻¹ ∨ y = 0} = (↑(φ.roots ∪ {0}).toFinset : Set K)
h₂ : ∀ (y : K), Membership.mem (γ := Set K) {y : K | x = y + y⁻¹ ∨ y = 0} y ↔ y ∈ (↑(φ.roots ∪ {0}).toFinset : Set K)
h₃ : ∀ (y : K), x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0
pos : ∀ (y : K) (hy : y = 0), x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0
neg neg₁ : ∀ (y : K) (hy : ¬y = 0), x = y + y⁻¹ ∨ y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0 ∨ y = 0
convert! : ∀ (y : K) (hy : ¬y = 0), x = y + y⁻¹ ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0
convert!₁ : ∀ (y : K) (hy : ¬y = 0), y * y + 1 - x * y = 0 ↔ HPow.hPow (β := ℕ) y 2 - x * y + 1 = 0
a : ∀ (y : K) (hy : ¬y = 0), y * y + 1 - x * y = HPow.hPow (β := ℕ) y 2 - x * y + 1
⊢ Set.Finite (α := K) {y : K | x = y + y⁻¹ ∨ y = 0}

Tactic:
classical
        convert! (φ.roots ∪ {0}).toFinset.finite_toSet using 1
        ext1 y
        simp only [φ, Multiset.mem_toFinset, Set.mem_setOf_eq, Finset.mem_coe, Multiset.mem_union,
          mem_roots hφ, IsRoot, eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one,
          Multiset.mem_singleton]
        by_cases hy : y = 0
        · simp only [hy, or_true]
        apply or_congr _ Iff.rfl
        rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel₀ hy]
        apply eq_iff_eq_cancel_right.mpr
        ring

Premises used: Iff.mpr, add_mul, or_congr, eq_iff_eq_cancel_right, Multiset.mem_union, Polynomial.eval_C, sub_eq_zero, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.IsRoot, Iff.rfl, Polynomial.eval_mul, Set.mem_setOf_eq, eq_comm, Multiset.mem_singleton, Polynomial.mem_roots, Polynomial.eval_add, Polynomial.eval_one, or_true, Polynomial.eval_sub, Finset.mem_coe, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
a :
  Eq (α := Set K) Set.univ
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})
⊢ Set.Finite (α := K) Set.univ

Tactic:
suffices (Set.univ : Set K) =
        ⋃ x ∈ { x : K | ∃ y : K, x = y + y⁻¹ ∧ y ≠ 0 }, { y | x = y + y⁻¹ ∨ y = 0 }  by
      rw [this]
      clear this
      refine h.biUnion fun x _ => ?_
      -- The following quadratic polynomial has as solutions the `y` for which `x = y + y⁻¹`.
      let φ : K[X] := X ^ 2 - C x * X + 1
      have hφ : φ ≠ 0 := by
        intro H
        have : φ.eval 0 = 0 := by rw [H, eval_zero]
        simpa [φ, eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul,
          mul_zero, sq, zero_add, one_ne_zero]
      classical
        convert! (φ.roots ∪ {0}).toFinset.finite_toSet using 1
        ext1 y
        simp only [φ, Multiset.mem_toFinset, Set.mem_setOf_eq, Finset.mem_coe, Multiset.mem_union,
          mem_roots hφ, IsRoot, eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one,
          Multiset.mem_singleton]
        by_cases hy : y = 0
        · simp only [hy, or_true]
        apply or_congr _ Iff.rfl
        rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel₀ hy]
        apply eq_iff_eq_cancel_right.mpr
        ring
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
apply :
  ∀ (x : K),
    Membership.mem (γ := Set K)
      (⋃ (x : K),
        ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})
      x
⊢ Eq (α := Set K) Set.univ
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})

Tactic:
apply (Set.eq_univ_of_forall _).symm

Premises used: Set.eq_univ_of_forall, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
simp : ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
⊢ Membership.mem (γ := Set K)
    (⋃ (x : K),
      ⋃ (_ : Membership.mem (γ := Set K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} x), {y : K | x = y + y⁻¹ ∨ y = 0})
    x

Tactic:
simp only [exists_prop, Set.mem_iUnion, Ne, Set.mem_setOf_eq]

Premises used: Set.mem_iUnion, Ne, Set.mem_setOf_eq, exists_prop
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
pos : ∀ (hx : x = 0), ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
neg : ∀ (hx : ¬x = 0), ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
⊢ ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
pos : ∃ (i : K) (y : K), i = y + y⁻¹ ∧ ¬y = 0
⊢ ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

Tactic:
simp only [hx, and_true, inv_zero, or_true]

Premises used: and_true, inv_zero, or_true
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ (i : K) (y : K), i = y + y⁻¹ ∧ ¬y = 0

Tactic:
⟨_, 1, rfl, one_ne_zero⟩

Premises used: And.intro, Exists.intro, one_ne_zero, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ (i : K) (y : K), i = y + y⁻¹ ∧ ¬y = 0

Tactic:
exact ⟨_, 1, rfl, one_ne_zero⟩
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
neg : ∃ (y : K), x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0
⊢ ∃ (i : K), (∃ (y : K), i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

Tactic:
simp only [hx, or_false, exists_eq_right]

Premises used: exists_eq_right, or_false
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ (y : K), x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0

Tactic:
⟨_, rfl, hx⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type
w : Field K
w_1 : CharP K p
H : Set.Infinite (α := K) Set.univ
h : Set.Finite (α := K) {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ (y : K), x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0

Tactic:
exact ⟨_, rfl, hx⟩
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
⊢ Eq (α := R) (1 : R) ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1 : R)

Tactic:
simp only [ZMod.castHom_apply, ZMod.cast_one']

Premises used: ZMod.castHom_apply, ZMod.cast_one'
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
⊢ Eq (α := R) (1 : R) ((ZMod.castHom ⋯ R : (a : ZMod p) → R) 1 : R)

Tactic:
have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1 := by
    simp only [ZMod.castHom_apply, ZMod.cast_one']