awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsEmpty.{u + 1} ↥(pullback (Y := subscheme (X := Y) ⊤) f (subschemeι ⊤))

Tactic:
exact 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
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
a : I.map (f ≫ g) ≤ (I.map f).map g
a₁ : (I.map f).map g ≤ I.map (f ≫ g)
⊢ I.map (f ≫ g) = (I.map f).map g

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
a : (I.map (f ≫ g)).comap (f ≫ g) ≤ I
⊢ I.map (f ≫ g) ≤ (I.map f).map g

Tactic:
rw [le_map_iff_comap_le, le_map_iff_comap_le, ← comap_comp]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_le, AlgebraicGeometry.Scheme.IdealSheafData.comap_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map (f ≫ g)).comap (f ≫ g) ≤ I

Tactic:
comap_map_le _ _

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map (f ≫ g)).comap (f ≫ g) ≤ I

Tactic:
exact comap_map_le _ _

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
a : (((I.map f).map g).comap g).comap f ≤ I
⊢ (I.map f).map g ≤ I.map (f ≫ g)

Tactic:
rw [le_map_iff_comap_le, comap_comp]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_le, AlgebraicGeometry.Scheme.IdealSheafData.comap_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (((I.map f).map g).comap g).comap f ≤ I

Tactic:
(comap_mono _ (comap_map_le _ _)).trans (comap_map_le _ _)

Premises used: Set.Mem, AlgebraicGeometry.Scheme.IdealSheafData.comap_mono, LE.le.trans, AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (((I.map f).map g).comap g).comap f ≤ I

Tactic:
exact (comap_mono _ (comap_map_le _ _)).trans (comap_map_le _ _)

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.comap_mono, LE.le.trans, AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
Z : Scheme
I : Z.IdealSheafData
⊢ I.map (𝟙 Z) = I

Tactic:
simp [map]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (Hom.ker f).map g = Hom.ker (f ≫ g)

Tactic:
simp [← map_bot]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map_bot
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.ker (f ≫ g) = (Hom.ker f).map g

Tactic:
(map_ker f g).symm

Premises used: Eq.symm, AlgebraicGeometry.Scheme.IdealSheafData.map_ker
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
a : (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))
a₁ : vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X))) ≤ (vanishingIdeal Z).map f
⊢ (vanishingIdeal Z).map f = vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
a : ⇑f '' (↑Z : Set ↥X) ⊆ (↑(Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support : Set ↥Y)
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))

Tactic:
rw [map, ← le_support_iff_le_vanishingIdeal, TopologicalSpace.Closeds.closure_le]

Premises used: TopologicalSpace.Closeds.closure_le, AlgebraicGeometry.Scheme.IdealSheafData.map, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' (↑Z : Set ↥X) ⊆ (↑(Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support : Set ↥Y)

Tactic:
.trans ?_ (Hom.range_subset_ker_support _)

Premises used: HasSubset.Subset.trans, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
a :
  Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))
⊢ ⇑f '' (↑Z : Set ↥X) ⊆ (↑(Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support : Set ↥Y)

Tactic:
refine .trans ?_ (Hom.range_subset_ker_support _)
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
a :
  Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme)
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) ((vanishingIdeal Z).subschemeι.base ≫ f.base)) :
        (a : ↥(vanishingIdeal Z).subscheme) → ↥Y))
a₁ :
  Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) (Function.comp (β := ↥X) ⇑f ⇑(vanishingIdeal Z).subschemeι))
a₂ :
  Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.image (α := ↥X) (⇑f) (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑(vanishingIdeal Z).subschemeι))
a₃ : Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X)) (⇑f '' (↑(vanishingIdeal Z).support : Set ↥X))
a₄ a₅ : Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X)) (⇑f '' (↑Z : Set ↥X))
⊢ Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.Scheme.Hom.comp_base, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X))) ≤ (vanishingIdeal Z).map f

Tactic:
simp [le_map_iff_comap_le, ← le_support_iff_le_vanishingIdeal, ← Set.image_subset_iff,
      subset_closure, ← SetLike.coe_subset_coe]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_le, subset_closure, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, SetLike.coe_subset_coe, Set.image_subset_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : QuasiCompact f
h : (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
⊢ (I.map f).support = TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : QuasiCompact f
h :
  (↑(Hom.ker (I.subschemeι ≫ f)).support : Set ↥Y) =
    (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
h₁ :
  closure (Set.range (ι := ↥I.subscheme) ⇑(I.subschemeι ≫ f)) =
    (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
h₂ :
  closure
      (Set.range (ι := ↥I.subscheme)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (I.subschemeι.base ≫ f.base)) :
          (a : ↥I.subscheme) → ↥Y)) =
    (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
h₃ :
  closure (Set.range (ι := ↥I.subscheme) (Function.comp (β := ↥X) ⇑f ⇑I.subschemeι)) =
    (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
h₄ :
  closure (Set.image (α := ↥X) (⇑f) (Set.range (ι := ↥I.subscheme) ⇑I.subschemeι)) =
    (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
h₅ :
  closure (⇑f '' (↑I.support : Set ↥X)) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
h₆ h₇ : Eq (α := Set ↥Y) (closure (⇑f '' (↑I.support : Set ↥X))) (closure (⇑f '' (↑I.support : Set ↥X)))
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)

Tactic:
rw [map, Scheme.Hom.support_ker, Scheme.Hom.comp_base, TopCat.coe_comp,
    Set.range_comp, range_subschemeι, TopologicalSpace.Closeds.coe_closure]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.IdealSheafData.map, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.Scheme.Hom.support_ker, TopologicalSpace.Closeds.coe_closure, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : QuasiCompact f
U : (↑Y.affineOpens : Type u)
H : IsAffineOpen (f ⁻¹ᵁ (↑U : Y.Opens))
⊢ Eq (α :=
    Ideal
      (↑(CommRingCat.of
            (HasQuotient.Quotient
              (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
                Type u)
              (B :=
              Ideal
                (↑Γ(X,
                      (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
                  Type u))
              (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H)))) :
        Type u))
    (RingHom.ker (F :=
      (↑(CommRingCat.of
              (HasQuotient.Quotient
                (↑Γ(X,
                      (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
                  Type u)
                (B :=
                Ideal
                  (↑Γ(X,
                        (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) :
                          X.Opens)) :
                    Type u))
                (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H)))) :
          Type u) →+*
        (↑Γ(I.subscheme,
              I.subschemeι ⁻¹ᵁ
                (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
          Type u))
      (CommRingCat.Hom.hom
        (Iso.inv
          (I.subschemeObjIso (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H)))))
    ⊥

Tactic:
have : RingHom.ker (I.subschemeObjIso ⟨_, H⟩).inv.hom = ⊥ :=
    RingHom.ker_coe_equiv (I.subschemeObjIso ⟨_, H⟩).symm.commRingCatIsoToRingEquiv
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : QuasiCompact f
U : (↑Y.affineOpens : Type u)
H : IsAffineOpen (f ⁻¹ᵁ (↑U : Y.Opens))
this :
  Eq (α :=
    Ideal
      (↑(CommRingCat.of
            (HasQuotient.Quotient
              (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
                Type u)
              (B :=
              Ideal
                (↑Γ(X,
                      (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
                  Type u))
              (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H)))) :
        Type u))
    (RingHom.ker (F :=
      (↑(CommRingCat.of
              (HasQuotient.Quotient
                (↑Γ(X,
                      (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
                  Type u)
                (B :=
                Ideal
                  (↑Γ(X,
                        (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) :
                          X.Opens)) :
                    Type u))
                (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H)))) :
          Type u) →+*
        (↑Γ(I.subscheme,
              I.subschemeι ⁻¹ᵁ
                (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) :
          Type u))
      (CommRingCat.Hom.hom
        (Iso.inv
          (I.subschemeObjIso (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H)))))
    ⊥
⊢ (I.map f).ideal U =
    Ideal.comap (S :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H) : X.Opens)) : Type u))
      (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app f (↑U : Y.Opens)))
      (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) H))

Tactic:
simp [map, ← RingHom.comap_ker, subschemeι_app _ ⟨_, H⟩,
    this, ← RingHom.ker_eq_comap_bot]

Premises used: RingHom.comap_ker, AlgebraicGeometry.Scheme.IdealSheafData.map, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, Subtype.mk, RingHom.ker_eq_comap_bot
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : IsAffineHom f
U : (↑Y.affineOpens : Type u)
⊢ (I.map f).ideal U =
    Ideal.comap (S :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) : X.Opens)) : Type u))
      (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app f (↑U : Y.Opens)))
      (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯))

Tactic:
ideal_map I f U (U.2.preimage f)

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
inst : IsOpenImmersion f
U : (↑X.affineOpens : Type u)
⊢ (I.comap f).ideal U =
    Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯) : Y.Opens)) : Type u))
      (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(Y, f ''ᵁ (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso f (↑U : X.Opens))))
      (I.ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯))

Tactic:
(ker_ideal_of_isPullback_of_isOpenImmersion _ _ _ _
    (IsPullback.of_hasPullback f I.subschemeι) U).trans ?_

Premises used: Set.Mem, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, setOf, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, CategoryTheory.IsPullback.of_hasPullback, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
inst : IsOpenImmersion f
U : (↑X.affineOpens : Type u)
refine :
  Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯) : Y.Opens)) : Type u))
      (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(Y, f ''ᵁ (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso f (↑U : X.Opens))))
      ((Hom.ker I.subschemeι).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯)))
    (Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯) : Y.Opens)) : Type u))
      (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(Y, f ''ᵁ (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso f (↑U : X.Opens))))
      (I.ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯)))
⊢ (I.comap f).ideal U =
    Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯) : Y.Opens)) : Type u))
      (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(Y, f ''ᵁ (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso f (↑U : X.Opens))))
      (I.ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯))

Tactic:
refine (ker_ideal_of_isPullback_of_isOpenImmersion _ _ _ _
    (IsPullback.of_hasPullback f I.subschemeι) U).trans ?_

Premises used: AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, CategoryTheory.IsPullback.of_hasPullback, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
inst : IsOpenImmersion f
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯) : Y.Opens)) : Type u))
      (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(Y, f ''ᵁ (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso f (↑U : X.Opens))))
      ((Hom.ker I.subschemeι).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯)))
    (Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯) : Y.Opens)) : Type u))
      (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(Y, f ''ᵁ (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso f (↑U : X.Opens))))
      (I.ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) ⋯)))

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

Tactic:
simpa using H
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : X.IdealSheafData
J : Y.IdealSheafData
f : X ⟶ Y
H : J ≤ I.map f
⊢ I.subschemeMap J f H ≫ J.subschemeι = I.subschemeι ≫ f

Tactic:
IsClosedImmersion.lift_fac _ _ _

Premises used: AlgebraicGeometry.IsClosedImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
rw : ((I.comapIso f).hom ≫ pullback.snd f I.subschemeι) ≫ I.subschemeι = (I.comap f).subschemeMap I f ⋯ ≫ I.subschemeι
⊢ (I.comapIso f).hom ≫ pullback.snd f I.subschemeι = (I.comap f).subschemeMap I f ⋯

Tactic:
rw [← cancel_mono I.subschemeι]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ ((I.comapIso f).hom ≫ pullback.snd f I.subschemeι) ≫ I.subschemeι = (I.comap f).subschemeMap I f ⋯ ≫ I.subschemeι

Tactic:
simp [← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
rw :
  IsClosed.{u} (X := ↥X)
    (⋃ (i : Set ↥X), ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {Z}) i), i)
⊢ IsOpen (X := ↥X) (⋃₀ (irreducibleComponents ↥X \ {Z}))ᶜ

Tactic:
rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]

Premises used: Set.sUnion_eq_biUnion, isOpen_compl_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ IsClosed.{u} (X := ↥X)
    (⋃ (i : Set ↥X), ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {Z}) i), i)

Tactic:
TopologicalSpace.NoetherianSpace.finite_irreducibleComponents.diff.isClosed_biUnion
      fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, Set.Finite.isClosed_biUnion
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ IsClosed.{u} (X := ↥X)
    (⋃ (i : Set ↥X), ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {Z}) i), i)

Tactic:
exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents.diff.isClosed_biUnion
      fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, Set.Finite.isClosed_biUnion
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
rw : Z = closure (↑(X.irreducibleComponentOpen Z) : Set ↥X)
⊢ Z =
    ⋂ (U : (↑X.affineOpens : Type u)),
      X.zeroLocus (↑((Hom.ker (X.irreducibleComponentOpen Z).ι).ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
rw [← IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, Hom.support_ker, Opens.range_ι]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.Scheme.Hom.support_ker
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ Z = closure (↑(X.irreducibleComponentOpen Z) : Set ↥X)

Tactic:
(closure_sUnion_irreducibleComponents_diff_singleton
      TopologicalSpace.NoetherianSpace.finite_irreducibleComponents Z hZ).symm

Premises used: setOf, closure_sUnion_irreducibleComponents_diff_singleton, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, Eq.symm, Not
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ Z = closure (↑(X.irreducibleComponentOpen Z) : Set ↥X)

Tactic:
exact (closure_sUnion_irreducibleComponents_diff_singleton
      TopologicalSpace.NoetherianSpace.finite_irreducibleComponents Z hZ).symm

Premises used: closure_sUnion_irreducibleComponents_diff_singleton, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
h :
  ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)),
    x_1 ∈ (X.irreducibleComponentIdeal Z hZ).ideal x ↔ x_1 ∈ (Hom.ker (X.irreducibleComponentOpen Z).ι).ideal x
⊢ X.irreducibleComponentIdeal Z hZ = Hom.ker (X.irreducibleComponentOpen Z).ι

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
x : (↑X.affineOpens : Type u)
x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)
⊢ x_1 ∈ (X.irreducibleComponentIdeal Z hZ).ideal x ↔ x_1 ∈ (Hom.ker (X.irreducibleComponentOpen Z).ι).ideal x

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
x : ↥(X.irreducibleComponent Z hZ)
⊢ (X.irreducibleComponentι Z hZ) x = (↑x : ↥X)

Tactic:
rfl

Premises used: rfl