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

Goal state before:
pp: case inr
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
this :
  ∀ {U' : T.Opens},
    IsAffineOpen U' →
      (∃ U, IsAffineOpen U ∧ ⇑f '' ↑U' ⊆ ↑U) →
        IsCompactOpenCovered (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) ↑U'
h : ¬∃ U, IsAffineOpen U ∧ ⇑f '' ↑U' ⊆ ↑U
x : ↥T
hxU : x ∈ ↑U'
⊢ ∃ t ⊆ ↑U', x ∈ t ∧ IsOpen t ∧ IsCompactOpenCovered (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t

Tactic:
obtain ⟨W, hW, hx, _⟩ := isBasis_iff_nbhd.mp S.isBasis_affineOpens (mem_top (f x))

Goal state after:
case inr
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
this :
  ∀ {U' : T.Opens},
    IsAffineOpen U' →
      (∃ U, IsAffineOpen U ∧ ⇑f '' ↑U' ⊆ ↑U) →
        IsCompactOpenCovered (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) ↑U'
h : ¬∃ U, IsAffineOpen U ∧ ⇑f '' ↑U' ⊆ ↑U
x : ↥T
hxU : x ∈ ↑U'
W : TopologicalSpace.Opens ↥S
hW : W ∈ S.affineOpens
hx : f x ∈ W
right✝ : W ≤ ⊤
⊢ ∃ t ⊆ ↑U', x ∈ t ∧ IsOpen t ∧ IsCompactOpenCovered (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) t
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst✝ : IsSplitEpi f
⊢ CategoryTheory.EffectiveEpi f

Tactic:
rw [← Category.comp_id f]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst✝ : IsSplitEpi f
⊢ CategoryTheory.EffectiveEpi (f ≫ 𝟙 B)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃.inr.refine_2
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
⊢ Submodule.span R₀ ({1} ∪ ⋃ i, coeff(c'.val i)) ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ

Tactic:
simp only [Submodule.span_le, Set.union_subset_iff, Set.singleton_subset_iff, SetLike.mem_coe,
        Set.iUnion_subset_iff, Set.range_subset_iff, c']

Goal state after:
case hP₃.inr.refine_2
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
⊢ 1 ∈ coeffSubmodule R₀ c ^ (c.val j).degree.succ ∧
    ∀ (i_1 : Fin n) (y : ℕ),
      (Function.update c.val j (c.val j %ₘ c.val i) i_1).coeff y ∈ coeffSubmodule R₀ c ^ (c.val j).degree.succ
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_3
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₀
this :
  (d.pullbackGluedIso i).inv ≫ (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map m =
    (d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)
⊢ 𝒱.f i ≫ m.left =
    𝒱.f i ≫
      {
          toCommaMorphism :=
            𝒱.glueMorphismsOverOfLocallyDirected
              (fun i ↦
                ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                  pullback.fst s.pt.hom (𝒰.f i))
              ⋯ ⋯,
          prop_hom_left := trivial, prop_hom_right := trivial }.left

Tactic:
rw [Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left]

Goal state after:
case refine_3
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₀
this :
  (d.pullbackGluedIso i).inv ≫ (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map m =
    (d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)
⊢ 𝒱.f i ≫ m.left =
    ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.fst s.pt.hom (𝒰.f i)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hab
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
⊢ coeffSubmodule ℤ { val := y.g } ≤ M

Tactic:
refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 4 = 1

Tactic:
linear_combination CharP.cast_eq_zero R 3

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) ^
        (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) *
      (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) ^ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1) *
        degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n)

Tactic:
numBound_succ

Goal state after:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) ^
        (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) *
      ((numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) ^
          (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) *
        degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ (n + 1)

Tactic:
numBound_succ

Goal state after:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ n * degBound k₂ D₂ n * D₂ n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
⊢ Δ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)) ≠ 0

Tactic:
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))

Tactic:
let e :=
    (b'.equiv ((span {f}).selfBasis b hI) <| Equiv.refl _).trans
      ((LinearEquiv.coord S S f hf).restrictScalars R)

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (fun x ↦ x ^ 2) Y - (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y) =
    W'.polynomial * 1

Tactic:
polynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (fun x ↦ x ^ 2) Y - (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y) =
    (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₆)) * 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
Y_sq : (mk W') Y ^ 2 = (mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y)
⊢ (p • 1 + q • (mk W') Y) * (mk W') Y =
    (q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1 + (p - q * (C W'.a₁ * X + C W'.a₃)) • (mk W') Y

Tactic:
simp only [smul, add_mul, mul_assoc, ← sq, Y_sq, map_sub, map_mul]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
Y_sq : (mk W') Y ^ 2 = (mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) - C (C W'.a₁ * X + C W'.a₃) * Y)
⊢ (mk W') (C p) * (1 * (mk W') Y) +
      (mk W') (C q) *
        ((mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) -
          (mk W') (C (C W'.a₁ * X + C W'.a₃)) * (mk W') Y) =
    (mk W') (C q) * ((mk W') (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) * 1) +
      ((mk W') (C p) - (mk W') (C q) * (mk W') (C (C W'.a₁ * X + C W'.a₃))) * (mk W') Y
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - C (C (-y - W.a₁ * x - W.a₃))) -
          C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) +
        C (C (y ^ 2 + W.a₁ * x * y + W.a₃ * y)) -
      (W.polynomial * 1 + C (C (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆))) =
    0

Tactic:
polynomial

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - C (C (-y - W.a₁ * x - W.a₃))) -
          C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) +
        C (C (y ^ 2 + W.a₁ * x * y + W.a₃ * y)) -
      ((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₆)) * 1 +
        C (C (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) = 0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ eval (W'.addX x₁ x₂ ℓ) (derivative (eval (C ℓ * (X - C x₁) + C y₁) W'.polynomial)) = 0

Tactic:
polynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
hx :
  W'.a₁ * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - (3 * W'.addX x₁ x₂ ℓ ^ 2 + 2 * W'.a₂ * W'.addX x₁ x₂ ℓ + W'.a₄) = 0 ∧
    2 * (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) + (W'.a₁ * W'.addX x₁ x₂ ℓ + W'.a₃) = 0
⊢ eval (W'.addX x₁ x₂ ℓ)
      (derivative
        (eval (C ℓ * (X - C x₁) + C y₁)
          (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₆)))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) W'.polynomial = 0 ↔
    eval (W'.addX x₁ x₂ ℓ) (eval (C ℓ * (X - C x₁) + C y₁) W'.polynomial) = 0

Tactic:
polynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (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₆)) =
      0 ↔
    eval (W'.addX x₁ x₂ ℓ)
        (eval (C ℓ * (X - C x₁) + C y₁)
          (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₆))) =
      0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : ℤ
⊢ id (x✝³ + x✝² + x✝) * id (x✝³ - x✝²) * id (x✝¹ + x✝) * id x✝¹ -
        id (x✝³ + x✝¹ + x✝) * id (x✝³ - x✝¹) * id (x✝² + x✝) * id x✝² +
      id (x✝² + x✝¹ + x✝) * id (x✝² - x✝¹) * id (x✝³ + x✝) * id x✝³ =
    0

Tactic:
id_eq

Goal state after:
x✝³ x✝² x✝¹ x✝ : ℤ
⊢ (x✝³ + x✝² + x✝) * (x✝³ - x✝²) * (x✝¹ + x✝) * x✝¹ - (x✝³ + x✝¹ + x✝) * (x✝³ - x✝¹) * (x✝² + x✝) * x✝² +
      (x✝² + x✝¹ + x✝) * (x✝² - x✝¹) * (x✝³ + x✝) * x✝³ =
    0
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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • dp < (fun x1 x2 ↦ x1 + x2) (2 • dq) ↑3

Tactic:
dsimp; linarith only [hpq]

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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ (fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 + x2) dp dq) 1 < (fun x1 x2 ↦ x1 + x2) (2 • dq) ↑3

Tactic:
dsimp; linarith only [hpq]

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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (fun x1 x2 ↦ x1 + x2) ((fun x1 x2 ↦ x1 + x2) dp dq) 1 < 2 • dp

Tactic:
dsimp; linarith only [hpq]

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]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (fun x1 x2 ↦ x1 + x2) (2 • dq) ↑3 < 2 • dp

Tactic:
dsimp; linarith only [hpq]

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
⊢ Function.Injective ⇑toClass

Tactic:
rintro (_ | ⟨_, _, h⟩) _ hP
  all_goals rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]
  · exact zero_add 0
  · exact CoordinateRing.mk_XYIdeal'_neg_mul h

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ((X * W.Ψ₃ ^ 2 * if Even 2 then 1 else W.Ψ₂Sq) - W.preΨ' (2 + 2) * W.preΨ' 2 * if Even 2 then W.Ψ₂Sq else 1) =
    X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

