awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_2 : g₂ = (inv i₃ ≫ f₂) ≫ i₂
refine_2₁ : g₂ = inv i₃ ≫ f₂ ≫ i₂
refine_2₂ : g₂ = inv i₃ ≫ i₃ ≫ g₂
refine_2₃ refine_2₄ : g₂ = g₂
⊢ g₂ ≫ inv i₂ = inv i₃ ≫ f₂

Tactic:
rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
⊢ f₁ ≫ 𝟙 Y = 𝟙 X ≫ f₂

Tactic:
simp [h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
⊢ g₁ ≫ 𝟙 Z = 𝟙 X ≫ g₂

Tactic:
simp [h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
⊢ f₂ ≫ 𝟙 Y = 𝟙 X ≫ f₁

Tactic:
simp [h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 X ≫ g₁

Tactic:
simp [h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
h₀ :
  Eq (α := Y ⟶ pushout f₁ g₁) (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (Iso.inv (congrHom h₁ h₂)))
    (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯))
h₃ :
  Eq (α := Z ⟶ pushout f₁ g₁) (CategoryStruct.comp (Y := pushout f₂ g₂) (inr f₂ g₂) (Iso.inv (congrHom h₁ h₂)))
    (CategoryStruct.comp (Y := pushout f₂ g₂) (inr f₂ g₂) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯))
⊢ Eq (α := pushout f₂ g₂ ⟶ pushout f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
⊢ Eq (α := Y ⟶ pushout f₁ g₁) (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (Iso.inv (congrHom h₁ h₂)))
    (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯))

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
⊢ Eq (α := Z ⟶ pushout f₁ g₁) (CategoryStruct.comp (Y := pushout f₂ g₂) (inr f₂ g₂) (Iso.inv (congrHom h₁ h₂)))
    (CategoryStruct.comp (Y := pushout f₂ g₂) (inr f₂ g₂) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯))

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := G.obj (pullback f g) ⟶ G.obj Z) (G.map (pullback.fst f g) ≫ G.map f) (G.map (pullback.snd f g) ≫ G.map g)

Tactic:
simp only [← G.map_comp, pullback.condition]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := G.obj (pullback f g) ⟶ G.obj X)
    (CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullbackComparison G f g)
      (pullback.fst (G.map f) (G.map g)))
    (G.map (pullback.fst f g))

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.pullback.lift_fst, CategoryTheory.Limits.pullbackComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := G.obj (pullback f g) ⟶ G.obj Y)
    (CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullbackComparison G f g)
      (pullback.snd (G.map f) (G.map g)))
    (G.map (pullback.snd f g))

Tactic:
pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.pullbackComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
h₀ :
  CategoryStruct.comp (Y := pullback (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
      (pullback.fst (G.map f) (G.map g)) =
    CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullback.lift (G.map h) (G.map k) ⋯)
      (pullback.fst (G.map f) (G.map g))
h₁ :
  CategoryStruct.comp (Y := pullback (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
      (pullback.snd (G.map f) (G.map g)) =
    CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullback.lift (G.map h) (G.map k) ⋯)
      (pullback.snd (G.map f) (G.map g))
⊢ Eq (α := G.obj W ⟶ pullback (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
    (pullback.lift (G.map h) (G.map k) ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ CategoryStruct.comp (Y := pullback (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
      (pullback.fst (G.map f) (G.map g)) =
    CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullback.lift (G.map h) (G.map k) ⋯)
      (pullback.fst (G.map f) (G.map g))

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ CategoryStruct.comp (Y := pullback (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
      (pullback.snd (G.map f) (G.map g)) =
    CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullback.lift (G.map h) (G.map k) ⋯)
      (pullback.snd (G.map f) (G.map g))

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
h₀ :
  Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X)
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
h₁ :
  Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj Y)
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
    (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
      (pullbackComparison G (F.map f) (F.map g)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
h₀ :
  Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X) ((F ⋙ G).map (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X)
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))

Tactic:
rw [pullbackComparison_comp_fst]

Premises used: CategoryTheory.Limits.pullbackComparison_comp_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X) ((F ⋙ G).map (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
h₁ :
  Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj Y) ((F ⋙ G).map (pullback.snd f g))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj Y)
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))

Tactic:
rw [pullbackComparison_comp_snd]

Premises used: CategoryTheory.Limits.pullbackComparison_comp_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj Y) ((F ⋙ G).map (pullback.snd f g))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := G.obj X ⟶ G.obj (pushout f g)) (G.map f ≫ G.map (pushout.inl f g)) (G.map g ≫ G.map (pushout.inr f g))

Tactic:
simp only [← G.map_comp, pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := G.obj Y ⟶ G.obj (pushout f g))
    (CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g)) (pushoutComparison G f g))
    (G.map (pushout.inl f g))

Tactic:
pushout.inl_desc _ _ _

Premises used: CategoryTheory.Limits.pushoutComparison, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.pushout.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := G.obj Z ⟶ G.obj (pushout f g))
    (CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g)) (pushoutComparison G f g))
    (G.map (pushout.inr f g))

Tactic:
pushout.inr_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inr_desc, CategoryTheory.Limits.pushoutComparison, CategoryTheory.Limits.colimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k

Tactic:
simp only [← G.map_comp, w]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
h₀ :
  CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w))) =
    CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
      (pushout.desc (G.map h) (G.map k) ⋯)
h₁ :
  CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w))) =
    CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g))
      (pushout.desc (G.map h) (G.map k) ⋯)
⊢ Eq (α := pushout (G.map f) (G.map g) ⟶ G.obj W)
    (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w)))
    (pushout.desc (G.map h) (G.map k) ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w))) =
    CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
      (pushout.desc (G.map h) (G.map k) ⋯)

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w))) =
    CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g))
      (pushout.desc (G.map h) (G.map k) ⋯)

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ HasPullback g f

Tactic:
⟨⟨⟨_, PullbackCone.flipIsLimit (pullbackIsPullback f g)⟩⟩⟩

Premises used: CategoryTheory.Limits.pullbackIsPullback, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.PullbackCone.flipIsLimit, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ Y) (Iso.hom (pullbackSymmetry f g) ≫ pullback.fst g f) (pullback.snd f g)

Tactic:
simp [pullbackSymmetry]

Premises used: CategoryTheory.Limits.pullbackSymmetry
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ X) (Iso.hom (pullbackSymmetry f g) ≫ pullback.snd g f) (pullback.fst f g)

Tactic:
simp [pullbackSymmetry]

Premises used: CategoryTheory.Limits.pullbackSymmetry
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq (α := pullback g f ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (Iso.inv (pullbackSymmetry f g)) (pullback.fst f g) : pullback g f ⟶ X)
    (pullback.snd g f : pullback g f ⟶ X)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq (α := pullback g f ⟶ Y)
    (CategoryStruct.comp (Y := pullback f g) (Iso.inv (pullbackSymmetry f g)) (pullback.snd f g) : pullback g f ⟶ Y)
    (pullback.fst g f : pullback g f ⟶ Y)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ HasPushout g f

Tactic:
⟨⟨⟨_, PushoutCocone.flipIsColimit (pushoutIsPushout f g)⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushoutIsPushout, CategoryTheory.Limits.PushoutCocone.flipIsColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ Eq (α := Y ⟶ pushout g f)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.hom (pushoutSymmetry f g)) : Y ⟶ pushout g f)
    (pushout.inr g f : Y ⟶ pushout g f)

Tactic:
(colimit.isColimit (span f g)).comp_coconePointUniqueUpToIso_hom
    (PushoutCocone.flipIsColimit (pushoutIsPushout g f)) _

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitAux, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.PushoutCocone.IsColimit.mk, CategoryTheory.Limits.colimit, CategoryTheory.Limits.pushoutIsPushout, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.Cocone.forget, CategoryTheory.Limits.PushoutCocone.flipIsColimit, CategoryTheory.Limits.PushoutCocone.flip, CategoryTheory.Limits.span, CategoryTheory.Limits.PushoutCocone.mk, CategoryTheory.Limits.colimit.ι