awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h :
  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
    ((HPow.hPow (β := ℕ) a 4)⁻¹ * W.a₄)
⊢ 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:
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]

Premises used: OfNat.ofNat_ne_zero, sub_zero, Units.val_inv_eq_inv_val, MulZeroClass.zero_mul, WeierstrassCurve.variableChange_def, inv_pow, ne_eq, MulZeroClass.mul_zero, add_zero, Units.val_mk0, not_false_eq_true, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h :
  HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 4)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₄ : ValueGroup R K) ≤
    1
⊢ 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)

Tactic:
simp only [map_mul, map_inv₀, map_pow, ha]

Premises used: map_inv₀, map_pow, map_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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

Tactic:
inv_mul_le_one_of_le₀ ?_ zero_le'

Premises used: zero_le', inv_mul_le_one_of_le₀
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : (valuation R K : (a : K) → ValueGroup R K) W.a₄ ≤ HPow.hPow (β := ℕ) lmax 4
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 4)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₄ : ValueGroup R K) ≤
    1

Tactic:
refine inv_mul_le_one_of_le₀ ?_ zero_le'

Premises used: zero_le', inv_mul_le_one_of_le₀
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 (α := ValueGroup R K) l ((valuation R K : (a : K) → ValueGroup R K) W.a₄ : ValueGroup R K)

Tactic:
simp [l₀, l]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : lmax ≤ HPow.hPow (β := ℕ) lmax 4
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₄ ≤ HPow.hPow (β := ℕ) lmax 4

Tactic:
refine (hlmax _ (by simp [l₀, l])).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
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₆
⊢ ∃ (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₆

Tactic:
apply (mem_integer_iff _ _ _).mp

Premises used: ValuationRing.mem_integer_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h :
  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup R K) (valuation R K))
    ((HPow.hPow (β := ℕ) a 6)⁻¹ * W.a₆)
⊢ 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:
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]

Premises used: OfNat.ofNat_ne_zero, sub_zero, Units.val_inv_eq_inv_val, MulZeroClass.zero_mul, WeierstrassCurve.variableChange_def, inv_pow, ne_eq, MulZeroClass.mul_zero, add_zero, Units.val_mk0, not_false_eq_true, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h :
  HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 6)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₆ : ValueGroup R K) ≤
    1
⊢ 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)

Tactic:
simp only [map_mul, map_inv₀, map_pow, ha]

Premises used: map_inv₀, map_pow, map_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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

Tactic:
inv_mul_le_one_of_le₀ ?_ zero_le'

Premises used: zero_le', inv_mul_le_one_of_le₀
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : (valuation R K : (a : K) → ValueGroup R K) W.a₆ ≤ HPow.hPow (β := ℕ) lmax 6
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 6)⁻¹
      ((valuation R K : (a : K) → ValueGroup R K) W.a₆ : ValueGroup R K) ≤
    1

Tactic:
refine inv_mul_le_one_of_le₀ ?_ zero_le'

Premises used: zero_le', inv_mul_le_one_of_le₀
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 (α := ValueGroup R K) l ((valuation R K : (a : K) → ValueGroup R K) W.a₆ : ValueGroup R K)

Tactic:
simp [l₀, l]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : lmax ≤ HPow.hPow (β := ℕ) lmax 6
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₆ ≤ HPow.hPow (β := ℕ) lmax 6

Tactic:
refine (hlmax _ (by simp [l₀, l])).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : Ne (α := ℕ) 2 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 2

Tactic:
apply le_self_pow hlmax_ge_1.le

Premises used: le_self_pow, GE.ge.le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
linarith₁ : Eq (α := ℕ) 2 0 → GT.gt (α := ℤ) 2 0
⊢ Ne (α := ℕ) 2 0

Tactic:
linarith
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : Ne (α := ℕ) 3 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 3

Tactic:
apply le_self_pow hlmax_ge_1.le

Premises used: le_self_pow, GE.ge.le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
linarith₁ : Eq (α := ℕ) 3 0 → GT.gt (α := ℤ) 3 0
⊢ Ne (α := ℕ) 3 0

Tactic:
linarith
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : Ne (α := ℕ) 4 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 4

Tactic:
apply le_self_pow hlmax_ge_1.le

Premises used: le_self_pow, GE.ge.le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
linarith₁ : Eq (α := ℕ) 4 0 → GT.gt (α := ℤ) 4 0
⊢ Ne (α := ℕ) 4 0

Tactic:
linarith
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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
h : Ne (α := ℕ) 6 0
⊢ lmax ≤ HPow.hPow (β := ℕ) lmax 6

Tactic:
apply le_self_pow hlmax_ge_1.le

Premises used: le_self_pow, GE.ge.le
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 (α := ℕ) 6 0 → HMul.hMul (α := ℤ) 6 (-1) + HSub.hSub (α := ℤ) 6 0 = 0
linarith₁ : Eq (α := ℕ) 6 0 → GT.gt (α := ℤ) 6 0
⊢ Ne (α := ℕ) 6 0

Tactic:
linarith
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
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 ≤ lmax

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
choose :
  ∀ (r : R) (hr : (algebraMap R K : (a : R) → K) r = W.Δ),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          W.Δ :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        W.Δ :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
choose r hr using Δ_integral_of_isIntegral R W

Premises used: WeierstrassCurve.Δ_integral_of_isIntegral
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
r : R
hr : (algebraMap R K : (a : R) → K) r = W.Δ
rw :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) r) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        W.Δ :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [← hr]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
r : R
hr : (algebraMap R K : (a : R) → K) r = W.Δ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) r) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
valuation_le_one (maximalIdeal R) r

Premises used: IsDiscreteValuationRing.maximalIdeal, IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
r : R
hr : (algebraMap R K : (a : R) → K) r = W.Δ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) r) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
exact valuation_le_one (maximalIdeal R) r

Premises used: IsDiscreteValuationRing.maximalIdeal, IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (↑(valuation_Δ_aux R W) : WithZero (Multiplicative ℤ)) =
    ((valuation K (maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      W.Δ

Tactic:
simp [valuation_Δ_aux, hW]

Premises used: WeierstrassCurve.valuation_Δ_aux
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
W : WeierstrassCurve K
inst_6 : IsMinimal R W
⊢ IsIntegral R W

Tactic:
simpa using IsMinimal.val_Δ_maximal.1

Premises used: WeierstrassCurve.IsMinimal.val_Δ_maximal, And.left