case intro.intro.intro
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 1 p = X ^ p
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ dickson 1 1 p = X ^ p
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
case intro.intro.intro.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ map (ZMod.castHom (_ : p ∣ p) K) (dickson 1 1 p) = map (ZMod.castHom (_ : p ∣ p) K) (X ^ p)
case intro.intro.intro
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 1 p = X ^ p
apply map_injective (ZMod.castHom (dvd_refl p) K) (RingHom.injective _)
case intro.intro.intro.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p = X ^ p
case intro.intro.intro.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ map (ZMod.castHom (_ : p ∣ p) K) (dickson 1 1 p) = map (ZMod.castHom (_ : p ∣ p) K) (X ^ p)
rw [map_dickson, Polynomial.map_pow, map_X]
case intro.intro.intro.a.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ Set.Infinite {x | eval x (dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
case intro.intro.intro.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p = X ^ p
apply eq_of_infinite_eval_eq
case intro.intro.intro.a.h.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
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 (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}

case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ Set.Infinite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
case intro.intro.intro.a.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ Set.Infinite {x | eval x (dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
apply @Set.Infinite.mono _ { x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0 }
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
⊢ ∃ K x x, Infinite K
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∃ K x x, Infinite K
let K := FractionRing (Polynomial (ZMod p))
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ ∃ K x x, Infinite K
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
⊢ ∃ K x x, Infinite K
let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this : CharP K p
⊢ ∃ K x x, Infinite K
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ ∃ K x x, Infinite K
have : CharP K p := by
  rw [← f.charP_iff_charP]
  infer_instance
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this✝ : CharP K p
this : Infinite K
⊢ ∃ K x x, Infinite K
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this : CharP K p
⊢ ∃ K x x, Infinite K
haveI : Infinite K :=
  Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
    (IsFractionRing.injective _ _)
no goals
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this✝ : CharP K p
this : Infinite K
⊢ ∃ K x x, Infinite K
refine' ⟨K, _, _, _⟩ <;> infer_instance
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ CharP (ZMod p) p
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ CharP K p
rw [← f.charP_iff_charP]
no goals
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ CharP (ZMod p) p
infer_instance
case intro.intro.intro.a.h.h.intro.intro
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
x : K
hx : x ≠ 0
⊢ x + x⁻¹ ∈ {x | eval x (dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
case intro.intro.intro.a.h.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
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 (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
rintro _ ⟨x, rfl, hx⟩
no goals
case intro.intro.intro.a.h.h.intro.intro
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
x : K
hx : x ≠ 0
⊢ x + x⁻¹ ∈ {x | eval x (dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
simp only [eval_X, eval_pow, Set.mem_setOf_eq, @add_pow_char K _ p,
  dickson_one_one_eval_add_inv _ _ (mul_inv_cancel hx), inv_pow, ZMod.castHom_apply,
  ZMod.cast_one']
case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ False
case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ Set.Infinite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
intro h
case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ False
case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ False
rw [← Set.infinite_univ_iff] at H
case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite Set.univ
case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ False
apply H
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
this :
  Set.univ = do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
⊢ Set.Finite do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
this :
  Set.univ = do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
⊢ Set.Finite Set.univ
rw [this]
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
this :
  Set.univ = do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
⊢ Set.Finite do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
clear this
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
refine' h.biUnion fun x _ => _
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
let φ : K[X] := X ^ 2 - C x * X + 1
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
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,
    MulZeroClass.mul_zero, sq, zero_add, one_ne_zero]
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
H : φ = 0
⊢ False
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
⊢ φ ≠ 0
intro H
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
H : φ = 0
⊢ False
have : φ.eval 0 = 0 := by rw [H, eval_zero]
no goals
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
simpa [eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul,
  MulZeroClass.mul_zero, sq, zero_add, one_ne_zero]
no goals
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
H : φ = 0
⊢ eval 0 φ = 0
rw [H, eval_zero]
case h.e'_2
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
⊢ (fun x => {y | x = y + y⁻¹ ∨ y = 0}) x = ↑(Multiset.toFinset (roots φ ∪ {0}))
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
convert(φ.roots ∪ {0}).toFinset.finite_toSet using 1
case h.e'_2.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
⊢ y ∈ (fun x => {y | x = y + y⁻¹ ∨ y = 0}) x ↔ y ∈ ↑(Multiset.toFinset (roots φ ∪ {0}))
case h.e'_2
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
⊢ (fun x => {y | x = y + y⁻¹ ∨ y = 0}) x = ↑(Multiset.toFinset (roots φ ∪ {0}))
ext1 y
case h.e'_2.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
case h.e'_2.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
⊢ y ∈ (fun x => {y | x = y + y⁻¹ ∨ y = 0}) x ↔ y ∈ ↑(Multiset.toFinset (roots φ ∪ {0}))
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]
case pos
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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

case neg
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
case h.e'_2.h
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
by_cases hy : y = 0
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
case neg
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
apply or_congr _ Iff.rfl
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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 = 0 ↔ y ^ 2 - x * y + 1 = 0
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel hy]
case a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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 = 0 ↔ y ^ 2 - x * y + 1 = 0
apply eq_iff_eq_cancel_right.mpr
no goals
case a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
ring
no goals
case pos
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
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
simp only [hy, eq_self_iff_true, or_true_iff]
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ ∀ (x : K),
    x ∈ do
      let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
      {y | x = y + y⁻¹ ∨ y = 0}
case intro.intro.intro.a.h.a
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.univ = do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
apply (Set.eq_univ_of_forall _).symm
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ x ∈ do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ ∀ (x : K),
    x ∈ do
      let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
      {y | x = y + y⁻¹ ∨ y = 0}
intro x
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ x ∈ do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
simp only [exists_prop, Set.mem_iUnion, Set.bind_def, Ne.def, Set.mem_setOf_eq]
case pos
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

case neg
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
by_cases hx : x = 0
case pos
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ i y, i = y + y⁻¹ ∧ ¬y = 0
case pos
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
simp only [hx, and_true_iff, eq_self_iff_true, inv_zero, or_true_iff]
no goals
case pos
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ i y, i = y + y⁻¹ ∧ ¬y = 0
exact ⟨_, 1, rfl, one_ne_zero⟩
case neg
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ y, x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0
case neg
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
simp only [hx, or_false_iff, exists_eq_right]
no goals
case neg
R : Type ?u.256583
S : Type ?u.256586
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ y, x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0
exact ⟨_, rfl, hx⟩