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) ⋯
⊢ lmax ∈ l

Tactic:
have hlmax_mem : lmax ∈ l :=
    List.maximum_of_length_pos_mem (by 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
v : ValueGroup R K
hv : v ∈ l
⊢ 0 < l.length

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
⊢ ∀ v ∈ l, v ≤ lmax

Tactic:
have hlmax : ∀ v ∈ l, v ≤ lmax := fun v hv ↦
    List.le_maximum_of_length_pos_of_mem hv (by 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
pos : ∀ (hlmax_le_1 : lmax ≤ 1), ∃ (C : VariableChange K), IsIntegral R (C • W)
neg : ∀ (hlmax_le_1 : ¬lmax ≤ 1), ∃ (C : VariableChange K), IsIntegral R (C • W)
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)

Tactic:
by_cases hlmax_le_1 : lmax ≤ 1
-- 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
h : IsIntegral R (HSMul.hSMul (α := VariableChange K) { u := 1, r := 0, s := 0, t := 0 : VariableChange K } W)
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)

Tactic:
use ⟨1, 0, 0, 0⟩
-- 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
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₄
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)

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
⊢ 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
⊢ ∃ (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:
simpa [← mem_integer_iff, variableChange_def, Valuation.mem_integer_iff]
      using (hlmax _ (by simp [l₀, l])).trans hlmax_le_1

Premises used: ValuationRing.mem_integer_iff, WeierstrassCurve.variableChange_def, LE.le.trans, Valuation.mem_integer_iff
-- 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
⊢ 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
⊢ ∃ (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:
simpa [← mem_integer_iff, variableChange_def, Valuation.mem_integer_iff]
      using (hlmax _ (by simp [l₀, l])).trans hlmax_le_1

Premises used: ValuationRing.mem_integer_iff, WeierstrassCurve.variableChange_def, LE.le.trans, Valuation.mem_integer_iff
-- 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
⊢ 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
⊢ ∃ (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:
simpa [← mem_integer_iff, variableChange_def, Valuation.mem_integer_iff]
      using (hlmax _ (by simp [l₀, l])).trans hlmax_le_1

Premises used: ValuationRing.mem_integer_iff, WeierstrassCurve.variableChange_def, LE.le.trans, Valuation.mem_integer_iff
-- 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
⊢ 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
⊢ ∃ (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:
simpa [← mem_integer_iff, variableChange_def, Valuation.mem_integer_iff]
      using (hlmax _ (by simp [l₀, l])).trans hlmax_le_1

Premises used: ValuationRing.mem_integer_iff, WeierstrassCurve.variableChange_def, LE.le.trans, Valuation.mem_integer_iff
-- 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
⊢ 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
⊢ ∃ (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:
simpa [← mem_integer_iff, variableChange_def, Valuation.mem_integer_iff]
      using (hlmax _ (by simp [l₀, l])).trans hlmax_le_1

Premises used: ValuationRing.mem_integer_iff, WeierstrassCurve.variableChange_def, LE.le.trans, Valuation.mem_integer_iff
-- 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
⊢ lmax ≥ 1

Tactic:
have hlmax_ge_1 : lmax ≥ 1 := le_of_not_ge hlmax_le_1
-- 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
i : ℕ := List.idxOf lmax l
⊢ i < l.length

Tactic:
have hi : i < l.length := List.idxOf_lt_length_of_mem hlmax_mem
-- 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
i : ℕ := List.idxOf lmax l
hi : i < l.length
h :
  (valuation R K : (a : K) → ValueGroup R K) (getElem (valid := fun (as : List K) (i : ℕ) ↦ i < as.length) l₀ i hi) =
    lmax
⊢ ∃ (a : K), (valuation R K : (a : K) → ValueGroup R K) a = lmax

Tactic:
use l₀[i]
-- 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
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) =
    getElem (valid := fun (as : List (ValueGroup R K)) (i : ℕ) ↦ i < as.length) l i hi

Tactic:
simp [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
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) =
    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]
-- 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
i : ℕ := List.idxOf lmax l
hi : i < l.length
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
⊢ (valuation R K : (a : K) → ValueGroup R K) (getElem (valid := fun (as : List K) (i : ℕ) ↦ i < as.length) l₀ i hi) =
    lmax

Tactic:
simpa only [hi₁] using (List.getElem_idxOf hi)

Premises used: List.getElem_idxOf
-- 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), (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)
-- 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
h : ∃ (a : K), (valuation R K : (a : K) → ValueGroup R K) a = lmax
neg :
  ∀ (a : K) (ha : (valuation R K : (a : K) → ValueGroup R K) a = lmax), ∃ (C : VariableChange K), IsIntegral R (C • W)
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)

Tactic:
choose a ha using h
-- 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
by_contra : ∀ (ha₀ : a = 0), False
⊢ a ≠ 0

Tactic:
by_contra ha₀
-- 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
⊢ 0 = lmax

Tactic:
simp only [ha₀, map_zero] at ha

Premises used: map_zero
-- 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₀ : a = 0
ha : 0 = lmax
⊢ False

Tactic:
exact (ha ▸ hlmax_le_1) zero_le_one
-- 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
⊢ 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
-- 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 :
  IsIntegral R
    (HSMul.hSMul (α := VariableChange K) { u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 : VariableChange K } W)
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)

Tactic:
use ⟨Units.mk0 a ha₀, 0, 0, 0⟩