awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst : QuasiCompact (Spec.map φ)
rw :
  closure (Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom (φ ≫ (ΓSpecIso R).inv)))) ⊆
    closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
⊢ (↑(ker (Spec.map φ)).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))

Tactic:
rw [ker_of_isAffine, coe_support_ofIdealTop, Spec_zeroLocus, ← Ideal.coe_comap,
      RingHom.comap_ker, ← PrimeSpectrum.closure_range_comap, ← CommRingCat.hom_comp,
      ← Scheme.ΓSpecIso_inv_naturality]

Premises used: PrimeSpectrum.closure_range_comap, RingHom.comap_ker, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, CommRingCat.hom_comp, Ideal.coe_comap, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst : QuasiCompact (Spec.map φ)
simp :
  closure
      (Set.range
        (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) ∘ PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv))) ⊆
    closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
⊢ closure (Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom (φ ≫ (ΓSpecIso R).inv)))) ⊆
    closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))

Tactic:
simp only [CommRingCat.hom_comp, PrimeSpectrum.comap_comp]

Premises used: CommRingCat.hom_comp, PrimeSpectrum.comap_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst : QuasiCompact (Spec.map φ)
⊢ closure
      (Set.range
        (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) ∘ PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv))) ⊆
    closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))

Tactic:
closure_mono (Set.range_comp_subset_range _ (Spec.map φ))

Premises used: Set.range_comp_subset_range, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Spec.map, closure_mono, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst : QuasiCompact (Spec.map φ)
⊢ closure
      (Set.range
        (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) ∘ PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv))) ⊆
    closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))

Tactic:
exact closure_mono (Set.range_comp_subset_range _ (Spec.map φ))

Premises used: Set.range_comp_subset_range, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Spec.map, closure_mono, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
a : Set.range (ι := ↥X) ⇑f ⊆ (↑(ker f).support : Set ↥Y)
⊢ closure (Set.range (ι := ↥X) ⇑f) ⊆ (↑(ker f).support : Set ↥Y)

Tactic:
rw [(support _).isClosed.closure_subset_iff]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, TopologicalSpace.Closeds.isClosed, IsClosed.closure_subset_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ Set.range (ι := ↥X) ⇑f ⊆ (↑(ker f).support : Set ↥Y)

Tactic:
f.range_subset_ker_support

Premises used: AlgebraicGeometry.Scheme.Hom.range_subset_ker_support
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ Set.range (ι := ↥X) ⇑f ⊆ (↑(ker f).support : Set ↥Y)

Tactic:
exact f.range_subset_ker_support

Premises used: AlgebraicGeometry.Scheme.Hom.range_subset_ker_support
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y_1 Z Y : Scheme
f g : (Over Y)ᵒᵖ
hfg : f ⟶ g
⊢ Hom.ker (Opposite.unop f).hom ≤ Hom.ker (Opposite.unop g).hom

Tactic:
simpa only [Functor.id_obj, Functor.const_obj_obj,
    OrderDual.toDual_le_toDual, ← Over.w hfg.unop] using hfg.unop.left.le_ker_comp f.unop.hom

Premises used: AlgebraicGeometry.Scheme.Hom.le_ker_comp, OrderDual.toDual_le_toDual, CategoryTheory.Over.Hom.left, Quiver.Hom.unop, CategoryTheory.Over.w, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.const_obj_obj, Opposite.unop, CategoryTheory.Over.hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H :
  Eq (α :=
    Ideal
      (↑Γ(Spec Γ(X, ⊤),
            (↑(Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ ⋯) :
              (Spec Γ(X, ⊤)).Opens)) :
        Type u))
    ((Hom.ker X.toSpecΓ).ideal
      (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ ⋯))
    (ideal ⊥
      (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ ⋯))
⊢ Hom.ker X.toSpecΓ = ⊥

Tactic:
apply IdealSheafData.ext_of_isAffine

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
⊢ Eq (α :=
    Ideal
      (↑Γ(Spec Γ(X, ⊤),
            (↑(Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ ⋯) :
              (Spec Γ(X, ⊤)).Opens)) :
        Type u))
    ((Hom.ker X.toSpecΓ).ideal
      (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ ⋯))
    (ideal ⊥
      (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ ⋯))

Tactic:
simpa using RingHom.ker_coe_equiv (ΓSpecIso Γ(X, ⊤)).commRingCatIsoToRingEquiv

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.ker_coe_equiv, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Top.top, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).inv ≫ (I.comap f).subschemeι = pullback.fst f I.subschemeι

