Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: case a₁
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₁ = x✝.a₁

pp: case a₂
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₂ = x✝.a₂

pp: case a₃
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₃ = x✝.a₃

pp: case a₄
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₄ = x✝.a₄

pp: case a₆
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₆ = x✝.a₆

Tactic:
<;>

Goal state after:
case a₁
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₁ = x✝.a₁

case a₂
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₂ = x✝.a₂

case a₃
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₃ = x✝.a₃

case a₄
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₄ = x✝.a₄

case a₆
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
x✝¹ x✝ : WeierstrassCurve R
h : (fun W ↦ W.map f) x✝¹ = (fun W ↦ W.map f) x✝
left✝³ : f x✝¹.a₁ = f x✝.a₁
left✝² : f x✝¹.a₂ = f x✝.a₂
left✝¹ : f x✝¹.a₃ = f x✝.a₃
left✝ : f x✝¹.a₄ = f x✝.a₄
right✝ : f x✝¹.a₆ = f x✝.a₆
⊢ x✝¹.a₆ = x✝.a₆