Tactic:
if_pos <| by decide,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * W.Ψ₃ ^ 2 * 1 - W.preΨ' (2 + 2) * W.preΨ' 2 * if Even 2 then W.Ψ₂Sq else 1) = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁵ : Category.{u, u} I
inst✝⁴ : IsCofiltered I
R : CommRingCat
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
φ : R ⟶ S
inst✝¹ : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
t : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp
ha : c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S),
    c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')) →
        ∃ i g,
          c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i

Tactic:
have inst : IsAffine c.pt := isAffine_of_isLimit _ hc

Goal state after:
case inr
I : Type u
inst✝⁵ : Category.{u, u} I
inst✝⁴ : IsCofiltered I
R : CommRingCat
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
φ : R ⟶ S
inst✝¹ : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
t : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp
ha : c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S),
    c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')) →
        ∃ i g,
          c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
inst : IsAffine c.pt
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
P Q : W'.Point
⊢ P.sym2x Q ≠ 0

Tactic:
cases P <;> cases Q

Goal state after:
case zero.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ zero.sym2x zero ≠ 0

case zero.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) ≠ 0

case some.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero ≠ 0

case some.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W' : Affine R
P Q : W'.Point
⊢ P.sym2x Q = Q.sym2x P

Tactic:
cases P <;> cases Q

Goal state after:
case zero.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
⊢ zero.sym2x zero = zero.sym2x zero

case zero.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x zero

case some.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero = zero.sym2x (some x✝ y✝ h✝)

case some.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x (some x✝¹ y✝¹ h✝¹)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: 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
⊢ 2 * 2 = 1

Tactic:
linear_combination CharP.cast_eq_zero R 3

Goal state after: