awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
⊢ liftCoborder f ⁻¹ᵁ U = f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
have conv_rhs : liftCoborder f ⁻¹ᵁ U = (liftCoborder f ≫ (coborderRange f).ι) ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
Tactic: conv_rhs => enter [1]; rw [← f.liftCoborder_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
⊢ liftCoborder f ⁻¹ᵁ U = (liftCoborder f ≫ (coborderRange f).ι) ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
have rw : liftCoborder f ⁻¹ᵁ U = liftCoborder f ⁻¹ᵁ (coborderRange f).ι ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
Tactic: rw [Scheme.Hom.comp_preimage, Scheme.Hom.preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
rw : liftCoborder f ⁻¹ᵁ U = liftCoborder f ⁻¹ᵁ (coborderRange f).ι ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
⊢ liftCoborder f ⁻¹ᵁ U = (liftCoborder f ≫ (coborderRange f).ι) ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
have rw₁ : liftCoborder f ⁻¹ᵁ U = liftCoborder f ⁻¹ᵁ U
Tactic: rw [Scheme.Hom.comp_preimage, Scheme.Hom.preimage_image_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(Scheme.Hom.coborderRange f) : Scheme).Opens
⊢ Scheme.Hom.app (Scheme.Hom.liftCoborder f) U =
    Scheme.Hom.app f ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have rw : 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 (Quiver.Hom.op (eqToHom sorry))) ≫
    X.presheaf.map (Quiver.Hom.op (eqToHom sorry))
Tactic: rw [Scheme.Hom.congr_app (f.liftCoborder_ι).symm (f.coborderRange.ι ''ᵁ U)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
have simp : IsPreimmersion f
Tactic: simp only [Scheme.Hom.liftCoborder_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ IsClosedImmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
have this : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
Tactic: have : IsPreimmersion (f.liftCoborder ≫ f.coborderRange.ι) := by
    simp only [Scheme.Hom.liftCoborder_ι]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
this : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
⊢ IsClosedImmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
have this₁ : IsPreimmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
Tactic: have : IsPreimmersion f.liftCoborder := .of_comp f.liftCoborder f.coborderRange.ι
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
this_1 : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
⊢ IsClosedImmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
have refine : IsClosed (X := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f))
Tactic: refine .of_isPreimmersion _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
this_1 : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
⊢ IsClosed (X := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f))
have h : Eq (α := Set ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f))
  (Subtype.val (p := fun (x : ↥Y) ↦ Membership.mem (γ := Set ↥Y) (coborder (Set.range (ι := ↥X) ⇑f)) x) ⁻¹'
    Set.range (ι := ↥X) ⇑f)
Tactic: convert! isClosed_preimage_val_coborder
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
this_1 : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
⊢ Eq (α := Set ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f))
    (Subtype.val (p := fun (x : ↥Y) ↦ Membership.mem (γ := Set ↥Y) (coborder (Set.range (ι := ↥X) ⇑f)) x) ⁻¹'
      Set.range (ι := ↥X) ⇑f)
have h : Eq (α := Set ↥Y)
  (Set.image (α := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (⇑(Scheme.Hom.coborderRange f).ι)
    (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f)))
  (Set.image (α := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (⇑(Scheme.Hom.coborderRange f).ι)
    (Subtype.val (p := fun (x : ↥Y) ↦ Membership.mem (γ := Set ↥Y) (coborder (Set.range (ι := ↥X) ⇑f)) x) ⁻¹'
      Set.range (ι := ↥X) ⇑f))
Tactic: apply Set.image_injective.mpr f.coborderRange.ι.isEmbedding.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
this_1 : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)
⊢ Eq (α := Set ↥Y)
    (Set.image (α := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (⇑(Scheme.Hom.coborderRange f).ι)
      (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f)))
    (Set.image (α := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (⇑(Scheme.Hom.coborderRange f).ι)
      (Subtype.val (p := fun (x : ↥Y) ↦ Membership.mem (γ := Set ↥Y) (coborder (Set.range (ι := ↥X) ⇑f)) x) ⁻¹'
        Set.range (ι := ↥X) ⇑f))
have h : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
  (Set.image (α := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (⇑(Scheme.Hom.coborderRange f).ι)
    (Subtype.val (p := fun (x : ↥Y) ↦ Membership.mem (γ := Set ↥Y) (coborder (Set.range (ι := ↥X) ⇑f)) x) ⁻¹'
      Set.range (ι := ↥X) ⇑f))
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.liftCoborder_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ IsDominant (Scheme.Hom.coborderRange f).ι
have rw : Dense (↑(Scheme.Hom.coborderRange f) : Set ↥Y)
Tactic: rw [isDominant_iff, DenseRange, Scheme.Opens.range_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
⊢ @IsImmersion =
    @IsPreimmersion ⊓
      topologically fun {x x_1 : Type u_1} (x_2 : TopologicalSpace x) (x_3 : TopologicalSpace x_1) (f : x → x_1) ↦
        IsLocallyClosed (Set.range f)
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  IsImmersion x_2 ↔
    (@IsPreimmersion ⊓
        topologically fun {x x_3 : Type u_1} (x_4 : TopologicalSpace x) (x_5 : TopologicalSpace x_3) (f : x → x_3) ↦
          IsLocallyClosed (Set.range f))
      x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget @IsImmersion
have suffices : IsZariskiLocalAtTarget.{u_1}
  (topologically fun {X Y : Type u_1} (x : TopologicalSpace X) (x_1 : TopologicalSpace Y) (f : X → Y) ↦
    IsLocallyClosed (Set.range f))
Tactic: suffices IsZariskiLocalAtTarget
      (topologically fun {X Y} _ _ f ↦ IsLocallyClosed (Set.range f)) from
    isImmersion_eq_inf ▸ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {X Y : Type u_1} (x : TopologicalSpace X) (x_1 : TopologicalSpace Y) (f : X → Y) ↦
      IsLocallyClosed (Set.range f))
have inst : (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦
    IsLocallyClosed (Set.range f)).RespectsIso
Tactic: apply +allowSynthFailures topologically_isZariskiLocalAtTarget'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst :
  (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦
      IsLocallyClosed (Set.range f)).RespectsIso
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {X Y : Type u_1} (x : TopologicalSpace X) (x_1 : TopologicalSpace Y) (f : X → Y) ↦
      IsLocallyClosed (Set.range f))
have 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 (Set.range ((U i).carrier.restrictPreimage f)))
Tactic: apply +allowSynthFailures topologically_isZariskiLocalAtTarget'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦
      IsLocallyClosed (Set.range f)).RespectsIso
have inst : ∀ {X Y Z : Scheme.{u_1}} (i : X ⟶ Y) (hi : MorphismProperty.isomorphisms Scheme i) (f : Y ⟶ Z)
  (hf :
    topologically
      (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f),
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) (i ≫ f)
Tactic: refine { precomp := ?_, postcomp := ?_ }
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst :
  ∀ {X Y Z : Scheme.{u_1}} (i : X ⟶ Y) (hi : MorphismProperty.isomorphisms Scheme i) (f : Y ⟶ Z)
    (hf :
      topologically
        (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f),
    topologically
      (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f))
      (i ≫ f)
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦
      IsLocallyClosed (Set.range f)).RespectsIso
have inst₁ : ∀ {X Y Z : Scheme.{u_1}} (i : Y ⟶ Z) (hi : MorphismProperty.isomorphisms Scheme i) (f : X ⟶ Y)
  (hf :
    topologically
      (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f),
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) (f ≫ i)
Tactic: refine { precomp := ?_, postcomp := ?_ }
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : X ⟶ Y
hi : MorphismProperty.isomorphisms Scheme i
f : Y ⟶ Z
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
⊢ topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) (i ≫ f)
have hi₁ : IsIso i
Tactic: change IsIso i at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
i : Y ⟶ Z
hi : MorphismProperty.isomorphisms Scheme i
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
⊢ topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) (f ≫ i)
have hi₁ : IsIso i
Tactic: change IsIso i at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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.range (ι := ↥X) ⇑(f ≫ i))
have inst : IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑i) (Set.range (ι := ↥X) ⇑f))
Tactic: simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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))
have inst : IsLocallyClosed (X := ↥Z) (Set.range (ι := ↥Y) ⇑i)
Tactic: refine hf.image i.homeomorph.isInducing ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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.range (ι := ↥Y) ⇑i)
have inst : IsLocallyClosed.{u_1} (X := ↥Z) Set.univ
Tactic: rw [Set.range_eq_univ.mpr i.surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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 (Set.range ((U i).carrier.restrictPreimage f)))
have 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))
Tactic: simp_rw [Set.range_restrictPreimage]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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)
have refine : IsLocallyClosed (X := ↥Z) (Set.range (ι := ↥X) ⇑(f ≫ g))
Tactic: refine { __ := (inferInstance : IsPreimmersion (f ≫ g)), isLocallyClosed_range := ?_ }
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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.range (ι := ↥X) ⇑(f ≫ g))
have simp : IsLocallyClosed (X := ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥X) ⇑f))
Tactic: simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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
have refine_2 : ∀ (this : IsPullback e f' (pullback.snd f (Scheme.Hom.coborderRange g).ι) (Scheme.Hom.liftCoborder 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 ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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
⊢ IsClosedImmersion e
have refine_1 : IsPullback (e ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι) f' f
  (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)
Tactic: have := (IsPullback.paste_horiz_iff (.of_hasPullback f g.coborderRange.ι)
        (show e ≫ Limits.pullback.snd _ _ = _ from Limits.pullback.lift_snd _ _ _)).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
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) ⋯
⊢ IsImmersion g'
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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 g'
have rw : IsImmersion
  (CategoryStruct.comp (Y := pullback f (Scheme.Hom.coborderRange g).ι)
    (pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) sorry) (pullback.fst f (Scheme.Hom.coborderRange g).ι))
Tactic: rw [← Limits.pullback.lift_fst (f := f) (g := g.coborderRange.ι) g' (f' ≫ g.liftCoborder)
      (by simpa using H.w.symm)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
inst : IsImmersion f
⊢ LocallyOfFiniteType f
have rw : LocallyOfFiniteType (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
Tactic: rw [← f.liftCoborder_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
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
⊢ IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
Tactic: have H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤ :=
    top_le_iff.mp fun _ _ ↦ range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
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 𝒰 𝒱 = ⊤
⊢ IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have this : IsClosedImmersion (X := (↑(pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme))
  (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
Tactic: have := isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (hypothesis)
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 (Y := pullback.diagonalObj f) (pullback.diagonal f)
have this₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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 𝒰 𝒱).ι)
⊢ IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have rwa : ∀
  (this :
    IsImmersion (Y := pullback.diagonalObj f)
      ((pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Immersion (goal)
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)
⊢ IsImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have rwa₁ : ∀ (this : IsImmersion (X := (↑⊤ : Scheme)) (Y := pullback.diagonalObj f) (Scheme.Opens.ι ⊤ ≫ 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
Cleared hypotheses: this