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
W : WeierstrassCurve K
h₁ : ∃ (r₁ : R), (algebraMap R K : (a : R) → K) r₁ = W.a₁
h₂ : ∃ (r₂ : R), (algebraMap R K : (a : R) → K) r₂ = W.a₂
h₃ : ∃ (r₃ : R), (algebraMap R K : (a : R) → K) r₃ = W.a₃
h₄ : ∃ (r₄ : R), (algebraMap R K : (a : R) → K) r₄ = W.a₄
h₆ : ∃ (r₆ : R), (algebraMap R K : (a : R) → K) r₆ = W.a₆
⊢ W.a₂ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₂
have h : W.a₂ = (algebraMap R K : (a : R) → K) (h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂))
Tactic: simp only [baseChange, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]
-- 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
W : WeierstrassCurve K
h₁ : ∃ (r₁ : R), (algebraMap R K : (a : R) → K) r₁ = W.a₁
h₂ : ∃ (r₂ : R), (algebraMap R K : (a : R) → K) r₂ = W.a₂
h₃ : ∃ (r₃ : R), (algebraMap R K : (a : R) → K) r₃ = W.a₃
h₄ : ∃ (r₄ : R), (algebraMap R K : (a : R) → K) r₄ = W.a₄
h₆ : ∃ (r₆ : R), (algebraMap R K : (a : R) → K) r₆ = W.a₆
⊢ W.a₃ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₃
have h : W.a₃ = (algebraMap R K : (a : R) → K) (h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃))
Tactic: simp only [baseChange, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]
-- 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
W : WeierstrassCurve K
h₁ : ∃ (r₁ : R), (algebraMap R K : (a : R) → K) r₁ = W.a₁
h₂ : ∃ (r₂ : R), (algebraMap R K : (a : R) → K) r₂ = W.a₂
h₃ : ∃ (r₃ : R), (algebraMap R K : (a : R) → K) r₃ = W.a₃
h₄ : ∃ (r₄ : R), (algebraMap R K : (a : R) → K) r₄ = W.a₄
h₆ : ∃ (r₆ : R), (algebraMap R K : (a : R) → K) r₆ = W.a₆
⊢ W.a₄ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₄
have h : W.a₄ = (algebraMap R K : (a : R) → K) (h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄))
Tactic: simp only [baseChange, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]
-- 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
W : WeierstrassCurve K
h₁ : ∃ (r₁ : R), (algebraMap R K : (a : R) → K) r₁ = W.a₁
h₂ : ∃ (r₂ : R), (algebraMap R K : (a : R) → K) r₂ = W.a₂
h₃ : ∃ (r₃ : R), (algebraMap R K : (a : R) → K) r₃ = W.a₃
h₄ : ∃ (r₄ : R), (algebraMap R K : (a : R) → K) r₄ = W.a₄
h₆ : ∃ (r₆ : R), (algebraMap R K : (a : R) → K) r₆ = W.a₆
⊢ W.a₆ =
    ({ a₁ := h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁),
          a₂ := h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂),
          a₃ := h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃),
          a₄ := h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄),
          a₆ := h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆) : WeierstrassCurve R }⁄K).a₆
have h : W.a₆ = (algebraMap R K : (a : R) → K) (h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆))
Tactic: simp only [baseChange, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]
-- 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
W : WeierstrassCurve K
inst_3 : IsIntegral R W
⊢ ∃ (r : R), (algebraMap R K : (a : R) → K) r = W.Δ
have obtain : ∀ (W_int : WeierstrassCurve R) (hW_int : W = W_int⁄K), ∃ (r : R), (algebraMap R K : (a : R) → K) r = W.Δ
Tactic: obtain ⟨W_int, hW_int⟩ : ∃ W_int : WeierstrassCurve R, W = W_int⁄K :=
    IsIntegral.integral
-- 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
W : WeierstrassCurve K
inst_3 : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ ∃ (r : R), (algebraMap R K : (a : R) → K) r = W.Δ
have h : (algebraMap R K : (a : R) → K) W_int.Δ = W.Δ
Tactic: use W_int.Δ
-- 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
W : WeierstrassCurve K
inst_3 : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ (algebraMap R K : (a : R) → K) W_int.Δ = W.Δ
have h : (algebraMap R K : (a : R) → K) W_int.Δ = (W_int⁄K).Δ
Tactic: rw [hW_int, baseChange, map_Δ]
-- 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
W : WeierstrassCurve K
inst_3 : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
h : (algebraMap R K : (a : R) → K) W_int.Δ = (W_int⁄K).Δ
⊢ (algebraMap R K : (a : R) → K) W_int.Δ = W.Δ
have h₁ : (algebraMap R K : (a : R) → K) W_int.Δ = (W_int.map (algebraMap R K)).Δ
Tactic: rw [hW_int, baseChange, map_Δ]
-- 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
W : WeierstrassCurve K
inst_3 : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
h : (algebraMap R K : (a : R) → K) W_int.Δ = (W_int⁄K).Δ
h₁ : (algebraMap R K : (a : R) → K) W_int.Δ = (W_int.map (algebraMap R K)).Δ
⊢ (algebraMap R K : (a : R) → K) W_int.Δ = W.Δ
have h₂ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) W_int.Δ : K) ((algebraMap R K : (a : R) → K) W_int.Δ : K)
Tactic: rw [hW_int, baseChange, map_Δ]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₁
have rw : ((integralModel R W)⁄K).a₁
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₁ = W.a₁
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₁ = ((integralModel R W)⁄K).a₁
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₂
have rw : ((integralModel R W)⁄K).a₂
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₂ = W.a₂
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₂ = ((integralModel R W)⁄K).a₂
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₃
have rw : ((integralModel R W)⁄K).a₃
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₃ = W.a₃
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₃ = ((integralModel R W)⁄K).a₃
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₄
have rw : ((integralModel R W)⁄K).a₄
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₄ = W.a₄
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₄ = ((integralModel R W)⁄K).a₄
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₆
have rw : ((integralModel R W)⁄K).a₆
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₆ = W.a₆
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₆ = ((integralModel R W)⁄K).a₆
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₂
have rw : ((integralModel R W)⁄K).b₂
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₂ = W.b₂
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₂ = ((integralModel R W)⁄K).b₂
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₄
have rw : ((integralModel R W)⁄K).b₄
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₄ = W.b₄
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₄ = ((integralModel R W)⁄K).b₄
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₆
have rw : ((integralModel R W)⁄K).b₆
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₆ = W.b₆
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₆ = ((integralModel R W)⁄K).b₆
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₈
have rw : ((integralModel R W)⁄K).b₈
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₈ = W.b₈
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₈ = ((integralModel R W)⁄K).b₈
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.c₄
have rw : ((integralModel R W)⁄K).c₄
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).c₄ = W.c₄
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).c₄ = ((integralModel R W)⁄K).c₄
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.c₆
have rw : ((integralModel R W)⁄K).c₆
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).c₆ = W.c₆
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).c₆ = ((integralModel R W)⁄K).c₆
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
| W.Δ
have rw : ((integralModel R W)⁄K).Δ
Tactic: rw [← baseChange_integralModel_eq R W]
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).Δ = W.Δ
have conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).Δ = ((integralModel R W)⁄K).Δ
Tactic: conv_rhs => rw [← baseChange_integralModel_eq R W]
-- 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) ⋯
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have hlmax_mem : lmax ∈ l
Tactic: have hlmax_mem : lmax ∈ l :=
    List.maximum_of_length_pos_mem (by simp [l₀, 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
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have hlmax : ∀ 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])
-- 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
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have pos : ∀ (hlmax_le_1 : lmax ≤ 1), ∃ (C : VariableChange K), IsIntegral R (C • W)
Tactic: by_cases hlmax_le_1 : lmax ≤ 1
-- 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
pos : ∀ (hlmax_le_1 : lmax ≤ 1), ∃ (C : VariableChange K), IsIntegral R (C • W)
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have neg : ∀ (hlmax_le_1 : ¬lmax ≤ 1), ∃ (C : VariableChange K), IsIntegral R (C • W)
Tactic: by_cases hlmax_le_1 : lmax ≤ 1
-- 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
⊢ ∃ (C : VariableChange K), IsIntegral R (C • W)
have h : IsIntegral R (HSMul.hSMul (α := VariableChange K) { u := 1, r := 0, s := 0, t := 0 : VariableChange K } W)
Tactic: use ⟨1, 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
⊢ 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 (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₁
⊢ 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 (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₂
⊢ 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 (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₃
⊢ 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