awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
q' : ι × ι' → K := fun (a : ι × ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (q a)
H :
  mulHeight x ^ (M + N) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
inr :
  mulHeight x ^ N * mulHeight x ^ M ≤
    (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1 *
        mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
      mulHeight x ^ M
⊢ (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have rw : 0 < HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1
Tactic: rw [inv_mul_le_iff₀ ?hC, ← mul_le_mul_iff_left₀ (by positivity : 0 < mulHeight x ^ M)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
q' : ι × ι' → K := fun (a : ι × ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (q a)
H :
  mulHeight x ^ (M + N) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
⊢ mulHeight x ^ N * mulHeight x ^ M ≤
    (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1 *
        mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
      mulHeight x ^ M
have inr : mulHeight x ^ (M + N) ≤
  (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1 *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
    mulHeight x ^ M
Tactic: rw [← pow_add, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
q' : ι × ι' → K := fun (a : ι × ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (q a)
H :
  mulHeight x ^ (M + N) ≤
    HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * mulHeight q' *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
⊢ mulHeight x ^ (M + N) ≤
    (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1 *
        mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
      mulHeight x ^ M
have inr : (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * (max (mulHeightBound q) 1 * mulHeight x ^ M) *
    mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) ≤
  (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1 *
      mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)) *
    mulHeight x ^ M
Tactic: grw [H, mulHeight_eval_le hq x]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}
      (_h :
        ∀ (k : ι),
          ∑ j : ι',
              HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
                ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
            x k ^ (M + N)),
      C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have inl : IsEmpty ι' →
  ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}
      (_h :
        ∀ (k : ι),
          ∑ j : ι',
              HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
                ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
            x k ^ (M + N)),
      C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
Tactic: rcases isEmpty_or_nonempty ι'
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
inl :
  IsEmpty ι' →
    ∃ C > 0,
      ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}
        (_h :
          ∀ (k : ι),
            ∑ j : ι',
                HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
                  ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
              x k ^ (M + N)),
        C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}
      (_h :
        ∀ (k : ι),
          ∑ j : ι',
              HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
                ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
            x k ^ (M + N)),
      C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have inr : Nonempty ι' →
  ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}
      (_h :
        ∀ (k : ι),
          ∑ j : ι',
              HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
                ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
            x k ^ (M + N)),
      C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
Tactic: rcases isEmpty_or_nonempty ι'
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
h : Nonempty ι'
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}
      (_h :
        ∀ (k : ι),
          ∑ j : ι',
              HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
                ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
            x k ^ (M + N)),
      C * mulHeight x ^ N ≤ mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)
have this : 0 < Nat.card ι'
Tactic: have : 0 < Nat.card ι' := Nat.card_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
⊢ -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
have inl : IsEmpty ι' →
  -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
Tactic: rcases isEmpty_or_nonempty ι'
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
inl :
  IsEmpty ι' →
    -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
        (↑N : ℝ) * log (mulHeight x) ≤
      log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
⊢ -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
have inr : Nonempty ι' →
  -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
Tactic: rcases isEmpty_or_nonempty ι'
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
⊢ -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
have this : HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) ≠ 0
Tactic: have : (Nat.card ι' : ℝ) ^ totalWeight K ≠ 0 := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_6
inst : Field K
ι : Type u_7
ι' : Type u_8
inst_1 : Fintype ι'
inst_2 : AdmissibleAbsValues K
inst_3 : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h :
  ∀ (k : ι),
    ∑ j : ι',
        HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial ι K) → K) (q (k, j)) : K)
          ((eval x : (a : MvPolynomial ι K) → K) (p j) : K) =
      x k ^ (M + N)
h_1 : Nonempty ι'
this : HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) ≠ 0
⊢ -log (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1) +
      (↑N : ℝ) * log (mulHeight x) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
have inr : log ((HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N) ≤
  log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))
Tactic: pull (disch := first | assumption | positivity) log
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ mulHeight ![a, b] * mulHeight ![c, d] = mulHeight ![a * c, a * d, b * c, b * d]
have simp : (mulHeight.{u_4, 0} (K := K) fun (a_1 : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ↦
    ![a, b] a_1.1 * ![c, d] a_1.2) =
  mulHeight ![a * c, a * d, b * c, b * d]
Tactic: simp only [← mulHeight_fun_mul_eq hab hcd]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ (mulHeight.{u_4, 0} (K := K) fun (a_1 : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ↦
      ![a, b] a_1.1 * ![c, d] a_1.2) =
    mulHeight ![a * c, a * d, b * c, b * d]
have h : ∀ (i : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ),
  ![a, b] i.1 * ![c, d] i.2 =
    (![a * c, a * d, b * c, b * d] ∘
        (⇑finProdFinEquiv :
          (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ)))
      i
Tactic: convert! mulHeight_comp_equiv finProdFinEquiv _ with i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
i : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ
⊢ ![a, b] i.1 * ![c, d] i.2 =
    (![a * c, a * d, b * c, b * d] ∘
        (⇑finProdFinEquiv :
          (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ)))
      i
have h : ![a, b]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)).1 *
    ![c, d]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)).2 =
  Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
    (⇑finProdFinEquiv :
      (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩, (fun (i : Fin (Nat.succ 0).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
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
i : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ
h :
  ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).1 *
      ![c, d]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).2 =
    Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
      (⇑finProdFinEquiv :
        (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![a, b] i.1 * ![c, d] i.2 =
    (![a * c, a * d, b * c, b * d] ∘
        (⇑finProdFinEquiv :
          (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ)))
      i
have h₁ : ![a, b]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)).1 *
    ![c, d]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)).2 =
  Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
    (⇑finProdFinEquiv :
      (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩, (fun (i : Fin (Nat.succ 0).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
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
i : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ
h :
  ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).1 *
      ![c, d]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).2 =
    Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
      (⇑finProdFinEquiv :
        (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)).1 *
      ![c, d]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)).2 =
    Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
      (⇑finProdFinEquiv :
        (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![a, b] i.1 * ![c, d] i.2 =
    (![a * c, a * d, b * c, b * d] ∘
        (⇑finProdFinEquiv :
          (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ)))
      i
have h₂ : ![a, b]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)).1 *
    ![c, d]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)).2 =
  Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
    (⇑finProdFinEquiv :
      (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩, (fun (i : Fin (Nat.succ 0).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]
i : Fin 3
⊢ (p i).IsHomogeneous 1
have 0 : (p ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))).IsHomogeneous 1
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]
i : Fin 3
0 : (p ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (p i).IsHomogeneous 1
have 1 : (p ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))).IsHomogeneous 1
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]
i : Fin 3
0 : (p ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (p ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (p i).IsHomogeneous 1
have 2 : (p ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
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]
⊢ ∃ C > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]
have hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
Tactic: have hom i : (p i).IsHomogeneous 1 := by
    fin_cases i <;> simp [p, isHomogeneous_X, IsHomogeneous.add]
-- 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 > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]
have obtain : ∀ (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 * HPow.hPow (β := ℕ) (mulHeight x) 1),
  ∃ C > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]
Tactic: obtain ⟨C, hC₀, hC⟩ := mulHeight_eval_le' hom
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
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 * HPow.hPow (β := ℕ) (mulHeight x) 1
⊢ ∃ C > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]
have 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
Tactic: simp only [pow_one] at hC
Cleared hypotheses: hC
-- 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
⊢ ∃ C > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]
have refine : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
Tactic: refine ⟨max C 1, by grind, 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
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
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
have pos : ∀ (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