Tactic:
(pullback.fst f I.subschemeι).toImage_imageι

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, AlgebraicGeometry.Scheme.IdealSheafData.comap, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
rw : (I.comapIso f).hom ≫ (I.comapIso f).inv ≫ (I.comap f).subschemeι = (I.comap f).subschemeι
rw₁ rw₂ : (I.comap f).subschemeι = (I.comap f).subschemeι
⊢ (I.comapIso f).hom ≫ pullback.fst f I.subschemeι = (I.comap f).subschemeι

Tactic:
rw [← comapIso_inv_subschemeι, Iso.hom_inv_id_assoc]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.comap g).subschemeι ≫ 𝟙 Y = (I.comapIso g).hom ≫ pullback.fst g I.subschemeι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
  Iso.trans (Y := pullback (Y := pullback g I.subschemeι) f (pullback.fst g I.subschemeι))
    (asIso (pullback.map f (I.comap g).subschemeι f (pullback.fst g I.subschemeι) (𝟙 X) (I.comapIso g).hom (𝟙 Y) ⋯ ⋯))
    (pullbackRightPullbackFstIso g I.subschemeι f)
rw :
  Hom.ker (e.hom ≫ pullback.fst (f ≫ g) I.subschemeι) =
    Hom.ker (X := pullback f (I.comap g).subschemeι) (pullback.fst f (I.comap g).subschemeι)
⊢ I.comap (f ≫ g) = (I.comap g).comap f

Tactic:
rw [comap, comap, ← Scheme.Hom.ker_comp_of_isIso e.hom]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.comap, AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
  Iso.trans (Y := pullback (Y := pullback g I.subschemeι) f (pullback.fst g I.subschemeι))
    (asIso (pullback.map f (I.comap g).subschemeι f (pullback.fst g I.subschemeι) (𝟙 X) (I.comapIso g).hom (𝟙 Y) ⋯ ⋯))
    (pullbackRightPullbackFstIso g I.subschemeι f)
⊢ Hom.ker (e.hom ≫ pullback.fst (f ≫ g) I.subschemeι) =
    Hom.ker (X := pullback f (I.comap g).subschemeι) (pullback.fst f (I.comap g).subschemeι)

Tactic:
simp [e]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
Z : Scheme
I : Z.IdealSheafData
rw : Hom.ker (X := pullback (𝟙 Z) I.subschemeι) (pullback.fst (𝟙 Z) I.subschemeι) = I
rw₁ :
  Hom.ker
      (CategoryStruct.comp (Y := pullback (𝟙 Z) I.subschemeι) (inv (pullback.snd (𝟙 Z) I.subschemeι))
        (pullback.fst (𝟙 Z) I.subschemeι)) =
    I
rw₂ : Hom.ker (I.subschemeι ≫ inv (𝟙 Z)) = I
rw₃ : Hom.ker (I.subschemeι ≫ 𝟙 Z) = I
rw₄ : Hom.ker I.subschemeι = I
rw₅ rw₆ : I = I
⊢ I.comap (𝟙 Z) = I

Tactic:
rw [comap, ← Scheme.Hom.ker_comp_of_isIso (inv (pullback.snd _ _)),
    pullback_inv_snd_fst_of_left_isIso, IsIso.inv_id, Category.comp_id, ker_subschemeι]

Premises used: CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso, CategoryTheory.Limits.pullback.snd, CategoryTheory.IsIso.inv_id, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.IdealSheafData.comap, AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι, CategoryTheory.inv
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
h : (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)
⊢ (I.comap f).support = I.support.preimage ⋯

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
h :
  (↑(Hom.ker (X := pullback f I.subschemeι) (pullback.fst f I.subschemeι)).support : Set ↥X) =
    (↑(I.support.preimage ⋯) : Set ↥X)
h₁ :
  closure (Set.range (ι := ↥(pullback f I.subschemeι)) ⇑(pullback.fst f I.subschemeι)) =
    (↑(I.support.preimage ⋯) : Set ↥X)
h₂ :
  closure (Set.preimage (β := ↥Y) (⇑f) (Set.range (ι := ↥I.subscheme) ⇑I.subschemeι)) =
    (↑(I.support.preimage ⋯) : Set ↥X)
h₃ : closure (⇑f ⁻¹' (↑I.support : Set ↥Y)) = (↑(I.support.preimage ⋯) : Set ↥X)
h₄ : Eq (α := Set ↥X) (closure (⇑f ⁻¹' (↑I.support : Set ↥Y))) (⇑f ⁻¹' (↑I.support : Set ↥Y))
h₅ h₆ : Eq (α := Set ↥X) (⇑f ⁻¹' (↑I.support : Set ↥Y)) (⇑f ⁻¹' (↑I.support : Set ↥Y))
⊢ (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)

Tactic:
rw [comap, Scheme.Hom.support_ker, Pullback.range_fst, range_subschemeι,
    TopologicalSpace.Closeds.coe_preimage, (I.support.isClosed.preimage f.continuous).closure_eq]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, TopologicalSpace.Closeds.isClosed, TopologicalSpace.Closeds.coe_preimage, IsClosed.closure_eq, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.Scheme.IdealSheafData.comap, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.Scheme.Hom.continuous, IsClosed.preimage, AlgebraicGeometry.Scheme.Hom.support_ker
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst : IsClosedImmersion i
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst : IsClosedImmersion i
⊢ i ≫ 𝟙 Y = Hom.toImage i ≫ Hom.imageι i

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst : IsClosedImmersion i
rw :
  Hom.ker (X := pullback f i) (pullback.fst f i) =
    Hom.ker (X := pullback f i)
      (CategoryStruct.comp (Y := pullback f (Hom.imageι i))
        (pullback.map f i f (Hom.imageι i) (𝟙 X) (Hom.toImage i) (𝟙 Y) ⋯ ⋯) (pullback.fst f (Hom.ker i).subschemeι))
rw₁ : Hom.ker (X := pullback f i) (pullback.fst f i) = Hom.ker (X := pullback f i) (pullback.fst f i ≫ 𝟙 X)
rw₂ rw₃ : Hom.ker (X := pullback f i) (pullback.fst f i) = Hom.ker (X := pullback f i) (pullback.fst f i)
⊢ Hom.ker (X := pullback f i) (pullback.fst f i) =
    Hom.ker (X := pullback f (Hom.ker i).subschemeι) (pullback.fst f (Hom.ker i).subschemeι)

Tactic:
rw [← Hom.ker_comp_of_isIso (pullback.map f i f i.imageι (𝟙 _) (i.toImage) (𝟙 _)
    (by simp) (by simp)), pullback.lift_fst, Category.comp_id]

Premises used: AlgebraicGeometry.Scheme.Hom.imageι, AlgebraicGeometry.Scheme.Hom.toImage, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso, CategoryTheory.Limits.pullback.map, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst : IsClosedImmersion iX
inst_1 : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (Y := pullback f iY) (pullback.lift iX Zf h)
⊢ iX ≫ 𝟙 X = CategoryStruct.comp (Y := pullback f iY) (pullback.lift iX Zf h) (pullback.fst f iY)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst : IsClosedImmersion iX
inst_1 : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
this : IsIso (Y := pullback f iY) (pullback.lift iX Zf h)
⊢ IsPullback iX Zf f iY

Tactic:
simpa using (IsPullback.of_vert_isIso (show CommSq iX (pullback.lift iX Zf h)
      (𝟙 X) (pullback.fst _ _) from ⟨by simp⟩)).paste_vert (IsPullback.of_hasPullback f iY)

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst : IsClosedImmersion iX
inst_1 : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
suffices : IsIso (Y := pullback f iY) (pullback.lift iX Zf h)
⊢ IsPullback iX Zf f iY

Tactic:
suffices IsIso (pullback.lift _ _ h) by
    simpa using (IsPullback.of_vert_isIso (show CommSq iX (pullback.lift iX Zf h)
      (𝟙 X) (pullback.fst _ _) from ⟨by simp⟩)).paste_vert (IsPullback.of_hasPullback f iY)
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst : IsClosedImmersion iX
inst_1 : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
⊢ CategoryStruct.comp (Y := pullback f iY) (pullback.lift iX Zf h) (pullback.fst f iY) = iX

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst : IsClosedImmersion iX
inst_1 : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
refine : Hom.ker iX = Hom.ker (X := pullback f iY) (pullback.fst f iY)
⊢ IsIso (Y := pullback f iY) (pullback.lift iX Zf h)

Tactic:
refine IsClosedImmersion.isIso_of_ker_eq iX (pullback.fst f iY) _ (by simp) ?_

Premises used: AlgebraicGeometry.IsClosedImmersion.isIso_of_ker_eq, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
ZX ZY X Y : Scheme
iX : ZX ⟶ X
iY : ZY ⟶ Y
Zf : ZX ⟶ ZY
f : X ⟶ Y
inst : IsClosedImmersion iX
inst_1 : IsClosedImmersion iY
h : iX ≫ f = Zf ≫ iY
h' : (Hom.ker iY).comap f = Hom.ker iX
rw : Hom.ker iX = (Hom.ker iY).comap f
rw₁ rw₂ : Hom.ker iX = Hom.ker iX
⊢ Hom.ker iX = Hom.ker (X := pullback f iY) (pullback.fst f iY)

Tactic:
rw [ker_fst_of_isClosedImmersion, h']

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ker_fst_of_isClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
mp : J ≤ I.map f → J.comap f ≤ I
mpr : J.comap f ≤ I → J ≤ I.map f
⊢ J ≤ I.map f ↔ J.comap f ≤ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ I.subschemeι ≫ f = (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) ≫ J.subschemeι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
mp :
  J.comap f ≤
    Hom.ker
      (CategoryStruct.comp (Y := pullback f J.subschemeι)
        (pullback.lift I.subschemeι (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) ⋯) (pullback.fst f J.subschemeι))
⊢ J.comap f ≤ I

Tactic:
rw [← I.ker_subschemeι, ← pullback.lift_fst (f := f) (g := J.subschemeι) I.subschemeι
      ((I.subschemeι ≫ f).toImage ≫ inclusion H) (by simp)]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.inclusion, AlgebraicGeometry.Scheme.Hom.toImage, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤
    Hom.ker
      (CategoryStruct.comp (Y := pullback f J.subschemeι)
        (pullback.lift I.subschemeι (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) ⋯) (pullback.fst f J.subschemeι))

Tactic:
Hom.le_ker_comp _ _

Premises used: AlgebraicGeometry.Scheme.Hom.le_ker_comp, Set.Mem, setOf
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤
    Hom.ker
      (CategoryStruct.comp (Y := pullback f J.subschemeι)
        (pullback.lift I.subschemeι (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) ⋯) (pullback.fst f J.subschemeι))

Tactic:
exact Hom.le_ker_comp _ _

Premises used: AlgebraicGeometry.Scheme.Hom.le_ker_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
⊢ (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f

Tactic:
simp [← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
⊢ (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f

Tactic:
have : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd _ _) ≫ J.subschemeι =
        I.subschemeι ≫ f := by simp [← pullback.condition]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
mpr : Hom.ker J.subschemeι ≤ Hom.ker ((inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι)
⊢ J ≤ I.map f

Tactic:
rw [map, ← J.ker_subschemeι, ← this]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ Hom.ker J.subschemeι ≤ Hom.ker ((inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι)

Tactic:
Hom.le_ker_comp _ _

Premises used: AlgebraicGeometry.Scheme.Hom.le_ker_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ Hom.ker J.subschemeι ≤ Hom.ker ((inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι)

Tactic:
exact Hom.le_ker_comp _ _

Premises used: AlgebraicGeometry.Scheme.Hom.le_ker_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ GaloisConnection (fun (x : Y.IdealSheafData) ↦ x.comap f) fun (x : X.IdealSheafData) ↦ x.map f

Tactic:
fun _ _ ↦ le_map_iff_comap_le.symm

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_le, Set.Mem, Iff.symm, GaloisConnection
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Monotone (β := Y.IdealSheafData) fun (x : X.IdealSheafData) ↦ x.map f

Tactic:
(map_gc f).monotone_u

Premises used: GaloisConnection.monotone_u, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Monotone (β := X.IdealSheafData) fun (x : Y.IdealSheafData) ↦ x.comap f

Tactic:
(map_gc f).monotone_l

Premises used: GaloisConnection.monotone_l, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
J : Y.IdealSheafData
f : X ⟶ Y
⊢ J ≤ (J.comap f).map f

Tactic:
(map_gc f).le_u_l J

Premises used: GaloisConnection.le_u_l, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
⊢ (I.map f).comap f ≤ I

Tactic:
(map_gc f).l_u_le I

Premises used: GaloisConnection.l_u_le, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ map ⊤ f = ⊤

Tactic:
(map_gc f).u_top

Premises used: GaloisConnection.u_top, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ comap ⊥ f = ⊥

Tactic:
(map_gc f).l_bot

Premises used: GaloisConnection.l_bot, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I₁ I₂ : X.IdealSheafData
f : X ⟶ Y
⊢ (I₁ ⊓ I₂).map f = I₁.map f ⊓ I₂.map f

Tactic:
(map_gc f).u_inf

Premises used: GaloisConnection.u_inf, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
J₁ J₂ : Y.IdealSheafData
f : X ⟶ Y
⊢ (J₁ ⊔ J₂).comap f = J₁.comap f ⊔ J₂.comap f

Tactic:
(map_gc f).l_sup

Premises used: GaloisConnection.l_sup, AlgebraicGeometry.Scheme.IdealSheafData.map_gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ map ⊥ f = Hom.ker f

Tactic:
simp [map, Scheme.Hom.ker_comp_of_isIso]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map, AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsEmpty.{u + 1} ↥(pullback (Y := subscheme (X := Y) ⊤) f (subschemeι ⊤))
⊢ comap ⊤ f = ⊤

Tactic:
rw [comap, Hom.ker_eq_top_iff_isEmpty]

Premises used: AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, AlgebraicGeometry.Scheme.IdealSheafData.comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsEmpty.{u + 1} ↥(pullback (Y := subscheme (X := Y) ⊤) f (subschemeι ⊤))

Tactic:
Function.isEmpty (pullback.snd f _)

Premises used: Function.isEmpty, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe