-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem morphismRestrict_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Opens Z) :
    (f ≫ g) ∣_ U = f ∣_ g ⁻¹ᵁ U ≫ g ∣_ U

Proof state:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U) =
    (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫
      pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U)

Tactic:
rw [pullbackRestrictIsoRestrict_inv_fst, pullbackRightPullbackFstIso_inv_snd_fst, ←
  pullback.condition, pullbackRestrictIsoRestrict_inv_fst_assoc,
  pullbackRestrictIsoRestrict_inv_fst_assoc]

Result:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (f ≫ g) ∣_ U = f ∣_ g ⁻¹ᵁ U ≫ g ∣_ U

Tactic:
delta morphismRestrict

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.snd (f ≫ g) (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
simp_rw [← Category.assoc]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.snd g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.snd g (Scheme.Opens.ι U)

Proof state:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.fst g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)

Tactic:
simp_rw [Category.assoc]

Result:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U) =
    (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫
      pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.snd (f ≫ g) (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
rw [← pullbackRightPullbackFstIso_inv_snd_snd]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Proof state:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
      pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv

Tactic:
rw [← cancel_mono (pullback.fst _ _)]

Result:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.fst g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.fst g (Scheme.Opens.ι U)

Proof state:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ ((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f

Tactic:
rfl

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ (((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫
      pullback.snd g (Scheme.Opens.ι U) =
    (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
        (pullbackRestrictIsoRestrict g U).inv) ≫
      pullback.snd g (Scheme.Opens.ι U)

Tactic:
congr 1

Result:
case e_a
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↑↑Z.toPresheafedSpace
⊢ ((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫
      pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv