awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
rw :
  RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv)) =
    I.ideal 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

Tactic:
rw [subschemeι_app]

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

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯))
change : RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U
⊢ RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv)) =
    I.ideal U

Tactic:
change RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp
    (Ideal.Quotient.mk (I.ideal U))) = _

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, Ideal.Quotient.mk, RingHom.comp, RingEquiv.toRingHom, RingHom.ker, AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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
rw₁ rw₂ : I.ideal U = I.ideal U
⊢ RingHom.ker (e.commRingCatIsoToRingEquiv.toRingHom.comp (Ideal.Quotient.mk (I.ideal U))) = I.ideal U

Tactic:
rw [RingHom.ker_equiv_comp, Ideal.mk_ker]

Premises used: RingHom.ker_equiv_comp, Ideal.mk_ker
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
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
⊢ Hom.ker I.subschemeι = I

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
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:
simp [ker_subschemeι_app]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
rw : Eq.{u + 1} (α := X.IdealSheafData) (Hom.ker (X := subscheme (X := X) ⊤) (subschemeι ⊤)) ⊤
rw₁ rw₂ : Eq.{u + 1} (α := X.IdealSheafData) ⊤ ⊤
⊢ IsEmpty.{u + 1} ↥(subscheme (X := X) ⊤)

Tactic:
rw [← (subschemeι _).ker_eq_top_iff_isEmpty, ker_subschemeι]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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
rw₅ rw₆ :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.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

Tactic:
rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom, Ideal.Quotient.factor_comp_mk, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, AlgebraicGeometry.Spec.map_comp_assoc, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
rw : glueDataObjHom ⋯ U ≫ I.glueDataObjι U = 𝟙 (I.glueDataObj U) ≫ I.glueDataObjι U
⊢ glueDataObjHom ⋯ U = 𝟙 (I.glueDataObj U)

Tactic:
rw [← cancel_mono (I.glueDataObjι U)]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ glueDataObjHom ⋯ U ≫ I.glueDataObjι U = 𝟙 (I.glueDataObj U) ≫ I.glueDataObjι U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I J K : X.IdealSheafData
hIJ : I ≤ J
hJK : J ≤ K
U : (↑X.affineOpens : Type u)
rw : (glueDataObjHom hJK U ≫ glueDataObjHom hIJ U) ≫ I.glueDataObjι U = glueDataObjHom ⋯ U ≫ I.glueDataObjι U
⊢ glueDataObjHom hJK U ≫ glueDataObjHom hIJ U = glueDataObjHom ⋯ U

Tactic:
rw [← cancel_mono (I.glueDataObjι U)]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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) ≫ I.glueDataObjι U = glueDataObjHom ⋯ U ≫ I.glueDataObjι U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I_1 I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
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).ι)
⊢ 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)

Tactic:
simp only [← cancel_mono I.subschemeι, AffineOpenCover.openCover_X, glueDataObjHom_ι_assoc,
      AffineOpenCover.openCover_f, Category.assoc, subschemeCover_map_subschemeι]

Premises used: AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι_assoc, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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).ι)
rw₂ 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).ι)
⊢ 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:
rw [← subschemeCover_map_subschemeι, pullback.condition_assoc, subschemeCover_map_subschemeι]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι, CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : J.subschemeCover.I₀ (P := IsOpenImmersion)
⊢ J.subschemeCover.f (P := IsOpenImmersion) U ≫ inclusion h =
    glueDataObjHom h U ≫ I.subschemeCover.f (P := IsOpenImmersion) U

Tactic:
J.subschemeCover.openCover.ι_glueMorphisms _ _ _

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
x : J.subschemeCover.openCover.I₀
⊢ J.subschemeCover.openCover.f x ≫ inclusion h ≫ I.subschemeι = J.subschemeCover.openCover.f x ≫ J.subschemeι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : I.subschemeCover.openCover.I₀
⊢ I.subschemeCover.openCover.f x ≫ inclusion ⋯ = I.subschemeCover.openCover.f x ≫ 𝟙 I.subscheme

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I J K : X.IdealSheafData
h₁ : I ≤ J
h₂ : J ≤ K
x : K.subschemeCover.openCover.I₀
⊢ K.subschemeCover.openCover.f x ≫ inclusion h₂ ≫ inclusion h₁ = K.subschemeCover.openCover.f x ≫ inclusion ⋯

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : (↑Y.affineOpens : Type u)
⊢ pullback.fst f (↑U : Y.Opens).ι ''ᵁ ⊤ = f ⁻¹ᵁ (↑U : Y.Opens)

Tactic:
simp [Scheme.Hom.opensRange_pullbackFst]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst
-- 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).ι, ⊤))
rw :
  (↑U : Y.Opens).topIso.hom ≫ Hom.app f (↑U : Y.Opens) ≫ e.hom =
    Hom.appTop (IsAffineOpen.isoSpec ⋯).inv ≫ Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)
⊢ 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Γ)

Tactic:
rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]

Premises used: Iff.mpr, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Iso.eq_inv_comp, Subtype.property
-- 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).ι, ⊤))
simp :
  Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ ⋯ :
      Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ ⋯ :
      Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
⊢ (↑U : Y.Opens).topIso.hom ≫ Hom.app f (↑U : Y.Opens) ≫ e.hom =
    Hom.appTop (IsAffineOpen.isoSpec ⋯).inv ≫ Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)

Tactic:
simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom,
      Iso.op_hom, eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, Hom.appLE_comp_appLE,
      Opens.map_top, e, pullback.condition, IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToIso.hom, CategoryTheory.Iso.op_hom, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, CategoryTheory.eqToHom_op, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.appIso_hom, TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.Hom.map_appLE, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, CategoryTheory.Functor.mapIso_hom, AlgebraicGeometry.Scheme.Hom.appLE_map, AlgebraicGeometry.Scheme.Opens.topIso_hom
-- 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).ι, ⊤))
rw :
  Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (CategoryStruct.comp (Y := Γ((↑(↑U : Y.Opens) : Scheme), (↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤))
        (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
        (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ ⋯) :
      Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ ⋯ :
      Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
⊢ Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ ⋯ :
      Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ ⋯ :
      Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))

Tactic:
rw [Hom.comp_appLE, Opens.ι_app]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_appLE, AlgebraicGeometry.Scheme.Opens.ι_app
-- 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).ι, ⊤))
⊢ Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (CategoryStruct.comp (Y := Γ((↑(↑U : Y.Opens) : Scheme), (↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤))
        (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
        (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ ⋯) :
      Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ ⋯ :
      Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))

Tactic:
Hom.map_appLE _ _ (homOfLE le_top).op

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.NatTrans.vcomp, IsOpenMap.functorMap, Set.Mem, Quiver.Hom.op, setOf, ContinuousMap.comp, AlgebraicGeometry.Scheme.restrict, CategoryTheory.Limits.limit, Set.preimage, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.comp, AlgebraicGeometry.LocallyRingedSpace.comp, AlgebraicGeometry.Scheme.Hom.map_appLE, AlgebraicGeometry.Scheme.Opens.toScheme
-- 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).ι, ⊤))
⊢ Eq (α := Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (CategoryStruct.comp (Y := Γ((↑(↑U : Y.Opens) : Scheme), (↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤))
        (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
        (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι) ((↑U : Y.Opens).ι ⁻¹ᵁ (↑U : Y.Opens).ι ''ᵁ ⊤) ⊤ ⋯) :
      Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))
    (Hom.appLE (pullback.snd f (↑U : Y.Opens).ι ≫ 𝟙 (↑(↑U : Y.Opens) : Scheme)) ⊤ ⊤ ⋯ :
      Γ((↑(↑U : Y.Opens) : Scheme), ⊤) ⟶ Γ(pullback f (↑U : Y.Opens).ι, ⊤))

Tactic:
exact Hom.map_appLE _ _ (homOfLE le_top).op

Premises used: Quiver.Hom.op, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Hom.map_appLE
-- 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).ι, ⊤))
⊢ 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Γ)

Tactic:
have he : f.app U ≫ e.hom =
      (ΓSpecIso Γ(Y, ↑U)).inv ≫ (pullback.snd f U.1.ι ≫ U.1.toSpecΓ).appTop := by
    rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]
    simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom,
      Iso.op_hom, eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, Hom.appLE_comp_appLE,
      Opens.map_top, e, pullback.condition, IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]
    rw [Hom.comp_appLE, Opens.ι_app]
    exact Hom.map_appLE _ _ (homOfLE le_top).op
-- 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Γ)
rw : (Hom.ker f).ideal U ≤ RingHom.ker (CommRingCat.Hom.hom (Hom.app f (↑U : Y.Opens) ≫ e.hom))
⊢ (Hom.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))) ≫
          Hom.appTop (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ)))

Tactic:
rw [← he]
-- 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:
(IdealSheafData.ideal_ofIdeals_le _ _).trans_eq
    (RingHom.ker_equiv_comp _ e.commRingCatIsoToRingEquiv).symm

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, LE.le.trans_eq, Set.Mem, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, RingHom.ker_equiv_comp, Eq.symm