awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : ¬P z = 0
⊢ (fromAffine (Affine.Point.some (P x / P z) (P y / P z) ⋯)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz

Premises used: Iff.mpr, WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero, Setoid.symm, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : ¬P z = 0
⊢ (fromAffine (Affine.Point.some (P x / P z) (P y / P z) ⋯)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
exact Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz

Premises used: Iff.mpr, WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero, Setoid.symm, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
inst_6 : DecidableEq F
zero : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine 0)) 0
zero₁ : Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift 0) 0
zero₂ zero₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift (fromAffine Affine.Point.zero)) Affine.Point.zero

Tactic:
rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffineLift_zero, WeierstrassCurve.Affine.Point.zero_def, WeierstrassCurve.Projective.Point.fromAffine_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
inst_6 : DecidableEq F
x y : F
h : W.toAffine.Nonsingular «x» «y»
some : { point := ⟦![«x», «y», 1]⟧, nonsingular := ⋯ : W.Point }.toAffineLift = Affine.Point.some «x» «y» h
some₁ some₂ : Affine.Point.some «x» «y» ⋯ = Affine.Point.some «x» «y» h
⊢ (fromAffine (Affine.Point.some «x» «y» h)).toAffineLift = Affine.Point.some «x» «y» h

Tactic:
rw [fromAffine_some, toAffineLift_some]

Premises used: WeierstrassCurve.Projective.Point.toAffineLift_some, WeierstrassCurve.Projective.Point.fromAffine_some
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 x_2 : W.Point
a :
  Eq (α := W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 x_2 : W.Point
⊢ Eq (α := W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)

Tactic:
simp only [map_add, add_assoc]

Premises used: add_assoc, map_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 x_2 : W.Point
a :
  Eq (α := W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + x_1 + x_2) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + (x_1 + x_2)) : W.toAffine.Point)
⊢ «x» + x_1 + x_2 = «x» + (x_1 + x_2)

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_assoc]

Premises used: add_assoc, map_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ 0 + «x» = «x»

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 : W.Point
⊢ Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)

Tactic:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, WeierstrassCurve.Projective.Point.toAffineLift_zero, map_add, zero_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) (0 + «x») : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ 0 + «x» = «x»

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, WeierstrassCurve.Projective.Point.toAffineLift_zero, map_add, zero_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ «x» + 0 = «x»

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 : W.Point
⊢ Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)

Tactic:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, WeierstrassCurve.Projective.Point.toAffineLift_zero, map_add, add_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 : W.Point
a :
  Eq (α := W.toAffine.Point) ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) («x» + 0) : W.toAffine.Point)
    ((toAffineAddEquiv W : (a : W.Point) → W.toAffine.Point) «x» : W.toAffine.Point)
⊢ «x» + 0 = «x»

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, WeierstrassCurve.Projective.Point.toAffineLift_zero, map_add, add_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
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)
⊢ -P + P = 0

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
⊢ 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:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, WeierstrassCurve.Projective.Point.toAffineLift_neg, WeierstrassCurve.Projective.Point.toAffineLift_zero, map_add, neg_add_cancel
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
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)
⊢ -P + P = 0

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, WeierstrassCurve.Projective.Point.toAffineLift_neg, WeierstrassCurve.Projective.Point.toAffineLift_zero, map_add, neg_add_cancel
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
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)
⊢ «x» + x_1 = x_1 + «x»

Tactic:
apply (toAffineAddEquiv W).injective

Premises used: WeierstrassCurve.Projective.Point.toAffineAddEquiv, AddEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
⊢ 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:
simp only [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
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)
⊢ «x» + x_1 = x_1 + «x»

Tactic:
classical
    apply (toAffineAddEquiv W).injective
    simp only [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
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)
⊢ (W'.map f).neg ((⇑f : (a : R) → S) ∘ P) = (⇑f : (a : R) → S) ∘ W'.neg P

Tactic:
simp only [neg, map_negY, comp_fin3]

Premises used: WeierstrassCurve.Projective.neg, WeierstrassCurve.Projective.comp_fin3, WeierstrassCurve.Projective.map_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ 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:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
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
⊢ (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
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
pos₂ pos₃ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.dblXYZ 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

Tactic:
rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]

Premises used: Iff.mpr, WeierstrassCurve.Projective.comp_equiv_comp, WeierstrassCurve.Projective.add_of_equiv, WeierstrassCurve.Projective.map_dblXYZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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
neg₂ neg₃ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.addXYZ P 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

Tactic:
rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]

Premises used: WeierstrassCurve.Projective.comp_equiv_comp, Function.comp, WeierstrassCurve.Projective.map_addXYZ, Iff.mp, WeierstrassCurve.Projective.add_of_not_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
rw₂ rw₃ : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄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

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_neg, map_baseChange]

Premises used: WeierstrassCurve.Projective.map_neg, RingHom.coe_coe, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
rw₂ 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)
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_add _ hP hQ, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_add, WeierstrassCurve.Projective.map_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
⊢ (integralModel R W)⁄K = W

Tactic:
hW.integral.choose_spec.symm

Premises used: Exists.choose_spec, WeierstrassCurve.integralModel, WeierstrassCurve.IsIntegral.integral, 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₆
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
⊢ IsIntegral R W

Tactic:
use ⟨h₁.choose, h₂.choose, h₃.choose, h₄.choose, h₆.choose⟩
-- 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₁