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]
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
have 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, sorry⟩ : 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, sorry⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
Tactic: fin_cases j
Cleared hypotheses: j
-- 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]]
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
⊢ ∑ 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
have 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, sorry⟩ : 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, sorry⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
Tactic: fin_cases j
Cleared hypotheses: j
-- 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]]
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
⊢ ∑ 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
have 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, sorry⟩ : 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, sorry⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
Tactic: fin_cases j
Cleared hypotheses: j
-- 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]]
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
⊢ ∑ 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
have 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, sorry⟩ : 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, sorry⟩ : Fin 4)) ^ HAdd.hAdd (α := ℕ) 1 1
Tactic: fin_cases j
Cleared hypotheses: j
-- 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]]
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 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
have 0 : a * c * (a * c) = HPow.hPow (β := ℕ) (a * c) 2
Tactic: simp [p, q, Fin.sum_univ_three]
-- 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]]
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 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
have 1 : a * d * (a * d + b * c) + -(a * c * (b * d)) = HPow.hPow (β := ℕ) (a * d) 2
Tactic: simp [p, q, Fin.sum_univ_three]
-- 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]]
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 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
have 2 : b * c * (a * d + b * c) + -(a * c * (b * d)) = HPow.hPow (β := ℕ) (b * c) 2
Tactic: simp [p, q, Fin.sum_univ_three]
-- 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]]
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 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
have 3 : b * d * (b * d) = HPow.hPow (β := ℕ) (b * d) 2
Tactic: simp [p, q, Fin.sum_univ_three]
-- 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]]
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
⊢ ![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]
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)))
⊢ ![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]
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)))
⊢ ![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
⊢ ∃ (C : ℝ), ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]
have obtain : ∀ (C' : ℝ) (hC₀ : C' > 0)
  (hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]),
  ∃ (C : ℝ), ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]
Tactic: obtain ⟨C', hC₀, hC⟩ := mulHeight_sym2_le K
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
⊢ ∃ (C : ℝ), ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]
have refine : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ log C' + logHeight ![a, b] + logHeight ![c, d]
Tactic: refine ⟨log C', fun a b c d ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
a b c d : K
⊢ log (mulHeight ![a * c, a * d + b * c, b * d]) ≤ log C' + log (mulHeight ![a, b]) + log (mulHeight ![c, d])
have pull : log (mulHeight ![a * c, a * d + b * c, b * d]) ≤ log (C' * mulHeight ![a, b] * mulHeight ![c, d])
Tactic: pull (disch := positivity) log
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
⊢ ∃ (C : ℝ),
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
have obtain : ∀ (C' : ℝ) (hC₀ : C' > 0)
  (hC :
    ∀ {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 : ℝ),
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
Tactic: obtain ⟨C', hC₀, hC⟩ := mulHeight_sym2_ge K
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {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 : ℝ),
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
have refine : ∀ {a b c d : K} (hab : ![a, b] ≠ 0) (hcd : ![c, d] ≠ 0),
  log C' + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
Tactic: refine ⟨log C', fun hab hcd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {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]
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ log C' + log (mulHeight ![a, b]) + log (mulHeight ![c, d]) ≤ log (mulHeight ![a * c, a * d + b * c, b * d])
have pull : log (C' * mulHeight ![a, b] * mulHeight ![c, d]) ≤ log (mulHeight ![a * c, a * d + b * c, b * d])
Tactic: pull (disch := positivity) log
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
⊢ ∃ (C : ℝ),
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 → |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ C
have obtain : ∀ (C₁ : ℝ)
  (hC₁ : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C₁ + logHeight ![a, b] + logHeight ![c, d]),
  ∃ (C : ℝ),
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 → |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ C
Tactic: obtain ⟨C₁, hC₁⟩ := logHeight_sym2_le K