-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ker_ideal_of_isPullback_of_isOpenImmersion {X Y U V : Scheme.{u}}
    (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y) [IsOpenImmersion iV]
    [QuasiCompact f] (H : IsPullback f' iU iV f) (W) :
    f'.ker.ideal W =
      (f.ker.ideal ⟨iV ''ᵁ W, W.2.image_of_isOpenImmersion _⟩).comap (iV.appIso W).inv.hom

Proof state:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝ : QuasiCompact f'
this : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
have : iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W :=
  IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback H W

Result:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Proof state:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]

Result:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ Hom.app f (iV ''ᵁ ↑W) ≫ e.hom = (Hom.appIso iV ↑W).hom ≫ Hom.app f' ↑W

Proof state:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝² : QuasiCompact f'
this✝¹ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this✝ : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this✝).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ (CommRingCat.Hom.hom (Hom.app f' ↑W)) x = 0 ↔ (CommRingCat.Hom.hom (Hom.app f' ↑W ≫ e.inv)) x = 0

Tactic:
simpa using (map_eq_zero_iff _ (ConcreteCategory.bijective_of_isIso e.inv).1).symm

Result:
no goals

Proof state:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
let e : Γ(X, f ⁻¹ᵁ iV ''ᵁ W) ≅ Γ(U, f' ⁻¹ᵁ W) :=
  X.presheaf.mapIso (eqToIso this).op ≪≫ iU.appIso _

Result:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Proof state:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this : QuasiCompact f'
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
have : IsOpenImmersion iU := MorphismProperty.of_isPullback H inferInstance

Result:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝ : QuasiCompact f'
this : IsOpenImmersion iU
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Proof state:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
have : (iV.appIso W).inv ≫ f.app _ = f'.app W ≫ e.inv := by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
  simp only [Scheme.Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
    eqToHom_op, Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE, e, Scheme.appLE_comp_appLE, H.w]

Result:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝² : QuasiCompact f'
this✝¹ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this✝ : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this✝).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Proof state:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ Hom.app f (iV ''ᵁ ↑W) ≫ e.hom = (Hom.appIso iV ↑W).hom ≫ Hom.app f' ↑W

Tactic:
simp only [Scheme.Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
  eqToHom_op, Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE, e, Scheme.appLE_comp_appLE, H.w]

Result:
no goals