Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨0, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨0, ⋯⟩) ^ (1 + 1)

pp: case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨1, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨1, ⋯⟩) ^ (1 + 1)

pp: case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨2, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨2, ⋯⟩) ^ (1 + 1)

pp: case «3»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨3, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨3, ⋯⟩) ^ (1 + 1)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨0, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨0, ⋯⟩) ^ (1 + 1)

case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨1, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨1, ⋯⟩) ^ (1 + 1)

case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨2, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨2, ⋯⟩) ^ (1 + 1)

case «3»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, 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},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨3, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨3, ⋯⟩) ^ (1 + 1)