awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Hom.app I.subschemeι (↑U : X.Opens) = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
have this : I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι = I.glueDataObjι U ≫ (↑U : X.Opens).ι
Tactic: have := I.subschemeCover_map_subschemeι U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
this : I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι = I.glueDataObjι U ≫ (↑U : X.Opens).ι
⊢ Hom.app I.subschemeι (↑U : X.Opens) = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
have this₁ : I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι =
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec sorry
Tactic: simp only [glueDataObjι, Category.assoc, IsAffineOpen.isoSpec_inv_ι] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
this :
  I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
⊢ Hom.app I.subschemeι (↑U : X.Opens) = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
have this₁ : Eq (α :=
  Γ(X, (↑U : X.Opens)) ⟶
    Γ(Spec (I.subschemeCover.X U), (I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι) ⁻¹ᵁ (↑U : X.Opens)))
  (Hom.app (I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι) (↑U : X.Opens))
  (Hom.app (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec sorry) (↑U : X.Opens) ≫
    (Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: replace this := Scheme.Hom.congr_app this U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
this_1 :
  I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  Eq (α :=
    Γ(X, (↑U : X.Opens)) ⟶
      Γ(Spec (I.subschemeCover.X U), (I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι) ⁻¹ᵁ (↑U : X.Opens)))
    (Hom.app (I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι) (↑U : X.Opens))
    (Hom.app (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯) (↑U : X.Opens) ≫
      (Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Hom.app I.subschemeι (↑U : X.Opens) = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
have this₁ : Hom.app I.subschemeι (↑U : X.Opens) ≫
    Hom.app (I.subschemeCover.f (P := IsOpenImmersion) U) (I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) =
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫
    Iso.inv (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) ≫
      (Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map
          (Quiver.Hom.op
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map
              (Quiver.Hom.unop (eqToHom sorry)))) ≫
        (Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (eqToHom sorry)
Tactic: simp only [Hom.comp_base, TopologicalSpace.Opens.map_comp_obj, Hom.comp_app,
    IsAffineOpen.fromSpec_app_self, eqToHom_op, Category.assoc, Hom.naturality_assoc,
    TopologicalSpace.Opens.map_top, ← ΓSpecIso_inv_naturality_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
this_1 :
  I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  Hom.app I.subschemeι (↑U : X.Opens) ≫
      Hom.app (I.subschemeCover.f (P := IsOpenImmersion) U) (I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫
      Iso.inv (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) ≫
        (Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map
            (Quiver.Hom.op
              ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map
                (Quiver.Hom.unop (eqToHom ⋯)))) ≫
          (Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (eqToHom ⋯)
⊢ Hom.app I.subschemeι (↑U : X.Opens) = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
have this₁ : (((Hom.app I.subschemeι (↑U : X.Opens) ≫
          Hom.app (I.subschemeCover.f (P := IsOpenImmersion) U) (I.subschemeι ⁻¹ᵁ (↑U : X.Opens))) ≫
        inv ((Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (eqToHom sorry))) ≫
      inv
        ((Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map
          (Quiver.Hom.op
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map
              (Quiver.Hom.unop (eqToHom sorry)))))) ≫
    inv (Iso.inv (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)))) =
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
Tactic: simp_rw [← Category.assoc, ← IsIso.comp_inv_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Function.Surjective (α := (↑Γ(X, (↑U : X.Opens)) : Type u)) (β :=
    (↑Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, (↑U : X.Opens))) (Hom.app I.subschemeι (↑U : X.Opens))) :
      (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Type u))
have rw : Function.Surjective (α := (↑Γ(X, (↑U : X.Opens)) : Type u)) (β :=
  (↑Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv)) :
    (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Type u))
Tactic: rw [I.subschemeι_app U]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ RingHom.ker (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app I.subschemeι (↑U : X.Opens))) =
    I.ideal U
have rw : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv)) =
  I.ideal U
Tactic: rw [subschemeι_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
e : CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) :=
  Iso.symm (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) ≪≫
    Iso.symm (Hom.appIso (I.subschemeCover.f (P := IsOpenImmersion) U) ⊤) ≪≫
      Functor.mapIso I.subscheme.presheaf (Iso.op (eqToIso ⋯))
⊢ RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv)) =
    I.ideal U
have change : RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U
Tactic: change RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp
    (Ideal.Quotient.mk (I.ideal U))) = _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
e : CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) :=
  Iso.symm (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) ≪≫
    Iso.symm (Hom.appIso (I.subschemeCover.f (P := IsOpenImmersion) U) ⊤) ≪≫
      Functor.mapIso I.subscheme.presheaf (Iso.op (eqToIso ⋯))
⊢ RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U
have rw : RingHom.ker (F :=
    (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
    (Ideal.Quotient.mk (I.ideal U)) =
  I.ideal U
Tactic: rw [RingHom.ker_equiv_comp, Ideal.mk_ker]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
e : CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) ≅ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) :=
  Iso.symm (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) ≪≫
    Iso.symm (Hom.appIso (I.subschemeCover.f (P := IsOpenImmersion) U) ⊤) ≪≫
      Functor.mapIso I.subscheme.presheaf (Iso.op (eqToIso ⋯))
rw :
  RingHom.ker (F :=
      (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
      (Ideal.Quotient.mk (I.ideal U)) =
    I.ideal U
⊢ RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U
have rw₁ : I.ideal U = I.ideal U
Tactic: rw [RingHom.ker_equiv_comp, Ideal.mk_ker]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ Hom.ker I.subschemeι = I
have h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)),
  x_1 ∈ (Hom.ker I.subschemeι).ideal x ↔ x_1 ∈ I.ideal x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ IsEmpty.{u + 1} ↥(subscheme (X := X) ⊤)
have rw : Eq.{u + 1} (α := X.IdealSheafData) (Hom.ker (X := subscheme (X := X) ⊤) (subschemeι ⊤)) ⊤
Tactic: rw [← (subschemeι _).ker_eq_top_iff_isEmpty, ker_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
rw : Eq.{u + 1} (α := X.IdealSheafData) (Hom.ker (X := subscheme (X := X) ⊤) (subschemeι ⊤)) ⊤
⊢ IsEmpty.{u + 1} ↥(subscheme (X := X) ⊤)
have rw₁ : Eq.{u + 1} (α := X.IdealSheafData) ⊤ ⊤
Tactic: rw [← (subschemeι _).ker_eq_top_iff_isEmpty, ker_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : (↑X.affineOpens : Type u)
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U
have rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor sorry)) ≫ I.glueDataObjι U = J.glueDataObjι U
Tactic: rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : (↑X.affineOpens : Type u)
rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫ I.glueDataObjι U = J.glueDataObjι U
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U
have rw₁ : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor sorry)) ≫
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv =
  J.glueDataObjι U
Tactic: rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : (↑X.affineOpens : Type u)
rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫ I.glueDataObjι U = J.glueDataObjι U
rw₁ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    J.glueDataObjι U
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U
have rw₂ : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor sorry)) ≫
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv =
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv
Tactic: rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : (↑X.affineOpens : Type u)
rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫ I.glueDataObjι U = J.glueDataObjι U
rw₁ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    J.glueDataObjι U
rw₂ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U
have rw₃ : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ CommRingCat.ofHom (Ideal.Quotient.factor sorry)) ≫
    (IsAffineOpen.isoSpec sorry).inv =
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv
Tactic: rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : (↑X.affineOpens : Type u)
rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫ I.glueDataObjι U = J.glueDataObjι U
rw₁ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    J.glueDataObjι U
rw₂ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
rw₃ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U
have rw₄ : Spec.map
      (CommRingCat.ofHom
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factor sorry)
          (Ideal.Quotient.mk (I.ideal U)))) ≫
    (IsAffineOpen.isoSpec sorry).inv =
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv
Tactic: rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : (↑X.affineOpens : Type u)
rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫ I.glueDataObjι U = J.glueDataObjι U
rw₁ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    J.glueDataObjι U
rw₂ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
rw₃ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
rw₄ :
  Spec.map
        (CommRingCat.ofHom
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Ideal.Quotient.factor ⋯)
            (Ideal.Quotient.mk (I.ideal U)))) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
⊢ glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U
have rw₅ : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv =
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv
Tactic: rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ glueDataObjHom ⋯ U = 𝟙 (I.glueDataObj U)
have rw : glueDataObjHom sorry U ≫ I.glueDataObjι U = 𝟙 (I.glueDataObj U) ≫ I.glueDataObjι U
Tactic: rw [← cancel_mono (I.glueDataObjι U)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I J K : X.IdealSheafData
hIJ : I ≤ J
hJK : J ≤ K
U : (↑X.affineOpens : Type u)
⊢ glueDataObjHom hJK U ≫ glueDataObjHom hIJ U = glueDataObjHom ⋯ U
have rw : (glueDataObjHom hJK U ≫ glueDataObjHom hIJ U) ≫ I.glueDataObjι U = glueDataObjHom sorry U ≫ I.glueDataObjι U
Tactic: rw [← cancel_mono (I.glueDataObjι U)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I_1 I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ Eq (α := pullback (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f V) ⟶ I.subscheme)
    (pullback.fst (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f V) ≫
      (fun (U : J.subschemeCover.openCover.I₀) ↦ glueDataObjHom h U ≫ I.subschemeCover.f (P := IsOpenImmersion) U) U)
    (pullback.snd (J.subschemeCover.openCover.f U) (J.subschemeCover.openCover.f V) ≫
      (fun (U : J.subschemeCover.openCover.I₀) ↦ glueDataObjHom h U ≫ I.subschemeCover.f (P := IsOpenImmersion) U) V)
have simp : Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
  (pullback.fst (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.glueDataObjι U ≫ (↑U : X.Opens).ι)
  (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.glueDataObjι V ≫ (↑V : X.Opens).ι)
Tactic: simp only [← cancel_mono I.subschemeι, AffineOpenCover.openCover_X, glueDataObjHom_ι_assoc,
      AffineOpenCover.openCover_f, Category.assoc, subschemeCover_map_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I_1 I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
    (pullback.fst (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι U ≫ (↑U : X.Opens).ι)
    (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι V ≫ (↑V : X.Opens).ι)
have rw : Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
  (pullback.fst (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.subschemeCover.f (P := IsOpenImmersion) U ≫ J.subschemeι)
  (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.glueDataObjι V ≫ (↑V : X.Opens).ι)
Tactic: rw [← subschemeCover_map_subschemeι, pullback.condition_assoc, subschemeCover_map_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I_1 I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
rw :
  Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
    (pullback.fst (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.subschemeCover.f (P := IsOpenImmersion) U ≫ J.subschemeι)
    (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι V ≫ (↑V : X.Opens).ι)
⊢ Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
    (pullback.fst (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι U ≫ (↑U : X.Opens).ι)
    (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι V ≫ (↑V : X.Opens).ι)
have rw₁ : Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
  (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.subschemeCover.f (P := IsOpenImmersion) V ≫ J.subschemeι)
  (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.glueDataObjι V ≫ (↑V : X.Opens).ι)
Tactic: rw [← subschemeCover_map_subschemeι, pullback.condition_assoc, subschemeCover_map_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I_1 I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
rw :
  Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
    (pullback.fst (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.subschemeCover.f (P := IsOpenImmersion) U ≫ J.subschemeι)
    (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι V ≫ (↑V : X.Opens).ι)
rw₁ :
  Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
    (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.subschemeCover.f (P := IsOpenImmersion) V ≫ J.subschemeι)
    (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι V ≫ (↑V : X.Opens).ι)
⊢ Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
    (pullback.fst (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι U ≫ (↑U : X.Opens).ι)
    (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
      J.glueDataObjι V ≫ (↑V : X.Opens).ι)
have rw₂ : Eq (α := pullback (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ⟶ X)
  (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.glueDataObjι V ≫ (↑V : X.Opens).ι)
  (pullback.snd (J.subschemeCover.f (P := IsOpenImmersion) U) (J.subschemeCover.f (P := IsOpenImmersion) V) ≫
    J.glueDataObjι V ≫ (↑V : X.Opens).ι)
Tactic: rw [← subschemeCover_map_subschemeι, pullback.condition_assoc, subschemeCover_map_subschemeι]