no goals
C : Type u_2
inst✝² : Category C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
        (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁) ≫
      fst =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
        (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂) ≫
      fst
rw [lift_fst, lift_fst]
no goals
C : Type u_2
inst✝² : Category C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ fst =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) fst
      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ fst = fst ≫ i₁)
simp
no goals
C : Type u_2
inst✝² : Category C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ snd =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) snd
      (_ : lift (fst ≫ i₁) (snd ≫ i₂) (_ : (fst ≫ i₁) ≫ f' = (snd ≫ i₂) ≫ g') ≫ snd = snd ≫ i₂)
simp