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

Goal state before:
pp: case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
⊢ ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h) =
    ↑U'

Tactic:
refine subset_antisymm (by simp) (fun x hx ↦ ?_)

Goal state after:
case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
⊢ x ∈
    ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h)
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:
Presieve.ofArrows_le_iff

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : UnivLE.{v, u}
S : Scheme
𝒰 : Cover (precoverage P) S
⊢ ∀ (i : 𝒰.sigma.I₀), Presieve.singleton (Sigma.desc 𝒰.f) (𝒰.sigma.f i)
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
⊢ coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ

Tactic:
rw [coeffSubmodule]

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
⊢ Submodule.span R₀ ({1} ∪ ⋃ i, coeff(c'.val i)) ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.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.252} 𝒰.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.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
⊢ ∀ (i : 𝒱.I₀),
    (((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
          pullback.fst s.pt.hom (𝒰.f i)) ≫
        Over.hom s.pt.toComma =
      𝒱.f i ≫ Over.hom d.glued.toComma

Tactic:
intro i
      have : _ ≫ pullback.snd _ _ = _ := Over.w ((d.isColimit i).desc (Functor.mapCocone _ s))
      simp only [glued, Category.assoc, 𝒱, pullback.condition]
      rw [reassoc_of% this]
      simp

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W.polynomial
f g : R[X]
h0 : { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly = f * g
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly = f + g
⊢ False

Tactic:
apply_fun degree at h0 h1

Goal state after:
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W.polynomial
f g : R[X]
h0 : { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly.degree = (f * g).degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y ℓ : A
⊢ (W'⁄B).addPolynomial (f x) (f y) (f ℓ) = Polynomial.map (↑f) ((W'⁄A).addPolynomial x y ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_addPolynomial, map_baseChange]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a a b c = W a * W 0 * atom W b c

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atom W a a * atom W b c - atom W a b * atom W a c + atom W a c * atom W a b = W a * W 0 * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atomRel W a b a c + (W a * W 0 * atom W b c + atom W a c * -atom W a b) -
      (W a * W 0 * atom W c b + (W a * W 0 * -atom W c b + atom W a c * atom W b a)) =
    0

Tactic:
atomRel,

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atom W a b * atom W a c - atom W a a * atom W b c + atom W a c * atom W b a +
        (W a * W 0 * atom W b c + atom W a c * -atom W a b) -
      (W a * W 0 * atom W c b + (W a * W 0 * -atom W c b + atom W a c * atom W b a)) =
    0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atomRel W a b c a = W a * W 0 * atom W b c

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atom W a b * atom W c a - atom W a c * atom W b a + atom W a a * atom W b c = W a * W 0 * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a b b c = W b * W 0 * atom W a c

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atom W a b * atom W b c - atom W a b * atom W b c + atom W a c * atom W b b = W b * W 0 * atom W a c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atomRel W a b c b + (W b * W 0 * atom W c a + atom W a b * -atom W b c) -
      (W b * W 0 * atom W c a + (W b * W 0 * -atom W a c + atom W a b * atom W c b)) =
    0

Tactic:
atomRel,

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atom W a b * atom W c b - atom W a c * atom W b b + atom W a b * atom W b c +
        (W b * W 0 * atom W c a + atom W a b * -atom W b c) -
      (W b * W 0 * atom W c a + (W b * W 0 * -atom W a c + atom W a b * atom W c b)) =
    0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atomRel W a b c c = W c * W 0 * atom W a b

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atom W a b * atom W c c - atom W a c * atom W b c + atom W a c * atom W b c = W c * W 0 * atom W a b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W (-a) b c d = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W (-a) b * atom W c d - atom W (-a) c * atom W b d + atom W (-a) d * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a (-b) c d = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a (-b) * atom W c d - atom W a c * atom W (-b) d + atom W a d * atom W (-b) c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a b (-c) d = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W (-c) d - atom W a (-c) * atom W b d + atom W a d * atom W b (-c) =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W a b c (-d) = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atom W a b * atom W c (-d) - atom W a c * atom W b (-d) + atom W a (-d) * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W |a| b c d = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W |a| b * atom W c d - atom W |a| c * atom W b d + atom W |a| d * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a |b| c d = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a |b| * atom W c d - atom W a c * atom W |b| d + atom W a d * atom W |b| c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a b |c| d = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atom W a b * atom W |c| d - atom W a |c| * atom W b d + atom W a d * atom W b |c| =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atomRel W a b c |d| = atomRel W a b c d

Tactic:
atomRel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
⊢ atom W a b * atom W c |d| - atom W a c * atom W b |d| + atom W a |d| * atom W b c =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
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
⊢ atomRel W ((a + b + (c + d)) / 2 - d) ((a + b + (c + d)) / 2 - c) ((a + b + (c + d)) / 2 - b)
      ((a + b + (c + d)) / 2 - a) =
    atomRel W a b c d

Tactic:
atomRel,

Goal state after:
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
⊢ atom W ((a + b + (c + d)) / 2 - d) ((a + b + (c + d)) / 2 - c) *
          atom W ((a + b + (c + d)) / 2 - b) ((a + b + (c + d)) / 2 - a) -
        atom W ((a + b + (c + d)) / 2 - d) ((a + b + (c + d)) / 2 - b) *
          atom W ((a + b + (c + d)) / 2 - c) ((a + b + (c + d)) / 2 - a) +
      atom W ((a + b + (c + d)) / 2 - d) ((a + b + (c + d)) / 2 - a) *
        atom W ((a + b + (c + d)) / 2 - c) ((a + b + (c + d)) / 2 - b) =
    atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c
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
a b c d : ℤ
⊢ f (atomRel W a b c d) = atomRel (⇑f ∘ W) a b c d

Tactic:
atomRel,

Goal state after:
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
a b c d : ℤ
⊢ f (atom W a b * atom W c d - atom W a c * atom W b d + atom W a d * atom W b c) =
    atom (⇑f ∘ W) a b * atom (⇑f ∘ W) c d - atom (⇑f ∘ W) a c * atom (⇑f ∘ W) b d +
      atom (⇑f ∘ W) a d * atom (⇑f ∘ W) b c
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 =
    atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s

Tactic:
atomRel,

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 =
    atom W (2 * p + s) (2 * q + s) * atom W (2 * r + s) s - atom W (2 * p + s) (2 * r + s) * atom W (2 * q + s) s +
      atom W (2 * p + s) s * atom W (2 * q + s) (2 * r + s)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

Tactic:
grw [degree_mul, degree_mul, degree_linear_le]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3.refine_1
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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
k : 𝒰.I₀
⊢ (IsOpenImmersion.lift (V k).ι (𝒰.f k ≫ c.π.app i) ⋯ ≫ ⋯.isoSpec.hom) ≫ ⋯.fromSpec = 𝒰.f k ≫ c.π.app i

Tactic:
simp [← IsAffineOpen.isoSpec_inv_ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3.refine_2
I : Type u
inst✝⁶ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
k : 𝒰.I₀
s : PullbackCone ⋯.fromSpec (c.π.app i)
y : ↥s.pt
⊢ (s.fst ≫ ⋯.fromSpec) y ∈ V k

Tactic:
simp [← IsAffineOpen.isoSpec_inv_ι]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ W.preΨ₄.coeff 6 ≠ 0

Tactic:
rwa [coeff_preΨ₄]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.c₆ = 0

Tactic:
by
  rw [c₆_of_isShortNF]
  linear_combination -288 * W.a₆ * CharP.cast_eq_zero R 3

Goal state after:
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:
c₆_of_isCharThreeJNeZeroNF

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ -64 * W.a₂ ^ 3 - 864 * W.a₆ = -W.a₂ ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case odd.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
⊢ ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
          W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2).coeff
      (expDegree (2 * (m + 2) + 1)) =
    ↑(expCoeff (2 * (m + 2) + 1))

Tactic:
nth_rw 1 [coeff_sub, (expDegree_rec m).2.1, cm (dm h₄.1 (dp h₂.1)), cm h₄.1 (dp h₂.1),
        h₄.2, cp h₂.1, h₂.2, apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_Ψ₂Sq, coeff_one_zero,
        (expDegree_rec m).2.2, cm (dm h₁.1 (dp h₃.1)), cm h₁.1 (dp h₃.1), h₁.2, cp h₃.1, h₃.2,
        apply_ite₂ coeff, cp W.natDegree_Ψ₂Sq_le, coeff_one_zero, coeff_Ψ₂Sq, (expCoeff_rec m).2]
      · norm_cast
      all_goals split_ifs <;> simp only [natDegree_one.le, dp W.natDegree_Ψ₂Sq_le]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.negY (u • P) = u ^ 3 * W'.negY P

Tactic:
by
  simp only [negY, smul_fin3_ext]
  ring1

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

Goal state before:
pp: case h.e'_3
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ P x ^ 2 * P x / P x ^ 2 * (Q x ^ 2 / Q y ^ 2) * Q x = P x

Tactic:
(hPx.pow 2).mul_div_cancel_left,

Goal state after:
case h.e'_3
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ P x * (Q x ^ 2 / Q y ^ 2) * Q x = P x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![P z ^ 2 * ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1] x,
      P z ^ 3 * ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1] y,
      P z * ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1] z]

Tactic:
simp only [fin3_def_ext]

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![P z ^ 2 * (P x / P z ^ 2), P z ^ 3 * W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), P z * 1]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).natDegree ≤ (↑n).natAbs ^ 2
n✝ : ℕ
⊢ (W.Φ (-↑n✝)).natDegree ≤ (-↑n✝).natAbs ^ 2

Tactic:
Φ_neg,

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).natDegree ≤ (↑n).natAbs ^ 2
n✝ : ℕ
⊢ (W.Φ ↑n✝).natDegree ≤ (-↑n✝).natAbs ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).coeff ((↑n).natAbs ^ 2) = 1
n✝ : ℕ
⊢ (W.Φ (-↑n✝)).coeff ((-↑n✝).natAbs ^ 2) = 1

Tactic:
Φ_neg,

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).coeff ((↑n).natAbs ^ 2) = 1
n✝ : ℕ
⊢ (W.Φ ↑n✝).coeff ((-↑n✝).natAbs ^ 2) = 1
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

Tactic:
use i

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ∈ {U | ∃ i, U = ↑(B i)}

Tactic:
use i

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case mp
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
⊢ ∃ i, {b | b - a ∈ B i} ⊆ s

Tactic:
use i

Goal state after:
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} ⊆ s