-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_one_one_zmod_p (p : ℕ) [Fact p.Prime] : dickson 1 (1 : ZMod p) p = X ^ p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
this : Set.univ = ⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}
⊢ (⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}).Finite

Tactic:
clear this

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ (⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}).Finite

Proof state:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : x = 0
⊢ ∃ i y, i = y + y⁻¹ ∧ ¬y = 0

Tactic:
exact ⟨_, 1, rfl, one_ne_zero⟩

Result:
no goals

Proof state:
case intro.intro.intro.a.h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ False

Tactic:
rw [← Set.infinite_univ_iff] at H

Result:
case intro.intro.intro.a.h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ False

Proof state:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0

Tactic:
simp only [hy, eq_self_iff_true, or_true]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C 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]

Result:
no goals

Proof state:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

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

Result:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : x = 0
⊢ ∃ i y, i = y + y⁻¹ ∧ ¬y = 0

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ ∀ (x : K), x ∈ ⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}

Tactic:
intro x

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
⊢ x ∈ ⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}

Proof state:
case intro.intro.intro.a.h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ False

Tactic:
apply H

Result:
case intro.intro.intro.a.h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ Set.univ.Finite

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0

Tactic:
apply or_congr _ Iff.rfl

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ↔ y ^ 2 - x * y + 1 = 0

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
H : φ = 0
⊢ False

Tactic:
have : φ.eval 0 = 0 := by rw [H, eval_zero]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
H : φ = 0
this : eval 0 φ = 0
⊢ False

Proof state:
case intro.intro.intro.a.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}.Infinite

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

Result:
case intro.intro.intro.a.h.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0} ⊆ {x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}

case intro.intro.intro.a.h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Infinite

Proof state:
case intro.intro.intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ map (ZMod.castHom ⋯ K) (dickson 1 1 p) = map (ZMod.castHom ⋯ K) (X ^ p)

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

Result:
case intro.intro.intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 ((ZMod.castHom ⋯ K) 1) p = X ^ p

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ y * y + 1 - x * y = y ^ 2 - x * y + 1

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_2.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
⊢ y ∈ {y | x = y + y⁻¹ ∨ y = 0} ↔ y ∈ ↑(φ.roots ∪ {0}).toFinset

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]

Result:
case h.e'_2.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0

Proof state:
case h.e'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
⊢ {y | x = y + y⁻¹ ∨ y = 0} = ↑(φ.roots ∪ {0}).toFinset

Tactic:
ext1 y

Result:
case h.e'_2.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
⊢ y ∈ {y | x = y + y⁻¹ ∨ y = 0} ↔ y ∈ ↑(φ.roots ∪ {0}).toFinset