K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : ¬∀ ⦃a : R⦄, (∃ a_1, a_1 ∈ univ ∧ eval a_1 f = a) → ¬∃ a_2, a_2 ∈ univ ∧ eval a_2 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
simp only [disjoint_left, mem_image] at this
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : Exists fun ⦃a⦄ => (∃ a_1, a_1 ∈ univ ∧ eval a_1 f = a) ∧ ∃ a_1, a_1 ∈ univ ∧ eval a_1 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : ¬∀ ⦃a : R⦄, (∃ a_1, a_1 ∈ univ ∧ eval a_1 f = a) → ¬∃ a_2, a_2 ∈ univ ∧ eval a_2 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0
push_neg  at this
case intro.intro.intro.intro.intro.intro
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : Exists fun ⦃a⦄ => (∃ a_1, a_1 ∈ univ ∧ eval a_1 f = a) ∧ ∃ a_1, a_1 ∈ univ ∧ eval a_1 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0
rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩
no goals
case intro.intro.intro.intro.intro.intro
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
exact ⟨a, b, by rw [ha, ← hb, eval_neg, neg_add_self]⟩
no goals
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
rw [ha, ← hb, eval_neg, neg_add_self]
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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 < degree f
rw [hf2]
no goals
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
exact by decide
no goals
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
decide
no goals
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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 = natDegree f * card (image (fun x => eval x f) univ) % 2
simp [natDegree_eq_of_degree_eq_some hf2, hR]
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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 < degree (-g)
rw [degree_neg, hg2]
no goals
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
exact by decide
no goals
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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
decide
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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)
⊢ natDegree f * card (image (fun x => eval x f) univ) + natDegree (-g) * card (image (fun x => eval x (-g)) univ) =
    2 * (card (image (fun x => eval x f) univ) + card (image (fun x => eval x (-g)) univ))
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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)
⊢ natDegree f * card (image (fun x => eval x f) univ) + natDegree (-g) * card (image (fun x => eval x (-g)) univ) =
    2 * card (image (fun x => eval x f) univ ∪ image (fun x => eval x (-g)) univ)
rw [card_disjoint_union hd]
no goals
K : Type ?u.86716
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 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)
⊢ natDegree f * card (image (fun x => eval x f) univ) + natDegree (-g) * card (image (fun x => eval x (-g)) univ) =
    2 * (card (image (fun x => eval x f) univ) + card (image (fun x => eval x (-g)) univ))
simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]