awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
have h₃ : closure (Set.range (ι := ↥I.subscheme) (Function.comp (β := ↥X) ⇑f ⇑I.subschemeι)) =
  (↑(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)
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)
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
have h₄ : closure (Set.image (α := ↥X) (⇑f) (Set.range (ι := ↥I.subscheme) ⇑I.subschemeι)) =
  (↑(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)
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)
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
have h₅ : closure (⇑f '' (↑I.support : Set ↥X)) = (↑(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)
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)
⊢ (↑(I.map f).support : Set ↥Y) = (↑(TopologicalSpace.Closeds.closure (⇑f '' (↑I.support : Set ↥X))) : Set ↥Y)
have h₆ : Eq (α := Set ↥Y) (closure (⇑f '' (↑I.support : Set ↥X))) (closure (⇑f '' (↑I.support : Set ↥X)))
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 (hypothesis)
Goal:
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
inst : QuasiCompact f
U : (↑Y.affineOpens : Type u)
H : IsAffineOpen (f ⁻¹ᵁ (↑U : Y.Opens))
⊢ (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))
have 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)))))
  ⊥
Tactic: have : RingHom.ker (I.subschemeObjIso ⟨_, H⟩).inv.hom = ⊥ :=
    RingHom.ker_coe_equiv (I.subschemeObjIso ⟨_, H⟩).symm.commRingCatIsoToRingEquiv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
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)) ⋯))
have 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)) sorry) : 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)) sorry)))
  (Ideal.comap (S :=
    (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑U : X.Opens)) sorry) : 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)) sorry)))
Tactic: refine (ker_ideal_of_isPullback_of_isOpenImmersion _ _ _ _
    (IsPullback.of_hasPullback f I.subschemeι) U).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).hom ≫ pullback.snd f I.subschemeι = (I.comap f).subschemeMap I f ⋯
have rw : ((I.comapIso f).hom ≫ pullback.snd f I.subschemeι) ≫ I.subschemeι = (I.comap f).subschemeMap I f sorry ≫ I.subschemeι
Tactic: rw [← cancel_mono I.subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent (goal)
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ IsOpen (X := ↥X) (⋃₀ (irreducibleComponents ↥X \ {Z}))ᶜ
have rw : IsClosed.{u} (X := ↥X)
  (⋃ (i : Set ↥X), ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {Z}) i), i)
Tactic: rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent (goal)
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ Z =
    ⋂ (U : (↑X.affineOpens : Type u)),
      X.zeroLocus (↑((Hom.ker (X.irreducibleComponentOpen Z).ι).ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
have rw : Z = closure (↑(X.irreducibleComponentOpen Z) : Set ↥X)
Tactic: rw [← IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, Hom.support_ker, Opens.range_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent (goal)
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ X.irreducibleComponentIdeal Z hZ = Hom.ker (X.irreducibleComponentOpen Z).ι
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent (hypothesis)
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ X.irreducibleComponentOpen Z = ⊤
have hZ₁ : Z = Set.univ
Tactic: rw [irreducibleComponents_eq_singleton, Set.mem_singleton_iff] at hZ
Cleared hypotheses: hZ, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent (goal)
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
have rw : CategoryTheory.IsIso.{u, u + 1} (X := (↑⊤ : Scheme)) (Opens.ι ⊤)
Tactic: rw [irreducibleComponentOpen_eq_top X Z hZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent (hypothesis)
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ CategoryTheory.IsIso (X := X.irreducibleComponent Z hZ) (X.irreducibleComponentι Z hZ)
have this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
Tactic: have : CategoryTheory.IsIso (irreducibleComponentOpen X Z).ι := by
    rw [irreducibleComponentOpen_eq_top X Z hZ]
    exact X.topIso.isIso_hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent (goal)
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
⊢ CategoryTheory.IsIso (X := X.irreducibleComponent Z hZ) (X.irreducibleComponentι Z hZ)
have rw : Eq.{u + 1} (α := X.IdealSheafData) (Hom.ker (X := (↑⊤ : Scheme)) (Opens.ι ⊤)) ⊥
Tactic: rw [irreducibleComponentι, isIso_subschemeι_iff_eq_bot, irreducibleComponentIdeal_def,
    irreducibleComponentOpen_eq_top X Z hZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ I.glueDataObjι U ≫ (↑U : X.Opens).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
have rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv ≫ (↑U : X.Opens).ι =
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec sorry
Tactic: rw [glueDataObjι, Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom) (I.ideal U))
have rw : Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
  (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))))
  (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom)
    (RingHom.ker (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
      (Ideal.Quotient.mk (I.ideal U))))
Tactic: rw [← Ideal.mk_ker (I := I.ideal _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom)
      (RingHom.ker (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
        (Ideal.Quotient.mk (I.ideal U))))
have change : Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
  (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec sorry).inv))))
  (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ)))
Tactic: change RingHom.ker (Spec.map φ ≫ _).appTop.hom = (RingHom.ker φ.hom).comap _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ)))
have rw : Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
  (RingHom.ker
    (CommRingCat.Hom.hom
      (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec sorry).inv) ≫
        Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))))))
  (RingHom.ker (CommRingCat.Hom.hom ((↑U : X.Opens).topIso.hom ≫ φ)))
Tactic: rw [← RingHom.ker_equiv_comp _ (Scheme.ΓSpecIso _).commRingCatIsoToRingEquiv, RingHom.comap_ker,
    RingEquiv.toRingHom_eq_coe, Iso.commRingCatIsoToRingEquiv_toRingHom, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
          Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))))))
    (RingHom.ker (CommRingCat.Hom.hom ((↑U : X.Opens).topIso.hom ≫ φ)))
have e_f : Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec sorry).inv) ≫
    Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) =
  (↑U : X.Opens).topIso.hom ≫ φ
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
      Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) =
    (↑U : X.Opens).topIso.hom ≫ φ
have e_f : Hom.app (IsAffineOpen.isoSpec sorry).inv ⊤ ≫ Iso.hom (ΓSpecIso Γ(X, (↑U : X.Opens))) ≫ φ =
  X.presheaf.map (Quiver.Hom.op (eqToHom sorry)) ≫ φ
Tactic: simp only [Scheme.Hom.comp_app, TopologicalSpace.Opens.map_top, Category.assoc,
    Scheme.ΓSpecIso_naturality, Scheme.Opens.topIso_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.app (IsAffineOpen.isoSpec ⋯).inv ⊤ ≫ Iso.hom (ΓSpecIso Γ(X, (↑U : X.Opens))) ≫ φ =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ φ
have e_f : (↑U : X.Opens).topIso.hom ≫ φ = X.presheaf.map (Quiver.Hom.op (eqToHom sorry)) ≫ φ
Tactic: rw [← Scheme.Hom.appTop, U.2.isoSpec_inv_appTop, Category.assoc, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme)) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U))
    (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))
have simp : Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
  (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec sorry).inv)
    (Set.range (ι := ↥(I.glueDataObj U)) ⇑(Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))))
  ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec sorry).inv a) ''
    PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: simp only [glueDataObjι, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (Set.range (ι := ↥(I.glueDataObj U)) ⇑(Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
have erw : Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
  (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec sorry).inv)
    (PrimeSpectrum.zeroLocus
      (↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) :
        Set (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u))))
  ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec sorry).inv a) ''
    PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: erw [range_comap_of_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
erw :
  Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus
        (↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) :
          Set (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (Set.range (ι := ↥(I.glueDataObj U)) ⇑(Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
have hf : Function.Surjective (α := (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) (β :=
  (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
  (⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) :
    (a : (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) →
      (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
Tactic: erw [range_comap_of_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus
        (↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) :
          Set (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
have simp : Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
  (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec sorry).inv)
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))
  ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec sorry).inv a) ''
    PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: simp