mathlib-initiative/mathlib-tactics huggingface dataset:
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) *
      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:
normEDS,

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 - 1) then b else 1) ^ 2 *
        (preNormEDS (b ^ 4) c d (k + 2) * if Even (k + 2) then b else 1) -
      (preNormEDS (b ^ 4) c d (k - 2) * if Even (k - 2) then b else 1) *
        (preNormEDS (b ^ 4) c d (k + 1) * if Even (k + 1) then b else 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
normEDS,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ 2 * (m + 1) = 2 * m + 2

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ 2 * (m + 1) + 1 = 2 * m + 3

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: 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 : ℕ
⊢ 2 * -(↑m + 1) + 1 = -(2 * ↑m + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 3), f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ f (preNormEDS' b c d (2 * (m✝ + 3))) = preNormEDS' (f b) (f c) (f d) (2 * (m✝ + 3))

Tactic:
| _ _ ih =>

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
m✝ : ℕ
ih : ∀ k < 2 * (m✝ + 2) + 1, f (preNormEDS' b c d k) = preNormEDS' (f b) (f c) (f d) k
⊢ f (preNormEDS' b c d (2 * (m✝ + 2) + 1)) = preNormEDS' (f b) (f c) (f d) (2 * (m✝ + 2) + 1)

Tactic:
| _ _ ih =>

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case even
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1), f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ f (complEDS' b c d k (2 * (m✝ + 1))) = complEDS' (f b) (f c) (f d) k (2 * (m✝ + 1))

Tactic:
| _ _ ih =>

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1) + 1, f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ f (complEDS' b c d k (2 * (m✝ + 1) + 1)) = complEDS' (f b) (f c) (f d) k (2 * (m✝ + 1) + 1)

Tactic:
| _ _ ih =>

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
⊢ (j : 𝒰.I₀) → 𝒰.X j ⟶ Spec ((fun k ↦ Γ(D.obj i, V k)) j)

pp: case refine_3
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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
⊢ ∀ (j : 𝒰.I₀), IsPullback (?refine_2 j) (𝒰.f j) ((fun k ↦ ⋯.isoSpec.inv ≫ (V k).ι) j) (c.π.app i)

Tactic:
· intro k
    exact IsOpenImmersion.lift (V k).ι (𝒰.f _ ≫ c.π.app i) (by simp [hV'', Set.range_comp]) ≫
      (hV' k).left.isoSpec.hom

Goal state after:
case refine_3
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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
⊢ ∀ (j : 𝒰.I₀),
    IsPullback ((fun k ↦ IsOpenImmersion.lift (V k).ι (𝒰.f k ≫ c.π.app i) ⋯ ≫ ⋯.isoSpec.hom) j) (𝒰.f j)
      ((fun k ↦ ⋯.isoSpec.inv ≫ (V k).ι) j) (c.π.app i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: 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✝⟩

Tactic:
rfl

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

Goal state before:
pp: 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✝⟩

Tactic:
rfl

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

Goal state before:
pp: 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

Tactic:
rfl

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

Goal state before:
pp: 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✝

Tactic:
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
⊢ W'.nonsingularPointEquiv (Point.some x y h) = some ⟨(x, y), h⟩

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝² : CommRing R
W' : Affine R
inst✝¹ : Nontrivial R
inst✝ : WeierstrassCurve.IsElliptic W'
x y : R
h : W'.Equation x y
⊢ W'.pointEquiv (Point.mk h) = some ⟨(x, y), h⟩

Tactic:
rfl

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

Goal state before:
pp: 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

Tactic:
rfl

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

Goal state before:
pp: 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

Tactic:
rfl

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

Goal state before:
pp: 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✝

Tactic:
rfl

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

Goal state before:
pp: 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

Tactic:
rfl

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

Goal state before:
pp: 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✝

Tactic:
rfl

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

Goal state before:
pp: case zero.zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
⊢ zero + zero = 0 ↔ zero = -zero

Tactic:
rfl

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

Goal state before:
pp: case zero.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ zero + some x₂ y₂ h✝ = 0 ↔ zero = -some x₂ y₂ h✝

Tactic:
rfl

Goal state after:
case zero.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ zero + some x₂ y₂ h✝ = 0 ↔ zero = -some x₂ y₂ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝ : W.Nonsingular x₁ y₁
⊢ some x₁ y₁ h✝ + zero = 0 ↔ some x₁ y₁ h✝ = -zero

Tactic:
rfl

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

Goal state before:
pp: case some.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0 ↔ some x₁ y₁ h✝¹ = -some x₂ y₂ h✝

Tactic:
rfl

Goal state after:
case some.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0 ↔ some x₁ y₁ h✝¹ = -some x₂ y₂ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case mp.zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
hP : toClass zero = 0
⊢ zero = 0

Tactic:
rfl

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some x✝ y✝ ⋯) = 0
⊢ ↑(CoordinateRing.XYIdeal' ⋯) = ↑?m.48

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 2 = ↑1 + 1

Tactic:
rfl

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

Goal state before:
pp: case zero.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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
⊢ (match zero + zero with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match zero with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match zero with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

Tactic:
rfl

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

Goal state before:
pp: case zero.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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
⊢ (match zero + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match zero with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

Tactic:
rfl

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

Goal state before:
pp: case some.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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
⊢ (match some x₁ y₁ h₁ + zero with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match zero with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

Tactic:
rfl

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

Goal state before:
pp: case some.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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

Tactic:
rfl

Goal state after:
case some.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
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 3 = ↑2 + 1

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 = ↑3 + 1

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 3 + 2 = 2 * 2 + 1

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (normEDS W.ψ₂ (C W.Ψ₃) (C W.preΨ₄) n) = (mk W) (W.Ψ n)

Tactic:
normEDS,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (preNormEDS (W.ψ₂ ^ 4) (C W.Ψ₃) (C W.preΨ₄) n * if Even n then W.ψ₂ else 1) = (mk W) (W.Ψ n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
F : Type u
inst✝³ : CommRing R
inst✝² : Field F
W' : Affine R
inst✝¹ : DecidableEq F
inst✝ : Algebra R F
⊢ (map (Algebra.ofId F F)) zero = zero

Tactic:
rfl

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

Goal state before:
pp: case some
R : Type r
F : Type u
inst✝³ : CommRing R
inst✝² : Field F
W' : Affine R
inst✝¹ : DecidableEq F
inst✝ : Algebra R F
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
⊢ (map (Algebra.ofId F F)) (some x✝ y✝ h✝) = some x✝ y✝ h✝

Tactic:
rfl

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

Goal state before:
pp: case zero
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
⊢ (map g) ((map f) zero) = (map (g.comp f)) zero

Tactic:
rfl

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

Goal state before:
pp: case some
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
⊢ (map g) ((map f) (some x✝ y✝ h✝)) = (map (g.comp f)) (some x✝ y✝ h✝)

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 + 1 = 2 * 2 + 1

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 2 - 1 = 1

Tactic:
rfl

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

Goal state before:
pp: case zero.zero
R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field F
inst✝⁹ : Field K
W' : Affine R
inst✝⁸ : DecidableEq F
inst✝⁷ : DecidableEq K
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
h : (map f) zero = (map f) zero
⊢ zero = zero

Tactic:
rfl

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 - 1 = 3

Tactic:
rfl

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).Φ n = Polynomial.map f (W.Φ n)

Tactic:
rw [← coe_mapRingHom]
  simp [Φ, map_sub, apply_ite <| mapRingHom f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
a₁_of_isCharTwoJNeZeroNF,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 1 * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 = W.a₆ + 4 * W.a₂ * W.a₆