awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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] ((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, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
pos : 1 ≤ max C 1 * mulHeight ![a, b]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

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]

Premises used: Height.mulHeight_zero, congrFun, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
pos : 1 ≤ max C 1 * 1
⊢ 1 ≤ max C 1 * mulHeight ![a, b]

Tactic:
grw [← one_le_mulHeight]

Premises used: Height.one_le_mulHeight
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 * 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
neg : mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a * c, a * d, b * c, b * d]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
rw [mul_assoc, mulHeight_mul_mulHeight hab hcd]

Premises used: Height.mulHeight_mul_mulHeight, mul_assoc
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
neg : mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a * c, a * d, b * c, b * d]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
grw [← le_max_left C 1]

Premises used: OfNat.ofNat, le_max_left
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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.{u_4, 0} (K := K) fun (j : Fin 3) ↦
      (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j)) ≤
    C * mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
hC _
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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)
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
convert! hC _ with i
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)))
h₂ :
  ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩ : 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:
fin_cases i
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 * 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)))

Tactic:
simp [p]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 * 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)))

Tactic:
simp [p]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp [p]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
6 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
7 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
8 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
9 : (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
10 : (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
11 : (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1

Tactic:
fin_cases a
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
0 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 0) 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
1 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
2 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
3 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
4 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 1) 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
5 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (-X 0) 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
6 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
7 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 2) 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
8 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (-X 0) 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
9 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
10 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
11 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 3) 1
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [q]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
⊢ IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 0) 1

Tactic:
grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.isHomogeneous_zero, MvPolynomial.IsHomogeneous.neg
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
⊢ IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1

Tactic:
grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.isHomogeneous_zero, MvPolynomial.IsHomogeneous.neg
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
⊢ IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 1) 1

Tactic:
grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.isHomogeneous_zero, MvPolynomial.IsHomogeneous.neg
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
⊢ IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (-X 0) 1

Tactic:
grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.isHomogeneous_zero, MvPolynomial.IsHomogeneous.neg
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
⊢ IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 2) 1

Tactic:
grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.isHomogeneous_zero, MvPolynomial.IsHomogeneous.neg
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
⊢ IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 3) 1

Tactic:
grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.isHomogeneous_zero, MvPolynomial.IsHomogeneous.neg
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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

Tactic:
have hom a : (q a).IsHomogeneous 1 := by
    fin_cases a <;> simp [q] <;> grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
obtain :
  ∀ (C : ℝ) (hC₀ : C > 0)
    (hC :
      ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K}
        (_h :
          ∀ (k : Fin 4),
            ∑ j : Fin 3,
                HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial (Fin 4) K) → K) (q (k, j)) : K)
                  ((eval x : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
              x k ^ HAdd.hAdd (α := ℕ) 1 1),
        C * HPow.hPow (β := ℕ) (mulHeight x) 1 ≤
          mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)),
    ∃ C > 0,
      ∀ {a b c d : K},
        ![a, b] ≠ 0 → ![c, d] ≠ 0 → C * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
⊢ ∃ C > 0,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]

Tactic:
obtain ⟨C, hC₀, hC⟩ := mulHeight_eval_ge' (M := 1) (N := 1) hom

Premises used: Height.mulHeight_eval_ge', MvPolynomial.C