awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
this :
  Eq (α := Spec (CommRingCat.of R) ⟶ X)
    (Spec.map (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)
    (Spec.map (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)
⊢ Eq (α := CommRingCat.of (↑(X.presheaf.1 (op V)) : Type u) ⟶ CommRingCat.of R)
    (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))

Tactic:
rw [cancel_mono, Spec.map_inj] at this

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Spec.map_inj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
this :
  Eq (α := CommRingCat.of (↑(X.presheaf.1 (op V)) : Type u) ⟶ CommRingCat.of R)
    (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
⊢ g₁ = g₂

Tactic:
AlgHom.ext fun x ↦ congr($this x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, AlgHom.ext, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
this :
  Eq (α := CommRingCat.of (↑(X.presheaf.1 (op V)) : Type u) ⟶ CommRingCat.of R)
    (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
⊢ g₁ = g₂

Tactic:
exact AlgHom.ext fun x ↦ congr($this x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, AlgHom.ext, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ IsLocallyClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)

Tactic:
IsImmersion.isLocallyClosed_range

Premises used: AlgebraicGeometry.IsImmersion.isLocallyClosed_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
inst : IsImmersion f
⊢ Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥(↑(coborderRange f) : Scheme)) ⇑(coborderRange f).ι)

Tactic:
simpa using subset_coborder

Premises used: subset_coborder
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ liftCoborder f ≫ (coborderRange f).ι = f

Tactic:
IsOpenImmersion.lift_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
enter : TopologicalSpace.Opens.map f.base
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
enter [1]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
rw : TopologicalSpace.Opens.map (liftCoborder f ≫ (coborderRange f).ι).base
| TopologicalSpace.Opens.map f.base

Tactic:
rw [← f.liftCoborder_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
enter : TopologicalSpace.Opens.map (liftCoborder f ≫ (coborderRange f).ι).base
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
enter [1]; rw [← f.liftCoborder_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(coborderRange f) : Scheme).Opens
conv_rhs : liftCoborder f ⁻¹ᵁ U = (liftCoborder f ≫ (coborderRange f).ι) ⁻¹ᵁ (coborderRange f).ι ''ᵁ U
⊢ liftCoborder f ⁻¹ᵁ U = f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
conv_rhs => enter [1]; rw [← f.liftCoborder_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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
rw₁ rw₂ : liftCoborder f ⁻¹ᵁ U = liftCoborder f ⁻¹ᵁ U
⊢ liftCoborder f ⁻¹ᵁ U = (liftCoborder f ≫ (coborderRange f).ι) ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
rw [Scheme.Hom.comp_preimage, Scheme.Hom.preimage_image_eq]

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq, AlgebraicGeometry.Scheme.Hom.comp_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
U : (↑(Scheme.Hom.coborderRange f) : Scheme).Opens
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 ⋯))) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
⊢ Scheme.Hom.app (Scheme.Hom.liftCoborder f) U =
    Scheme.Hom.app f ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rw [Scheme.Hom.congr_app (f.liftCoborder_ι).symm (f.coborderRange.ι ''ᵁ U)]

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.coborderRange, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.liftCoborder_ι, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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 (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
          ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
simp [Scheme.Hom.app_eq f.liftCoborder (f.coborderRange.ι.preimage_image_eq U),
    ← Functor.map_comp_assoc, -Functor.map_comp, Subsingleton.elim _ (𝟙 _)]

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq, CategoryTheory.CategoryStruct.id, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.Scheme.Hom.liftCoborder, AlgebraicGeometry.Scheme.Hom.coborderRange, CategoryTheory.Functor.map_comp_assoc, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Functor.map_comp, Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
simp : IsPreimmersion f
⊢ IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)

Tactic:
simp only [Scheme.Hom.liftCoborder_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.liftCoborder_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ IsPreimmersion f

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

Tactic:
have : IsPreimmersion (f.liftCoborder ≫ f.coborderRange.ι) := by
    simp only [Scheme.Hom.liftCoborder_ι]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
this : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
⊢ IsPreimmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)

Tactic:
have : IsPreimmersion f.liftCoborder := .of_comp f.liftCoborder f.coborderRange.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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)

Tactic:
.of_isPreimmersion _ ?_

Premises used: AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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)
refine : IsClosed (X := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f))
⊢ IsClosedImmersion (Y := (↑(Scheme.Hom.coborderRange f) : Scheme)) (Scheme.Hom.liftCoborder f)

Tactic:
refine .of_isPreimmersion _ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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 := (↑(coborder (Set.range (ι := ↥X) ⇑f)) : Type u))
    (Subtype.val (p := fun (x : ↥Y) ↦ Membership.mem (γ := Set ↥Y) (coborder (Set.range (ι := ↥X) ⇑f)) x) ⁻¹'
      Set.range (ι := ↥X) ⇑f)

Tactic:
isClosed_preimage_val_coborder

Premises used: isClosed_preimage_val_coborder
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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)
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)
⊢ IsClosed (X := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) (Set.range (ι := ↥X) ⇑(Scheme.Hom.liftCoborder f))

Tactic:
convert! isClosed_preimage_val_coborder

Premises used: isClosed_preimage_val_coborder
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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)
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))
⊢ 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:
apply Set.image_injective.mpr f.coborderRange.ι.isEmbedding.injective

Premises used: Iff.mpr, Set.image_injective, AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.Scheme.Hom.coborderRange, Topology.IsEmbedding.injective, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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)
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))
⊢ 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:
rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.liftCoborder_ι]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.liftCoborder_ι, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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)
⊢ Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f)
    (Set.range (ι := ↥(↑(Scheme.Hom.coborderRange f) : Scheme)) ⇑(Scheme.Hom.coborderRange f).ι)

Tactic:
simpa using subset_coborder

Premises used: subset_coborder
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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.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:
exact (Set.image_preimage_eq_of_subset (by simpa using subset_coborder)).symm

Premises used: Set.image_preimage_eq_of_subset, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
rw : Dense (↑(Scheme.Hom.coborderRange f) : Set ↥Y)
⊢ IsDominant (Scheme.Hom.coborderRange f).ι

Tactic:
rw [isDominant_iff, DenseRange, Scheme.Opens.range_ι]

Premises used: AlgebraicGeometry.isDominant_iff, AlgebraicGeometry.Scheme.Opens.range_ι, DenseRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ Dense (↑(Scheme.Hom.coborderRange f) : Set ↥Y)

Tactic:
dense_coborder

Premises used: dense_coborder, setOf, coborder, Not
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ Dense (↑(Scheme.Hom.coborderRange f) : Set ↥Y)

Tactic:
exact dense_coborder

Premises used: dense_coborder
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
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
⊢ @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)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
x x_1 : Scheme
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:
isImmersion_iff _

Premises used: AlgebraicGeometry.topologically, AlgebraicGeometry.isImmersion_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
x x_1 : Scheme
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:
exact isImmersion_iff _

Premises used: AlgebraicGeometry.isImmersion_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
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))
⊢ IsZariskiLocalAtTarget @IsImmersion

Tactic:
suffices IsZariskiLocalAtTarget
      (topologically fun {X Y} _ _ f ↦ IsLocallyClosed (Set.range f)) from
    isImmersion_eq_inf ▸ inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst :
  (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦
      IsLocallyClosed (Set.range f)).RespectsIso
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)))
⊢ 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:
apply +allowSynthFailures topologically_isZariskiLocalAtTarget'

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦
      IsLocallyClosed (Set.range f)).RespectsIso

Tactic:
{ precomp := ?_, postcomp := ?_ }

Premises used: CategoryTheory.MorphismProperty.Respects.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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)
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)
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦
      IsLocallyClosed (Set.range f)).RespectsIso

Tactic:
refine { precomp := ?_, postcomp := ?_ }
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
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
⊢ IsIso i

Tactic:
change IsIso i at hi

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

Tactic:
simpa only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
        Set.range_eq_univ.mpr i.surjective, Set.image_univ]

Premises used: Iff.mpr, Set.range_eq_univ, Set.range_comp, Set.image_univ, AlgebraicGeometry.Scheme.Hom.surjective, 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
hi : MorphismProperty.isomorphisms Scheme i
f : X ⟶ Y
hf :
  topologically
    (fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) ↦ IsLocallyClosed (Set.range f)) f
⊢ IsIso i

Tactic:
change IsIso i at hi

Premises used: CategoryTheory.IsIso