-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem lift_comp_ι (i : 𝒰.J) :
    pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ p2 𝒰 f g)
          (by rw [← pullback.condition_assoc, Category.assoc, p_comm]) ≫
        (gluing 𝒰 f g).ι i =
      (pullback.fst _ _ : pullback (p1 𝒰 f g) (𝒰.map i) ⟶ _)

Proof state:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.map i)

Tactic:
trans pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι _

Result:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j

X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.map i)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
i : 𝒰.J
⊢ pullback.snd (p1 𝒰 f g) (𝒰.map i) ≫ 𝒰.map i ≫ f = (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ≫ g

Tactic:
rw [← pullback.condition_assoc, Category.assoc, p_comm]

Result:
no goals

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫ (gluing 𝒰 f g).openCover.map j

Tactic:
simp_rw [pullbackFstιToV_fst, GlueData.openCover_map]

Result:
no goals

Proof state:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j

Tactic:
rw [gluing_f, gluing_t]

Result:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
⊢ pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
      (gluing 𝒰 f g).ι i =
    pullback.fst (p1 𝒰 f g) (𝒰.map i)

Tactic:
apply ((gluing 𝒰 f g).openCover.pullbackCover (pullback.fst _ _)).hom_ext

Result:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
⊢ ∀ (x : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J),
    (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).map x ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
          (gluing 𝒰 f g).ι i =
      (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).map x ≫
        pullback.fst (p1 𝒰 f g) (𝒰.map i)

Proof state:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).map j ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).map j ≫
      pullback.fst (p1 𝒰 f g) (𝒰.map i)

Tactic:
dsimp only [Cover.pullbackCover]

Result:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
        (gluing 𝒰 f g).ι i =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.map i)

Proof state:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Tactic:
apply pullback.hom_ext <;> simp_rw [Category.assoc]

Result:
case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.fst (𝒰.map i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.fst (𝒰.map i ≫ f) g

case e_a.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.snd (𝒰.map i ≫ f) g =
    pullbackFstιToV 𝒰 f g i j ≫
      t 𝒰 f g j i ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g