mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r) =
    (D.obj l).basicOpen
      ((ConcreteCategory.hom ((D.obj l).presheaf.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r))

Tactic:
Scheme.basicOpen_res,

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r) =
    D.map (flk ≫ fki) ⁻¹ᵁ U ⊓ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -↑m + 1) =
    (preNormEDS b c d (-↑m + 2) * preNormEDS b c d (-↑m) ^ 3 * if Even (-↑m) then b else 1) -
      preNormEDS b c d (-↑m - 1) * preNormEDS b c d (-↑m + 1) ^ 3 * if Even (-↑m) then 1 else b

Tactic:
rcases m with _ | m

Goal state after:
case neg.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
⊢ preNormEDS b c d (2 * -↑0 + 1) =
    (preNormEDS b c d (-↑0 + 2) * preNormEDS b c d (-↑0) ^ 3 * if Even (-↑0) then b else 1) -
      preNormEDS b c d (-↑0 - 1) * preNormEDS b c d (-↑0 + 1) ^ 3 * if Even (-↑0) then 1 else b

case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -↑(m + 1) + 1) =
    (preNormEDS b c d (-↑(m + 1) + 2) * preNormEDS b c d (-↑(m + 1)) ^ 3 * if Even (-↑(m + 1)) then b else 1) -
      preNormEDS b c d (-↑(m + 1) - 1) * preNormEDS b c d (-↑(m + 1) + 1) ^ 3 * if Even (-↑(m + 1)) then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (-(2 * ↑m + 1)) =
    (preNormEDS b c d (-(↑m - 1)) * preNormEDS b c d (-(↑m + 1)) ^ 3 * if Even (-(↑m + 1)) then b else 1) -
      preNormEDS b c d (-(↑m + 2)) * preNormEDS b c d (-↑m) ^ 3 * if Even (-(↑m + 1)) then 1 else b

Tactic:
preNormEDS_neg,

Goal state after:
case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ -preNormEDS b c d (2 * ↑m + 1) =
    (-preNormEDS b c d (↑m - 1) * (-preNormEDS b c d (↑m + 1)) ^ 3 * if Even (-(↑m + 1)) then b else 1) -
      -preNormEDS b c d (↑m + 2) * (-preNormEDS b c d ↑m) ^ 3 * if Even (-(↑m + 1)) then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ ((preNormEDS (b ^ 4) c d (-(k - -1)) ^ 2 * preNormEDS (b ^ 4) c d (-(k - 2)) -
        preNormEDS (b ^ 4) c d (-(k - -2)) * preNormEDS (b ^ 4) c d (-(k - 1)) ^ 2) *
      if Even (-k) then 1 else b) =
    (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k - -2) -
        preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k - -1) ^ 2) *
      if Even k then 1 else b

Tactic:
preNormEDS_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ (((-preNormEDS (b ^ 4) c d (k - -1)) ^ 2 * -preNormEDS (b ^ 4) c d (k - 2) -
        -preNormEDS (b ^ 4) c d (k - -2) * (-preNormEDS (b ^ 4) c d (k - 1)) ^ 2) *
      if Even (-k) then 1 else b) =
    (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k - -2) -
        preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k - -1) ^ 2) *
      if Even k then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ (preNormEDS (b ^ 4) c d (-n) * if Even (-n) then b else 1) = -(preNormEDS (b ^ 4) c d n * if Even n then b else 1)

Tactic:
preNormEDS_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ (-preNormEDS (b ^ 4) c d n * if Even (-n) then b else 1) = -(preNormEDS (b ^ 4) c d n * if Even n then b else 1)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ complEDS₂ b c d k * b =
    normEDS b c d (k - 1) ^ 2 * normEDS b c d (k + 2) - normEDS b c d (k - 2) * normEDS b c d (k + 1) ^ 2

Tactic:
simp_rw [complEDS₂, normEDS, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one,
    iff_false]

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ ((preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        if Even k then 1 else b) *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * if ¬Even k then b else 1) ^ 2 *
        (preNormEDS (b ^ 4) c d (k + 2) * if Even k then b else 1) -
      (preNormEDS (b ^ 4) c d (k - 2) * if Even k then b else 1) *
        (preNormEDS (b ^ 4) c d (k + 1) * if ¬Even k then b else 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ complEDS b c d k (2 * -↑m + 1) =
    complEDS b c d k (-↑m) ^ 2 * normEDS b c d ((-↑m + 1) * k + 1) * normEDS b c d ((-↑m + 1) * k - 1) -
      complEDS b c d k (-↑m + 1) ^ 2 * normEDS b c d (-↑m * k + 1) * normEDS b c d (-↑m * k - 1)

Tactic:
rcases m with _ | m

Goal state after:
case neg.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
⊢ complEDS b c d k (2 * -↑0 + 1) =
    complEDS b c d k (-↑0) ^ 2 * normEDS b c d ((-↑0 + 1) * k + 1) * normEDS b c d ((-↑0 + 1) * k - 1) -
      complEDS b c d k (-↑0 + 1) ^ 2 * normEDS b c d (-↑0 * k + 1) * normEDS b c d (-↑0 * k - 1)

case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ complEDS b c d k (2 * -↑(m + 1) + 1) =
    complEDS b c d k (-↑(m + 1)) ^ 2 * normEDS b c d ((-↑(m + 1) + 1) * k + 1) *
        normEDS b c d ((-↑(m + 1) + 1) * k - 1) -
      complEDS b c d k (-↑(m + 1) + 1) ^ 2 * normEDS b c d (-↑(m + 1) * k + 1) * normEDS b c d (-↑(m + 1) * k - 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case none.bot
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • none) (2 • ⊥ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case none.coe
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ max (2 • none) (2 • ↑a✝ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.zero.bot
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some 0) (2 • ⊥ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.zero.coe
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ max (2 • some 0) (2 • ↑a✝ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.succ.zero.bot
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • some (0 + 1)) (2 • ⊥ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.succ.zero.coe
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
a✝ : ℕ
⊢ max (2 • some (0 + 1)) (2 • ↑a✝ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * C W.Ψ₂Sq ^ 2 - C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) * 1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)

Tactic:
rw [C_Ψ₂Sq]

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) *
      1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.succ.succ.bot
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ : ℕ
⊢ max (2 • some (n✝ + 1 + 1)) (2 • ⊥ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.succ.succ.coe
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
n✝ a✝ : ℕ
⊢ max (2 • some (n✝ + 1 + 1)) (2 • ↑a✝ + 3) ≠ 1

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ Function.LeftInverse (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) fun x ↦
    match x with
    | ⟨Point.zero, property⟩ => none
    | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩

Tactic:
rintro (_ | _)

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 property✝ : p Point.zero
⊢ (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
        ⟨Point.zero, property✝⟩) =
    ⟨Point.zero, property✝⟩

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
property✝ : p (Point.some x✝ y✝ h✝)
⊢ (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨Point.zero, property⟩ => none
          | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
        ⟨Point.some x✝ y✝ h✝, property✝⟩) =
    ⟨Point.some x✝ y✝ h✝, property✝⟩
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 - C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * C W.Ψ₂Sq ^ 2) * 1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)

Tactic:
rw [C_Ψ₂Sq]

Goal state after:
case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2) *
      1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ Function.LeftInverse (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) fun x ↦
    match x with
    | ⟨Point.zero, property⟩ => none
    | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩

Tactic:
rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ Function.RightInverse (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) fun x ↦
    match x with
    | ⟨Point.zero, property⟩ => none
    | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩

Tactic:
rintro (_ | _)

Goal state after:
case none
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ (fun x ↦
        match x with
        | ⟨Point.zero, property⟩ => none
        | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
      ((fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) none) =
    none

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
val✝ : { xy // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }
⊢ (fun x ↦
        match x with
        | ⟨Point.zero, property⟩ => none
        | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩)
      ((fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) (some val✝)) =
    some val✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
p : W'.Point → Prop
p0 : p Point.zero
⊢ Function.RightInverse (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) fun x ↦
    match x with
    | ⟨Point.zero, property⟩ => none
    | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩

Tactic:
rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
⊢ some x y h ≠ 0

Tactic:
rintro (_ | _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
⊢ ∀ (x : W'.Point), - -x = x

Tactic:
rintro (_ | _)

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
⊢ - -zero = zero

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Field L
W' : Affine R
W : Affine F
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ - -some x✝ y✝ h✝ = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ ∀ (a : W.Point), 0 + a = a

Tactic:
rintro (_ | _)

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ 0 + zero = zero

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝ y✝ : F
h✝ : W.Nonsingular x✝ y✝
⊢ 0 + some x✝ y✝ h✝ = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ ∀ (a : W.Point), 0 + a = a

Tactic:
rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ ∀ (a : W.Point), a + 0 = a

Tactic:
rintro (_ | _)

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ zero + 0 = zero

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝ y✝ : F
h✝ : W.Nonsingular x✝ y✝
⊢ some x✝ y✝ h✝ + 0 = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ ∀ (a : W.Point), a + 0 = a

Tactic:
rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : IsAffine S
inst✝¹ : IsAffine X
inst✝ : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
this :
  ∀ {S : Scheme} (t : D ⟶ (Functor.const I).obj S) (f : X ⟶ S) [LocallyOfFinitePresentation f] [IsAffine S],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ R, S = Spec R) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hS : ¬∃ R, S = Spec R
i : I
g : D.obj i ⟶ X
hg : c.π.app i ≫ g = a
hg' : g ≫ f ≫ S.isoSpec.hom = (t ≫ ((Functor.const I).mapIso S.isoSpec).hom).app i
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
exact ⟨i, g, hg, by simpa using! congr($hg' ≫ S.isoSpec.inv)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ toClass (-zero) + toClass zero = 0

Tactic:
exact zero_add 0

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝ : W.Point
⊢ -x✝ + x✝ = 0

Tactic:
by rw [add_eq_zero]

Goal state after: