-- Mathlib/FieldTheory/Finite/Basic.lean
theorem exists_root_sum_quadratic [Fintype R] {f g : R[X]} (hf2 : degree f = 2) (hg2 : degree g = 2)
    (hR : Fintype.card R % 2 = 1) : ∃ a b, f.eval a + g.eval b = 0 :=
  letI := Classical.decEq R
  suffices ¬Disjoint (univ.image fun x : R => eval x f)
    (univ.image fun x : R => eval x (-g)) by
    simp only [disjoint_left, mem_image] at this
    push_neg at this
    rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩
    exact ⟨a, b, by rw [ha, ← hb, eval_neg, neg_add_cancel]⟩
  fun hd : Disjoint _ _ =>
  lt_irrefl (2 * #((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g))) <|
    calc 2 * #((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g))
        ≤ 2 * Fintype.card R := Nat.mul_le_mul_left _ (Finset.card_le_univ _)
      _ = Fintype.card R + Fintype.card R := two_mul _
      _ < natDegree f * #(univ.image fun x : R => eval x f) +
            natDegree (-g) * #(univ.image fun x : R => eval x (-g)) :=
        (add_lt_add_of_lt_of_le
          (lt_of_le_of_ne (card_image_polynomial_eval (by rw [hf2]; decide))
            (mt (congr_arg (· % 2)) (by simp [natDegree_eq_of_degree_eq_some hf2, hR])))
          (card_image_polynomial_eval (by rw [degree_neg, hg2]; decide)))
      _ = 2 * #((univ.image fun x : R => eval x f) ∪ univ.image fun x : R => eval x (-g))

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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
this : ¬Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ ∃ a b, eval a f + eval b g = 0

Tactic:
simp only [disjoint_left, mem_image] at this

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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
this : ¬∀ ⦃a : R⦄, (∃ a_1 ∈ univ, eval a_1 f = a) → ¬∃ a_2 ∈ univ, eval a_2 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ f.natDegree * #(image (fun x => eval x f) univ) + (-g).natDegree * #(image (fun x => eval x (-g)) univ) =
    2 * (#(image (fun x => eval x f) univ) + #(image (fun x => eval x (-g)) univ))

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

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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✝¹ : a ∈ univ
ha : eval a f = x
b : R
left✝ : b ∈ univ
hb : eval b (-g) = x
⊢ eval a f + eval b g = 0

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

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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
this : ∃ a, (∃ a_1 ∈ univ, eval a_1 f = a) ∧ ∃ a_1 ∈ univ, eval a_1 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0

Tactic:
rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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✝¹ : a ∈ univ
ha : eval a f = x
b : R
left✝ : b ∈ univ
hb : eval b (-g) = x
⊢ ∃ a b, eval a f + eval b g = 0

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < f.degree

Tactic:
rw [hf2]

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < 2

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < (-g).degree

Tactic:
rw [degree_neg, hg2]

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < 2

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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✝¹ : a ∈ univ
ha : eval a f = x
b : R
left✝ : b ∈ univ
hb : eval b (-g) = x
⊢ ∃ a b, eval a f + eval b g = 0

Tactic:
exact ⟨a, b, by rw [ha, ← hb, eval_neg, neg_add_cancel]⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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
this : ¬∀ ⦃a : R⦄, (∃ a_1 ∈ univ, eval a_1 f = a) → ¬∃ a_2 ∈ univ, eval a_2 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0

Tactic:
push_neg at this

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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
this : ∃ a, (∃ a_1 ∈ univ, eval a_1 f = a) ∧ ∃ a_1 ∈ univ, eval a_1 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ ¬Fintype.card R % 2 = f.natDegree * #(image (fun x => eval x f) univ) % 2

Tactic:
simp [natDegree_eq_of_degree_eq_some hf2, hR]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ f.natDegree * #(image (fun x => eval x f) univ) + (-g).natDegree * #(image (fun x => eval x (-g)) univ) =
    2 * #(image (fun x => eval x f) univ ∪ image (fun x => eval x (-g)) univ)

Tactic:
rw [card_union_of_disjoint hd]

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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 (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ f.natDegree * #(image (fun x => eval x f) univ) + (-g).natDegree * #(image (fun x => eval x (-g)) univ) =
    2 * (#(image (fun x => eval x f) univ) + #(image (fun x => eval x (-g)) univ))