no goals
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁
simp [h₁]
no goals
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁
simp [h₂]
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ fst =
    map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) (_ : f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁) ≫ fst

case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ snd =
    map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) (_ : f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁) ≫ snd
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) (_ : f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁)
ext
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ fst = fst ≫ 𝟙 X
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ fst =
    map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) (_ : f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁) ≫ fst
erw [pullback.lift_fst]
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ fst = (congrHom h₁ h₂).hom ≫ fst ≫ 𝟙 X
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ fst = fst ≫ 𝟙 X
rw [Iso.inv_comp_eq]
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ fst = (fst ≫ 𝟙 X) ≫ 𝟙 X
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ fst = (congrHom h₁ h₂).hom ≫ fst ≫ 𝟙 X
erw [pullback.lift_fst_assoc]
no goals
case h₀
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ fst = (fst ≫ 𝟙 X) ≫ 𝟙 X
rw [Category.comp_id, Category.comp_id]
case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ snd = snd ≫ 𝟙 Y
case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ snd =
    map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) (_ : f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁) ≫ snd
erw [pullback.lift_snd]
case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ snd = (congrHom h₁ h₂).hom ≫ snd ≫ 𝟙 Y
case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv ≫ snd = snd ≫ 𝟙 Y
rw [Iso.inv_comp_eq]
case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ snd = (snd ≫ 𝟙 Y) ≫ 𝟙 Y
case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ snd = (congrHom h₁ h₂).hom ≫ snd ≫ 𝟙 Y
erw [pullback.lift_snd_assoc]
no goals
case h₁
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ snd = (snd ≫ 𝟙 Y) ≫ 𝟙 Y
rw [Category.comp_id, Category.comp_id]