awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst_1 : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h_1 : abv.IsAdmissible
A : Fin (h_1.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h_1.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h :
  ∀ (k : Fin (Fintype.card ι)),
    (↑((abv : (a : R) → ℤ)
            (A i₁ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b -
              A i₀ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
k : ι
h₁ h₂ : k = (e.symm : (a : Fin (Fintype.card ι)) → ι) ((e : (a : ι) → Fin (Fintype.card ι)) k : Fin (Fintype.card ι))
⊢ (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
convert! h (e k)

Premises used: DFunLike.coe
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst_1 : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h_1 : abv.IsAdmissible
A : Fin (h_1.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h_1.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h :
  ∀ (k : Fin (Fintype.card ι)),
    (↑((abv : (a : R) → ℤ)
            (A i₁ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b -
              A i₀ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
k : ι
⊢ k = (e.symm : (a : Fin (Fintype.card ι)) → ι) ((e : (a : ι) → Fin (Fintype.card ι)) k : Fin (Fintype.card ι))

Tactic:
simp only [e.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
⊢ Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)

Tactic:
simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)

Premises used: lt_of_le_of_lt, Nat.lt_succ_self
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
⊢ Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)

Tactic:
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)
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
obtain :
  ∀ (i₀ i₁ : Fin m.succ) (i_ne : i₀ ≠ i₁) (i_eq : f i₀ = f i₁),
    ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀

Tactic:
obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this

Premises used: Fintype.exists_ne_map_eq_of_card_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
right : A i₁ = A i₀
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀

Tactic:
use i₀, i₁, i_ne
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
right : ∀ (j : ℕ), (A i₁).coeff j = (A i₀).coeff j
⊢ A i₁ = A i₀

Tactic:
ext j
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
pos : ∀ (hbj : b.degree ≤ (↑j : WithBot ℕ)), (A i₁).coeff j = (A i₀).coeff j
neg : ∀ (hbj : (↑j : WithBot ℕ) < b.degree), (A i₁).coeff j = (A i₀).coeff j
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
by_cases! hbj : degree b ≤ j

Premises used: Polynomial.degree
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : b.degree ≤ (↑j : WithBot ℕ)
pos : 0 = (A i₀).coeff j
pos₁ pos₂ : Eq.{u_1 + 1} (α := Fq) 0 0
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
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)]

Premises used: lt_of_lt_of_le, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : (↑j : WithBot ℕ) < b.degree
apply : j < d
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
apply congr_fun i_eq.symm ⟨j, _⟩

Premises used: Fin.mk, congr_fun, Eq.symm
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : (↑j : WithBot ℕ) < b.degree
⊢ j < d

Tactic:
lt_of_lt_of_le (coe_lt_degree.mp hbj) hb

Premises used: Polynomial.coe_lt_degree, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : (↑j : WithBot ℕ) < b.degree
⊢ j < d

Tactic:
exact lt_of_lt_of_le (coe_lt_degree.mp hbj) hb

Premises used: Polynomial.coe_lt_degree, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < degree.{u_1} (R := Fq) 0
⊢ (A 0).degree < degree.{u_1} (R := Fq) 0

Tactic:
specialize hA 0

Premises used: OfNat.ofNat
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : (A 0).degree < degree.{u_1} (R := Fq) 0
⊢ (A 0).degree < ⊥

Tactic:
rw [degree_zero] at hA

Premises used: Polynomial.degree_zero
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : (A 0).degree < ⊥
⊢ False

Tactic:
not_lt_of_ge bot_le hA

Premises used: bot_le, not_lt_of_ge
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : (A 0).degree < ⊥
⊢ False

Tactic:
exact not_lt_of_ge bot_le hA

Premises used: bot_le, not_lt_of_ge
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
⊢ b ≠ 0

Tactic:
have hb : b ≠ 0 := by
    rintro rfl
    specialize hA 0
    rw [degree_zero] at hA
    exact not_lt_of_ge bot_le hA
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
⊢ Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)

Tactic:
simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)

Premises used: lt_of_le_of_lt, Nat.lt_succ_self
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
⊢ Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)

Tactic:
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)
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
obtain :
  ∀ (i₀ i₁ : Fin m.succ) (i_ne : i₀ ≠ i₁) (i_eq : f i₀ = f i₁),
    ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)

