awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 2)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₂ : ValueGroup R K) ≤
    1
have h : (valuation R K : (a : K) → ValueGroup R K) W.a₂ ≤ HPow.hPow (β := ℕ) lmax 2
Tactic: refine inv_mul_le_one_of_le₀ ?_ zero_le'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₂ ≤ HPow.hPow (β := ℕ) lmax 2
have h : lmax ≤ HPow.hPow (β := ℕ) lmax 2
Tactic: refine (hlmax _ (by simp [l₀, l])).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ (r₃ : R),
    (algebraMap R K : (a : R) → K) r₃ =
      (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₃
have h : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
  (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₃
Tactic: apply (mem_integer_iff _ _ _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
    (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₃
have h : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
  ((HPow.hPow (β := ℕ) a 3)⁻¹ * W.a₃)
Tactic: simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ LE.le (α := ValueGroup R K)
    ((valuation R K : (a : K) → ValueGroup R K) ((HPow.hPow (β := ℕ) a 3)⁻¹ * W.a₃) : ValueGroup R K)
    (1 : ValueGroup R K)
have h : HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 3)⁻¹
    ((valuation R K : (a : K) → ValueGroup R K) W.a₃ : ValueGroup R K) ≤
  1
Tactic: simp only [map_mul, map_inv₀, map_pow, ha]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 3)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₃ : ValueGroup R K) ≤
    1
have h : (valuation R K : (a : K) → ValueGroup R K) W.a₃ ≤ HPow.hPow (β := ℕ) lmax 3
Tactic: refine inv_mul_le_one_of_le₀ ?_ zero_le'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₃ ≤ HPow.hPow (β := ℕ) lmax 3
have h : lmax ≤ HPow.hPow (β := ℕ) lmax 3
Tactic: refine (hlmax _ (by simp [l₀, l])).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ (r₄ : R),
    (algebraMap R K : (a : R) → K) r₄ =
      (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₄
have h : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
  (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₄
Tactic: apply (mem_integer_iff _ _ _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
    (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₄
have h : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
  ((HPow.hPow (β := ℕ) a 4)⁻¹ * W.a₄)
Tactic: simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ LE.le (α := ValueGroup R K)
    ((valuation R K : (a : K) → ValueGroup R K) ((HPow.hPow (β := ℕ) a 4)⁻¹ * W.a₄) : ValueGroup R K)
    (1 : ValueGroup R K)
have h : HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 4)⁻¹
    ((valuation R K : (a : K) → ValueGroup R K) W.a₄ : ValueGroup R K) ≤
  1
Tactic: simp only [map_mul, map_inv₀, map_pow, ha]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 4)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₄ : ValueGroup R K) ≤
    1
have h : (valuation R K : (a : K) → ValueGroup R K) W.a₄ ≤ HPow.hPow (β := ℕ) lmax 4
Tactic: refine inv_mul_le_one_of_le₀ ?_ zero_le'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₄ ≤ HPow.hPow (β := ℕ) lmax 4
have h : lmax ≤ HPow.hPow (β := ℕ) lmax 4
Tactic: refine (hlmax _ (by simp [l₀, l])).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ (r₆ : R),
    (algebraMap R K : (a : R) → K) r₆ =
      (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₆
have h : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
  (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₆
Tactic: apply (mem_integer_iff _ _ _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
    (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W).a₆
have h : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
  ((HPow.hPow (β := ℕ) a 6)⁻¹ * W.a₆)
Tactic: simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ LE.le (α := ValueGroup R K)
    ((valuation R K : (a : K) → ValueGroup R K) ((HPow.hPow (β := ℕ) a 6)⁻¹ * W.a₆) : ValueGroup R K)
    (1 : ValueGroup R K)
have h : HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 6)⁻¹
    ((valuation R K : (a : K) → ValueGroup R K) W.a₆ : ValueGroup R K) ≤
  1
Tactic: simp only [map_mul, map_inv₀, map_pow, ha]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 6)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₆ : ValueGroup R K) ≤
    1
have h : (valuation R K : (a : K) → ValueGroup R K) W.a₆ ≤ HPow.hPow (β := ℕ) lmax 6
Tactic: refine inv_mul_le_one_of_le₀ ?_ zero_le'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₆ ≤ HPow.hPow (β := ℕ) lmax 6
have h : lmax ≤ HPow.hPow (β := ℕ) lmax 6
Tactic: refine (hlmax _ (by simp [l₀, l])).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 2
have h : Ne (α := ℕ) 2 0
Tactic: apply le_self_pow hlmax_ge_1.le
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ Ne (α := ℕ) 2 0
have linarith : Eq (α := ℕ) 2 0 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
linarith : Eq (α := ℕ) 2 0 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 0 = 0
⊢ Ne (α := ℕ) 2 0
have linarith₁ : Eq (α := ℕ) 2 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 3
have h : Ne (α := ℕ) 3 0
Tactic: apply le_self_pow hlmax_ge_1.le
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ Ne (α := ℕ) 3 0
have linarith : Eq (α := ℕ) 3 0 → HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 3 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
linarith : Eq (α := ℕ) 3 0 → HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 3 0 = 0
⊢ Ne (α := ℕ) 3 0
have linarith₁ : Eq (α := ℕ) 3 0 → GT.gt (α := ℤ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 4
have h : Ne (α := ℕ) 4 0
Tactic: apply le_self_pow hlmax_ge_1.le
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
⊢ Ne (α := ℕ) 4 0
have linarith : Eq (α := ℕ) 4 0 → HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 4 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun (a : K) ↦ (valuation R K : (a : K) → ValueGroup R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos (l := l) ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax
ha₀ : a ≠ 0
linarith : Eq (α := ℕ) 4 0 → HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 4 0 = 0
⊢ Ne (α := ℕ) 4 0
have linarith₁ : Eq (α := ℕ) 4 0 → GT.gt (α := ℤ) 4 0
Tactic: linarith