awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
pos : ∀ (hab : ![a, b] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
have neg : ∀ (hab : ¬![a, b] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
Tactic: by_cases hab : ![a, b] = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] = 0
have h : ∀ (i : Fin (Nat.succ 0).succ.succ), ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 i
have h : ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
i : Fin (Nat.succ 0).succ.succ
h :
  ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 i
have h₁ : ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
i : Fin (Nat.succ 0).succ.succ
h :
  ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 i
have h₂ : ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
have pos : 1 ≤ max C 1 * mulHeight ![c, d]
Tactic: rw [hab, mulHeight_zero, mul_one, show a = 0 from congrFun hab 0,
      show b = 0 from congrFun hab 1,
      show ![0 * c, 0 * d + 0 * c, 0 * d] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ 1 ≤ max C 1 * mulHeight ![c, d]
have pos : 1 ≤ max C 1 * 1
Tactic: grw [← one_le_mulHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
have pos : ∀ (hcd : ![c, d] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
Tactic: by_cases hcd : ![c, d] = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
pos : ∀ (hcd : ![c, d] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
have neg : ∀ (hcd : ¬![c, d] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
Tactic: by_cases hcd : ![c, d] = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] = 0
have h : ∀ (i : Fin (Nat.succ 0).succ.succ), ![a * 0, a * 0 + b * 0, b * 0] i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![a * 0, a * 0 + b * 0, b * 0] i = 0 i
have h : ![a * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
h :
  ![a * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![a * 0, a * 0 + b * 0, b * 0] i = 0 i
have h₁ : ![a * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
h :
  ![a * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![a * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![a * 0, a * 0 + b * 0, b * 0] i = 0 i
have h₂ : ![a * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
have pos : 1 ≤ max C 1 * mulHeight ![a, b]
Tactic: rw [hcd, mulHeight_zero, mul_one, show c = 0 from congrFun hcd 0,
      show d = 0 from congrFun hcd 1,
      show ![a * 0, a * 0 + b * 0, b * 0] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ 1 ≤ max C 1 * mulHeight ![a, b]
have pos : 1 ≤ max C 1 * 1
Tactic: grw [← one_le_mulHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
have neg : mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a * c, a * d, b * c, b * d]
Tactic: rw [mul_assoc, mulHeight_mul_mulHeight hab hcd]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a * c, a * d, b * c, b * d]
have neg : mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a * c, a * d, b * c, b * d]
Tactic: grw [← le_max_left C 1]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a * c, a * d, b * c, b * d]
have h : ∀ (i : Fin (Nat.succ 0).succ.succ),
  ![a * c, a * d + b * c, b * d] i = (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p i)
Tactic: convert! hC _ with i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![a * c, a * d + b * c, b * d] i = (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p i)
have h : ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
    (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
h :
  ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
      (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
⊢ ![a * c, a * d + b * c, b * d] i = (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p i)
have h₁ : ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
    (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (x : Fin 4 → K),
    (mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
h :
  ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
      (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
h₁ :
  ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
      (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
⊢ ![a * c, a * d + b * c, b * d] i = (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p i)
have h₂ : ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
    (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
a : Fin 4 × Fin 3
⊢ (q a).IsHomogeneous 1
have 0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a