mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
m : ℤ
⊢ W (m + 1 + (m - 1) + 0) * W (m + 1 - (m - 1)) * W (1 + 0) * W 1 -
        W (m + 1 + 1 + 0) * W (m + 1 - 1) * W (m - 1 + 0) * W (m - 1) +
      W (m - 1 + 1 + 0) * W (m - 1 - 1) * W (m + 1 + 0) * W (m + 1) =
    W (2 * m) * W 2 * W 1 ^ 2 - W (m - 1) ^ 2 * W m * W (m + 2) + W (m - 2) * W m * W (m + 1) ^ 2

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
m : ℤ
⊢ W (m + 1 + (m - 1) + 0) * W (m + 1 - (m - 1)) * W (1 + 0) * W 1 -
        W (m + 1 + 1 + 0) * W (m + 1 - 1) * W (m - 1 + 0) * W (m - 1) +
      W (m - 1 + 1 + 0) * W (m - 1 - 1) * W (m + 1 + 0) * W (m + 1) =
    W (2 * m) * W 2 * W 1 ^ 2 - W (m - 1) ^ 2 * W m * W (m + 2) + W (m - 2) * W m * W (m + 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
m : ℤ
⊢ W (m + 1 + m + 0) * W (m + 1 - m) * W (1 + 0) * W 1 - W (m + 1 + 1 + 0) * W (m + 1 - 1) * W (m + 0) * W m +
      W (m + 1 + 0) * W (m - 1) * W (m + 1 + 0) * W (m + 1) =
    W (2 * m + 1) * W 1 ^ 3 - W (m + 2) * W m ^ 3 + W (m - 1) * W (m + 1) ^ 3

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
m : ℤ
⊢ W (m + 1 + m + 0) * W (m + 1 - m) * W (1 + 0) * W 1 - W (m + 1 + 1 + 0) * W (m + 1 - 1) * W (m + 0) * W m +
      W (m + 1 + 0) * W (m - 1) * W (m + 1 + 0) * W (m + 1) =
    W (2 * m + 1) * W 1 ^ 3 - W (m + 2) * W m ^ 3 + W (m - 1) * W (m + 1) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0

Tactic:
]

Goal state after:
case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : ℤ
⊢ rel id x✝³ x✝² x✝¹ x✝ = 0

Tactic:
by simp_rw [rel, id_eq]; ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ c = c

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ d = d

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (have this := ⋯;
    preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
      preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 4) ^ 2) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (have this := ⋯;
    preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
      preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 4) ^ 2) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
]

Goal state after:
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
⊢ (((Functor.const I).obj c.pt).obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r) ≤ c.π.app i ⁻¹ᵁ U

Tactic:
]

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
⊢ (((Functor.const I).obj c.pt).obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r) ≤ c.π.app i ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ C (C (x₁ - x₂)) * (0 * (Y - W.negPolynomial)) =
    C (C (x₁ - x₂)) * (1 + C (C (x₁ - x₂)⁻¹) * C (X - C x₁) + C (C ((x₁ - x₂)⁻¹ * -1)) * C (X - C x₂))

Tactic:
]

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ C (C (x₁ - x₂)) * (0 * (Y - W.negPolynomial)) =
    C (C (x₁ - x₂)) * (1 + C (C (x₁ - x₂)⁻¹) * C (X - C x₁) + C (C ((x₁ - x₂)⁻¹ * -1)) * C (X - C x₂))
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.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U

Tactic:
]

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.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
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 *
      ((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 * preNormEDS (b ^ 4) c d (k + 2) -
        preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d k * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
      if Even k then 1 else b

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ preNormEDS (b ^ 4) c d 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 * preNormEDS (b ^ 4) c d (k + 2) -
        preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d k * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
      if Even k then 1 else b
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 y : F
h : W.Nonsingular x y
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯ * XYIdeal' h) = 1

Tactic:
]

Goal state after:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯ * XYIdeal' h) = 1
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)
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
⊢ x ∈ (((Functor.const I).obj c.pt).obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)

Tactic:
]

Goal state after:
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)
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
⊢ x ∈ (((Functor.const I).obj c.pt).obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' h₁ * XYIdeal' h₂) = (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯)

Tactic:
]

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField) (XYIdeal' h₁ * XYIdeal' h₂) = (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ normEDS b c d m *
      (normEDS b c d (m - 1) ^ 2 * normEDS b c d (m + 2) - normEDS b c d (m - 2) * normEDS b c d (m + 1) ^ 2) =
    normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2
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
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
x : ↥(((Functor.const I).obj c.pt).obj j)
x✝ : x ∈ ⊤
⊢ (c.π.app (i (σi x))) x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))

Tactic:
]

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
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
x : ↥(((Functor.const I).obj c.pt).obj j)
x✝ : x ∈ ⊤
⊢ (c.π.app (i (σi x))) x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
P : ℕ → Sort u_4
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
⊢ (n : ℕ) → ((k : ℕ) → k < 2 * n → P k) → P (2 * n)

Tactic:
rintro (_ | _ | _ | _) h; exacts [zero, two, four, even _ h]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
⊢ p.degree + q.degree + 1 ≤ p.degree + q.degree + 1

Tactic:
]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
⊢ 2 • q.degree + 3 = 2 • q.degree + 3

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h
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
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
y : ↥c.pt
hy : (D.map fkj) x ∈ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))
⊢ IsAffineOpen (D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))) ∧
    x ∈ D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))

Tactic:
]

Goal state after:
case h
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
i : ↥c.pt → I
f : (x : ↥c.pt) → ↑Γ(D.obj (i x), ⊤)
hf : ∀ (x : ↥c.pt), IsAffineOpen ((D.obj (i x)).basicOpen (f x))
hi : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ (D.obj (i x)).basicOpen (f x)
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ (D.obj (i x)).basicOpen (f x)).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ (D.obj (i (σi x))).basicOpen (f (σi x))).carrier
j : I
fj : (i_1 : I) → i_1 ∈ Finset.image i σ → (j ⟶ i_1)
k : I
fkj : k ⟶ j
hk : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤
x : ↥(D.obj k)
y : ↥c.pt
hy : (D.map fkj) x ∈ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))
⊢ IsAffineOpen (D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))) ∧
    x ∈ D.map fkj ⁻¹ᵁ D.map (fj (i (σi y)) ⋯) ⁻¹ᵁ (D.obj (i (σi y))).basicOpen (f (σi y))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)

Tactic:
]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • p.degree) (2 • q.degree + 3)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
]

Goal state after: