-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ker_glueDataObjι_appTop (U : X.affineOpens) :
    RingHom.ker (I.glueDataObjι U).appTop.hom = (I.ideal U).comap U.1.topIso.hom.hom

Proof state:
case e_f.e_f
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ (↑U).topIso.hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ

Tactic:
simp only [Scheme.Opens.topIso_hom]

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (Ideal.Quotient.mk (I.ideal U)))

Tactic:
show RingHom.ker (Spec.map φ ≫ _).appTop.hom = (RingHom.ker φ.hom).comap _

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ))

Proof state:
case e_f.e_f
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.app (IsAffineOpen.isoSpec ⋯).inv ⊤ ≫ (ΓSpecIso (CommRingCat.of ↑Γ(X, ↑U))).hom ≫ φ =
    X.presheaf.map (eqToHom ⋯).op ≫ φ

Tactic:
rw [← Scheme.Hom.appTop, U.2.isoSpec_inv_appTop, Category.assoc, Iso.inv_hom_id_assoc]

Result:
case e_f.e_f
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ (↑U).topIso.hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

Tactic:
let φ := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

Proof state:
case e_f.e_f
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫ (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom =
    (↑U).topIso.hom ≫ φ

Tactic:
simp only [Scheme.comp_app, TopologicalSpace.Opens.map_top, Category.assoc,
  Scheme.ΓSpecIso_naturality, Scheme.Opens.topIso_hom]

Result:
case e_f.e_f
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.app (IsAffineOpen.isoSpec ⋯).inv ⊤ ≫ (ΓSpecIso (CommRingCat.of ↑Γ(X, ↑U))).hom ≫ φ =
    X.presheaf.map (eqToHom ⋯).op ≫ φ

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

Tactic:
rw [← Ideal.mk_ker (I := I.ideal _)]

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (Ideal.Quotient.mk (I.ideal U)))

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (CommRingCat.Hom.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]

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
          (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom)) =
    RingHom.ker (CommRingCat.Hom.hom ((↑U).topIso.hom ≫ φ))

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
          (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom)) =
    RingHom.ker (CommRingCat.Hom.hom ((↑U).topIso.hom ≫ φ))

Tactic:
congr 2

Result:
case e_f.e_f
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : CommRingCat.of ↑Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫ (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom =
    (↑U).topIso.hom ≫ φ