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

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField (Triplet.ofPoint t).y =
    Spec.map (Hom.residueFieldMap (pullback.snd f g) t) ≫ Y.fromSpecResidueField ((pullback.snd f g) t)

Tactic:
← pushout.inr_desc _ _ (residueFieldCongr_inv_residueFieldMap_ofPoint t),

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ Spec.map (Triplet.ofPoint t).tensorInr ≫ Y.fromSpecResidueField (Triplet.ofPoint t).y =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x)
            ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y) ≫
          pushout.desc (Hom.residueFieldMap (pullback.fst f g) t) (Hom.residueFieldMap (pullback.snd f g) t) ⋯) ≫
      Y.fromSpecResidueField ((pullback.snd f g) t)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y✝ Z Y : Scheme
f g : (Over Y)ᵒᵖ
hfg : f ⟶ g
⊢ Hom.ker (Opposite.unop f).hom ≤ Hom.ker (Opposite.unop g).hom

Tactic:
simpa using

Goal state after:
X Y✝ Z Y : Scheme
f g : (Over Y)ᵒᵖ
hfg : f ⟶ g
⊢ Hom.ker (Opposite.unop f).hom ≤ Hom.ker (Over.Hom.left hfg.unop ≫ (Opposite.unop f).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen
    (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appIso U.ι ⊤).inv) ((ConcreteCategory.hom U.topIso.inv) j)))

Tactic:
simpa using

Goal state after:
case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : ↑Γ(X, U)
hj : j ∈ s
⊢ IsAffineOpen (X.basicOpen j)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ = inv (X.homOfLE ⋯)

Tactic:
← hom_comp_eq_id

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑U ⊓ ↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
x : ↥Y
x✝ : x ∈ ⊤
⊢ x ∈ ⨆ i, ↑⟨U i, ⋯⟩

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
x : ↥Y
x✝ : x ∈ ⊤
⊢ ∃ i, x ∈ U i
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
⊢ IsAffineOpen (coprod.desc f g ⁻¹ᵁ W)

Tactic:
have : IsAffine (f ⁻¹ᵁ W).toScheme := hW.preimage f

Goal state after:
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this : IsAffine ↑(f ⁻¹ᵁ W)
⊢ IsAffineOpen (coprod.desc f g ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : (coprodMk U V) (Sum.inl x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ f x ∈ W

Tactic:
simpa using

Goal state after:
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : (coprodMk U V) (Sum.inl x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ f x ∈ W
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : (coprodMk U V) (Sum.inr x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ g x ∈ W

Tactic:
simpa using

Goal state after:
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : (coprodMk U V) (Sum.inr x) ∈ coprod.desc f g ⁻¹ᵁ W
⊢ g x ∈ W
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Submonoid R
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
ha : a ∈ ↑M
e : ⟨(algebraMap R S) a, ⋯⟩ • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ ⟨a, ha⟩ • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Submonoid R
S' : Type u_4
inst✝⁴ : CommRing S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
ha : a ∈ ↑M
e : ⟨(algebraMap R S) a, ⋯⟩ • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ a • x ∈ Algebra.adjoin R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a.inl
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : x ∈ f ⁻¹ᵁ W
⊢ i ((coprodMk ↑(f ⁻¹ᵁ W) ↑(g ⁻¹ᵁ W)) (Sum.inl ⟨x, hx⟩)) ∈ coprod.desc f g ⁻¹ᵁ W

Tactic:
simpa using

Goal state after:
case a.inl
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : x ∈ f ⁻¹ᵁ W
⊢ f x ∈ W
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a.inr
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : x ∈ g ⁻¹ᵁ W
⊢ i ((coprodMk ↑(f ⁻¹ᵁ W) ↑(g ⁻¹ᵁ W)) (Sum.inr ⟨x, hx⟩)) ∈ coprod.desc f g ⁻¹ᵁ W

Tactic:
simpa using

Goal state after:
case a.inr
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : x ∈ g ⁻¹ᵁ W
⊢ g x ∈ W
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
U' : Set ↥Y
hU' : IsOpen U'
e : ⇑f ⁻¹' U' = V.carrier
⊢ ↑(f ⁻¹ᵁ ({ carrier := U', is_open' := hU' } ⊓ U)) = ↑V

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
U' : Set ↥Y
hU' : IsOpen U'
e : ⇑f ⁻¹' U' = V.carrier
⊢ ↑V ⊆ ⇑f ⁻¹' ↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
hrU' : Y.basicOpen r ≤ U'
hxr : ↑⟨f x, hxV⟩ ∈ Y.basicOpen r
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r) =
    X.basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app f U ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE hU'U).op.unop).op))
        r)

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
hrU' : Y.basicOpen r ≤ U'
hxr : ↑⟨f x, hxV⟩ ∈ Y.basicOpen r
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r) ≤ f ⁻¹ᵁ U'
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) →
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

Tactic:
intro H U V hU hV
    dsimp at H
    have : IsAffine _ := hU
    have : IsAffine _ := hV
    let g : pullback U.ι V.ι ⟶ X := pullback.fst _ _ ≫ U.ι
    have := IsOpenImmersion.isPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right)
      U.ι V.ι (by simp) (by ext; simp)
    exact .of_isIso this.isoPullback.hom

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

Goal state before:
pp: case refine_1
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
⊢ Q
    ((RingHom.fst ↑Γ(U, f ⁻¹ᵁ W) ↑Γ(V, g ⁻¹ᵁ W)).comp
      (CommRingCat.Hom.hom
        ((Scheme.Hom.app (Limits.coprod.desc f g) W ≫ e.hom) ≫
          ((Limits.limit.isLimit (Limits.pair Γ(U, f ⁻¹ᵁ W) Γ(V, g ⁻¹ᵁ W))).conePointUniqueUpToIso
              (Γ(U, f ⁻¹ᵁ W).prodFanIsLimit Γ(V, g ⁻¹ᵁ W))).hom)))

Tactic:
have : (Limits.coprod.desc f g).app W ≫ e.hom ≫ Limits.prod.fst = f.app W := by
      simp [e, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE]
    convert! (hf W hW).2
    exact congr(($this).1)

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (pullback.lift iX Zf h)
⊢ IsPullback iX Zf f iY

Tactic:
simpa using

Goal state after:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst✝¹ : IsClosedImmersion iX
inst✝ : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (pullback.lift iX Zf h)
⊢ IsPullback iX Zf f iY
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
⊢ IsIso (Scheme.Hom.imageι f)

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
⊢ IsIso (Scheme.Hom.ker f).subschemeι
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h✝ : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h✝ True.intro
h : IsIso f'.op
⊢ IsIso f

Tactic:
rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h

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

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso ((overEquivIdealSheafData X).functor.map f'.op)

Tactic:
simpa using

Goal state after:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso (homOfLE ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop X.toSpecΓ))

Tactic:
simpa using

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, ⊤)).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
H : IsAffineHom (f ∣_ ↑U)
⊢ IsSeparated (f ∣_ ↑U)

Tactic:
exact this _ U.2

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

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
⊢ g' ≫ f = (f' ≫ Scheme.Hom.liftCoborder g) ≫ (Scheme.Hom.coborderRange g).ι

Tactic:
simpa using

Goal state after:
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
⊢ g' ≫ f = f' ≫ g
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsPullback (e ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι) f' f
    (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Tactic:
simpa using

Goal state after:
case refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsPullback g' f' f g
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ g' ≫ f = (f' ≫ Scheme.Hom.liftCoborder g) ≫ (Scheme.Hom.coborderRange g).ι

Tactic:
simpa using

Goal state after:
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ g' ≫ f = f' ≫ g
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e : R✝ ≃+* S✝
⊢ (ker e.toRingHom).FG

Tactic:
by simpa using! Submodule.fg_bot

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

Goal state before:
pp: case inr.mp
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
i : ℕ
hi : i < ((LinearMap.mul R A) f).charpoly.natDegree
e :
  (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i
⊢ ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

Tactic:
simpa using

Goal state after:
case inr.mp
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
i : ℕ
hi : i < ((LinearMap.mul R A) f).charpoly.natDegree
e :
  (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i
⊢ ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mpr.inr.inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : i < ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

Tactic:
simpa using

Goal state after:
case inr.mpr.inr.inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : i < ((LinearMap.mul R A) f).charpoly.natDegree
⊢ ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
x✝ : ↑↑t
⊢ IsCompact (zeroLocus {↑x✝})ᶜ

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
x✝ : ↑↑t
⊢ IsCompact (zeroLocus {↑x✝})ᶜ
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
this✝¹ : IsArtinianRing ↑Γ(X, W)
this✝ : DiscreteTopology ↥(Spec Γ(X, W))
this : DiscreteTopology ↥↑W
⊢ IsOpen {x}

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
this✝¹ : IsArtinianRing ↑Γ(X, W)
this✝ : DiscreteTopology ↥(Spec Γ(X, W))
this : DiscreteTopology ↥↑W
⊢ IsOpen {x}
Module: Mathlib.AlgebraicGeometry.Artinian

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

Tactic:
simpa using

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.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
⊢ IsReduced X

Tactic:
have H : IsSchemeTheoreticallyDominant g := by
    rw [isSchemeTheoreticallyDominant_iff_isDominant, isDominant_iff, denseRange_iff_closure_range,
      Set.eq_univ_iff_forall]
    intro y
    let z : Z := Sigma.ι (fun Z ↦ Spec (pt Z)) ⟨_, irreducibleComponent_mem_irreducibleComponents y⟩
      (IsLocalRing.closedPoint _)
    have hz : g z ⤳ y := by
      simp only [g, z, Z, ← Scheme.Hom.comp_apply, Sigma.ι_desc, pt,
        Scheme.fromSpecStalk_closedPoint]
      exact (IsIrreducible.isGenericPoint_genericPoint _
        isClosed_irreducibleComponent).specializes mem_irreducibleComponent
    exact hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)

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 := 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
⊢ IsReduced X