awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 (CommRingCat.Hom.hom (Hom.app f (↑U : Y.Opens) ≫ e.hom))

Tactic:
refine (IdealSheafData.ideal_ofIdeals_le _ _).trans_eq
    (RingHom.ker_equiv_comp _ e.commRingCatIsoToRingEquiv).symm

Premises used: LE.le.trans_eq, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U_1 : (↑Y.affineOpens : Type u)
U :
  (Precoverage.ZeroHypercover.pullback₁ f
      (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀
⊢ (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))) ≫ appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)))

Tactic:
ideal_ker_le_ker_ΓSpecIso_inv_comp f U

Premises used: AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U_1 : (↑Y.affineOpens : Type u)
U :
  (Precoverage.ZeroHypercover.pullback₁ f
      (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀
⊢ (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))) ≫ appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)))

Tactic:
exact ideal_ker_le_ker_ΓSpecIso_inv_comp f U

Premises used: AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U_1 : (↑Y.affineOpens : Type u)
U V :
  (Precoverage.ZeroHypercover.pullback₁ f
      (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀
⊢ Eq (α :=
    pullback
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          U)
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          V) ⟶
      Y)
    ((pullback.fst
          ((Precoverage.ZeroHypercover.pullback₁ f
                (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
            U)
          ((Precoverage.ZeroHypercover.pullback₁ f
                (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
            V) ≫
        (fun
              (U :
                (Precoverage.ZeroHypercover.pullback₁ f
                    (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀) ↦
            liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) ⋯ ≫
              (ker f).subschemeCover.f (P := IsOpenImmersion) U)
          U) ≫
      imageι f)
    ((pullback.snd
          ((Precoverage.ZeroHypercover.pullback₁ f
                (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
            U)
          ((Precoverage.ZeroHypercover.pullback₁ f
                (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
            V) ≫
        (fun
              (U :
                (Precoverage.ZeroHypercover.pullback₁ f
                    (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀) ↦
            liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) ⋯ ≫
              (ker f).subschemeCover.f (P := IsOpenImmersion) U)
          V) ≫
      imageι f)

Tactic:
simp [IdealSheafData.glueDataObjι, Scheme.Hom.liftQuotient_comp_assoc,
      ← pullback.condition, ← pullback.condition_assoc]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ∀
    (x :
      (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
          x ≫
        toImageAux f ≫ imageι f =
      (Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          x ≫
        f
⊢ toImageAux f ≫ imageι f = f

Tactic:
apply Cover.hom_ext ((Y.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top Y)).pullback₁ f)

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U :
  (Precoverage.ZeroHypercover.pullback₁ f
      (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀
h :
  (liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) ⋯ ≫
        (ker f).subschemeCover.f (P := IsOpenImmersion) U) ≫
      imageι f =
    (Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
        U ≫
      f
⊢ (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

Tactic:
simp only [Hom.toImageAux, Cover.ι_glueMorphisms_assoc]

Premises used: AlgebraicGeometry.Scheme.Hom.toImageAux, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U :
  (Precoverage.ZeroHypercover.pullback₁ f
      (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀
⊢ (liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) ⋯ ≫
        (ker f).subschemeCover.f (P := IsOpenImmersion) U) ≫
      imageι f =
    (Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
        U ≫
      f

Tactic:
simp [IdealSheafData.glueDataObjι, Scheme.Hom.liftQuotient_comp_assoc, pullback.condition]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ toImageAux f ≫ imageι f = f

Tactic:
f.toImageAux_spec

Premises used: AlgebraicGeometry.Scheme.Hom.toImageAux_spec
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
h : toImage f = toImageAux f
⊢ toImage f ≫ imageι f = f

Tactic:
convert! f.toImageAux_spec using 2

Premises used: AlgebraicGeometry.Scheme.Hom.toImageAux_spec
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ toImage f = toImageAux f

Tactic:
Scheme.Hom.copyBase_eq _ _ _

Premises used: AlgebraicGeometry.Scheme.Hom.toImage, AlgebraicGeometry.Scheme.Hom.copyBase_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ toImage f = toImageAux f

Tactic:
exact Scheme.Hom.copyBase_eq _ _ _

Premises used: AlgebraicGeometry.Scheme.Hom.copyBase_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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)))
rw₉ :
  Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f))
    (closure (Set.range (ι := ↥X) ⇑(Hom.toImage f ≫ Hom.imageι f)))
rw₁₀ rw₁₁ : Subset (α := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) (closure (Set.range (ι := ↥X) ⇑f))
⊢ DenseRange (X := ↥(Hom.image f)) (α := ↥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ι]

Premises used: Set.univ_subset_iff, Set.range_comp, Set.image_univ, AlgebraicGeometry.Scheme.Hom.imageι, AlgebraicGeometry.Scheme.Hom.toImage_imageι, AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, AlgebraicGeometry.Scheme.Hom.isEmbedding, denseRange_iff_closure_range, AlgebraicGeometry.Scheme.Hom.support_ker, Set.image_subset_iff, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
⊢ QuasiCompact (Hom.toImage f ≫ Hom.imageι f)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
⊢ IdealSheafData.subschemeι ⊥ ≫ Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion ⋯ = 𝟙 (IdealSheafData.subscheme (X := X) ⊥)

Tactic:
simp [← cancel_mono (IdealSheafData.subschemeι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
⊢ CategoryStruct.comp (Y := IdealSheafData.subscheme (X := X) ⊥) (Hom.toImage (𝟙 X) ≫ IdealSheafData.inclusion ⋯)
      (IdealSheafData.subschemeι ⊥) =
    𝟙 X

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
h : IsIso I.subschemeι
⊢ I = ⊥

Tactic:
simp [← I.ker_subschemeι]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
⊢ Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))

Tactic:
have := ConcreteCategory.epi_of_surjective _ (f.ker.subschemeι_app_surjective U)
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
rw :
  app f (↑U : Y.Opens) =
    ((CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫ ((ker f).subschemeObjIso U).inv) ≫
        ((ker f).subschemeObjIso U).hom ≫
          CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯)) ≫
      X.presheaf.map (inv (Quiver.Hom.op (eqToHom ⋯)))
⊢ app (toImage f) (imageι f ⁻¹ᵁ (↑U : Y.Opens)) =
    ((ker f).subschemeObjIso U).hom ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯)

Tactic:
rw [← cancel_epi (f.ker.subschemeι.app U), ← Scheme.Hom.comp_app,
    Scheme.Hom.congr_app f.toImage_imageι, f.ker.subschemeι_app,
    ← IsIso.eq_comp_inv, ← Functor.map_inv]

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.ker, CategoryTheory.Functor.map_inv, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, AlgebraicGeometry.Scheme.Hom.app, CategoryTheory.IsIso.eq_comp_inv, Subtype.val, CategoryTheory.cancel_epi
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
simp :
  app f (↑U : Y.Opens) =
    CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯) ≫
        X.presheaf.map (eqToHom ⋯)
⊢ app f (↑U : Y.Opens) =
    ((CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫ ((ker f).subschemeObjIso U).inv) ≫
        ((ker f).subschemeObjIso U).hom ≫
          CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯)) ≫
      X.presheaf.map (inv (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
simp only [Hom.comp_base, Opens.map_comp_obj, Category.assoc,
    Iso.inv_hom_id_assoc, eqToHom_op, inv_eqToHom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.eqToHom_op, CategoryTheory.inv_eqToHom, TopologicalSpace.Opens.map_comp_obj, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
rw :
  app f (↑U : Y.Opens) =
    app f (↑U : Y.Opens) ≫ 𝟙 Γ(X, (Opens.map (toImage f).base).obj ((Opens.map (imageι f).base).obj (↑U : Y.Opens)))
⊢ app f (↑U : Y.Opens) =
    CommRingCat.ofHom (Ideal.Quotient.mk ((ker f).ideal U)) ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯) ≫
        X.presheaf.map (eqToHom ⋯)

Tactic:
rw [← reassoc_of% CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk, CommRingCat.ofHom_hom,
    eqToHom_refl, CategoryTheory.Functor.map_id]

Premises used: CommRingCat.ofHom_hom, CategoryTheory.eqToHom_refl, CategoryTheory.Functor.map_id, CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
⊢ app f (↑U : Y.Opens) =
    app f (↑U : Y.Opens) ≫ 𝟙 Γ(X, (Opens.map (toImage f).base).obj ((Opens.map (imageι f).base).obj (↑U : Y.Opens)))

Tactic:
(Category.comp_id _).symm

Premises used: Set.Mem, setOf, CategoryTheory.Category.comp_id, Set.preimage, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
this : Epi (X := Γ(Y, (↑U : Y.Opens))) (app (ker f).subschemeι (↑U : Y.Opens))
⊢ app f (↑U : Y.Opens) =
    app f (↑U : Y.Opens) ≫ 𝟙 Γ(X, (Opens.map (toImage f).base).obj ((Opens.map (imageι f).base).obj (↑U : Y.Opens)))

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
simp :
  Function.Injective (α := (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) (β :=
    (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (Function.comp (β := (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U)
      (⇑(Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U) →
          (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (⇑(CommRingCat.Hom.hom ((ker f).subschemeObjIso U).hom) :
        (a : (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U))
⊢ Function.Injective (α := (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) (β :=
    (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)))
          (app (toImage f) (imageι f ⁻¹ᵁ (↑U : Y.Opens)))) :
      (a : (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
        (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))

Tactic:
simp only [f.toImage_app U, CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp]

Premises used: CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp, AlgebraicGeometry.Scheme.Hom.toImage_app
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
⊢ RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ≤
    (ker f).ideal U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
inst : QuasiCompact f
⊢ Function.Injective (α := (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) (β :=
    (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (Function.comp (β := (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U)
      (⇑(Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f (↑U : Y.Opens))) ⋯) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U) →
          (↑Γ(X, toImage f ⁻¹ᵁ imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (⇑(CommRingCat.Hom.hom ((ker f).subschemeObjIso U).hom) :
        (a : (↑Γ(image f, imageι f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, (↑U : Y.Opens)) : Type u) ⧸ (ker f).ideal U))

Tactic:
exact (RingHom.lift_injective_of_ker_le_ideal _ _ (by simp)).comp
    (f.ker.subschemeObjIso U).commRingCatIsoToRingEquiv.injective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso, RingEquiv.injective, RingHom.lift_injective_of_ker_le_ideal, AlgebraicGeometry.Scheme.Hom.ker, Function.Injective.comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
x : ↥(image f)
hα :
  ∀ (U : TopologicalSpace.Opens ↥(image f)),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥(image f)))
        {x : TopologicalSpace.Opens ↥(image f) |
          ∃ U ∈ Y.affineOpens,
            { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ : TopologicalSpace.Opens ↥(image f) } = x}
        U →
      Function.Injective (α := (↑((image f).presheaf.obj (Opposite.op U)) : Type u)) (β :=
        (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toImage f).base) X.presheaf).obj (Opposite.op U)) :
          Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := (image f).presheaf.obj (Opposite.op U)) ((toImage f).c.app (Opposite.op U))) :
          (a : (↑((image f).presheaf.obj (Opposite.op U)) : Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat (toImage f).base).obj X.presheaf).obj (Opposite.op U)) :
              Type u))
⊢ Function.Injective (α := (↑(Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat x) (image f).presheaf) : Type u))
    (β :=
    (↑(Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat x)
          (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toImage f).base) X.presheaf)) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Functor.obj (TopCat.Presheaf.stalkFunctor CommRingCat x) (image f).presheaf)
          (CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor CommRingCat x) (toImage f).c)) :
      (a : (↑((TopCat.Presheaf.stalkFunctor CommRingCat x).obj (image f).presheaf) : Type u)) →
        (↑((TopCat.Presheaf.stalkFunctor CommRingCat x).obj
              ((TopCat.Presheaf.pushforward CommRingCat (toImage f).base).obj X.presheaf)) :
          Type u))

Tactic:
apply TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis
    (hB := (Y.isBasis_affineOpens.of_isInducing f.imageι.isEmbedding.isInducing))

Premises used: AlgebraicGeometry.Scheme.Hom.imageι, TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis, TopologicalSpace.Opens.IsBasis.of_isInducing, Topology.IsEmbedding.isInducing, AlgebraicGeometry.Scheme.Hom.isEmbedding, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
x : ↥(image f)
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
⊢ Function.Injective (α :=
    (↑((image f).presheaf.obj (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) : Type u))
    (β :=
    (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toImage f).base) X.presheaf).obj
          (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X :=
          (image f).presheaf.obj (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ }))
          ((toImage f).c.app (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ }))) :
      (a :
          (↑((image f).presheaf.obj (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) :
            Type u)) →
        (↑(((TopCat.Presheaf.pushforward CommRingCat (toImage f).base).obj X.presheaf).obj
              (Opposite.op { carrier := ⇑(imageι f) ⁻¹' (↑U : Set ↥Y), is_open' := ⋯ })) :
          Type u))

Tactic:
f.toImage_app_injective ⟨U, hU⟩

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_app_injective, Subtype.mk