Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
set f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff j
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
  simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ A i₁ = A i₀
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
use i₀, i₁, i_ne
case intro.intro.intro.a
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
⊢ coeff (A i₁) j = coeff (A i₀) j
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ A i₁ = A i₀
ext j
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : degree b ≤ ↑j
⊢ coeff (A i₁) j = coeff (A i₀) j

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ¬degree b ≤ ↑j
⊢ coeff (A i₁) j = coeff (A i₀) j
case intro.intro.intro.a
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
⊢ coeff (A i₁) j = coeff (A i₀) j
by_cases hbj : degree b ≤ j
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < degree b
⊢ coeff (A i₁) j = coeff (A i₀) j
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ¬degree b ≤ ↑j
⊢ coeff (A i₁) j = coeff (A i₀) j
rw [not_le] at hbj
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < degree b
⊢ j < d
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < degree b
⊢ coeff (A i₁) j = coeff (A i₀) j
apply congr_fun i_eq.symm ⟨j, _⟩
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < degree b
⊢ j < d
exact lt_of_lt_of_le (coe_lt_degree.mp hbj) hb
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
⊢ Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)
no goals
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : degree b ≤ ↑j
⊢ coeff (A i₁) j = coeff (A i₀) j
rw [coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj),
  coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj)]