awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
P : W.Point
⊢ -P + P = 0
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (-P + P) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) 0 : W.toAffine.Point)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
P : W.Point
⊢ -P + P = 0
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (-P + P) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) 0 : W.toAffine.Point)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x x_1 : W.Point
⊢ «x» + x_1 = x_1 + «x»
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (x_1 + «x») : W.toAffine.Point)
Tactic: apply (toAffineAddEquiv W).injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
x x_1 : W.Point
⊢ «x» + x_1 = x_1 + «x»
have a : Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1) : W.toAffine.Point)
  ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (x_1 + «x») : W.toAffine.Point)
Tactic: classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).neg ((⇑f : (a : R) → S) ∘ P) = (⇑f : (a : R) → S) ∘ W'.neg P
have simp : Eq.{s + 1} (α := Fin 3 → S)
  (![((⇑f : (a : R) → S) ∘ P) x, (f : (a : R) → S) (W'.negY P), ((⇑f : (a : R) → S) ∘ P) z] : Fin (Nat.succ 2) → S)
  (![(f : (a : R) → S) (P x), (f : (a : R) → S) (W'.negY P), (f : (a : R) → S) (P z)] : Fin (Nat.succ 0).succ.succ → S)
Tactic: simp only [neg, map_negY, comp_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have pos : ∀ (h : P ≈ Q), (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
Tactic: by_cases h : P ≈ Q
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
pos : ∀ (h : P ≈ Q), (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have neg : ∀ (h : ¬P ≈ Q), (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
Tactic: by_cases h : P ≈ Q
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have pos : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.add P Q
Tactic: rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
pos : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.add P Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have pos₁ : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.dblXYZ P
Tactic: rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
pos : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.add P Q
pos₁ : (W.map f).dblXYZ ((⇑f : (a : F) → K) ∘ P) = (⇑f : (a : F) → K) ∘ W.dblXYZ P
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have pos₂ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.dblXYZ P) ((⇑f : (a : F) → K) ∘ W.dblXYZ P)
Tactic: rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have neg : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
Tactic: rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
neg : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have neg₁ : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.addXYZ P Q
Tactic: rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
neg : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
neg₁ : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.addXYZ P Q
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
have neg₂ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.addXYZ P Q) ((⇑f : (a : F) → K) ∘ W.addXYZ P Q)
Tactic: rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).neg P
have rw : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).neg P
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_neg, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).neg P
⊢ (W'⁄B).neg ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).neg P
have rw₁ : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((W'⁄A).map (↑f : A →+* B)).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_neg, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).neg P
rw₁ :
  (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).neg ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).neg P
have rw₂ : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_neg, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R F
inst_6 : Algebra S F
inst_7 : IsScalarTower R S F
inst_8 : Algebra R K
inst_9 : Algebra S K
inst_10 : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q
have rw : (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
  (⇑(↑f : F →+* K) : (a : F) → K) ∘ (W'⁄F).add P Q
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_add _ hP hQ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R F
inst_6 : Algebra S F
inst_7 : IsScalarTower R S F
inst_8 : Algebra R K
inst_9 : Algebra S K
inst_10 : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
rw :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    (⇑(↑f : F →+* K) : (a : F) → K) ∘ (W'⁄F).add P Q
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q
have rw₁ : (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
  ((W'⁄F).map (↑f : F →+* K)).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_add _ hP hQ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R F
inst_6 : Algebra S F
inst_7 : IsScalarTower R S F
inst_8 : Algebra R K
inst_9 : Algebra S K
inst_10 : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
rw :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    (⇑(↑f : F →+* K) : (a : F) → K) ∘ (W'⁄F).add P Q
rw₁ :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    ((W'⁄F).map (↑f : F →+* K)).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q
have rw₂ : (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
Tactic: rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_add _ hP hQ, map_baseChange]
-- 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₆
⊢ IsIntegral R W
have h : W =
  { 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
Tactic: use ⟨h₁.choose, h₂.choose, h₃.choose, h₄.choose, h₆.choose⟩
-- 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₁ := 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
have h : 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: ext
-- 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₆
h :
  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₁
⊢ W =
    { 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
have h₅ : 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: ext
-- 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₆
h :
  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₁
h₅ :
  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₂
⊢ W =
    { 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
have h₇ : 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: ext
-- 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₆
h :
  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₁
h₅ :
  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₂
h₇ :
  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₃
⊢ W =
    { 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
have h₈ : 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: ext
-- 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₆]