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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
    Q f → Q g → Q (f.prod g)
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
hf : ∀ (U_1 : X.Opens), IsAffineOpen U_1 → IsAffineOpen (f ⁻¹ᵁ U_1) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U_1))
hg : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (g ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app g U))
this✝¹ : IsAffineHom f
this✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
e : Γ(U ⨿ V, Limits.coprod.desc f g ⁻¹ᵁ W) ≅ Γ(U, f ⁻¹ᵁ W) ⨯ Γ(V, g ⁻¹ᵁ W) :=
  Scheme.coprodPresheafObjIso (Limits.coprod.desc f g ⁻¹ᵁ W) ≪≫
    Limits.prod.mapIso (Functor.mapIso U.presheaf (eqToIso ⋯).op) (Functor.mapIso V.presheaf (eqToIso ⋯).op)
this :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S × T),
    Q ((RingHom.fst S T).comp f) → Q ((RingHom.snd S T).comp f) → Q f
⊢ Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom ≫ Limits.prod.snd = Scheme.Hom.app g W

Tactic:
simp [e, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFinitePresentation = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation

Tactic:
ext X Y f
    rw [locallyOfFinitePresentation_iff, affineLocally_iff_forall_isAffineOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
x : ↥X
⊢ IsOpen {x}

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Goal state after:
case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
i : 𝒰.I₀
x : ↥(𝒰.X i)
⊢ IsOpen {(𝒰.f i) x}
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
hU : IsAffineOpen U
hU2 : x ∈ U
hU3 : U.carrier ⊆ ↑⊤
⊢ IsNoetherianRing ↑(X.presheaf.stalk x)

Tactic:
have := AlgebraicGeometry.IsAffineOpen.isLocalization_stalk hU ⟨x, hU2⟩

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
hU : IsAffineOpen U
hU2 : x ∈ U
hU3 : U.carrier ⊆ ↑⊤
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hU2⟩)) (hU.primeIdealOf ⟨x, hU2⟩).asIdeal
⊢ IsNoetherianRing ↑(X.presheaf.stalk x)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ⇑(f ∣_ U i)
⊢ topologically (@IsOpenMap) f

Tactic:
morphismRestrict_base

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage ⇑f)
⊢ topologically (@IsOpenMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ⇑(f ∣_ U i)
⊢ topologically (@IsClosedMap) f

Tactic:
morphismRestrict_base

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage ⇑f)
⊢ topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case mpr
X : Scheme
inst✝ : JacobsonSpace ↥X
x : ↥X
H : LocallyOfFiniteType (X.fromSpecResidueField x)
⊢ IsClosed {x}

Tactic:
simpa using (X.fromSpecResidueField x).closePoints_subset_preimage_closedPoints
      (IsLocalRing.isClosed_singleton_closedPoint _)

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (s ∩ Set.range ⇑(𝒰.f i))

Tactic:
← Set.image_preimage_eq_inter_range

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(𝒰.f i) '' ⇑(𝒰.f i) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
⊢ (fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f) = f

Tactic:
ext : 2

Goal state after:
case h₁
n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
⊢ ↑((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩) ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f)) ≫
      𝔸(n; S) ↘ S =
    ↑f ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S X : Scheme
inst✝ : X.Over S
f : { f // Scheme.Hom.IsOver f S }
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ↑((fun v ↦ ⟨homOfVector (X ↘ S) v, ⋯⟩)
              ((fun f i ↦ (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)) f))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i✝)
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
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
s t : ↑Γ(X, UX)
est : ψ s = ψ t
⊢ s = t

Tactic:
apply X.IsSheaf.section_ext fun x hx ↦ ?_

Goal state after:
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
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
s t : ↑Γ(X, UX)
est : ψ s = ψ t
x : ↥X
hx : x ∈ unop (op UX)
⊢ ∃ V,
    ∃ (hV : V ≤ unop (op UX)),
      x ∈ V ∧
        (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) s =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) t
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
⊢ CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv =
    (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C

Tactic:
ext : 2

Goal state after:
n : Type u
R : CommRingCat
x✝ : ↑(CommRingCat.of ↑((Spec R).presheaf.1 (Opposite.op ⊤)))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv))
      x✝ =
    (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom C)) x✝
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type uᵒᵖ
⊢ { app := reindex ⇑(ConcreteCategory.hom (𝟙 n).unop), naturality := ⋯ } =
    𝟙 { obj := AffineSpace (Opposite.unop n), map := fun {X Y} ↦ map (Opposite.unop n), map_id := ⋯, map_comp := ⋯ }

Tactic:
ext : 2

Goal state after:
n✝ : Type u
S : Scheme
n : Type uᵒᵖ
x✝ : Scheme
⊢ { app := reindex ⇑(ConcreteCategory.hom (𝟙 n).unop), naturality := ⋯ }.app x✝ =
    (𝟙
          { obj := AffineSpace (Opposite.unop n), map := fun {X Y} ↦ map (Opposite.unop n), map_id := ⋯,
            map_comp := ⋯ }).app
      x✝
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { app := reindex ⇑(ConcreteCategory.hom (f ≫ g).unop), naturality := ⋯ } =
    { app := reindex ⇑(ConcreteCategory.hom f.unop), naturality := ⋯ } ≫
      { app := reindex ⇑(ConcreteCategory.hom g.unop), naturality := ⋯ }

Tactic:
ext : 2

Goal state after:
n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ { app := reindex ⇑(ConcreteCategory.hom (f ≫ g).unop), naturality := ⋯ }.app x✝ =
    ({ app := reindex ⇑(ConcreteCategory.hom f.unop), naturality := ⋯ } ≫
          { app := reindex ⇑(ConcreteCategory.hom g.unop), naturality := ⋯ }).app
      x✝
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
f : locallyFinsupp X Y
x✝ : X
⊢ x✝ ∈ univ

Tactic:
by trivial

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
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
x : X
⊢ 0 ≤ max (f₁ x) 0 + max (f₂ x) 0

Tactic:
· simp [add_nonneg]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
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
x : X
⊢ 0 ≤ max (-f₁ x) 0 + max (-f₂ x) 0

Tactic:
· simp [add_nonneg]

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

Goal state before:
pp: X S : Scheme
U : X.Opens
sX : X ⟶ S
hU : Dense ↑U
inst✝ : IsRationalOver sX
⊢ IsRationalOver (U.ι ≫ sX)

Tactic:
by
  obtain ⟨n, hn⟩ := IsRationalOver.exists_birationalOver_affineSpace sX
  exact ⟨n, (U.birationalOver_of_dense sX hU).trans hn⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.trans fi ≫ 𝒰.f k) xi = (𝒰.f j) xj

Tactic:
← 𝒰.trans_map fj,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.trans fi ≫ 𝒰.f k) xi = (𝒰.trans fj ≫ 𝒰.f k) xj
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.trans fi ≫ 𝒰.f k) xi = (𝒰.f j) xj

Tactic:
← 𝒰.trans_map fj,

Goal state after:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_1, u_1} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j k : 𝒰.I₀
fi : i ⟶ k
fj : j ⟶ k
xi : (𝒰.functorOfLocallyDirected ⋙ forget).obj i
xj : (𝒰.functorOfLocallyDirected ⋙ forget).obj j
hxij : (𝒰.trans fi) xi = (𝒰.trans fj) xj
⊢ (𝒰.trans fi ≫ 𝒰.f k) xi = (𝒰.trans fj ≫ 𝒰.f k) xj
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ D.map j.hom ⁻¹ᵁ U

Tactic:
rintro x ⟨⟨y, h₁ : (D.map k.hom).base y ∈ U⟩, h₂, e⟩

Goal state after:
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
x : ↥(D.obj j.left)
y : ↥(D.obj k.left)
h₁ : (D.map k.hom) y ∈ U
h₂ : ⟨y, h₁⟩ ∈ ↑V
e :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom (D.map k.hom ⁻¹ᵁ U).ι)).hom.base) ⟨y, h₁⟩ =
    (D.map (Over.Hom.left f)) x
⊢ x ∈ D.map j.hom ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
inst✝⁶ : IsCofiltered I
i j : I
R : CommRingCat
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝² : ∀ (i : I), CompactSpace ↥((D ⋙ Scheme.Spec).obj i)
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
inst✝ : IsAffine c.pt
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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.whiskerRight { app := fun i ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ }.rightOp
        Scheme.Spec ≫
      e.hom

Tactic:
ext : 2

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
inst✝⁶ : IsCofiltered I
i j : I
R : CommRingCat
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝² : ∀ (i : I), CompactSpace ↥((D ⋙ Scheme.Spec).obj i)
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
inst✝ : IsAffine c.pt
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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)) ⋯
x✝ : I
⊢ t.app x✝ =
    (Functor.whiskerRight { app := fun i ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ }.rightOp
            Scheme.Spec ≫
          e.hom).app
      x✝
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
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
⊢ ∃ T,
    comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T, C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀✝ g ^ g.powBound

Tactic:
have : Module.Free R M := .of_basis (AdjoinRoot.powerBasis' hi).basis

Goal state after:
case hP₂
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this : Module.Free R M
⊢ ∃ T,
    comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T, C.n ≤ g.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀✝ g ^ g.powBound
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ True

Tactic:
by trivial

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

Goal state before:
pp: case neg
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
l : Fin n
m : ℕ
hlj : ¬l = j
⊢ (c.val l).coeff m ∈ coeffSubmodule R₀ c ^ (c.val j).degree.succ

Tactic:
have : (c.val j).degree.succ ≠ 0 := by
            rw [← Nat.pos_iff_ne_zero]
            apply WithBot.succ_lt_succ (x := ⊥)
            refine lt_of_lt_of_le ?_ hle
            rw [bot_lt_iff_ne_bot, ne_eq, degree_eq_bot]
            intro e
            simp [e] at hi

Goal state after:
case neg
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
l : Fin n
m : ℕ
hlj : ¬l = j
this : (c.val j).degree.succ ≠ 0
⊢ (c.val l).coeff m ∈ coeffSubmodule R₀ c ^ (c.val j).degree.succ
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))).inv ≫
        pullback.fst (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f i) ≫ f =
    (pullbackLeftPullbackSndIso π (𝒰.f j) (pullback.snd (𝒰.f i) (𝒰.f j))).inv ≫
      pullback.fst (pullback.snd π (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≫ pullback.snd π (𝒰.f j) ≫ u j

Tactic:
← hfac j

Goal state after:
case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this✝ : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
i j : 𝒰.I₀
this : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
⊢ (pullback.congrHom ⋯ ⋯).hom ≫
      (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))).inv ≫
        pullback.fst (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f i) ≫ f =
    (pullbackLeftPullbackSndIso π (𝒰.f j) (pullback.snd (𝒰.f i) (𝒰.f j))).inv ≫
      pullback.fst (pullback.snd π (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f j) ≫ f
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
W : WeierstrassCurve R
inst✝² : W.IsElliptic
inst✝¹ : CharP R 2
inst✝ : IsReduced R
⊢ W.j = 0 ↔ W.a₁ = 0

Tactic:
rw [j_eq_zero_iff_of_char_two', pow_eq_zero_iff (Nat.succ_ne_zero _)]

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

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

Tactic:
by
  rw [nonsingular_iff, equation_neg, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]
  exact and_congr_right' <| (iff_congr not_and_or.symm not_and_or.symm).mpr <|
    not_congr <| and_congr_left fun h => by rw [← h]

Goal state after: