awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
inst : IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑i) (Set.range (ι := ↥X) ⇑f))
⊢ IsLocallyClosed (X := ↥Z) (Set.range (ι := ↥X) ⇑(f ≫ i))

Tactic:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑i) (Set.range (ι := ↥X) ⇑f))

Tactic:
hf.image i.homeomorph.isInducing ?_

Premises used: IsLocallyClosed.image, Homeomorph.isInducing, AlgebraicGeometry.Scheme.Hom.homeomorph
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
inst : IsLocallyClosed (X := ↥Z) (Set.range (ι := ↥Y) ⇑i)
⊢ IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑i) (Set.range (ι := ↥X) ⇑f))

Tactic:
refine hf.image i.homeomorph.isInducing ?_

Premises used: IsLocallyClosed.image, Homeomorph.isInducing, AlgebraicGeometry.Scheme.Hom.homeomorph
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
inst : IsLocallyClosed.{u_1} (X := ↥Z) Set.univ
⊢ IsLocallyClosed (X := ↥Z) (Set.range (ι := ↥Y) ⇑i)

Tactic:
rw [Set.range_eq_univ.mpr i.surjective]

Premises used: Iff.mpr, Set.range_eq_univ, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed.{u_1} (X := ↥Z) Set.univ

Tactic:
isOpen_univ.isLocallyClosed

Premises used: IsOpen.isLocallyClosed, isOpen_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ IsLocallyClosed.{u_1} (X := ↥Z) Set.univ

Tactic:
exact isOpen_univ.isLocallyClosed

Premises used: IsOpen.isLocallyClosed, isOpen_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
hP :
  ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f →
        (IsLocallyClosed (Set.range f) ↔
          ∀ (i : ι),
            IsLocallyClosed (X := (↑(U i).carrier : Type u_1))
              (Subtype.val (p := fun (x : β) ↦ x ∈ (U i).carrier) ⁻¹' Set.range f))
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f →
        (IsLocallyClosed (Set.range f) ↔ ∀ (i : ι), IsLocallyClosed (Set.range ((U i).carrier.restrictPreimage f)))

Tactic:
simp_rw [Set.range_restrictPreimage]

Premises used: Set.range_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ ∀ (f : α → β) {ι : Type u_1} (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f →
        (IsLocallyClosed (Set.range f) ↔
          ∀ (i : ι),
            IsLocallyClosed (X := (↑(U i).carrier : Type u_1))
              (Subtype.val (p := fun (x : β) ↦ x ∈ (U i).carrier) ⁻¹' Set.range f))

Tactic:
fun _ _ _ hU _ ↦ hU.isLocallyClosed_iff_coe_preimage

Premises used: Set.Mem, TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f →
        (IsLocallyClosed (Set.range f) ↔
          ∀ (i : ι),
            IsLocallyClosed (X := (↑(U i).carrier : Type u_1))
              (Subtype.val (p := fun (x : β) ↦ x ∈ (U i).carrier) ⁻¹' Set.range f))

Tactic:
exact fun _ _ _ hU _ ↦ hU.isLocallyClosed_iff_coe_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
⊢ IsImmersion (f ≫ g)

Tactic:
{ __ := (inferInstance : IsPreimmersion (f ≫ g)), isLocallyClosed_range := ?_ }

Premises used: inferInstance, AlgebraicGeometry.IsImmersion.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
refine : IsLocallyClosed (X := ↥Z) (Set.range (ι := ↥X) ⇑(f ≫ g))
⊢ IsImmersion (f ≫ g)

Tactic:
refine { __ := (inferInstance : IsPreimmersion (f ≫ g)), isLocallyClosed_range := ?_ }

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
simp : IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))
⊢ IsLocallyClosed (X := ↥Z) (Set.range (ι := ↥X) ⇑(f ≫ g))

Tactic:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
⊢ IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))

Tactic:
f.isLocallyClosed_range.image g.isEmbedding.isInducing g.isLocallyClosed_range

Premises used: IsLocallyClosed.image, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, Topology.IsEmbedding.isInducing, AlgebraicGeometry.Scheme.Hom.isEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
⊢ IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))

Tactic:
exact f.isLocallyClosed_range.image g.isEmbedding.isInducing g.isLocallyClosed_range

Premises used: IsLocallyClosed.image, AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range, Topology.IsEmbedding.isInducing, AlgebraicGeometry.Scheme.Hom.isEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsImmersion f
inst_1 : IsImmersion g
⊢ IsImmersion (f ≫ g)

Tactic:
MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsImmersion f ↔ ∃ (Z : Scheme.{u}) (g₁ : X ⟶ Z) (g₂ : Z ⟶ Y), IsClosedImmersion g₁ ∧ IsOpenImmersion g₂ ∧ g₁ ≫ g₂ = f

Tactic:
⟨fun _ ↦ ⟨_, f.liftCoborder, f.coborderRange.ι, inferInstance, inferInstance, f.liftCoborder_ι⟩,
    fun ⟨_, _, _, _, _, e⟩ ↦ e ▸ inferInstance⟩

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.Scheme.Hom.liftCoborder, AlgebraicGeometry.Scheme.Hom.coborderRange, AlgebraicGeometry.IsImmersion, And.intro, Iff.intro, Exists.intro, _private.0.AlgebraicGeometry.IsImmersion.isImmersion_iff_exists.match_1, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.liftCoborder_ι, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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 H.w.symm

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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) ⋯
refine_2 :
  ∀ (this : IsPullback e f' (pullback.snd f (Scheme.Hom.coborderRange g).ι) (Scheme.Hom.liftCoborder g)),
    IsClosedImmersion e
refine_1 :
  IsPullback (e ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι) f' f
    (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)
⊢ IsClosedImmersion e

Tactic:
have := (IsPullback.paste_horiz_iff (.of_hasPullback f g.coborderRange.ι)
        (show e ≫ Limits.pullback.snd _ _ = _ from Limits.pullback.lift_snd _ _ _)).mp ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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 : IsPullback e f' (pullback.snd f (Scheme.Hom.coborderRange g).ι) (Scheme.Hom.liftCoborder g)
⊢ IsClosedImmersion e

Tactic:
MorphismProperty.of_isPullback this.flip inferInstance

Premises used: CategoryTheory.MorphismProperty.of_isPullback, inferInstance, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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 : IsPullback e f' (pullback.snd f (Scheme.Hom.coborderRange g).ι) (Scheme.Hom.liftCoborder g)
⊢ IsClosedImmersion e

Tactic:
exact MorphismProperty.of_isPullback this.flip inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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 [e] using H.flip

Premises used: CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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) ⋯
⊢ IsClosedImmersion e

