-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
theorem of_comp_isClosedImmersion {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion g]
    [IsClosedImmersion (f ≫ g)] : IsClosedImmersion f where
  base_closed

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Tactic:
intro Z hZ

Result:
X Y Z✝ : Scheme
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h :
  Function.Surjective
    ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
exact Function.Surjective.of_comp h

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsClosedEmbedding ⇑(ConcreteCategory.hom f.base)

Tactic:
simp only [Scheme.comp_coeBase, TopCat.coe_comp] at h

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
⊢ IsClosedEmbedding ⇑(ConcreteCategory.hom f.base)

Proof state:
X Y Z✝ : Scheme
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Tactic:
rw [IsClosedEmbedding.isClosed_iff_image_isClosed g.isClosedEmbedding,
  ← Set.image_comp]

Result:
X Y Z✝ : Scheme
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
⊢ IsClosed (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base) '' Z)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
have h := (f ≫ g).stalkMap_surjective x

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
simp_rw [Scheme.stalkMap_comp] at h

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h :
  Function.Surjective
    ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y Z✝ : Scheme
f : X ⟶ Y
g : Y ⟶ Z✝
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
⊢ IsClosed (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base) '' Z)

Tactic:
exact h.isClosedMap _ hZ

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
⊢ IsClosedEmbedding ⇑(ConcreteCategory.hom f.base)

Tactic:
refine .of_continuous_injective_isClosedMap (Scheme.Hom.continuous f) h.injective.of_comp ?_

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
⊢ IsClosedEmbedding ⇑(ConcreteCategory.hom f.base)

Tactic:
have h := (f ≫ g).isClosedEmbedding

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsClosedEmbedding ⇑(ConcreteCategory.hom f.base)