-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma isPullback_opens_inf_le {X : Scheme} {U V W : X.Opens} (hU : U ≤ W) (hV : V ≤ W) :
    IsPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right) (X.homOfLE hU) (X.homOfLE hV)

Proof state:
case refine_2
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ W.ι ''ᵁ W.ι ⁻¹ᵁ U = U

Tactic:
exact (W.functor_map_eq_inf U).trans (by simpa)

Result:
no goals

Proof state:
case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

case refine_4
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

case refine_5
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑W).hom = (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU

case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV

Tactic:
all_goals { simp [← cancel_mono (Scheme.Opens.ι _)] }

Result:
no goals

Proof state:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ U ⊓ W = U

Tactic:
simpa

Result:
no goals

Proof state:
case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V

Tactic:
exact V.functor_map_eq_inf U

Result:
no goals

Proof state:
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)

Tactic:
refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
  X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_

Result:
case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V

case refine_2
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ W.ι ''ᵁ W.ι ⁻¹ᵁ U = U

case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ?refine_2).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ?refine_1).hom ≫ X.homOfLE ⋯

case refine_4
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ?refine_1).hom ≫ X.homOfLE ⋯

case refine_5
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑W).hom = (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ?refine_2).hom ≫ X.homOfLE hU

case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV

Proof state:
case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV

Tactic:
simp [← cancel_mono (Scheme.Opens.ι _)]

Result:
no goals

Proof state:
case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U = U ⊓ V

Tactic:
rw [← TopologicalSpace.Opens.map_comp_obj, ← Scheme.comp_base, Scheme.homOfLE_ι]

Result:
case refine_1
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ V.ι ''ᵁ (Opens.map V.ι.base).obj U = U ⊓ V