Tactic:
have : IsClosedImmersion e := by
      have := (IsPullback.paste_horiz_iff (.of_hasPullback f g.coborderRange.ι)
        (show e ≫ Limits.pullback.snd _ _ = _ from Limits.pullback.lift_snd _ _ _)).mp ?_
      · exact MorphismProperty.of_isPullback this.flip inferInstance
      · simpa [e] using H.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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 H.w.symm

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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
rw :
  IsImmersion
    (CategoryStruct.comp (Y := pullback f (Scheme.Hom.coborderRange g).ι)
      (pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯) (pullback.fst f (Scheme.Hom.coborderRange g).ι))
⊢ IsImmersion g'

Tactic:
rw [← Limits.pullback.lift_fst (f := f) (g := g.coborderRange.ι) g' (f' ≫ g.liftCoborder)
      (by simpa using H.w.symm)]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
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
    (CategoryStruct.comp (Y := pullback f (Scheme.Hom.coborderRange g).ι)
      (pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯) (pullback.fst f (Scheme.Hom.coborderRange g).ι))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : IsImmersion g
⊢ IsImmersion (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst _ _ ‹_›

Premises used: CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : IsImmersion f
⊢ IsImmersion (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd _ _ ‹_›

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
V : Y.Opens
inst : IsImmersion f
⊢ IsImmersion (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : IsImmersion f
⊢ IsImmersion (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
inst : IsImmersion f
rw : LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
⊢ LocallyOfFiniteType f

Tactic:
rw [← f.liftCoborder_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
inst : IsImmersion f
⊢ LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
⊢ pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤

Tactic:
have H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤ :=
    top_le_iff.mp fun _ _ ↦ range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ⟨_, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
⊢ IsClosedImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
    (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

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

Tactic:
have : IsImmersion ((pullback.diagonal f ∣_
    diagonalCoverDiagonalRange f 𝒰 𝒱) ≫ Scheme.Opens.ι _) := inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun (i : 𝒰.I₀) ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this_1 :
  IsClosedImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
    (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
this :
  IsImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
    (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱 ≫ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι)
rwa :
  ∀
    (this :
      IsImmersion (Y := pullback.diagonalObj f)
        ((pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱).ι ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
rwa₁ :
  ∀ (this : IsImmersion (X := (↑⊤ : Scheme)) (Y := pullback.diagonalObj f) (Scheme.Opens.ι ⊤ ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
rwa₂ :
  ∀ (this : IsImmersion (Y := pullback.diagonalObj f) (X.topIso.hom ≫ pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)),
    IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
rwa [morphismRestrict_ι, H, ← Scheme.topIso_hom,
    MorphismProperty.cancel_left_of_respectsIso (P := @IsImmersion)] at this

Premises used: AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.IsImmersion, AlgebraicGeometry.Scheme.topIso_hom, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
S T : Scheme
f : X ⟶ S
g : Y ⟶ S
i : S ⟶ T
⊢ IsImmersion (X := pullback f g) (Y := pullback (f ≫ i) (g ≫ i)) (pullback.mapDesc f g i)

Tactic:
MorphismProperty.of_isPullback (pullback_map_diagonal_isPullback f g i) inferInstance

Premises used: CategoryTheory.MorphismProperty.of_isPullback, inferInstance, CategoryTheory.Limits.pullback_map_diagonal_isPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ MorphismProperty.HasOfPostcompProperty @IsImmersion ⊤

Tactic:
MorphismProperty.hasOfPostcompProperty_iff_le_diagonal.mpr
    fun _ _ _ _ ↦ inferInstanceAs (IsImmersion _)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsImmersion (f ≫ g)
⊢ IsImmersion f

Tactic:
MorphismProperty.HasOfPostcompProperty.of_postcomp (W' := ⊤) _ g trivial ‹_›

Premises used: trivial, CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsImmersion g
⊢ IsImmersion (f ≫ g) ↔ IsImmersion f

Tactic:
⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.IsImmersion.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
rw :
  IsImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
⊢ IsImmersion (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rw [← MorphismProperty.cancel_right_of_respectsIso @IsImmersion _ (prodIsoPullback X X).hom]

Premises used: AlgebraicGeometry.IsImmersion, prodIsoPullback, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X)) (pullback.diagonal (terminal.from X))

Tactic:
(inferInstance : IsImmersion (pullback.diagonal (terminal.from X)))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
h :
  Eq (α := X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
⊢ IsImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))

Tactic:
convert! (inferInstance : IsImmersion (pullback.diagonal (terminal.from X)))

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
h :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X))
h₁ :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.snd (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X))
⊢ Eq (α := X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))

Tactic:
ext : 1