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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ f₂ ≫ 𝟙 Y = 𝟙 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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 X ≫ 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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl ≫ (congrHom h₁ h₂).inv =
    inl ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) (_ : f₂ ≫ 𝟙 Y = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 X ≫ g₁)

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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr ≫ (congrHom h₁ h₂).inv =
    inr ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) (_ : f₂ ≫ 𝟙 Y = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 X ≫ g₁)
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) (_ : f₂ ≫ 𝟙 Y = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 X ≫ 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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl ≫ (congrHom h₁ h₂).inv = 𝟙 Y ≫ inl
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl ≫ (congrHom h₁ h₂).inv =
    inl ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) (_ : f₂ ≫ 𝟙 Y = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 X ≫ g₁)
erw [pushout.inl_desc]
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl = inl ≫ (congrHom h₁ h₂).hom
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl ≫ (congrHom h₁ h₂).inv = 𝟙 Y ≫ inl
rw [Iso.comp_inv_eq, Category.id_comp]
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl = 𝟙 Y ≫ inl
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl = inl ≫ (congrHom h₁ h₂).hom
erw [pushout.inl_desc]
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inl = 𝟙 Y ≫ inl
rw [Category.id_comp]
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr ≫ (congrHom h₁ h₂).inv = 𝟙 Z ≫ inr
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr ≫ (congrHom h₁ h₂).inv =
    inr ≫ map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) (_ : f₂ ≫ 𝟙 Y = 𝟙 X ≫ f₁) (_ : g₂ ≫ 𝟙 Z = 𝟙 X ≫ g₁)
erw [pushout.inr_desc]
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr = inr ≫ (congrHom h₁ h₂).hom
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr ≫ (congrHom h₁ h₂).inv = 𝟙 Z ≫ inr
rw [Iso.comp_inv_eq, Category.id_comp]
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr = 𝟙 Z ≫ inr
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr = inr ≫ (congrHom h₁ h₂).hom
erw [pushout.inr_desc]
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 ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ inr = 𝟙 Z ≫ inr
rw [Category.id_comp]