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

Goal state before:
pp: X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
        map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField))) ≫
      𝟙 (Spec (CommRingCat.of R)) =
    map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
      map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField))

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f ((Scheme.SpecToEquivOfField K Y).symm ⟨y, φ⟩)
⊢ P Z

Tactic:
let p : Z ⟶ f.fiber y :=
    pullback.lift fst (snd ≫ Spec.map φ) (by simp [h.w, Scheme.SpecToEquivOfField])

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f ((Scheme.SpecToEquivOfField K Y).symm ⟨y, φ⟩)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ P Z
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ map (CommRingCat.ofHom (algebraMap R S)) ≫ 𝟙 (Spec (CommRingCat.of R)) =
    𝟙 (Spec (CommRingCat.of S)) ≫ map (CommRingCat.ofHom (algebraMap R S))

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ X.fromSpecResidueField x ≫ f = Spec.map (residueFieldMap f x) ≫ Y.fromSpecResidueField (f x)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
x : ↥X
⊢ x ∈ ⊤

Tactic:
by simp

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

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsIso f
⊢ Scheme.Hom.ker f = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
H✝ : IsSchemeTheoreticallyDominant g
H :
  IsPullback
    (Cofan.IsColimit.desc (coproductIsCoproduct fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)) fun x ↦
      pullback.fst f (Y.fromSpecStalk ⋯.genericPoint))
    (Cofan.IsColimit.desc (coproductIsCoproduct fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)) fun x ↦
      pullback.snd f (Y.fromSpecStalk ⋯.genericPoint) ≫
        (Cofan.mk (∐ fun Z ↦ Spec (pt Z)) (Sigma.ι fun Z ↦ Spec (pt Z))).inj x)
    f g
⊢ IsReduced (pullback f g)

Tactic:
apply +allowSynthFailures @isReduced_of_isOpenImmersion (f := H.isoPullback.inv)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := ⋯
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := ⋯
Z : Scheme := ⋯
g : Z ⟶ Y := ⋯
this✝ : Finite ↥Z
this : QuasiCompact g
H✝ : IsSchemeTheoreticallyDominant g
H :
  IsPullback
    (Cofan.IsColimit.desc (coproductIsCoproduct fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)) fun x ↦
      pullback.fst f (Y.fromSpecStalk ⋯.genericPoint))
    (Cofan.IsColimit.desc (coproductIsCoproduct fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)) fun x ↦
      pullback.snd f (Y.fromSpecStalk ⋯.genericPoint) ≫
        (Cofan.mk (∐ fun Z ↦ Spec (pt Z)) (Sigma.ι fun Z ↦ Spec (pt Z))).inj x)
    f g
⊢ IsReduced
    (Cofan.mk (∐ fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint))
        (Sigma.ι fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint))).pt
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
s : ↥S
K : Type u
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
⊢ (f ≫ g) ≫ 𝟙 S = f ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
s : ↥S
K : Type u
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
⊢ S.fromSpecResidueField s ≫ 𝟙 S = 𝟙 (Spec (S.residueField s)) ≫ S.fromSpecResidueField s

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
s : ↥S
K : Type u
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
⊢ x ≫ 𝟙 (Spec (S.residueField s)) = 𝟙 (Spec (CommRingCat.of K)) ≫ x

Tactic:
by simp

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ i ∈ σ, (pullback.fst f q) z ∉ (U i).carrier
this : ∀ (i : 𝒰.I₀), t ∈ (Opens.comap { toFun := comap φ, continuous_toFun := ⋯ }) (Ti i) → p z ∉ U i
⊢ z ∈ Z

Tactic:
simpa [Z, p, fT, hzr]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
y : ↥Y
this : CompactSpace ↥(pullback f (Y.fromSpecResidueField y))
⊢ IsCompact (Set.range ⇑(pullback.fst f (Y.fromSpecResidueField y)))

Tactic:
exact isCompact_range (Scheme.Hom.continuous _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (Y.presheaf.map (homOfLE ⋯).op).op ≫ (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(Y, ⊤)))).hom =
    ⋯.isoSpec.symm.hom ≫ Y.openCoverBasicOpenTop.f r ≫ Y.toSpecΓ

Tactic:
by simp

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
x✝ : IsIso (pushoutSection H hUST hUSX hUY)
⊢ Scheme.Hom.appLE iX US UX hUSX ≫ (Iso.refl Γ(X, UX)).hom = (Iso.refl Γ(S, US)).hom ≫ Scheme.Hom.appLE iX US UX hUSX

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (Hom.appTop f).op ≫ (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(Y, ⊤)))).hom =
    (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))).hom ≫ Spec.map (Hom.appTop f)

Tactic:
by simp

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
x✝ : IsIso (pushoutSection H hUST hUSX hUY)
⊢ Scheme.Hom.appLE f US UT hUST ≫ (Iso.refl Γ(T, UT)).hom = (Iso.refl Γ(S, US)).hom ≫ Scheme.Hom.appLE f US UT hUST

Tactic:
by simp

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
x✝ : IsIso (pushoutSection H hUST hUSX hUY)
⊢ pushout.inl (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≫
      (asIso (pushoutSection H hUST hUSX hUY)).hom =
    (Iso.refl Γ(X, UX)).hom ≫ Scheme.Hom.appLE g UX UY ⋯

Tactic:
by simp

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
x✝ : IsIso (pushoutSection H hUST hUSX hUY)
⊢ pushout.inr (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≫
      (asIso (pushoutSection H hUST hUSX hUY)).hom =
    (Iso.refl Γ(T, UT)).hom ≫ Scheme.Hom.appLE iY UT UY ⋯

Tactic:
by simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE iY UT UY ⋯ ≫ hUT.isoSpec.hom =
    hUY'.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE ⋯).op))

Tactic:
by simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE g UX UY ⋯ ≫ hUX.isoSpec.hom =
    hUY'.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE ⋯).op))

Tactic:
by simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE f US UT hUST ≫ hUS.isoSpec.hom =
    hUT.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app f US ≫ T.presheaf.map (homOfLE hUST).op))

Tactic:
by simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE iX US UX hUSX ≫ hUS.isoSpec.hom =
    hUX.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app iX US ≫ X.presheaf.map (homOfLE hUSX).op))

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp

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
ι : 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 : ↑Γ(X, UX)
⊢ ∀ ⦃a₂ : ↑Γ(X, UX)⦄, ψ s = ψ a₂ → s = a₂

Tactic:
t

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)
⊢ ψ s = ψ t → s = t
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
⊢ s.π.app (Classical.arbitrary I) ≫ α.app (Classical.arbitrary I) =
    hcG.lift ((Cone.postcompose α).obj s) ≫ cG.π.app (Classical.arbitrary I)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j i : I
⊢ s.π.app i ≫ α.app i = hcG.lift ((Cone.postcompose α).obj s) ≫ cG.π.app i

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
⊢ cF.ι.app (Classical.arbitrary I) ≫ hcF.desc ((Cocone.precompose α).obj s) =
    α.app (Classical.arbitrary I) ≫ s.ι.app (Classical.arbitrary I)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j i : I
⊢ cF.ι.app i ≫ hcF.desc ((Cocone.precompose α).obj s) = α.app i ≫ s.ι.app i

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mp.inr.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
this : ∀ {n : Type u} (S : Scheme), IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↥S → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
x : ↥S
⊢ IsEmpty n

Tactic:
obtain ⟨y, hy⟩ := S.affineCover.covers x

Goal state after:
case mp.inr.inr
n : Type u
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↥S
this : ∀ {n : Type u} (S : Scheme), IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↥S → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
x : ↥S
y : ↥(S.affineCover.X (Scheme.Cover.idx S.affineCover x))
hy : (S.affineCover.f (Scheme.Cover.idx S.affineCover x)) y = x
⊢ IsEmpty n
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x✝ : ↥X
hx : IsClosed {x✝}
x : ↑(closedPoints ↥X)
⊢ (fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) ((fun x ↦ ⟨pointOfClosedPoint f ↑x ⋯, ⋯⟩) x) = x

Tactic:
by simp

Goal state after:
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
⊢ (support fun x ↦ 0) ⊆ U

Tactic:
by simp

Goal state after:
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
x✝¹ x✝ : locallyFinsuppWithin U Y
toFun✝¹ : X → Y
supportWithinDomain'✝¹ : support toFun✝¹ ⊆ U
supportLocallyFiniteWithinDomain'✝¹ : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support toFun✝¹).Finite
toFun✝ : X → Y
supportWithinDomain'✝ : support toFun✝ ⊆ U
supportLocallyFiniteWithinDomain'✝ : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support toFun✝).Finite
⊢ (fun D ↦ D.toFun)
        { toFun := toFun✝¹, supportWithinDomain' := supportWithinDomain'✝¹,
          supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝¹ } =
      (fun D ↦ D.toFun)
        { toFun := toFun✝, supportWithinDomain' := supportWithinDomain'✝,
          supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝ } →
    { toFun := toFun✝¹, supportWithinDomain' := supportWithinDomain'✝¹,
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝¹ } =
      { toFun := toFun✝, supportWithinDomain' := supportWithinDomain'✝,
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝ }

Tactic:
by simp

Goal state after:
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
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
⊢ ⇑D =ᶠ[codiscreteWithin U] 0

Tactic:
apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
  have : D.support = (U \ {x | D x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_sdiff, Set.mem_ofPred_eq, iff_and_self]
    exact (support_subset_iff.1 D.supportWithinDomain) x
  rw [← this]
  exact D.supportLocallyFiniteWithinDomain

Goal state after: