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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ (Opens.map (𝒰.f i).base).obj ((Opens.map f.base).obj (Y.basicOpen s)) ≤ 𝒰.f i ⁻¹ᵁ U

Tactic:
]

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ (Opens.map (𝒰.f i).base).obj ((Opens.map f.base).obj (Y.basicOpen s)) ≤ 𝒰.f i ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion (pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion ((pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv)

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion ((pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
⊢ ⊤ ≤ diagonalCoverDiagonalRange f 𝒰 𝒱

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
⊢ ⊤ ≤ diagonalCoverDiagonalRange f 𝒰 𝒱
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
⊢ (pullback.snd f f ≫ f) x = (pullback.snd f f ≫ f) x

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom
        ((X.presheaf.map w.op ≫ Scheme.Hom.appLE (𝒰.f i) U (𝒰.f i ⁻¹ᵁ U) ⋯) ≫ (𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom φ) g) =
    0

Tactic:
]

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom
        ((X.presheaf.map w.op ≫ Scheme.Hom.appLE (𝒰.f i) U (𝒰.f i ⁻¹ᵁ U) ⋯) ≫ (𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom φ) g) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
⊢ liftCoborder f ⁻¹ᵁ U = liftCoborder f ⁻¹ᵁ U

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(Scheme.Hom.coborderRange f)).Opens
⊢ Scheme.Hom.app (Scheme.Hom.liftCoborder f) U =
    (Scheme.Hom.app (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
          ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫
        X.presheaf.map (eqToHom ⋯).op) ≫
      X.presheaf.map (eqToHom ⋯).op

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(Scheme.Hom.coborderRange f)).Opens
⊢ Scheme.Hom.app (Scheme.Hom.liftCoborder f) U =
    (Scheme.Hom.app (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
          ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫
        X.presheaf.map (eqToHom ⋯).op) ≫
      X.presheaf.map (eqToHom ⋯).op
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑f = ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f

Tactic:
]

Goal state after:
case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑f = ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Dense ↑(Scheme.Hom.coborderRange f)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Dense ↑(Scheme.Hom.coborderRange f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ x ∈
    ⇑(pullback.fst f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ∩
      ⇑(pullback.snd f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ x ∈
    ⇑(pullback.fst f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ∩
      ⇑(pullback.snd f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom ((𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) U (𝒰.f i ⁻¹ᵁ U) ⋯)) 0) =
    0

Tactic:
]

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom ((𝒰.X i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) U (𝒰.f i ⁻¹ᵁ U) ⋯)) 0) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed Set.univ

Tactic:
]

Goal state after:
case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w) =
    ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i) ≫ pullback.diagonal f) w

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w) =
    ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i) ≫ pullback.diagonal f) w
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ 1 ∈ ⊤

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ 1 ∈ ⊤
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
⊢ IsImmersion (pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯ ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι)

Tactic:
]

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
⊢ IsImmersion (pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯ ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)

Tactic:
]

Goal state after:
X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this✝ : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this : IsImmersion (pullback.diagonal f)
⊢ IsImmersion (pullback.diagonal f)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this✝ : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this : IsImmersion (pullback.diagonal f)
⊢ IsImmersion (pullback.diagonal f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : ∑ i ∈ s.attach, l i • ↑i = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0

pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ l ∈ Finsupp.supported S S ↑s.attach

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : ∑ i ∈ s.attach, l i • ↑i = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0

R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ l ∈ Finsupp.supported S S ↑s.attach
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
i : 𝒰.I₀
n : ℕ
hn :
  (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (Scheme.Hom.app (𝒰.f i) ⊤).hom' ((ConcreteCategory.hom φ) g) =
    0
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) g) =
    0

Tactic:
]

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
i : 𝒰.I₀
n : ℕ
hn :
  (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (Scheme.Hom.app (𝒰.f i) ⊤).hom' ((ConcreteCategory.hom φ) g) =
    0
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) g) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ (Hom.ker f).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ (Hom.ker f).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : ∑ i ∈ s.attach, l i • ↑i = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - ∑ i ∈ s.attach, l i • ↑i) * f q = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : ∑ i ∈ s.attach, l i • ↑i = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - ∑ i ∈ s.attach, l i • ↑i) * f q = 0