-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma Hom.iInf_ker_openCover_map_comp_apply
    (f : X.Hom Y) [QuasiCompact f] (𝒰 : X.OpenCover) (U : Y.affineOpens) :
    ⨅ i, (𝒰.map i ≫ f).ker.ideal U = f.ker.ideal U

Proof state:
case intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
      (ConcreteCategory.hom (𝒰.map i).base) x ∈ V ∧
        (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0

Tactic:
simp only [homOfLE_leOfHom, CommRingCat.forget_map, map_zero, exists_and_left]

Result:
case intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ∃ V,
    (ConcreteCategory.hom (𝒰.map i).base) x ∈ V ∧
      ∃ (x : V ≤ f ⁻¹ᵁ ↑U),
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) = 0

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
      x ∈ V ∧
        (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Result:
case intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ∃ V,
    ∃ (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))),
      (ConcreteCategory.hom (𝒰.map i).base) x ∈ V ∧
        (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE hV).op)) 0

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
⊢ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U ≤ f.ker.ideal U

Tactic:
intro s hs

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
⊢ s ∈ f.ker.ideal U

Proof state:
case intro.intro.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (CommRingCat.Hom.hom (appLE (𝒰.map i ≫ f) (↑U) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U) ⋯)) s = 0

Tactic:
simpa [Scheme.Hom.appLE] using ideal_ofIdeals_le _ _ (Ideal.mem_iInf.mp hs i)

Result:
no goals

Proof state:
case intro.intro.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (appIso (𝒰.map i) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    (appIso (𝒰.map i) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv 0

Tactic:
rw [map_zero, ← RingEquiv.coe_toRingHom, Iso.commRingCatIsoToRingEquiv_toRingHom,
  Scheme.Hom.appIso_hom']

Result:
case intro.intro.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (CommRingCat.Hom.hom (appLE (𝒰.map i) (𝒰.map i ''ᵁ 𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U) ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    0

Proof state:
case intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ ∃ V,
    (ConcreteCategory.hom (𝒰.map i).base) x ∈ V ∧
      ∃ (x : V ≤ f ⁻¹ᵁ ↑U),
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) = 0

Tactic:
refine ⟨𝒰.map i ''ᵁ 𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ U.1, ⟨_, hxU, rfl⟩,
  Set.image_preimage_subset (𝒰.map i).base (f ⁻¹ᵁ U), ?_⟩

Result:
case intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) = 0

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
⊢ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U = f.ker.ideal U

Tactic:
refine le_antisymm ?_ (le_iInf fun i ↦ f.le_ker_comp (𝒰.map i) U)

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
⊢ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U ≤ f.ker.ideal U

Proof state:
case intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s) = 0

Tactic:
apply ((𝒰.map i).appIso _).commRingCatIsoToRingEquiv.injective

Result:
case intro.intro.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (appIso (𝒰.map i) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    (appIso (𝒰.map i) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U)).commRingCatIsoToRingEquiv 0

Proof state:
case intro.intro.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (CommRingCat.Hom.hom (appLE (𝒰.map i) (𝒰.map i ''ᵁ 𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U) ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (f.app ↑U)) s)) =
    0

Tactic:
simp only [homOfLE_leOfHom, Scheme.Hom.app_eq_appLE, ← RingHom.comp_apply,
  ← CommRingCat.hom_comp, Scheme.Hom.appLE_map, Scheme.appLE_comp_appLE]

Result:
case intro.intro.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.map i ≫ f)).ideal U
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hxU : (ConcreteCategory.hom (𝒰.map i).base) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (CommRingCat.Hom.hom (appLE (𝒰.map i ≫ f) (↑U) (𝒰.map i ⁻¹ᵁ f ⁻¹ᵁ ↑U) ⋯)) s = 0