awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₂ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₃ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₄ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
a₅ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    (↑(↑U : X.Opens) : Set ↥X) ∩ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo
a₆ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
a₇ : (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) = (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
a₈ a₉ : (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X) = (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))

Tactic:
rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, Set.inter_comm, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.ι_gluedTo, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.Scheme.IdealSheafData.range_gluedTo, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥I.glueData.glued) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U))
    (Set.range (ι := ↥(↑(I.gluedTo ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) ⇑(I.gluedTo ⁻¹ᵁ (↑U : X.Opens)).ι)

Tactic:
simp only [Scheme.Opens.range_ι, TopologicalSpace.Opens.map_coe, range_glueData_ι]

Premises used: TopologicalSpace.Opens.map_coe, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.range_glueData_ι, AlgebraicGeometry.Scheme.Opens.range_ι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (I.glueDataObjIso U).hom ≫ (I.gluedTo ⁻¹ᵁ (↑U : X.Opens)).ι = I.glueData.ι U

Tactic:
IsOpenImmersion.isoOfRangeEq_hom_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ ((I.glueDataObjIso U).hom ≫ I.gluedTo ∣_ (↑U : X.Opens)) ≫ (↑U : X.Opens).ι = I.glueDataObjι U ≫ (↑U : X.Opens).ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
rw :
  ∀ (i : (↑X.affineOpens : Type u)),
    IsPreimmersion (X := (↑(I.gluedTo ⁻¹ᵁ (↑i : X.Opens)) : Scheme)) (I.gluedTo ∣_ (↑i : X.Opens))
⊢ IsPreimmersion I.gluedTo

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsPreimmersion)
    _ (iSup_affineOpens_eq_top X)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
rw : IsPreimmersion (I.glueDataObjι U)
⊢ IsPreimmersion (X := (↑(I.gluedTo ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (I.gluedTo ∣_ (↑U : X.Opens))

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsPreimmersion (I.glueDataObjIso U).hom,
    glueDataObjIso_hom_restrict]

Premises used: AlgebraicGeometry.IsPreimmersion, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso_hom_restrict, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjIso
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ IsPreimmersion (I.glueDataObjι U)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
⊢ QuasiCompact I.gluedTo

Tactic:
⟨fun _ _ ↦ (Topology.IsClosedEmbedding.isProperMap
    ⟨I.gluedTo.isEmbedding, I.range_gluedTo ▸ I.support.isClosed⟩).isCompact_preimage⟩

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, TopologicalSpace.Closeds.isClosed, Eq.rec, IsProperMap.isCompact_preimage, AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.Scheme.IdealSheafData.gluedTo, Topology.IsClosedEmbedding.isProperMap, AlgebraicGeometry.Scheme.IdealSheafData.range_gluedTo, AlgebraicGeometry.QuasiCompact.mk, Eq.symm, Topology.IsClosedEmbedding.mk
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
h : ∀ (x : ↥I.subscheme), (I.subschemeIso.hom ≫ I.gluedTo) x = (↑x : ↥X)
⊢ Eq (α := (a : ↥I.subscheme) → ↥X) (⇑(I.subschemeIso.hom ≫ I.gluedTo))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ I.support))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
h h₁ : (↑x : ↥X) = (↑x : ↥X)
⊢ (↑((I.gluedHomeo : (a : ↥I.glueData.glued) → ↥I.support)
          ((I.gluedHomeo.symm : (a : ↥I.support) → ↥I.glueData.glued) x)) :
      ↥X) =
    (↑x : ↥X)

Tactic:
rw [I.gluedHomeo.apply_symm_apply]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.gluedHomeo, Homeomorph.apply_symm_apply
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
⊢ I.subschemeι x = (↑x : ↥X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
⊢ I.subschemeι = I.subschemeIso.hom ≫ I.gluedTo

Tactic:
Scheme.Hom.copyBase_eq _ _ _

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, AlgebraicGeometry.Scheme.Hom.copyBase_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
rw : IsPreimmersion (I.subschemeIso.hom ≫ I.gluedTo)
⊢ IsPreimmersion I.subschemeι

Tactic:
rw [subschemeι_def]

Premises used: _private.0.AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_def
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
⊢ IsPreimmersion (I.subschemeIso.hom ≫ I.gluedTo)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
rw : QuasiCompact (I.subschemeIso.hom ≫ I.gluedTo)
⊢ QuasiCompact I.subschemeι

Tactic:
rw [subschemeι_def]

Premises used: _private.0.AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_def
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
⊢ QuasiCompact (I.subschemeIso.hom ≫ I.gluedTo)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
⊢ Set.range (ι := ↥I.subscheme) ⇑I.subschemeι = (↑I.support : Set ↥X)

Tactic:
simp [← range_gluedTo, I.subschemeι_def, Set.range_comp]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.IdealSheafData.range_gluedTo, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_def
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
h :
  (↑(Hom.opensRange (X := I.glueData.U U) (I.glueData.ι U ≫ I.subschemeIso.inv)) : Set ↥I.subscheme) =
    (↑(I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Set ↥I.subscheme)
⊢ Hom.opensRange (X := I.glueData.U U) (I.glueData.ι U ≫ I.subschemeIso.inv) = I.subschemeι ⁻¹ᵁ (↑U : X.Opens)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (↑(Hom.opensRange (X := I.glueData.U U) (I.glueData.ι U ≫ I.subschemeIso.inv)) : Set ↥I.subscheme) =
    (↑(I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Set ↥I.subscheme)

Tactic:
simp [Set.range_comp, I.range_glueData_ι, subschemeι_def, ← coe_homeoOfIso_symm,
    ← homeoOfIso_symm, ← Homeomorph.coe_symm_toEquiv, Equiv.image_symm_eq_preimage]

Premises used: Set.range_comp, Homeomorph.coe_symm_toEquiv, AlgebraicGeometry.Scheme.homeoOfIso_symm, AlgebraicGeometry.Scheme.coe_homeoOfIso_symm, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.range_glueData_ι, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_def, Equiv.image_symm_eq_preimage
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).I₀ :=
  Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯) (↑x : ↥X)
⊢ (↑x : ↥X) ∈ (↑U : X.Opens)

Tactic:
obtain ⟨⟨y, hy : y ∈ U.1⟩, rfl : y = x.1⟩ :=
      (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X)).covers x.1

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, AlgebraicGeometry.Scheme.Cover.covers, Subtype.val, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).I₀ :=
  Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯) (↑x : ↥X)
hy : (↑x : ↥X) ∈ (↑U : X.Opens)
⊢ Membership.mem (γ := Set ↥I.subscheme)
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (HasQuotient.Quotient
              (↑Γ(X,
                    (↑(Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                          (↑x : ↥X)) :
                      X.Opens)) :
                Type u)
              (B :=
              Ideal
                (↑Γ(X,
                      (↑(Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                            (↑x : ↥X)) :
                        X.Opens)) :
                  Type u))
              (I.ideal
                (Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                  (↑x : ↥X)))))))
      ⇑(I.glueData.ι
            (Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯) (↑x : ↥X)) ≫
          I.subschemeIso.inv))
    x

Tactic:
(I.opensRange_glueData_ι_subschemeIso_inv U).ge hy

Premises used: Eq.ge, Set.Mem, setOf, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueData_ι_subschemeIso_inv, Set.range
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).I₀ :=
  Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯) (↑x : ↥X)
hy : (↑x : ↥X) ∈ (↑U : X.Opens)
⊢ Membership.mem (γ := Set ↥I.subscheme)
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (HasQuotient.Quotient
              (↑Γ(X,
                    (↑(Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                          (↑x : ↥X)) :
                      X.Opens)) :
                Type u)
              (B :=
              Ideal
                (↑Γ(X,
                      (↑(Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                            (↑x : ↥X)) :
                        X.Opens)) :
                  Type u))
              (I.ideal
                (Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                  (↑x : ↥X)))))))
      ⇑(I.glueData.ι
            (Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯) (↑x : ↥X)) ≫
          I.subschemeIso.inv))
    x

Tactic:
exact (I.opensRange_glueData_ι_subschemeIso_inv U).ge hy

Premises used: Eq.ge, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueData_ι_subschemeIso_inv
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Hom.opensRange (I.subschemeCover.f (P := IsOpenImmersion) U) = I.subschemeι ⁻¹ᵁ (↑U : X.Opens)

Tactic:
I.opensRange_glueData_ι_subschemeIso_inv U

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueData_ι_subschemeIso_inv
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι = I.glueDataObjι U ≫ (↑U : X.Opens).ι

Tactic:
simp [subschemeCover, subschemeι_def]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_def
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ ⊤ = I.subschemeι ⁻¹ᵁ (↑U : X.Opens)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι = I.glueDataObjι U ≫ (↑U : X.Opens).ι

Tactic:
have := I.subschemeCover_map_subschemeι U
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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).ι
⊢ I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
simp only [glueDataObjι, Category.assoc, IsAffineOpen.isoSpec_inv_ι] at this

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯
⊢ 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 ⋯)))

Tactic:
replace this := Scheme.Hom.congr_app this U
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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) ≫
      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 ⋯)

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

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.Scheme.Hom.naturality_assoc, CategoryTheory.eqToHom_op, TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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) ≫
            Hom.app (I.subschemeCover.f (P := IsOpenImmersion) U) (I.subschemeι ⁻¹ᵁ (↑U : X.Opens))) ≫
          inv ((Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (eqToHom ⋯))) ≫
        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 ⋯)))))) ≫
      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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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))) ≫
          inv ((Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (eqToHom ⋯))) ≫
        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 ⋯)))))) ≫
      inv (Iso.inv (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)))) =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.app I.subschemeι (↑U : X.Opens) =
    Hom.app I.subschemeι (↑U : X.Opens) ≫ 𝟙 Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens))

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
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))
⊢ 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))

Tactic:
rw [I.subschemeι_app U]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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) (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:
(I.subschemeObjIso U).commRingCatIsoToRingEquiv.symm.surjective.comp
    Ideal.Quotient.mk_surjective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso, RingEquiv.surjective, Ideal.Quotient.mk_surjective, Function.Surjective.comp, RingEquiv.symm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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) (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:
exact (I.subschemeObjIso U).commRingCatIsoToRingEquiv.symm.surjective.comp
    Ideal.Quotient.mk_surjective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso, RingEquiv.surjective, Ideal.Quotient.mk_surjective, Function.Surjective.comp, RingEquiv.symm