Tactic:
obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this

Premises used: Fintype.exists_ne_map_eq_of_card_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
right : (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)

Tactic:
use i₀, i₁, i_ne
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)

Tactic:
(degree_lt_iff_coeff_zero _ _).mpr fun j hj => ?_

Premises used: Iff.mpr, Polynomial.degree_lt_iff_coeff_zero
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
right : ∀ (j : ℕ) (hj : b.natDegree - d ≤ j), (A i₁ - A i₀).coeff j = 0
⊢ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)

Tactic:
refine (degree_lt_iff_coeff_zero _ _).mpr fun j hj => ?_

Premises used: Iff.mpr, Polynomial.degree_lt_iff_coeff_zero
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
pos : ∀ (hbj : b.degree ≤ (↑j : WithBot ℕ)), (A i₁ - A i₀).coeff j = 0
neg : ∀ (hbj : (↑j : WithBot ℕ) < b.degree), (A i₁ - A i₀).coeff j = 0
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
by_cases! hbj : degree b ≤ j

Premises used: Polynomial.degree
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ (↑j : WithBot ℕ)
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
coeff_eq_zero_of_degree_lt (lt_of_lt_of_le ?_ hbj)

Premises used: lt_of_lt_of_le, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ (↑j : WithBot ℕ)
pos : (A i₁ - A i₀).degree < b.degree
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
refine coeff_eq_zero_of_degree_lt (lt_of_lt_of_le ?_ hbj)

Premises used: lt_of_lt_of_le, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ (↑j : WithBot ℕ)
⊢ (A i₁ - A i₀).degree < b.degree

Tactic:
lt_of_le_of_lt (degree_sub_le _ _) (max_lt (hA _) (hA _))

Premises used: lt_of_le_of_lt, max_lt, Polynomial.degree_sub_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ (↑j : WithBot ℕ)
⊢ (A i₁ - A i₀).degree < b.degree

Tactic:
exact lt_of_le_of_lt (degree_sub_le _ _) (max_lt (hA _) (hA _))

Premises used: lt_of_le_of_lt, max_lt, Polynomial.degree_sub_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : (↑j : WithBot ℕ) < b.degree
neg : (A i₁).coeff j = (A i₀).coeff j
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
rw [coeff_sub, sub_eq_zero]

Premises used: sub_eq_zero, Polynomial.coeff_sub
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : (↑j : WithBot ℕ) < b.degree
⊢ LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)

Tactic:
rw [degree_eq_natDegree hb] at hbj

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
⊢ j < b.natDegree

Tactic:
have hbj : j < natDegree b := (@WithBot.coe_lt_coe _ _ _).mp hbj
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
pos : ∀ (hd : b.natDegree < d), b.natDegree - j.succ < d
neg : ∀ (hd : d ≤ b.natDegree), b.natDegree - j.succ < d
⊢ b.natDegree - j.succ < d

Tactic:
by_cases! hd : natDegree b < d

Premises used: Polynomial.natDegree
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hd : b.natDegree < d
⊢ b.natDegree - j.succ < d

Tactic:
lt_of_le_of_lt tsub_le_self hd

Premises used: lt_of_le_of_lt, tsub_le_self
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hd : b.natDegree < d
⊢ b.natDegree - j.succ < d

Tactic:
exact lt_of_le_of_lt tsub_le_self hd

Premises used: lt_of_le_of_lt, tsub_le_self
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hd : d ≤ b.natDegree
⊢ b.natDegree - d < j.succ

Tactic:
have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this_1 : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hd : d ≤ b.natDegree
this : b.natDegree - d < j.succ
neg neg₁ neg₂ neg₃ : ∀ (this : b.natDegree - j.succ < d), b.natDegree - j.succ < d
⊢ b.natDegree - j.succ < d

Tactic:
rwa [tsub_lt_iff_tsub_lt hd hbj] at this

Premises used: tsub_lt_iff_tsub_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
⊢ b.natDegree - j.succ < d

Tactic:
have hj : natDegree b - j.succ < d := by
    by_cases! hd : natDegree b < d
    · exact lt_of_le_of_lt tsub_le_self hd
    · have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
      rwa [tsub_lt_iff_tsub_lt hd hbj] at this