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
h :
  ∃ (r₁ : R),
    (algebraMap R K : (a : R) → K) r₁ =
      (HSMul.hSMul (α := VariableChange K) { u := 1, 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 := 1, 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 := 1, 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 := 1, r := 0, s := 0, t := 0 : VariableChange K } W).a₄
⊢ IsIntegral R (HSMul.hSMul (α := VariableChange K) { u := 1, r := 0, s := 0, t := 0 : VariableChange K } W)
have h₄ : ∃ (r₆ : R),
  (algebraMap R K : (a : R) → K) r₆ =
    (HSMul.hSMul (α := VariableChange K) { u := 1, r := 0, s := 0, t := 0 : VariableChange K } W).a₆
Tactic: apply isIntegral_of_exists_lift R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
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
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have hlmax_ge_1 : lmax ≥ 1
Tactic: have hlmax_ge_1 : lmax ≥ 1 := le_of_not_ge hlmax_le_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
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
i : ℕ := List.idxOf lmax l
⊢ ∃ (a : K), (valuation R K : (a : K) → ValueGroup R K) a = lmax
have hi : i < l.length
Tactic: have hi : i < l.length := List.idxOf_lt_length_of_mem hlmax_mem
-- 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
i : ℕ := List.idxOf lmax l
hi : i < l.length
⊢ ∃ (a : K), (valuation R K : (a : K) → ValueGroup R K) a = lmax
have h : (valuation R K : (a : K) → ValueGroup R K) (getElem (valid := fun (as : List K) (i : ℕ) ↦ i < as.length) l₀ i hi) = lmax
Tactic: use l₀[i]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
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
i : ℕ := List.idxOf lmax l
hi : i < l.length
⊢ (valuation R K : (a : K) → ValueGroup R K) (getElem (valid := fun (as : List K) (i : ℕ) ↦ i < as.length) l₀ i hi) =
    lmax
have hi₁ : (valuation R K : (a : K) → ValueGroup R K) (getElem (valid := fun (as : List K) (i : ℕ) ↦ i < as.length) l₀ i hi) =
  getElem (valid := fun (as : List (ValueGroup R K)) (i : ℕ) ↦ i < as.length) l i hi
Tactic: have hi₁ : (valuation R K) l₀[i] = l[i] := by simp [l]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
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
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have h : ∃ (a : K), (valuation R K : (a : K) → ValueGroup R K) a = lmax
Tactic: have h : ∃ a : K, valuation R K a = lmax := by
      let i : ℕ := l.idxOf lmax
      have hi : i < l.length := List.idxOf_lt_length_of_mem hlmax_mem
      use l₀[i]
      have hi₁ : (valuation R K) l₀[i] = l[i] := by simp [l]
      simpa only [hi₁] using (List.getElem_idxOf hi)
-- 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
h : ∃ (a : K), (valuation R K : (a : K) → ValueGroup R K) a = lmax
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have neg : ∀ (a : K) (ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax), ∃ (C : VariableChange K), IsIntegral R (C • W)
Tactic: choose a ha using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
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
⊢ False
have ha₁ : 0 = lmax
Tactic: simp only [ha₀, map_zero] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Reduction (hypothesis)
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
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have ha₀ : a ≠ 0
Tactic: have ha₀ : a ≠ 0 := by
      by_contra ha₀; simp only [ha₀, map_zero] at ha
      exact (ha ▸ hlmax_le_1) zero_le_one
-- 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
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have h : IsIntegral R (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W)
Tactic: use ⟨Units.mk0 a ha₀, 0, 0, 0⟩
-- 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
⊢ IsIntegral R
    (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W)
have 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₁
Tactic: apply isIntegral_of_exists_lift R
-- 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
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)
have 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₂
Tactic: apply isIntegral_of_exists_lift R
-- 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
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)
have 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₃
Tactic: apply isIntegral_of_exists_lift R
-- 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
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)
have 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₄
Tactic: apply isIntegral_of_exists_lift R
-- 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
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)
have 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₆
Tactic: apply isIntegral_of_exists_lift R
-- 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)) (a⁻¹ * 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) (a⁻¹ * W.a₁) : ValueGroup R K)
    (1 : ValueGroup R K)
have h : HMul.hMul (β := ValueGroup R K) lmax⁻¹ ((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) lmax⁻¹ ((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₁ ≤ lmax
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₁ ≤ lmax
have h : lmax ≤ lmax
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 2)⁻¹ * 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 2)⁻¹ * W.a₂) : ValueGroup R K)
    (1 : ValueGroup R K)
have h : HMul.hMul (β := ValueGroup R K) (HPow.hPow (β := ℕ) lmax 2)⁻¹
    ((valuation R K : (a : K) → ValueGroup R K) W.a₂ : ValueGroup R K) ≤
  1
Tactic: simp only [map_mul, map_inv₀, map_pow, ha]