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]
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
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)
⊢ ∀ (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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)

Tactic:
simp only [pow_one] at hC

Premises used: pow_one
-- 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
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 * mulHeight x ≤ 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]

Tactic:
⟨C, hC₀, fun hab hcd ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
refine :
  ∀ {a b c d : K} (hab : ![a, b] ≠ 0) (hcd : ![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:
refine ⟨C, hC₀, fun hab hcd ↦ ?_⟩
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
rw : C * mulHeight ![a * c, a * d, b * c, b * d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
⊢ C * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * 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]
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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ C * mulHeight ![a * c, a * d, b * c, b * d] ≤
    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)

Tactic:
hC p fun j ↦ ?H
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
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)
convert! :
  ∀ (j : Fin 4),
    ∑ j_1 : Fin 3,
        HMul.hMul (α := K) (β := K)
          ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (q (j, j_1)) : K)
          ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j_1) : K) =
      ![a * c, a * d, b * c, b * d] j ^ HAdd.hAdd (α := ℕ) 1 1
⊢ C * mulHeight ![a * c, a * d, b * c, b * d] ≤ mulHeight ![a * c, a * d + b * c, b * d]

Tactic:
convert! hC p fun j ↦ ?H 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]
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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
j : Fin 4
0 :
  ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
1 :
  ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
2 :
  ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
3 :
  ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
⊢ ∑ j_1 : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (q (j, j_1)) : K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j_1) : K) =
    ![a * c, a * d, b * c, b * d] j ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
fin_cases j
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
0 : a * c * (a * c) = HPow.hPow (β := ℕ) (a * c) 2
⊢ ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
simp [p, q, Fin.sum_univ_three]

Premises used: Fin.sum_univ_three
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
1 : a * d * (a * d + b * c) + -(a * c * (b * d)) = HPow.hPow (β := ℕ) (a * d) 2
⊢ ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
simp [p, q, Fin.sum_univ_three]

Premises used: Fin.sum_univ_three
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
2 : b * c * (a * d + b * c) + -(a * c * (b * d)) = HPow.hPow (β := ℕ) (b * c) 2
⊢ ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
simp [p, q, Fin.sum_univ_three]

Premises used: Fin.sum_univ_three
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
3 : b * d * (b * d) = HPow.hPow (β := ℕ) (b * d) 2
⊢ ∑ j : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
            (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), j)) :
          K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
    ![a * c, a * d, b * c, b * d] ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
simp [p, q, Fin.sum_univ_three]

Premises used: Fin.sum_univ_three
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ a * c * (a * c) = HPow.hPow (β := ℕ) (a * c) 2

Tactic:
ring
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ a * d * (a * d + b * c) + -(a * c * (b * d)) = HPow.hPow (β := ℕ) (a * d) 2

Tactic:
ring
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ b * c * (a * d + b * c) + -(a * c * (b * d)) = HPow.hPow (β := ℕ) (b * c) 2

Tactic:
ring
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ b * d * (b * d) = HPow.hPow (β := ℕ) (b * d) 2

Tactic:
ring
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
j : Fin 4
⊢ ∑ j_1 : Fin 3,
      HMul.hMul (α := K) (β := K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (q (j, j_1)) : K)
        ((eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K) (p j_1) : K) =
    ![a * c, a * d, b * c, b * d] j ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
case H => fin_cases j <;> simp [p, q, Fin.sum_univ_three] <;> ring

Premises used: Fin.sum_univ_three
-- 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
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 * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
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