awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ I.comap (𝟙 Z) = I
have rw₃ : Hom.ker (I.subschemeι ≫ 𝟙 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ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ I.comap (𝟙 Z) = I
have rw₄ : Hom.ker I.subschemeι = 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ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ I.comap (𝟙 Z) = I
have rw₅ : I = 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ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comap f).support = I.support.preimage ⋯
have h : (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage sorry) : Set ↥X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)
have h : (↑(Hom.ker (X := pullback f I.subschemeι) (pullback.fst f I.subschemeι)).support : Set ↥X) =
  (↑(I.support.preimage sorry) : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)
⊢ (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)
have h₁ : closure (Set.range (ι := ↥(pullback f I.subschemeι)) ⇑(pullback.fst f I.subschemeι)) =
  (↑(I.support.preimage sorry) : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)
⊢ (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)
have h₂ : closure (Set.preimage (β := ↥Y) (⇑f) (Set.range (ι := ↥I.subscheme) ⇑I.subschemeι)) = (↑(I.support.preimage sorry) : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)
⊢ (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)
have h₃ : closure (⇑f ⁻¹' (↑I.support : Set ↥Y)) = (↑(I.support.preimage sorry) : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)
⊢ (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)
have h₄ : Eq (α := Set ↥X) (closure (⇑f ⁻¹' (↑I.support : Set ↥Y))) (⇑f ⁻¹' (↑I.support : Set ↥Y))
Tactic: rw [comap, Scheme.Hom.support_ker, Pullback.range_fst, range_subschemeι,
    TopologicalSpace.Closeds.coe_preimage, (I.support.isClosed.preimage f.continuous).closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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))
⊢ (↑(I.comap f).support : Set ↥X) = (↑(I.support.preimage ⋯) : Set ↥X)
have h₅ : Eq (α := Set ↥X) (⇑f ⁻¹' (↑I.support : Set ↥Y)) (⇑f ⁻¹' (↑I.support : Set ↥Y))
Tactic: rw [comap, Scheme.Hom.support_ker, Pullback.range_fst, range_subschemeι,
    TopologicalSpace.Closeds.coe_preimage, (I.support.isClosed.preimage f.continuous).closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst : IsClosedImmersion 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ι)
have 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) sorry sorry) (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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ι))
⊢ 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ι)
have rw₁ : Hom.ker (X := pullback f i) (pullback.fst f i) = Hom.ker (X := pullback f i) (pullback.fst f i ≫ 𝟙 X)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)
⊢ 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ι)
have rw₂ : Hom.ker (X := pullback f i) (pullback.fst f i) = Hom.ker (X := pullback f i) (pullback.fst f i)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ IsPullback iX Zf f iY
have suffices : IsIso (Y := pullback f iY) (pullback.lift iX Zf h)
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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ IsIso (Y := pullback f iY) (pullback.lift iX Zf h)
have refine : Hom.ker iX = Hom.ker (X := pullback f iY) (pullback.fst f iY)
Tactic: refine IsClosedImmersion.isIso_of_ker_eq iX (pullback.fst f iY) _ (by simp) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ Hom.ker iX = Hom.ker (X := pullback f iY) (pullback.fst f iY)
have rw : Hom.ker iX = (Hom.ker iY).comap f
Tactic: rw [ker_fst_of_isClosedImmersion, h']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ Hom.ker iX = Hom.ker (X := pullback f iY) (pullback.fst f iY)
have rw₁ : Hom.ker iX = Hom.ker iX
Tactic: rw [ker_fst_of_isClosedImmersion, h']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J ≤ I.map f ↔ J.comap f ≤ I
have mp : J ≤ I.map f → J.comap f ≤ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
mp : J ≤ I.map f → J.comap f ≤ I
⊢ J ≤ I.map f ↔ J.comap f ≤ I
have mpr : J.comap f ≤ I → J ≤ I.map f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤ I
have mp : J.comap f ≤
  Hom.ker
    (CategoryStruct.comp (Y := pullback f J.subschemeι)
      (pullback.lift I.subschemeι (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) sorry) (pullback.fst f J.subschemeι))
Tactic: rw [← I.ker_subschemeι, ← pullback.lift_fst (f := f) (g := J.subschemeι) I.subschemeι
      ((I.subschemeι ≫ f).toImage ≫ inclusion H) (by simp)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (hypothesis)
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
⊢ J ≤ I.map f
have this : (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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
⊢ J ≤ I.map f
have mpr : Hom.ker J.subschemeι ≤ Hom.ker ((inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι)
Tactic: rw [map, ← J.ker_subschemeι, ← this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ comap ⊤ f = ⊤
have rw : IsEmpty.{u + 1} ↥(pullback (Y := subscheme (X := Y) ⊤) f (subschemeι ⊤))
Tactic: rw [comap, Hom.ker_eq_top_iff_isEmpty]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.map (f ≫ g) = (I.map f).map g
have a : I.map (f ≫ g) ≤ (I.map f).map g
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
a : I.map (f ≫ g) ≤ (I.map f).map g
⊢ I.map (f ≫ g) = (I.map f).map g
have a₁ : (I.map f).map g ≤ I.map (f ≫ g)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ I.map (f ≫ g) ≤ (I.map f).map g
have a : (I.map (f ≫ g)).comap (f ≫ g) ≤ I
Tactic: rw [le_map_iff_comap_le, le_map_iff_comap_le, ← comap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map f).map g ≤ I.map (f ≫ g)
have a : (((I.map f).map g).comap g).comap f ≤ I
Tactic: rw [le_map_iff_comap_le, comap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f = vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))
have a : (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
a : (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))
⊢ (vanishingIdeal Z).map f = vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))
have a₁ : vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X))) ≤ (vanishingIdeal Z).map f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' (↑Z : Set ↥X)))
have a : ⇑f '' (↑Z : Set ↥X) ⊆ (↑(Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support : Set ↥Y)
Tactic: rw [map, ← le_support_iff_le_vanishingIdeal, TopologicalSpace.Closeds.closure_le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' (↑Z : Set ↥X) ⊆ (↑(Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support : Set ↥Y)
have a : Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
  (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))
Tactic: refine .trans ?_ (Hom.range_subset_ker_support _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))
have 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))
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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))
⊢ Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))
have a₁ : Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
  (Set.range (ι := ↥(vanishingIdeal Z).subscheme) (Function.comp (β := ↥X) ⇑f ⇑(vanishingIdeal Z).subschemeι))
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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ι))
⊢ Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))
have a₂ : Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
  (Set.image (α := ↥X) (⇑f) (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑(vanishingIdeal Z).subschemeι))
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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ι))
⊢ Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))
have a₃ : Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X)) (⇑f '' (↑(vanishingIdeal Z).support : Set ↥X))
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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))
⊢ Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X))
    (Set.range (ι := ↥(vanishingIdeal Z).subscheme) ⇑((vanishingIdeal Z).subschemeι ≫ f))
have a₄ : Subset (α := Set ↥Y) (⇑f '' (↑Z : Set ↥X)) (⇑f '' (↑Z : Set ↥X))
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
      range_subschemeι, coe_support_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : QuasiCompact f
⊢ (I.map f).support = TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))
have h : (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : QuasiCompact f
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
have h : (↑(Hom.ker (I.subschemeι ≫ 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
have h₁ : closure (Set.range (ι := ↥I.subscheme) ⇑(I.subschemeι ≫ f)) =
  (↑(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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
have 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)
Tactic: rw [map, Scheme.Hom.support_ker, Scheme.Hom.comp_base, TopCat.coe_comp,
    Set.range_comp, range_subschemeι, TopologicalSpace.Closeds.coe_closure]