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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
⊢ ∃ k hki hkj y,
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
obtain ⟨k, ⟨k, rfl⟩, ⟨y, hy⟩, h⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp H this

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ ∃ k hki hkj y,
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case pos
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
i : ι
h : i ∈ s
⊢ IsOpen (Sigma.mk i ⁻¹' s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅)

pp: case neg
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
i : ι
h : i ∉ s
⊢ IsOpen (Sigma.mk i ⁻¹' s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅)

Tactic:
· simpa [h] using (V _ _).2

Goal state after:
case neg
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
i : ι
h : i ∉ s
⊢ IsOpen (Sigma.mk i ⁻¹' s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ C⁻¹ * C = 1

Tactic:
mul_def,

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ { u := C⁻¹.u * C.u, r := C⁻¹.r * ↑C.u ^ 2 + C.r, s := ↑C.u * C⁻¹.s + C.s,
      t := C⁻¹.t * ↑C.u ^ 3 + C⁻¹.r * C.s * ↑C.u ^ 2 + C.t } =
    1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ evalEval x y W.polynomialX = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)

Tactic:
simp only [polynomialX]

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ evalEval x y (C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄)) =
    W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W.map f).polynomialX = Polynomial.map (mapRingHom f) W.polynomialX

Tactic:
simp only [polynomialX]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ C (C (W.map f).a₁) * Y - C (C 3 * X ^ 2 + C (2 * (W.map f).a₂) * X + C (W.map f).a₄) =
    Polynomial.map (mapRingHom f) (C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - W'.negPolynomial = W'.polynomialY

Tactic:
← Y_sub_polynomialY,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (Y - W'.polynomialY) = W'.polynomialY
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
x : ↥c.pt
⊢ ∃ i U,
    ∃ (_ : IsAffineOpen U) (_ : (c.π.app i) x ∈ U),
      ∃ t, (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) t = (s |_ c.π.app i ⁻¹ᵁ U) ⋯

Tactic:
have i := IsCofiltered.nonempty (C := I).some

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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
x : ↥c.pt
i : I
⊢ ∃ i U,
    ∃ (_ : IsAffineOpen U) (_ : (c.π.app i) x ∈ U),
      ∃ t, (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) t = (s |_ c.π.app i ⁻¹ᵁ U) ⋯
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ span
      {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))),
        (mk W') (Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)))} =
    span {-(mk W') (C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y)} ⊔
      span {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ)))}

Tactic:
span_singleton_neg,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ span
      {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))),
        (mk W') (Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)))} =
    span {(mk W') (C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y)} ⊔
      span {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ)))}
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.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
⊢ span {-(mk W) (C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span
            {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                  YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂ *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
span_singleton_neg,

Goal state after:
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
⊢ span {(mk W) (C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span
            {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                  YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
                XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span
          {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
              XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
      span
        {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂ *
            XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ W ((2 * ((a + b + (c + d)) / 2) - (d + c)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - c)).tdiv 2) *
          (W ((2 * ((a + b + (c + d)) / 2) - (b + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - b - ((a + b + (c + d)) / 2 - a)).tdiv 2)) -
        W ((2 * ((a + b + (c + d)) / 2) - (d + b)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - b)).tdiv 2) *
          (W ((2 * ((a + b + (c + d)) / 2) - (c + a)).tdiv 2) *
            W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - a)).tdiv 2)) +
      W ((2 * ((a + b + (c + d)) / 2) - (d + a)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - d - ((a + b + (c + d)) / 2 - a)).tdiv 2) *
        (W ((2 * ((a + b + (c + d)) / 2) - (c + b)).tdiv 2) *
          W (((a + b + (c + d)) / 2 - c - ((a + b + (c + d)) / 2 - b)).tdiv 2)) =
    W ((a + b).tdiv 2) * W ((a - b).tdiv 2) * (W ((c + d).tdiv 2) * W ((c - d).tdiv 2)) -
        W ((a + c).tdiv 2) * W ((a - c).tdiv 2) * (W ((b + d).tdiv 2) * W ((b - d).tdiv 2)) +
      W ((a + d).tdiv 2) * W ((a - d).tdiv 2) * (W ((b + c).tdiv 2) * W ((b - c).tdiv 2))

Tactic:
rw [Int.mul_ediv_cancel'] <;> grind

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:

Tactic:
rw [Int.mul_ediv_cancel'] <;> grind

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ ¬Even 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
by decide

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ΨSq 3 = W.Ψ₃ ^ 2

Tactic:
simp [ΨSq, show ¬Even (3 : ℤ) by decide]

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
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₁) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)

Tactic:
by_cases hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

Goal state after:
case pos
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₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₁) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)

case neg
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₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₁) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)
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 : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
⊢ ((Cone.postcompose (asIso e).hom).obj c).π ≫ inv e ≫ t = (Functor.const I).map (a ≫ Spec.map φ)

Tactic:
by simpa using! ha

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 : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ (e.app i ≫ g) ≫ Spec.map φ = t.app i

Tactic:
simp [hg']

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ Even 2

Tactic:
by decide

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ¬Even 3

Tactic:
by decide

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
P Q : W.Point
x₁ y✝¹ : F
h✝¹ : W.Nonsingular x₁ y✝¹
x₂ y✝ : F
h✝ : W.Nonsingular x₂ y✝
h : x₁ = x₂
⊢ some x₁ y✝¹ h✝¹ = some x₂ y✝ h✝ ∨ some x₁ y✝¹ h✝¹ = -some x₂ y✝ h✝

Tactic:
exact X_eq_iff.mp h

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

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ W.j ≠ 0

Tactic:
rw [j_of_isCharTwoJNeZeroNF_of_char_two, div_ne_zero_iff]

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ 1 ≠ 0 ∧ W.a₆ ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₁
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ * (E.a₁ + 2 * 0) = E'.a₁

Tactic:
a₁_of_isCharThreeJNeZeroNF

Goal state after:
case h.a₁
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ * (0 + 2 * 0) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case of_j_ne_zero.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharThreeJNeZeroNF
⊢ ∃ C, C • E = E'

Tactic:
rw [← variableChange_j E C, ← variableChange_j E' C'] at heq
      obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_ne_zero _ _ heq
      use C'⁻¹ * C'' * C
      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: case neg.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
hm : n.natAbs = 0
⊢ W.ΨSq n ≠ 0

pp: case neg.succ
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
m : ℕ
hm : n.natAbs = m + 1
⊢ W.ΨSq n ≠ 0

Tactic:
· push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h

Goal state after:
case neg.succ
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
m : ℕ
hm : n.natAbs = m + 1
⊢ W.ΨSq n ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 →
        W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * a ^ 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0

Tactic:
intro h

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
h :
  b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
      (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
    0
⊢ W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
    2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 →
      W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * a ^ 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ Odd 3

Tactic:
by decide

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case coe
e : ℝ≥0
he : 1 < e
x : WithZero (Multiplicative ℤ)
a✝ : Multiplicative ℤ
⊢ x < ↑a✝ → (toNNReal ⋯) x < (toNNReal ⋯) ↑a✝

Tactic:
cases x

Goal state after:
case coe.zero
e : ℝ≥0
he : 1 < e
a✝ : Multiplicative ℤ
⊢ 0 < ↑a✝ → (toNNReal ⋯) 0 < (toNNReal ⋯) ↑a✝

case coe.coe
e : ℝ≥0
he : 1 < e
a✝¹ a✝ : Multiplicative ℤ
⊢ ↑a✝ < ↑a✝¹ → (toNNReal ⋯) ↑a✝ < (toNNReal ⋯) ↑a✝¹
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
⊢ W'.add P Q = (P x * Q z) • Q

Tactic:
by
  rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

Tactic:
· simp only [add_of_Y_eq hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.Nonsingular (W.add P Q)
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
constructor <;> rintro ⟨h', h⟩

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
⊢ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

case mpr
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ toAffine W (W.add P Q) = 0

pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ toAffine W (W.add P Q) = 0

Tactic:
· rw [add_of_Y_eq hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ toAffine W (W.add P Q) = 0