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

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝ : IsAffine (A.𝒰D.X j)
this : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
⊢ ∃ k hki',
    (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.b

Tactic:
have : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone
      ((Over.conePost D A.i').obj A.c)).pt := by
    dsimp; infer_instance

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝¹ : IsAffine (A.𝒰D.X j)
this✝ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
⊢ ∃ k hki',
    (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j ≫ D.map (hki' ≫ A.hii') ≫ A.b
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case pos
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝¹ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k✝ : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
k : Fin n
h✝ : k = j
⊢ coeff(0) ⊆ ↑(coeffSubmodule R₀ c)

Tactic:
rintro _ ⟨_, rfl⟩
                exact zero_mem _

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.71} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.71} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
⊢ Cocone D

Tactic:
letI 𝒱 (a : J) : (D.obj a).left.OpenCover := 𝒰.pullback₁ (D.obj a).hom

Goal state after:
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.95} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.95} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
⊢ Cocone D
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
by
    suffices g = ofHom (hπ.liftEquiv ⟨e.hom,
      fun a b hab ↦ CategoryTheory.congr_fun (h
          (ofHom ⟨fun _ ↦ a, continuous_const⟩)
          (ofHom ⟨fun _ ↦ b, continuous_const⟩)
          (by ext; exact hab))
        a⟩) by assumption
    apply hom_ext
    rw [hom_ofHom, ← Equiv.symm_apply_eq hπ.liftEquiv]
    ext
    simp only [IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case h₀
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.499} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ ((Comma.Hom.hom ((d.cocone i).ι.app a)).left ≫
        (Comma.Hom.hom (d.pullbackGluedIso i).inv).left ≫
          pullback.lift (pullback.fst d.glued.hom (𝒰.f i) ≫ m.left) (pullback.snd d.glued.hom (𝒰.f i)) ⋯) ≫
      pullback.fst s.pt.hom (𝒰.f i) =
    pullback.lift (pullback.fst (D.obj a).hom (𝒰.f i) ≫ (s.ι.app a).left) (pullback.snd (D.obj a).hom (𝒰.f i)) ⋯ ≫
      pullback.fst s.pt.hom (𝒰.f i)

Tactic:
simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          pullbackGluedIso_inv_fst_assoc]

Goal state after:
case h₀
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.499} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ (Comma.Hom.hom ((d.cocone i).ι.app a)).left ≫ colimit.ι d.relativeGluingData.functor i ≫ m.left =
    pullback.fst (D.obj a).hom (𝒰.f i) ≫ (s.ι.app a).left
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)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op ⊤)),
      x ∈ V ∧
        (ConcreteCategory.hom ((D.obj k).presheaf.map (homOfLE hV).op))
            ((ConcreteCategory.hom (Scheme.Hom.appTop (D.map (fk ⋯)))) s) =
          (ConcreteCategory.hom ((D.obj k).presheaf.map (homOfLE hV).op)) 0

Tactic:
obtain ⟨l, hl, hlU⟩ := Set.mem_iUnion₂.mp (ht.ge (Set.mem_univ ((D.map (fk (by simp))).base x)))

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)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : (D.map (fk ⋯)) x ∈ ↑(U l)
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op ⊤)),
      x ∈ V ∧
        (ConcreteCategory.hom ((D.obj k).presheaf.map (homOfLE hV).op))
            ((ConcreteCategory.hom (Scheme.Hom.appTop (D.map (fk ⋯)))) s) =
          (ConcreteCategory.hom ((D.obj k).presheaf.map (homOfLE hV).op)) 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.negY x (W'.negY x y) = y

Tactic:
simp only [negY]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.negPolynomial = W'.negY x y

Tactic:
by
  rw [negY, sub_sub, negPolynomial]
  eval_simp

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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝ : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
this :
  ∀ (x y : ↥c.pt),
    ∃ j fjx fjy,
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjx) (U x))) (t x) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯ =
        ((ConcreteCategory.hom (Scheme.Hom.app (D.map fjy) (U y))) (t y) |_ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) ⋯
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t

Tactic:
choose j fjx fjy hj using this

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
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
⊢ ∃ i t, s = (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ (CoordinateRing.basis W') 0 = 1

Tactic:
simpa only [basis_apply] using! pow_zero _

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
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)
⊢ c.π.app j ⁻¹ᵁ ⨆ k, D.map (fj (i (σi k)) ⋯) ⁻¹ᵁ (D.obj (i (σi k))).basicOpen (f (σi k)) = ⊤

Tactic:
refine top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, ?_⟩
      change (c.π.app j ≫ D.map _).base x ∈ (D.obj (i (σi x))).basicOpen (f (σi x))
      rw [Cone.w]
      exact hσi _

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:
simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]

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:
simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 - 4 * W.toAffine.polynomial

Tactic:
Affine.polynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 -
      4 *
        (Y ^ 2 + C (C W.toAffine.a₁ * X + C W.toAffine.a₃) * Y -
          C (X ^ 3 + C W.toAffine.a₂ * X ^ 2 + C W.toAffine.a₄ * X + C W.toAffine.a₆))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 3 = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

Tactic:
rw [show 3 = ((2 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_three, if_pos <| by decide, mul_one,
    preΨ'_four, preΨ'_two, mul_one, if_pos even_two]

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
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₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ f ((W'⁄F).negY x₂ y₂) = (W'⁄K).negY (f x₂) (f y₂)

Tactic:
baseChange_negY

Goal state after:
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₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ f ((W'⁄F).negY x₂ y₂) = f ((W'⁄F).negY x₂ y₂)
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).preΨ' n = Polynomial.map f (W.preΨ' n)

Tactic:
by
  simp [preΨ', ← coe_mapRingHom]

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
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).Ψ₂Sq = Polynomial.map (↑f) (W⁄A).Ψ₂Sq

Tactic:
rw [← map_Ψ₂Sq, map_baseChange]

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨s, hs⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 2
    1 1 (E.a₂ + E'.a₂) (by simp) (by simp) one_ne_zero

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ (W.a₂ ^ 2) ^ 3 / W.Δ = -W.a₂ ^ 3 / W.a₆

Tactic:
Δ_of_isCharThreeJNeZeroNF_of_char_three,

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ (W.a₂ ^ 2) ^ 3 / (-W.a₂ ^ 3 * W.a₆) = -W.a₂ ^ 3 / W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : W.Δ ≠ 0
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
Δ_of_isCharThreeJNeZeroNF_of_char_three,

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero 3
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₃ / E'.a₃) 3

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
this : NeZero 3
u : F
hu : u ^ 3 = E.a₃ / E'.a₃
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W✝ : WeierstrassCurve R
inst✝¹ : CharP R 3
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (W.toCharThreeNF • W).IsCharThreeNF

Tactic:
have := W.toCharThreeNF_spec_of_b₂_eq_zero hb₂

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W✝ : WeierstrassCurve R
inst✝¹ : CharP R 3
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
this : (W.toCharThreeNF • W).IsShortNF
⊢ (W.toCharThreeNF • W).IsCharThreeNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: 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
h : E.Δ ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
Δ_of_isCharThreeJNeZeroNF_of_char_three,

Goal state after:
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
h : -E.a₂ ^ 3 * E.a₆ ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: 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
h : E'.Δ ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
Δ_of_isCharThreeJNeZeroNF_of_char_three,

Goal state after:
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
h : -E'.a₂ ^ 3 * E'.a₆ ≠ 0
⊢ ∃ C, C • E = E'
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := r, s := 0, t := 0 } • E).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, a₁_of_isShortNF, a₃_of_isShortNF]
    ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑n ≠ 0
⊢ (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
  · rw [coeff_preΨ', if_pos <| even_two_mul n, n.mul_div_cancel_left two_pos]
    exact right_ne_zero_of_mul <| by rwa [← Nat.cast_mul]
  · rwa [coeff_preΨ', if_neg n.not_even_two_mul_add_one]

Goal state after: