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

Goal state before:
pp: n : Type u
S : Scheme
⊢ geometrically IsReduced (𝔸(n; S) ↘ S)

Tactic:
introv K h

Goal state after:
n : Type u
S : Scheme
K : Type u
inst✝ : Field K
y : Spec (CommRingCat.of K) ⟶ S
Z : Scheme
fst : Z ⟶ 𝔸(n; S)
snd : Z ⟶ Spec (CommRingCat.of K)
h : IsPullback fst snd (𝔸(n; S) ↘ S) y
⊢ IsReduced Z
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺

Tactic:
rw [posPart_def]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁⁺ + f₂⁺
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁⁺ + f₂⁺

Tactic:
rw [posPart_def]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂⁺
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂⁺

Tactic:
rw [posPart_def]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0

Tactic:
rw [posPart_def]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ EqOn (⇑(D.restrict h)) 0 Vᶜ

Tactic:
intro _ hx

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x✝ : X
hx : x✝ ∈ Vᶜ
⊢ (D.restrict h) x✝ = 0 x✝
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)

Tactic:
exact @isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2.hy
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (algebraMap ↑R ↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x *
      IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
⊢ IsUnit (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s)

Tactic:
exact @isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = (genericPoint ↥(Spec R)).asIdeal.primeCompl

Tactic:
rw [genericPoint_eq_bot_of_affine]

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ nonZeroDivisors ↑R = ⊥.asIdeal.primeCompl
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝¹⁰ : PreirreducibleSpace ↥X
inst✝⁹ : Nonempty ↥Y
S : Scheme
inst✝⁸ : IrreducibleSpace ↥Y
inst✝⁷ : Nonempty ↥Z
inst✝⁶ : X.Over S
inst✝⁵ : Y.Over S
inst✝⁴ : Z.Over S
f : X ⤏ Y
inst✝³ : f.IsDominant
inst✝² : IsOver S f
g : Y ⤏ Z
inst✝¹ : g.IsDominant
inst✝ : IsOver S g
⊢ IsOver S (f.comp g)

Tactic:
isOver_iff,

Goal state after:
X Y Z : Scheme
inst✝¹⁰ : PreirreducibleSpace ↥X
inst✝⁹ : Nonempty ↥Y
S : Scheme
inst✝⁸ : IrreducibleSpace ↥Y
inst✝⁷ : Nonempty ↥Z
inst✝⁶ : X.Over S
inst✝⁵ : Y.Over S
inst✝⁴ : Z.Over S
f : X ⤏ Y
inst✝³ : f.IsDominant
inst✝² : IsOver S f
g : Y ⤏ Z
inst✝¹ : g.IsDominant
inst✝ : IsOver S g
⊢ (f.comp g).compHom (Z ↘ S) = Hom.toRationalMap (X ↘ S)
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
U V : (D.obj i).Opens
hU : IsCompact ↑U
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
⊢ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ⁻¹ᵁ c.π.app i ⁻¹ᵁ V

Tactic:
exact .trans (by simp) (Scheme.Hom.preimage_mono _ H)

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_4
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
m : s.pt ⟶ d.functor.obj i
⊢ m ≫ d.natTrans.app i = s.fst →
    m ≫ colimit.ι d.functor i = s.snd → m = IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯

Tactic:
h1

Goal state after:
case refine_4
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
s : PullbackCone (𝒰.f i) d.toBase
m : s.pt ⟶ d.functor.obj i
h1 : m ≫ d.natTrans.app i = s.fst
⊢ m ≫ colimit.ι d.functor i = s.snd → m = IsOpenImmersion.lift (colimit.ι d.functor i) s.snd ⋯
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered f (Us x a)
⊢ ⋃ t ∈ {x | ∃ x_1, ∃ (h : x_1 ∈ U), Us x_1 h = ↑x}, ↑t = U

pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered f (Us x a)
⊢ ∀ t ∈ {x | ∃ x_1, ∃ (h : x_1 ∈ U), Us x_1 h = ↑x}, IsCompactOpenCovered f ↑t

Tactic:
· refine subset_antisymm (fun x ↦ ?_) fun x hx ↦ ?_
    · simp [Opens.forall]
      grind
    · simpa using ⟨⟨Us x hx, hUo _ _⟩, ⟨x, by simpa⟩, hUx _ _⟩

Goal state after:
case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
Us : (x : S) → x ∈ U → Set S
hU' : ∀ (x : S) (a : x ∈ U), Us x a ⊆ U
hUx : ∀ (x : S) (a : x ∈ U), x ∈ Us x a
hUo : ∀ (x : S) (a : x ∈ U), IsOpen (Us x a)
hU'' : ∀ (x : S) (a : x ∈ U), IsCompactOpenCovered f (Us x a)
⊢ ∀ t ∈ {x | ∃ x_1, ∃ (h : x_1 ∈ U), Us x_1 h = ↑x}, IsCompactOpenCovered f ↑t
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case intro
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB✝ : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU✝ : IsCompactOpenCovered f U
κ : Type ?u.68
w✝ : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), V i ∈ B (a i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ i, f (a i) '' ↑(V i) = U
val✝ : Fintype κ
⊢ ∃ n a V, (∀ (i : Fin n), V i ∈ B (a i)) ∧ ⋃ i, f (a i) '' ↑(V i) = U

Tactic:
refine ⟨Fintype.card κ, a ∘ (Fintype.equivFin κ).symm, fun i ↦ V _, fun i ↦ hB _, ?_⟩

Goal state after:
case intro
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB✝ : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
hU✝ : IsCompactOpenCovered f U
κ : Type ?u.68
w✝ : Finite κ
a : κ → ι
V : (i : κ) → Opens (X (a i))
hB : ∀ (i : κ), V i ∈ B (a i)
hc : ∀ (i : κ), IsCompact (V i).carrier
hU : ⋃ i, f (a i) '' ↑(V i) = U
val✝ : Fintype κ
⊢ ⋃ i, f ((a ∘ ⇑(Fintype.equivFin κ).symm) i) '' ↑((fun i ↦ V ((Fintype.equivFin κ).symm i)) i) = U
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:
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_1
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.117} 𝒰.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.117} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
⊢ (i : 𝒱.I₀) → 𝒱.X i ⟶ Over.left s.pt.toComma

Tactic:
intro i
      exact ((d.isColimit i).desc (Functor.mapCocone _ s)).left ≫ pullback.fst _ _

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

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

Tactic:
simp only [mul_def, one_def, zero_add, zero_mul, mul_zero, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ ((preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        if Even k then 1 else b) *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * if ¬Even k then b else 1) ^ 2 *
        (preNormEDS (b ^ 4) c d (k + 2) * if Even k then b else 1) -
      (preNormEDS (b ^ 4) c d (k - 2) * if Even k then b else 1) *
        (preNormEDS (b ^ 4) c d (k + 1) * if ¬Even k then b else 1) ^ 2

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        1 *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * 1) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * b) -
      preNormEDS (b ^ 4) c d (k - 2) * b * (preNormEDS (b ^ 4) c d (k + 1) * 1) ^ 2

case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
h✝ : ¬Even k
⊢ (preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
          preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
        b *
      b =
    (preNormEDS (b ^ 4) c d (k - 1) * b) ^ 2 * (preNormEDS (b ^ 4) c d (k + 2) * 1) -
      preNormEDS (b ^ 4) c d (k - 2) * 1 * (preNormEDS (b ^ 4) c d (k + 1) * b) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
⊢ ((preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * if Even m then b ^ 4 else 1) -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * if Even m then 1 else b ^ 4) *
      1 =
    (preNormEDS (b ^ 4) c d (m + 2) * if Even m then b else 1) *
        (preNormEDS (b ^ 4) c d m * if Even m then b else 1) ^ 3 -
      (preNormEDS (b ^ 4) c d (m - 1) * if ¬Even m then b else 1) *
        (preNormEDS (b ^ 4) c d (m + 1) * if ¬Even m then b else 1) ^ 3

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * b ^ 4 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * 1) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * b * (preNormEDS (b ^ 4) c d m * b) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * 1 * (preNormEDS (b ^ 4) c d (m + 1) * 1) ^ 3

case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℤ
h✝ : ¬Even m
⊢ (preNormEDS (b ^ 4) c d (m + 2) * preNormEDS (b ^ 4) c d m ^ 3 * 1 -
        preNormEDS (b ^ 4) c d (m - 1) * preNormEDS (b ^ 4) c d (m + 1) ^ 3 * b ^ 4) *
      1 =
    preNormEDS (b ^ 4) c d (m + 2) * 1 * (preNormEDS (b ^ 4) c d m * 1) ^ 3 -
      preNormEDS (b ^ 4) c d (m - 1) * b * (preNormEDS (b ^ 4) c d (m + 1) * b) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * s ^ 2 +
          C (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * s * t +
        C (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * s * u).IsHomogeneous
    2

pp: case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

pp: case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

pp: case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

pp: case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

pp: case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2

Tactic:
· exact CXX.add CXY |>.add CXY

Goal state after:
case «3»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (96 * W.b₆) * s * t + C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * t ^ 2 + C (16 * W.b₄ * W.b₆) * t * u).IsHomogeneous 2

case «4»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(48 * W.b₆)) * s ^ 2 + C (32 * W.b₈) * s * t + C (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * t ^ 2 +
        C (16 * W.b₄ * W.b₈) * t * u).IsHomogeneous
    2

case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

case «6»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-12) * t ^ 2 + C (-(4 * W.b₂)) * t * u + C (W.b₂ ^ 2 - 32 * W.b₄) * u ^ 2).IsHomogeneous 2

case «7»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 6 * s * t + C (-W.b₂) * s * u + C (-(5 * W.b₄)) * t * u + C (W.b₂ * W.b₄ - 27 * W.b₆) * u ^ 2).IsHomogeneous 2

case «8»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(8 * W.b₄)) * s * u + C (-(12 * W.b₆)) * t * u + C (W.b₄ ^ 2 - 28 * W.b₈) * u ^ 2).IsHomogeneous 2
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✝ : IsAffine c.pt
this✝² : ∀ (i : I), IsAffineHom (c.π.app i)
i : I
hi : (D.obj i).IsQuasiAffine
this✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).map f)
this✝ : ∀ (j : I), CompactSpace ↥((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj j)
j : I
fij : j ⟶ i
hj : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).map fij ⁻¹ᵁ Hom.opensRange (D.obj i).toSpecΓ = ⊤
this : (D.obj j).IsQuasiAffine
⊢ ∃ i, IsAffine (D.obj i)

Tactic:
exact ⟨j, ⟨isIso_of_isOpenImmersion_of_opensRange_eq_top _
    ((preimage_opensRange_toSpecΓ (D.map fij)).symm.trans hj)⟩⟩

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ C (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) * W.ψ₂ * W.ψ₂ =
    (C (W.preΨ (m - 1)) * if ¬Even m then W.ψ₂ else 1) ^ 2 * (C (W.preΨ m) * if Even m then W.ψ₂ else 1) *
        (C (W.preΨ (m + 2)) * if Even m then W.ψ₂ else 1) -
      (C (W.preΨ (m - 2)) * if Even m then W.ψ₂ else 1) * (C (W.preΨ m) * if Even m then W.ψ₂ else 1) *
        (C (W.preΨ (m + 1)) * if ¬Even m then W.ψ₂ else 1) ^ 2

Tactic:
split_ifs

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ C (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) * W.ψ₂ * W.ψ₂ =
    (C (W.preΨ (m - 1)) * 1) ^ 2 * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 2)) * W.ψ₂) -
      C (W.preΨ (m - 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 1)) * 1) ^ 2

case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ C (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) * W.ψ₂ * W.ψ₂ =
    (C (W.preΨ (m - 1)) * W.ψ₂) ^ 2 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 2)) * 1) -
      C (W.preΨ (m - 2)) * 1 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 2