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
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₆
h : W.a₃ = (algebraMap R K : (a : R) → K) (h₃.choose (p := fun (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₃

Tactic:
simp only [baseChange, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]

Premises used: WeierstrassCurve.map_a₂, WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆, WeierstrassCurve.baseChange, WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₁
-- 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
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₆
h : W.a₄ = (algebraMap R K : (a : R) → K) (h₄.choose (p := fun (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₄

Tactic:
simp only [baseChange, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]

Premises used: WeierstrassCurve.map_a₂, WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆, WeierstrassCurve.baseChange, WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₁
-- 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
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₆
h : W.a₆ = (algebraMap R K : (a : R) → K) (h₆.choose (p := fun (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₆

Tactic:
simp only [baseChange, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]

Premises used: WeierstrassCurve.map_a₂, WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆, WeierstrassCurve.baseChange, WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₁
-- 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
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₁ = (algebraMap R K : (a : R) → K) (h₁.choose (p := fun (r₁ : R) ↦ (algebraMap R K : (a : R) → K) r₁ = W.a₁))

Tactic:
apply h₁.choose_spec.symm

Premises used: Exists.choose_spec, Eq.symm
-- 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
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₂ = (algebraMap R K : (a : R) → K) (h₂.choose (p := fun (r₂ : R) ↦ (algebraMap R K : (a : R) → K) r₂ = W.a₂))

Tactic:
apply h₂.choose_spec.symm

Premises used: Exists.choose_spec, Eq.symm
-- 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
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₃ = (algebraMap R K : (a : R) → K) (h₃.choose (p := fun (r₃ : R) ↦ (algebraMap R K : (a : R) → K) r₃ = W.a₃))

Tactic:
apply h₃.choose_spec.symm

Premises used: Exists.choose_spec, Eq.symm
-- 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
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₄ = (algebraMap R K : (a : R) → K) (h₄.choose (p := fun (r₄ : R) ↦ (algebraMap R K : (a : R) → K) r₄ = W.a₄))

Tactic:
apply h₄.choose_spec.symm

Premises used: Exists.choose_spec, Eq.symm
-- 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
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₆ = (algebraMap R K : (a : R) → K) (h₆.choose (p := fun (r₆ : R) ↦ (algebraMap R K : (a : R) → K) r₆ = W.a₆))

Tactic:
apply h₆.choose_spec.symm

Premises used: Exists.choose_spec, Eq.symm
-- 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
W : WeierstrassCurve K
inst_3 : IsIntegral R W
⊢ ∃ (W_int : WeierstrassCurve R), W = W_int⁄K

Tactic:
IsIntegral.integral

Premises used: WeierstrassCurve.IsIntegral.integral
-- 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
W : WeierstrassCurve K
inst_3 : IsIntegral R W
obtain : ∀ (W_int : WeierstrassCurve R) (hW_int : W = W_int⁄K), ∃ (r : R), (algebraMap R K : (a : R) → K) r = W.Δ
⊢ ∃ (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

Premises used: WeierstrassCurve, WeierstrassCurve.IsIntegral.integral
-- 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
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.Δ
⊢ ∃ (r : R), (algebraMap R K : (a : R) → K) r = W.Δ

Tactic:
use W_int.Δ

Premises used: WeierstrassCurve.Δ
-- 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
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)).Δ
h₂ h₃ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) W_int.Δ : K) ((algebraMap R K : (a : R) → K) W_int.Δ : K)
⊢ (algebraMap R K : (a : R) → K) W_int.Δ = W.Δ

Tactic:
rw [hW_int, baseChange, map_Δ]

Premises used: WeierstrassCurve.baseChange, WeierstrassCurve.map_Δ
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).a₁
| W.a₁

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₁ = ((integralModel R W)⁄K).a₁
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₁ = W.a₁

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₁ = ((integralModel R W)⁄K).a₁

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).a₂
| W.a₂

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₂ = ((integralModel R W)⁄K).a₂
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₂ = W.a₂

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₂ = ((integralModel R W)⁄K).a₂

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).a₃
| W.a₃

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₃ = ((integralModel R W)⁄K).a₃
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₃ = W.a₃

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₃ = ((integralModel R W)⁄K).a₃

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).a₄
| W.a₄

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₄ = ((integralModel R W)⁄K).a₄
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₄ = W.a₄

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₄ = ((integralModel R W)⁄K).a₄

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).a₆
| W.a₆

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).a₆ = ((integralModel R W)⁄K).a₆
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₆ = W.a₆

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).a₆ = ((integralModel R W)⁄K).a₆

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).b₂
| W.b₂

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₂ = ((integralModel R W)⁄K).b₂
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₂ = W.b₂

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₂ = ((integralModel R W)⁄K).b₂

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).b₄
| W.b₄

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₄ = ((integralModel R W)⁄K).b₄
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₄ = W.b₄

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₄ = ((integralModel R W)⁄K).b₄

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).b₆
| W.b₆

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₆ = ((integralModel R W)⁄K).b₆
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₆ = W.b₆

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₆ = ((integralModel R W)⁄K).b₆

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).b₈
| W.b₈

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).b₈ = ((integralModel R W)⁄K).b₈
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₈ = W.b₈

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).b₈ = ((integralModel R W)⁄K).b₈

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).c₄
| W.c₄

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).c₄ = ((integralModel R W)⁄K).c₄
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).c₄ = W.c₄

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).c₄ = ((integralModel R W)⁄K).c₄

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).c₆
| W.c₆

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).c₆ = ((integralModel R W)⁄K).c₆
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).c₆ = W.c₆

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).c₆ = ((integralModel R W)⁄K).c₆

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
rw : ((integralModel R W)⁄K).Δ
| W.Δ

Tactic:
rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
conv_rhs : (algebraMap R K : (a : R) → K) (integralModel R W).Δ = ((integralModel R W)⁄K).Δ
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).Δ = W.Δ

Tactic:
conv_rhs => rw [← baseChange_integralModel_eq R W]

Premises used: WeierstrassCurve.baseChange_integralModel_eq
-- 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
W : WeierstrassCurve K
hW : IsIntegral R W
⊢ (algebraMap R K : (a : R) → K) (integralModel R W).Δ = ((integralModel R W)⁄K).Δ

Tactic:
simp [baseChange]

Premises used: WeierstrassCurve.baseChange
-- 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₀
⊢ 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) ⋯
⊢ 0 < l.length

Tactic:
simp [l₀, l]