awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ ∀ (s : PushoutCocone f g),
    CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        ((fun (s : PushoutCocone f g) ↦ (pushout.desc s.inl s.inr ⋯ : pushout f g ⟶ s.pt)) s) =
      s.inl

Tactic:
simp
-- 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 : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ ∀ (s : PushoutCocone f g),
    CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        ((fun (s : PushoutCocone f g) ↦ (pushout.desc s.inl s.inr ⋯ : pushout f g ⟶ s.pt)) s) =
      s.inr

Tactic:
simp
-- 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
h₀ : CategoryStruct.comp (Y := pullback f g) (lift (fst f g) (snd f g) ⋯) (fst f g) = 𝟙 (pullback f g) ≫ fst f g
h₁ : CategoryStruct.comp (Y := pullback f g) (lift (fst f g) (snd f g) ⋯) (snd f g) = 𝟙 (pullback f g) ≫ snd f g
⊢ lift (fst f g) (snd f g) ⋯ = 𝟙 (pullback f g)

Tactic:
apply hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- 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
⊢ CategoryStruct.comp (Y := pullback f g) (lift (fst f g) (snd f g) ⋯) (fst f g) = 𝟙 (pullback f g) ≫ fst f g

Tactic:
simp
-- 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
⊢ CategoryStruct.comp (Y := pullback f g) (lift (fst f g) (snd f g) ⋯) (snd f g) = 𝟙 (pullback f g) ≫ snd f g

Tactic:
simp
-- 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
h₀ : CategoryStruct.comp (Y := pushout f g) (inl f g) (desc (inl f g) (inr f g) ⋯) = inl f g ≫ 𝟙 (pushout f g)
h₁ : CategoryStruct.comp (Y := pushout f g) (inr f g) (desc (inl f g) (inr f g) ⋯) = inr f g ≫ 𝟙 (pushout f g)
⊢ desc (inl f g) (inr f g) ⋯ = 𝟙 (pushout f g)

Tactic:
apply hom_ext

Premises used: CategoryTheory.Limits.pushout.hom_ext
-- 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
⊢ CategoryStruct.comp (Y := pushout f g) (inl f g) (desc (inl f g) (inr f g) ⋯) = inl f g ≫ 𝟙 (pushout f g)

Tactic:
simp
-- 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
⊢ CategoryStruct.comp (Y := pushout f g) (inr f g) (desc (inl f g) (inr f g) ⋯) = inr f g ≫ 𝟙 (pushout f g)

Tactic:
simp
-- 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₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Eq (α := pullback f₁ f₂ ⟶ T) ((fst f₁ f₂ ≫ i₁) ≫ g₁) ((snd f₁ f₂ ≫ i₂) ≫ g₂)

Tactic:
simp only [Category.assoc, ← eq₁, ← eq₂, pullback.condition_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition_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 X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
rw : i₁ ≫ f' ≫ j₃ = (i₁ ≫ j₁) ≫ f''
rw₁ : i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
rw₂ rw₃ : i₁ ≫ j₁ ≫ f'' = i₁ ≫ j₁ ≫ f''
⊢ f ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ f''

Tactic:
rw [reassoc_of% e₁, e₃, Category.assoc]

Premises used: CategoryTheory.Category.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 X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
rw : i₂ ≫ g' ≫ j₃ = (i₂ ≫ j₂) ≫ g''
rw₁ : i₂ ≫ j₂ ≫ g'' = (i₂ ≫ j₂) ≫ g''
rw₂ rw₃ : i₂ ≫ j₂ ≫ g'' = i₂ ≫ j₂ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''

Tactic:
rw [reassoc_of% e₂, e₄, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
h₀ :
  Eq (α := pullback f g ⟶ X'')
    (CategoryStruct.comp (Y := pullback f'' g'')
      (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
      (fst f'' g''))
    (CategoryStruct.comp (Y := pullback f'' g'') (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯) (fst f'' g''))
h₁ :
  Eq (α := pullback f g ⟶ Y'')
    (CategoryStruct.comp (Y := pullback f'' g'')
      (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
      (snd f'' g''))
    (CategoryStruct.comp (Y := pullback f'' g'') (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯) (snd f'' g''))
⊢ Eq (α := pullback f g ⟶ pullback f'' g'')
    (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
    (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ Eq (α := pullback f g ⟶ X'')
    (CategoryStruct.comp (Y := pullback f'' g'')
      (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
      (fst f'' g''))
    (CategoryStruct.comp (Y := pullback f'' g'') (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯) (fst f'' g''))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ Eq (α := pullback f g ⟶ Y'')
    (CategoryStruct.comp (Y := pullback f'' g'')
      (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
      (snd f'' g''))
    (CategoryStruct.comp (Y := pullback f'' g'') (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯) (snd f'' g''))

Tactic:
simp
-- 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 : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp
-- 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 : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp
-- 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
h₀ : CategoryStruct.comp (Y := pullback f g) (map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (fst f g) = 𝟙 (pullback f g) ≫ fst f g
h₁ : CategoryStruct.comp (Y := pullback f g) (map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (snd f g) = 𝟙 (pullback f g) ≫ snd f g
⊢ map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯ = 𝟙 (pullback f g)

Tactic:
ext
-- 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
⊢ CategoryStruct.comp (Y := pullback f g) (map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (fst f g) = 𝟙 (pullback f g) ≫ fst f g

Tactic:
simp
-- 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
⊢ CategoryStruct.comp (Y := pullback f g) (map f g f g (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (snd f g) = 𝟙 (pullback f g) ≫ snd f g

Tactic:
simp
-- 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₂
⊢ Eq (α := S ⟶ pushout g₁ g₂) (f₁ ≫ i₁ ≫ inl g₁ g₂) (f₂ ≫ i₂ ≫ inr g₁ g₂)

Tactic:
simp only [reassoc_of% eq₁, reassoc_of% eq₂, condition]

Premises used: CategoryTheory.Limits.pushout.condition
-- 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 X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
rw : i₁ ≫ f' ≫ j₂ = (i₁ ≫ j₁) ≫ f''
rw₁ : i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
rw₂ rw₃ : i₁ ≫ j₁ ≫ f'' = i₁ ≫ j₁ ≫ f''
⊢ f ≫ i₂ ≫ j₂ = (i₁ ≫ j₁) ≫ f''

Tactic:
rw [reassoc_of% e₁, e₃, Category.assoc]

Premises used: CategoryTheory.Category.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 X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
rw : i₁ ≫ g' ≫ j₃ = (i₁ ≫ j₁) ≫ g''
rw₁ : i₁ ≫ j₁ ≫ g'' = (i₁ ≫ j₁) ≫ g''
rw₂ rw₃ : i₁ ≫ j₁ ≫ g'' = i₁ ≫ j₁ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''

Tactic:
rw [reassoc_of% e₂, e₄, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
h₀ :
  Eq (α := Y ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f g) (inl f g)
      (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄)))
    (CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯))
h₁ :
  Eq (α := Z ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f g) (inr f g)
      (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄)))
    (CategoryStruct.comp (Y := pushout f g) (inr f g) (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯))
⊢ Eq (α := pushout f g ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄))
    (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ Eq (α := Y ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f g) (inl f g)
      (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄)))
    (CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPushout f g
inst_2 : HasPushout f' g'
inst_3 : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ Eq (α := Z ⟶ pushout f'' g'')
    (CategoryStruct.comp (Y := pushout f g) (inr f g)
      (CategoryStruct.comp (Y := pushout f' g') (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄)))
    (CategoryStruct.comp (Y := pushout f g) (inr f g) (map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯))

Tactic:
simp
-- 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 : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
simp
-- 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 : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ g ≫ 𝟙 Z = 𝟙 X ≫ g

Tactic:
simp
-- 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
h₀ : CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯) = inl f g ≫ 𝟙 (pushout f g)
h₁ : CategoryStruct.comp (Y := pushout f g) (inr f g) (map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯) = inr f g ≫ 𝟙 (pushout f g)
⊢ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = 𝟙 (pushout f g)

Tactic:
ext
-- 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
⊢ CategoryStruct.comp (Y := pushout f g) (inl f g) (map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯) = inl f g ≫ 𝟙 (pushout f g)

Tactic:
simp
-- 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
⊢ CategoryStruct.comp (Y := pushout f g) (inr f g) (map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯) = inr f g ≫ 𝟙 (pushout f g)

Tactic:
simp
-- 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₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback 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₃
⊢ IsIso (X := pullback f₁ f₂) (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Tactic:
⟨⟨pullback.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩

Premises used: CategoryTheory.Limits.pullback.map, And.intro, Exists.intro, CategoryTheory.inv, CategoryTheory.IsIso.mk
-- 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₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback 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_1 : g₁ ≫ inv i₃ = inv i₁ ≫ f₁
refine_2 : g₂ ≫ inv i₃ = inv i₂ ≫ f₂
refine_3 :
  CategoryStruct.comp (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
      (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯) =
    𝟙 (pullback f₁ f₂)
refine_4 :
  CategoryStruct.comp (Y := pullback f₁ f₂) (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯)
      (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =
    𝟙 (pullback g₁ g₂)
⊢ IsIso (X := pullback f₁ f₂) (Y := pullback g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Tactic:
refine ⟨⟨pullback.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- 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₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback 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_1 : g₁ = (inv i₁ ≫ f₁) ≫ i₃
refine_1₁ : g₁ = inv i₁ ≫ f₁ ≫ i₃
refine_1₂ : g₁ = inv i₁ ≫ i₁ ≫ g₁
refine_1₃ refine_1₄ : 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_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst_1 : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst_2 : HasPullback 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 ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
⊢ f₁ ≫ 𝟙 Z = 𝟙 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 ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
⊢ g₁ ≫ 𝟙 Z = 𝟙 Y ≫ 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 ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
⊢ f₂ ≫ 𝟙 Z = 𝟙 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 ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 Y ≫ 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 ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
h₀ :
  Eq (α := pullback f₂ g₂ ⟶ X) (CategoryStruct.comp (Y := pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (fst f₁ g₁))
    (CategoryStruct.comp (Y := pullback f₁ g₁) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (fst f₁ g₁))
h₃ :
  Eq (α := pullback f₂ g₂ ⟶ Y) (CategoryStruct.comp (Y := pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (snd f₁ g₁))
    (CategoryStruct.comp (Y := pullback f₁ g₁) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (snd f₁ g₁))
⊢ Eq (α := pullback f₂ g₂ ⟶ pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯)

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 ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
⊢ Eq (α := pullback f₂ g₂ ⟶ X) (CategoryStruct.comp (Y := pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (fst f₁ g₁))
    (CategoryStruct.comp (Y := pullback f₁ g₁) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (fst f₁ g₁))

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₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPullback f₁ g₁
inst_2 : HasPullback f₂ g₂
⊢ Eq (α := pullback f₂ g₂ ⟶ Y) (CategoryStruct.comp (Y := pullback f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (snd f₁ g₁))
    (CategoryStruct.comp (Y := pullback f₁ g₁) (map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯) (snd f₁ g₁))

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
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₃
⊢ IsIso (X := pushout f₁ f₂) (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Tactic:
⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩

Premises used: CategoryTheory.Limits.pushout.map, And.intro, Exists.intro, CategoryTheory.inv, CategoryTheory.IsIso.mk
-- 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_1 : g₁ ≫ inv i₁ = inv i₃ ≫ f₁
refine_2 : g₂ ≫ inv i₂ = inv i₃ ≫ f₂
refine_3 :
  CategoryStruct.comp (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
      (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯) =
    𝟙 (pushout f₁ f₂)
refine_4 :
  CategoryStruct.comp (Y := pushout f₁ f₂) (map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯)
      (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =
    𝟙 (pushout g₁ g₂)
⊢ IsIso (X := pushout f₁ f₂) (Y := pushout g₁ g₂) (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Tactic:
refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
-- 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_1 : g₁ = (inv i₃ ≫ f₁) ≫ i₁
refine_1₁ : g₁ = inv i₃ ≫ f₁ ≫ i₁
refine_1₂ : g₁ = inv i₃ ≫ i₃ ≫ g₁
refine_1₃ refine_1₄ : 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