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]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 6 : (q ((fun (i : Fin 4) ↦ i) (⟨2, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- 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]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
6 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 7 : (q ((fun (i : Fin 4) ↦ i) (⟨2, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- 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]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
6 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
7 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 8 : (q ((fun (i : Fin 4) ↦ i) (⟨2, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- 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]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
6 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
7 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
8 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 9 : (q ((fun (i : Fin 4) ↦ i) (⟨3, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- 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]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
6 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
7 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
8 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
9 : (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 10 : (q ((fun (i : Fin 4) ↦ i) (⟨3, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- 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]]
a : Fin 4 × Fin 3
0 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
1 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
2 : (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
3 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
4 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
5 : (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
6 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
7 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
8 : (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
9 : (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
10 : (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
⊢ (q a).IsHomogeneous 1
have 11 : (q ((fun (i : Fin 4) ↦ i) (⟨3, sorry⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))).IsHomogeneous 1
Tactic: fin_cases a
Cleared hypotheses: a
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 0 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 0) 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 1 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨0, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 2 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 3 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 4 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 1) 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨1, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 5 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (-X 0) 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 6 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 7 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 2) 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 8 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (-X 0) 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 9 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 10 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) 0 1
Tactic: simp [q]
-- 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]]
⊢ (q ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4), (fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))).IsHomogeneous 1
have 11 : IsHomogeneous.{0, u_4} (σ := Fin 4) (R := K) (X 3) 1
Tactic: simp [q]
-- 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]
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]]
⊢ ∃ 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]
have hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
Tactic: have hom a : (q a).IsHomogeneous 1 := by
    fin_cases a <;> simp [q] <;> grind [!isHomogeneous_X, isHomogeneous_zero, IsHomogeneous.neg]
-- 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 > 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]
have obtain : ∀ (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)),
  ∃ 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: obtain ⟨C, hC₀, hC⟩ := mulHeight_eval_ge' (M := 1) (N := 1) 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]
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)
⊢ ∃ 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]
have 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)
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]
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]
have 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]
Tactic: refine ⟨C, hC₀, 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
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, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
have rw : C * mulHeight ![a * c, a * d, b * c, b * d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
Tactic: rw [mul_assoc, mulHeight_mul_mulHeight hab hcd]
-- 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
⊢ C * mulHeight ![a * c, a * d, b * c, b * d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
have 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)
Tactic: convert! hC p fun j ↦ ?H with 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
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)
⊢ C * mulHeight ![a * c, a * d, b * c, b * d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
have 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
Tactic: convert! hC p fun j ↦ ?H with i