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

Goal state before:
pp: case inr
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
S : CommRingCat
inst✝¹ : IsAffine (Spec S)
a : D.obj i ⟶ Spec S
b : D.obj j ⟶ Spec S
hab : c.π.app i ≫ a = c.π.app j ≫ b
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
ha : t.app i = a ≫ Spec.map φ
hb : t.app j = b ≫ Spec.map φ
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), IsAffine (D.obj i)]
    [IsAffine c.pt] (t : D ⟶ (Functor.const I).obj (Spec R)) (a : D.obj i ⟶ Spec S) (b : D.obj j ⟶ Spec S),
    c.π.app i ≫ a = c.π.app j ≫ b →
      t.app i = a ≫ Spec.map φ →
        t.app j = b ≫ Spec.map φ → (∃ D', D = D' ⋙ Scheme.Spec) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
let e : D ⟶ D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
    have inst (i) : IsIso (e.app i) := by dsimp [e]; infer_instance
    have inst : IsIso e := NatIso.isIso_of_isIso_app e
    have inst (i) : IsAffine ((D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec).obj i) := by
      dsimp; infer_instance
    have inst : IsAffine ((Cone.postcompose (asIso e).hom).obj c).pt := by
      dsimp; infer_instance
    have := this (D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec) ((Cone.postcompose (asIso e).hom).obj c)
      ((IsLimit.postcomposeHomEquiv (asIso e) c).symm hc) (inv e ≫ t)
      ((inv e).app _ ≫ a) ((inv e).app _ ≫ b) (by simp [hab]) (by simp [ha]) (by simp [hb])
      ⟨D ⋙ Scheme.Γ.rightOp, rfl⟩
    simp_rw [(inv e).naturality_assoc] at this
    simpa using! this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∃ 𝒱 f, Finite 𝒱.I₀ ∧ ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f.h₀ j)

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩

Goal state after:
case refine_1
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Scheme.AffineCover P S

case refine_2
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Scheme.AffineCover.cover ?refine_1 ⟶ 𝒰

case refine_3
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ Finite (Scheme.AffineCover.I₀ ?refine_1)

case refine_4
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
⊢ ∀ (j : (Scheme.AffineCover.cover ?refine_1).I₀), IsOpenImmersion (PreZeroHypercover.Hom.h₀ ?refine_2 j)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: 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
⊢ ∀ i_1 ∈ Finset.univ, (Function.update c.val j (c.val j %ₘ c.val i) i_1).degree.succ ≤ (c.val i_1).degree.succ

Tactic:
intro k _
            rw [update_apply]
            split_ifs with hkj
            · subst hkj; gcongr; exact (degree_modByMonic_le _ hi).trans hle
            · rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
S : Scheme
𝒰 : Cover (precoverage P) S
⊢ 𝒰.sigma.presieve₀ = Presieve.singleton (Sigma.desc 𝒰.f)

Tactic:
refine le_antisymm ?_ fun T g ⟨⟩ ↦ ⟨⟨⟩⟩

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
S : Scheme
𝒰 : Cover (precoverage P) S
⊢ 𝒰.sigma.presieve₀ ≤ Presieve.singleton (Sigma.desc 𝒰.f)
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
⊢ f i ≫ EffectiveEpiFamily.desc Z (fun i ↦ g i ≫ f i) (fun i ↦ g i ≫ φ i) ⋯ = φ i

Tactic:
← cancel_epi (g i),

Goal state after:
C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
⊢ g i ≫ f i ≫ EffectiveEpiFamily.desc Z (fun i ↦ g i ≫ f i) (fun i ↦ g i ≫ φ i) ⋯ = g i ≫ φ i
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : R
i : Fin n
⊢ ∀ (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
            Statement R₀ (Away c) n
              { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
          (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
              Statement R₀ (R ⧸ Ideal.span {c}) n
                { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
            ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e

Tactic:
e

Goal state after:
case hP₄
R✝ : Type u_2
inst✝¹ : CommRing R✝
n : ℕ
R : Type u_2
inst✝ : CommRing R
c : R
i : Fin n
e : InductionObj R n
⊢ c = (e.val i).leadingCoeff →
    c ≠ 0 →
      (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (Away c)],
          Statement R₀ (Away c) n
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val }) →
        (∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ (R ⧸ Ideal.span {c})],
            Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val }) →
          ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R], Statement R₀ R n e
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) = ⊤
⊢ Finset
    ((X : I) ×' (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y))

Tactic:
by
    exact t.attach.image fun x ↦ ⟨j x.1, i, Finset.mem_insert_of_mem
      (Finset.mem_image_of_mem _ x.2), by simp, f x.1⟩

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)
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 ∈ Opposite.unop (Opposite.op ⊤),
    ∃ 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:
rintro 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)
⊢ ∃ 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.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆

Tactic:
rw [equation_iff', sub_eq_zero]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomialY = W.a₃

Tactic:
by
  simp only [evalEval_polynomialY, zero_add, mul_zero]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
⊢ y₁ = y₂ ∨ y₁ = W.negY x₂ y₂

Tactic:
rw [equation_iff] at h₁ h₂
  rw [← sub_eq_zero, ← sub_eq_zero (a := y₁), ← mul_eq_zero, negY]
  linear_combination (norm := (rw [hx]; ring1)) h₁ - h₂

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

Tactic:
simp_rw [slope_of_X_ne hx, addX, negY, ← neg_sub x₁, neg_sq]
  simp [field]
  ring1

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
i : Fin 3
⊢ (W.addSubMap i).IsHomogeneous 2

Tactic:
simp only [addSubMap]

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
i : Fin 3
⊢ (![s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2,
          C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2, t ^ 2 - C 4 * s * u]
        i).IsHomogeneous
    2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
      W (q + r + s) * W (q - r) * W (p + s) * W p =
    W ((2 * p + s + (2 * q + s)).tdiv 2) * W ((2 * p + s - (2 * q + s)).tdiv 2) *
          (W ((2 * r + s + s).tdiv 2) * W ((2 * r + s - s).tdiv 2)) -
        W ((2 * p + s + (2 * r + s)).tdiv 2) * W ((2 * p + s - (2 * r + s)).tdiv 2) *
          (W ((2 * q + s + s).tdiv 2) * W ((2 * q + s - s).tdiv 2)) +
      W ((2 * p + s + s).tdiv 2) * W ((2 * p + s - s).tdiv 2) *
        (W ((2 * q + s + (2 * r + s)).tdiv 2) * W ((2 * q + s - (2 * r + s)).tdiv 2))

Tactic:
add_add_add_comm _ s,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
      W (q + r + s) * W (q - r) * W (p + s) * W p =
    W ((2 * p + 2 * q + (s + s)).tdiv 2) * W ((2 * p + s - (2 * q + s)).tdiv 2) *
          (W ((2 * r + s + s).tdiv 2) * W ((2 * r + s - s).tdiv 2)) -
        W ((2 * p + 2 * r + (s + s)).tdiv 2) * W ((2 * p + s - (2 * r + s)).tdiv 2) *
          (W ((2 * q + s + s).tdiv 2) * W ((2 * q + s - s).tdiv 2)) +
      W ((2 * p + s + s).tdiv 2) * W ((2 * p + s - s).tdiv 2) *
        (W ((2 * q + 2 * r + (s + s)).tdiv 2) * W ((2 * q + s - (2 * r + s)).tdiv 2))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
by
  simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]

Goal state after:
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 : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x✝ : ℕ
ih : (k : ℕ) → k < 2 * (x✝ + 3) → P k
⊢ P (2 * (x✝ + 3))

Tactic:
by apply even <;> exact 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
n : ℤ
⊢ C X * (-W.ψ n) ^ 2 - W.ψ (-n + 1) * W.ψ (-n - 1) = C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)

Tactic:
neg_sq,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ C X * W.ψ n ^ 2 - W.ψ (-n + 1) * W.ψ (-n - 1) = C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
P Q : W.Point
⊢ P.xRep = Q.xRep ↔ P = Q ∨ P = -Q

Tactic:
by
  refine ⟨eq_or_eq_neg_of_xRep_eq_xRep, fun H ↦ ?_⟩
  rcases H with rfl | rfl <;> simp

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) (W.φ n) = (mk W) (C (W.Φ n))

Tactic:
by
  simp_rw [φ, Φ, map_sub, map_mul, map_pow, mk_ψ, mk_Ψ_sq, Ψ, map_mul,
    mul_mul_mul_comm _ <| mk W <| ite .., Int.even_add_one, Int.even_sub_one, ite_not, ← sq,
    apply_ite C, apply_ite <| mk W, ite_pow, map_one, one_pow, mk_ψ₂_sq]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₂ = 4 * W.a₂

Tactic:
by
  rw [b₂, a₁_of_isCharNeTwoNF]
  ring1

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
n : ℕ
⊢ (W⁄B).preΨ' n = Polynomial.map (↑f) ((W⁄A).preΨ' n)

Tactic:
by
  rw [← map_preΨ', map_baseChange]

Goal state after:
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✝² : 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
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₂ = E'.a₂

Tactic:
simp_rw [variableChange_a₂, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]

Goal state after:
case h.a₂
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
⊢ 1 ^ 2 * (E.a₂ - s * 1 + 3 * 0 - s ^ 2) = E'.a₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.c₆ = -W.a₂ ^ 3

Tactic:
rw [c₆_of_isCharThreeJNeZeroNF]
  linear_combination (-21 * W.a₂ ^ 3 - 288 * W.a₆) * CharP.cast_eq_zero R 3

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.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : ↑W.Δ' ≠ 0
⊢ W.j = -W.a₂ ^ 3 / W.a₆

Tactic:
rw [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three] at h

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.j = -W.a₂ ^ 3 / W.a₆
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
⊢ ∃ C, C • E = E'

Tactic:
have ha₃' := E'.Δ'.ne_zero

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'.Δ' ≠ 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 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : ↑E'.Δ' ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
rw [E'.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃'

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
⊢ ∃ C, C • E = E'