awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 ι'
⊢ HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) ≠ 0

Tactic:
have : (Nat.card ι' : ℝ) ^ totalWeight K ≠ 0 := by simp
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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))
⊢ -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:
pull (disch := first | assumption | positivity) log

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ 0 < (HPow.hPow (α := ℝ) (↑(Nat.card ι') : ℝ) (totalWeight K) * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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)⁻¹ * mulHeight x ^ N) ≤
    log (mulHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j))

Tactic:
exact (log_le_log <| by positivity) <| mulHeight_eval_ge hq p h

Premises used: Real.log_le_log, Height.mulHeight_eval_ge
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 : ℝ),
    ∀ (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 + (↑N : ℝ) * logHeight x ≤
        logHeight.{u_6, u_8} (K := K) fun (j : ι') ↦ (eval x : (a : MvPolynomial ι K) → K) (p j)

Tactic:
⟨_, logHeight_eval_ge hq⟩

Premises used: Height.logHeight_eval_ge, Exists.intro
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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]
⊢ mulHeight ![a, b] * mulHeight ![c, d] = mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
simp only [← mulHeight_fun_mul_eq hab hcd]

Premises used: Height.mulHeight_fun_mul_eq
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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 (ι := 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))) =
    mulHeight ![a * c, a * d, b * c, b * d]

Tactic:
mulHeight_comp_equiv finProdFinEquiv _

Premises used: Height.mulHeight_comp_equiv, finProdFinEquiv
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
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
⊢ (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:
convert! mulHeight_comp_equiv finProdFinEquiv _ with i

Premises used: Height.mulHeight_comp_equiv, finProdFinEquiv
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ ![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, ⋯⟩)

Tactic:
simp [finProdFinEquiv]

Premises used: finProdFinEquiv
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ ![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, ⋯⟩)

Tactic:
simp [finProdFinEquiv]

Premises used: finProdFinEquiv
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : 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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [finProdFinEquiv]

Premises used: finProdFinEquiv
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : 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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [finProdFinEquiv]

Premises used: finProdFinEquiv
-- 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]
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
2 : (p ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (p i).IsHomogeneous 1

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]
⊢ (p ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [p, isHomogeneous_X, IsHomogeneous.add]

Premises used: MvPolynomial.IsHomogeneous.add, MvPolynomial.isHomogeneous_X
-- 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]
⊢ (p ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [p, isHomogeneous_X, IsHomogeneous.add]

Premises used: MvPolynomial.IsHomogeneous.add, MvPolynomial.isHomogeneous_X
-- 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]
⊢ (p ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1

Tactic:
simp [p, isHomogeneous_X, IsHomogeneous.add]

Premises used: MvPolynomial.IsHomogeneous.add, MvPolynomial.isHomogeneous_X
-- 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]
⊢ ∀ (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]
-- 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
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]
⊢ ∃ 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

Premises used: Height.mulHeight_eval_le', MvPolynomial.C
-- 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 * HPow.hPow (β := ℕ) (mulHeight x) 1
⊢ ∀ (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

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]
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
⊢ max C 1 > 0

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
refine : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
⊢ ∃ C > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
refine ⟨max C 1, by grind, fun a b c d ↦ ?_⟩
-- 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
pos : ∀ (hab : ![a, b] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
neg : ∀ (hab : ¬![a, b] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
by_cases hab : ![a, b] = 0
-- 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
h : ∀ (i : Fin (Nat.succ 0).succ.succ), ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 i
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] = 0

Tactic:
ext 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
i : Fin (Nat.succ 0).succ.succ
h :
  ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h₂ :
  ![0 * c, 0 * d + 0 * c, 0 * d] ((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, ⋯⟩)
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 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
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)

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
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)

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
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((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
pos : 1 ≤ max C 1 * mulHeight ![c, d]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
rw [hab, mulHeight_zero, mul_one, show a = 0 from congrFun hab 0,
      show b = 0 from congrFun hab 1,
      show ![0 * c, 0 * d + 0 * c, 0 * d] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]

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
pos : 1 ≤ max C 1 * 1
⊢ 1 ≤ max C 1 * mulHeight ![c, d]

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
⊢ 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
pos : ∀ (hcd : ![c, d] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
neg : ∀ (hcd : ¬![c, d] = 0), mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
by_cases hcd : ![c, d] = 0
-- 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 * 0, a * 0 + b * 0, b * 0] i = 0 i
⊢ ![a * 0, a * 0 + b * 0, b * 0] = 0

Tactic:
ext 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 * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![a * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h₂ :
  ![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, ⋯⟩)
⊢ ![a * 0, a * 0 + b * 0, b * 0] i = 0 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 * 0, a * 0 + b * 0, b * 0] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    0 ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp