awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
e : Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤) :=
  Iso.trans (Y := Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯)) :
      Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Hom.appIso (pullback.fst f (↑U : Y.Opens).ι) ⊤ :
      Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
⊢ Hom.app f (↑U : Y.Opens) ≫ e.hom =
    Iso.inv (ΓSpecIso Γ(Y, (↑U : Y.Opens))) ≫ Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)
have rw : (↑U : Y.Opens).topIso.hom ≫ Hom.app f (↑U : Y.Opens) ≫ e.hom =
  Hom.appTop (IsAffineOpen.isoSpec sorry).inv ≫ Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)
Tactic: rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
e : Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤) :=
  Iso.trans (Y := Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯)) :
      Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Hom.appIso (pullback.fst f (↑U : Y.Opens).ι) ⊤ :
      Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
⊢ (↑U : Y.Opens).topIso.hom ≫ Hom.app f (↑U : Y.Opens) ≫ e.hom =
    Hom.appTop (IsAffineOpen.isoSpec ⋯).inv ≫ Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)
have simp : Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
  (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ sorry :
    Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
  (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ sorry :
    Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
Tactic: simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom,
      Iso.op_hom, eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, Hom.appLE_comp_appLE,
      Opens.map_top, e, pullback.condition, IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
e : Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤) :=
  Iso.trans (Y := Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯)) :
      Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Hom.appIso (pullback.fst f (↑U : Y.Opens).ι) ⊤ :
      Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
⊢ Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ ⋯ :
      Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ ⋯ :
      Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
have rw : Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
  (CategoryStruct.comp (Y := Γ((↑(↑U : Y.Opens) : Scheme), (↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤))
      (Y.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
      (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ sorry) :
    Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
  (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ sorry :
    Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
Tactic: rw [Hom.comp_appLE, Opens.ι_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
e : Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤) :=
  Iso.trans (Y := Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯)) :
      Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Hom.appIso (pullback.fst f (↑U : Y.Opens).ι) ⊤ :
      Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(pullback f (↑U : Y.Opens).ι, ⊤) : Type u))
      (CommRingCat.Hom.hom
        (Iso.inv (ΓSpecIso Γ(Y, (↑U : Y.Opens))) ≫
          Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)))
have he : Hom.app f (↑U : Y.Opens) ≫ e.hom =
  Iso.inv (ΓSpecIso Γ(Y, (↑U : Y.Opens))) ≫ Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)
Tactic: have he : f.app U ≫ e.hom =
      (ΓSpecIso Γ(Y, ↑U)).inv ≫ (pullback.snd f U.1.ι ≫ U.1.toSpecΓ).appTop := by
    rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]
    simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom,
      Iso.op_hom, eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, Hom.appLE_comp_appLE,
      Opens.map_top, e, pullback.condition, IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]
    rw [Hom.comp_appLE, Opens.ι_app]
    exact Hom.map_appLE _ _ (homOfLE le_top).op
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
e : Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤) :=
  Iso.trans (Y := Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯)) :
      Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) ≅ Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤))
    (Hom.appIso (pullback.fst f (↑U : Y.Opens).ι) ⊤ :
      Γ(X, pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤) ≅ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
he :
  Hom.app f (↑U : Y.Opens) ≫ e.hom =
    Iso.inv (ΓSpecIso Γ(Y, (↑U : Y.Opens))) ≫ Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(pullback f (↑U : Y.Opens).ι, ⊤) : Type u))
      (CommRingCat.Hom.hom
        (Iso.inv (ΓSpecIso Γ(Y, (↑U : Y.Opens))) ≫
          Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)))
have rw : (Hom.ker f).ideal U ≤ RingHom.ker (CommRingCat.Hom.hom (Hom.app f (↑U : Y.Opens) ≫ e.hom))
Tactic: rw [← he]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ toImageAux f ≫ imageι f = f
have h : ∀
  (x :
    (Precoverage.ZeroHypercover.pullback₁ f
        (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).I₀),
  (Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
        x ≫
      toImageAux f ≫ imageι f =
    (Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
        x ≫
      f
Tactic: apply Cover.hom_ext ((Y.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top Y)).pullback₁ f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U :
  (Precoverage.ZeroHypercover.pullback₁ f
      (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
        U ≫
      toImageAux f ≫ imageι f =
    (Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
        U ≫
      f
have h : (liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) sorry ≫
      (ker f).subschemeCover.f (P := IsOpenImmersion) U) ≫
    imageι f =
  (Precoverage.ZeroHypercover.pullback₁ f
          (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
      U ≫
    f
Tactic: simp only [Hom.toImageAux, Cover.ι_glueMorphisms_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ toImage f ≫ imageι f = f
have h : toImage f = toImageAux f
Tactic: convert! f.toImageAux_spec using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₁ : Eq (α := Set ↥(Hom.image f))
  (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
  Set.univ
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₂ : Subset (α := Set ↥(Hom.image f)) Set.univ
  (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₃ : Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
  (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
rw₃ :
  Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₄ : Subset (α := Set ↥Y) (Set.range (ι := ↥(Hom.image f)) ⇑(Hom.imageι f))
  (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
rw₃ :
  Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₄ :
  Subset (α := Set ↥Y) (Set.range (ι := ↥(Hom.image f)) ⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₅ : (↑(Hom.ker f).support : Set ↥Y) ⊆
  closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
rw₃ :
  Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₄ :
  Subset (α := Set ↥Y) (Set.range (ι := ↥(Hom.image f)) ⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₅ :
  (↑(Hom.ker f).support : Set ↥Y) ⊆
    closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₆ : Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
  (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
rw₃ :
  Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₄ :
  Subset (α := Set ↥Y) (Set.range (ι := ↥(Hom.image f)) ⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₅ :
  (↑(Hom.ker f).support : Set ↥Y) ⊆
    closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))
rw₆ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₇ : Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
  (closure (Set.range (ι := ↥X) (Function.comp (β := ↥(Hom.image f)) ⇑(Hom.imageι f) ⇑(Hom.toImage f))))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
rw₃ :
  Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₄ :
  Subset (α := Set ↥Y) (Set.range (ι := ↥(Hom.image f)) ⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₅ :
  (↑(Hom.ker f).support : Set ↥Y) ⊆
    closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))
rw₆ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₇ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.range (ι := ↥X) (Function.comp (β := ↥(Hom.image f)) ⇑(Hom.imageι f) ⇑(Hom.toImage f))))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₈ : Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
  (closure
    (Set.range (ι := ↥X)
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((Hom.toImage f).base ≫ (Hom.imageι f).base)) :
        (a : ↥X) → ↥Y)))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
rw : Eq (α := Set ↥(Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f))) Set.univ
rw₁ :
  Eq (α := Set ↥(Hom.image f))
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
    Set.univ
rw₂ :
  Subset (α := Set ↥(Hom.image f)) Set.univ
    (Set.preimage (β := ↥Y) (⇑(Hom.imageι f))
      (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))))
rw₃ :
  Subset (α := Set ↥Y) (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) Set.univ)
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₄ :
  Subset (α := Set ↥Y) (Set.range (ι := ↥(Hom.image f)) ⇑(Hom.imageι f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₅ :
  (↑(Hom.ker f).support : Set ↥Y) ⊆
    closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f)))
rw₆ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.image (α := ↥(Hom.image f)) (⇑(Hom.imageι f)) (Set.range (ι := ↥X) ⇑(Hom.toImage f))))
rw₇ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.range (ι := ↥X) (Function.comp (β := ↥(Hom.image f)) ⇑(Hom.imageι f) ⇑(Hom.toImage f))))
rw₈ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure
      (Set.range (ι := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              ((Hom.toImage f).base ≫ (Hom.imageι f).base)) :
          (a : ↥X) → ↥Y)))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥X) ⇑(Hom.toImage f)
have rw₉ : Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f ≫ Hom.imageι f)))
Tactic: rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]