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 :
  ∃ (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₁
h₁ :
  ∃ (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₂
h₂ :
  ∃ (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₃
h₃ :
  ∃ (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₄
h₄ :
  ∃ (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₆
⊢ IsIntegral R
    (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W)

Tactic:
apply isIntegral_of_exists_lift R

Premises used: WeierstrassCurve.isIntegral_of_exists_lift
-- 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)) (a⁻¹ * 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) lmax⁻¹ ((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) (a⁻¹ * 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) lmax⁻¹ ((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₁ ≤ lmax
⊢ HMul.hMul (β := ValueGroup R K) lmax⁻¹ ((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 ≤ lmax
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₁ ≤ lmax

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 2)⁻¹ * 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 2)⁻¹
      ((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 2)⁻¹ * 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 2)⁻¹
      ((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 2
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 2)⁻¹
      ((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 2
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₂ ≤ HPow.hPow (β := ℕ) lmax 2

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 3)⁻¹ * 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 3)⁻¹
      ((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 3)⁻¹ * 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 3)⁻¹
      ((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 3
⊢ HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 3)⁻¹
      ((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 3
⊢ (valuation R K : (a : K) → ValueGroup R K) W.a₃ ≤ HPow.hPow (β := ℕ) lmax 3

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