-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem gluedLift_p1 : gluedLift 𝒰 f g s ≫ p1 𝒰 f g = s.fst

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
⊢ gluedLift 𝒰 f g s ≫ p1 𝒰 f g = s.fst

Tactic:
rw [← cancel_epi (𝒰.pullbackCover s.fst).fromGlued]

Result:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
⊢ (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
    (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ s.fst

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
⊢ (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
    (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ s.fst

Tactic:
apply Multicoequalizer.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
s : PullbackCone f g
⊢ ∀ (b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R),
    Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
        (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
      Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
        (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ s.fst

Proof state:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R
⊢ Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
      (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
    Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
      (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ s.fst

Tactic:
simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]

Result:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R
⊢ ((Cover.pullbackCover 𝒰 s.fst).map b ≫
        (Cover.pullbackCover 𝒰 s.fst).glueMorphisms
          (fun i =>
            ((pullbackSymmetry s.fst (𝒰.map i)).hom ≫
                pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f ⋯ ⋯) ≫
              (gluing 𝒰 f g).ι i)
          ⋯) ≫
      p1 𝒰 f g =
    (Cover.pullbackCover 𝒰 s.fst).map b ≫ s.fst

Proof state:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
⊢ ∀ (b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R),
    Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
        (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
      Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
        (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ s.fst

Tactic:
intro b

Result:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R
⊢ Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
      (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
    Multicoequalizer.π (Cover.pullbackCover 𝒰 s.fst).gluedCover.diagram b ≫
      (Cover.pullbackCover 𝒰 s.fst).fromGlued ≫ s.fst

Proof state:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R
⊢ ((Cover.pullbackCover 𝒰 s.fst).map b ≫
        (Cover.pullbackCover 𝒰 s.fst).glueMorphisms
          (fun i =>
            ((pullbackSymmetry s.fst (𝒰.map i)).hom ≫
                pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f ⋯ ⋯) ≫
              (gluing 𝒰 f g).ι i)
          ⋯) ≫
      p1 𝒰 f g =
    (Cover.pullbackCover 𝒰 s.fst).map b ≫ s.fst

Tactic:
simp_rw [(𝒰.pullbackCover s.fst).ι_glueMorphisms]

Result:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R
⊢ (((pullbackSymmetry s.fst (𝒰.map b)).hom ≫ pullback.map (𝒰.map b) s.fst (𝒰.map b ≫ f) g (𝟙 (𝒰.obj b)) s.snd f ⋯ ⋯) ≫
        (gluing 𝒰 f g).ι b) ≫
      p1 𝒰 f g =
    (Cover.pullbackCover 𝒰 s.fst).map b ≫ s.fst

Proof state:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.pullbackCover 𝒰 s.fst).gluedCover.J).R
⊢ (((pullbackSymmetry s.fst (𝒰.map b)).hom ≫ pullback.map (𝒰.map b) s.fst (𝒰.map b ≫ f) g (𝟙 (𝒰.obj b)) s.snd f ⋯ ⋯) ≫
        (gluing 𝒰 f g).ι b) ≫
      p1 𝒰 f g =
    (Cover.pullbackCover 𝒰 s.fst).map b ≫ s.fst

Tactic:
simp [p1, pullback.condition]

Result:
no goals