-- 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:
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 ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i

Tactic:
congr 1

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 ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i 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
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 ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i

Tactic:
simp_rw [← Category.assoc]

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 ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i

Proof state:
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.snd (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j) ≫
      (gluing 𝒰 f g).ι j ≫ Multicoequalizer.desc (gluing 𝒰 f g).diagram Y (fun i => pullback.snd (𝒰.map i ≫ f) g) ⋯ =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.map j ≫ f) g

Tactic:
simp

Result:
no goals

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
⊢ ∀ (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)

Tactic:
intro j

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
⊢ (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)

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
⊢ 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

Tactic:
rw [← show _ = fV 𝒰 f g j i ≫ _ from (gluing 𝒰 f g).glue_condition j i]

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 ≫ (gluing 𝒰 f g).t j i ≫ (gluing 𝒰 f g).f i j ≫ (gluing 𝒰 f g).ι i

Proof state:
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

Tactic:
simp_rw [t_fst_fst, pullback.lift_fst, pullbackFstιToV_snd, GlueData.openCover_map]

Result:
no goals

Proof state:
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

Tactic:
simp_rw [t_fst_snd, pullback.lift_snd, pullbackFstιToV_fst_assoc, pullback.condition_assoc,
  GlueData.openCover_map, p2]

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.snd (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j) ≫
      (gluing 𝒰 f g).ι j ≫ Multicoequalizer.desc (gluing 𝒰 f g).diagram Y (fun i => pullback.snd (𝒰.map i ≫ f) g) ⋯ =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j) ≫ pullback.snd (𝒰.map j ≫ f) g