-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma map_ideal {U V : X.affineOpens} (h : U ≤ V) :
    (I.ideal V).map (X.presheaf.map (homOfLE h).op).hom = I.ideal U

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (h_1 : x ∈ ↑U),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1)) (I.ideal U)

Tactic:
intro x hxU

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Proof state:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
have := I.map_ideal_basicOpen_of_eq (V := X.affineBasicOpen g) f (Subtype.ext hfg.symm)

Result:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this : Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen g)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Proof state:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x ⋯)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑V) x ⋯)) (I.ideal V)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op ≫ X.presheaf.germ (↑U) x hxU)) (I.ideal V) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
simp only [homOfLE_leOfHom, TopCat.Presheaf.germ_res', this]

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, h hxU⟩

Result:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Proof state:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this : Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen g)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
rw [← I.map_ideal_basicOpen] at this

Result:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) = I.ideal U

Tactic:
rw [U.2.ideal_ext_iff]

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (h_1 : x ∈ ↑U),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1)) (I.ideal U)

Proof state:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V))
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
simp only [Ideal.map_map, ← RingHom.comp_apply, ← CommRingCat.hom_comp,
  affineBasicOpen_coe, X.presheaf.germ_res] at this ⊢

Result:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x ⋯)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑V) x ⋯)) (I.ideal V)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op ≫ X.presheaf.germ (↑U) x hxU)) (I.ideal V) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)