awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Eq (α := pullback f f ⟶ X) (pullback.fst f f) (pullback.snd f f)

Tactic:
PullbackCone.fst_eq_snd_of_mono_eq (getLimitCone (cospan f f)).cone

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.PullbackCone.fst_eq_snd_of_mono_eq, CategoryTheory.Limits.LimitCone.cone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h₀ : Iso.hom (pullbackSymmetry f f) ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f
h₁ : Iso.hom (pullbackSymmetry f f) ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f
⊢ Iso.hom (pullbackSymmetry f f) = 𝟙 (pullback f f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
⊢ Iso.hom (pullbackSymmetry f f) ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f

Tactic:
simp [fst_eq_snd_of_mono_eq]

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

Tactic:
simp [fst_eq_snd_of_mono_eq]

Premises used: CategoryTheory.Limits.fst_eq_snd_of_mono_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ ≫ t.fst = 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
refine : t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt
⊢ IsIso t.fst

Tactic:
refine ⟨⟨PullbackCone.IsLimit.lift ht (𝟙 _) (𝟙 _) (by simp), ?_, by simp⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
h₀ : (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.fst = 𝟙 t.pt ≫ t.fst
h₁ : (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.snd = 𝟙 t.pt ≫ t.snd
⊢ t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ = 𝟙 t.pt

Tactic:
apply PullbackCone.IsLimit.hom_ext ht

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.fst = 𝟙 t.pt ≫ t.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.snd = 𝟙 t.pt ≫ t.snd

Tactic:
simp [fst_eq_snd_of_mono_eq]

Premises used: CategoryTheory.Limits.PullbackCone.fst_eq_snd_of_mono_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsIso t.snd

Tactic:
t.fst_eq_snd_of_mono_eq ▸ t.isIso_fst_of_mono_of_isLimit ht

Premises used: Eq.rec, CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit, CategoryTheory.Limits.PullbackCone.fst_eq_snd_of_mono_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
inst_1 : Mono f
⊢ IsIso (X := pullback f f) (pullback.fst f f)

Tactic:
PullbackCone.isIso_fst_of_mono_of_isLimit (getLimitCone (cospan f f)).isLimit

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
inst_1 : Mono f
⊢ IsIso (X := pullback f f) (pullback.snd f f)

Tactic:
PullbackCone.isIso_snd_of_mono_of_isLimit (getLimitCone (cospan f f)).isLimit

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.PullbackCone.isIso_snd_of_mono_of_isLimit, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
inst_1 : Epi f
W : C
h k : t.pt ⟶ W
i : t.inr ≫ h = t.inr ≫ k
⊢ t.inl ≫ h = t.inl ≫ k

Tactic:
simp [← cancel_epi f, t.condition_assoc, i]

Premises used: CategoryTheory.Limits.PushoutCocone.condition_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
inst_1 : Epi g
W : C
h k : t.pt ⟶ W
i : t.inl ≫ h = t.inl ≫ k
⊢ t.inr ≫ h = t.inr ≫ k

Tactic:
simp [← cancel_epi g, ← t.condition_assoc, i]

Premises used: CategoryTheory.Limits.PushoutCocone.condition_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst_1 : Epi f
s : PushoutCocone f f
rw : f ≫ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = f ≫ s.inr
rw₁ : f ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = f ≫ s.inr
rw₂ rw₃ : f ≫ s.inr = f ≫ s.inr
⊢ 𝟙 Y ≫ (fun (s : PushoutCocone f f) ↦ s.inl) s = s.inr

Tactic:
rw [← cancel_epi f, Category.id_comp, s.condition]

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.cancel_epi, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst_1 : Epi f
s : PushoutCocone f f
m : Y ⟶ s.pt
m₁ : 𝟙 Y ≫ m = s.inl
h : 𝟙 Y ≫ m = s.inr
⊢ m = (fun (s : PushoutCocone f f) ↦ s.inl) s

Tactic:
simpa using m₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit.{0, v, 0, u} (F := span f f) (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
g h : Y ⟶ Z
eq : f ≫ g = f ≫ h
rcases :
  ∀ (val : Cocone.pt.{0, v, 0, u} (F := span f f) (mk (𝟙 Y) (𝟙 Y) ⋯) ⟶ Z)
    (eq : f ≫ inl (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val = f ≫ inr (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val),
    inl (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val = inr (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val
⊢ g = h

Tactic:
rcases PushoutCocone.IsColimit.desc' t _ _ eq with ⟨_, rfl, rfl⟩

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.desc', rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit.{0, v, 0, u} (F := span f f) (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
val : Cocone.pt.{0, v, 0, u} (F := span f f) (mk (𝟙 Y) (𝟙 Y) ⋯) ⟶ Z
eq : f ≫ inl (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val = f ≫ inr (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val
⊢ inl (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val = inr (mk (𝟙 Y) (𝟙 Y) ⋯) ≫ val

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
rw : (h ≫ x) ≫ s.inl = f ≫ s.inl
⊢ h ≫ x ≫ s.inl = f ≫ s.inl

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
⊢ (h ≫ x) ≫ s.inl = f ≫ s.inl

Tactic:
apply congrArg (· ≫ inl s) hhx

Premises used: congrArg, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
rw : (h ≫ y) ≫ s.inr = g ≫ s.inr
⊢ h ≫ y ≫ s.inr = g ≫ s.inr

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ (h ≫ y) ≫ s.inr = g ≫ s.inr

Tactic:
apply congrArg (· ≫ inr s) hhy

Premises used: congrArg, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
rw : f ≫ s.inl = h ≫ y ≫ s.inr
rw₁ : f ≫ s.inl = g ≫ s.inr
rw₂ rw₃ : g ≫ s.inr = g ≫ s.inr
⊢ h ≫ x ≫ s.inl = h ≫ y ≫ s.inr

Tactic:
rw [reassoc₁, reassoc₂, s.condition]

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
rw : (h ≫ x) ≫ t.inl = g ≫ t.inr
rw₁ : (h ≫ x) ≫ t.inl = (h ≫ y) ≫ t.inr
rw₂ : h ≫ x ≫ t.inl = (h ≫ y) ≫ t.inr
rw₃ : h ≫ x ≫ t.inl = h ≫ y ≫ t.inr
rw₄ rw₅ : h ≫ y ≫ t.inr = h ≫ y ≫ t.inr
⊢ f ≫ t.inl = g ≫ t.inr

Tactic:
rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : inl (mk s.inl s.inr ⋯) ≫ m = t.inl
hr' : inr (mk s.inl s.inr ⋯) ≫ m = t.inr
h₀ : s.inl ≫ m = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)
h₁ : s.inr ≫ m = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)
⊢ m = hs.desc (mk t.inl t.inr ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext hs

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
h₀ : t.inl = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)
⊢ s.inl ≫ m = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
simp only [hr]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
h₀ : s.inl ≫ hs.desc (mk t.inl t.inr ⋯) = t.inl
⊢ t.inl = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ s.inl ≫ hs.desc (mk t.inl t.inr ⋯) = t.inl

Tactic:
hs.fac _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.span
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ s.inl ≫ hs.desc (mk t.inl t.inr ⋯) = t.inl

Tactic:
exact hs.fac _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
h₁ : t.inr = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)
⊢ s.inr ≫ m = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
simp only [hr']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
h₁ : s.inr ≫ hs.desc (mk t.inl t.inr ⋯) = t.inr
⊢ t.inr = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ s.inr ≫ hs.desc (mk t.inl t.inr ⋯) = t.inr

Tactic:
hs.fac _ WalkingSpan.right

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.span
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst_1 : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m : Cocone.pt (F := span x y) (mk s.inl s.inr ⋯) ⟶ t.pt
hr : s.inl ≫ m = t.inl
hr' : s.inr ≫ m = t.inr
⊢ s.inr ≫ hs.desc (mk t.inl t.inr ⋯) = t.inr

Tactic:
exact hs.fac _ WalkingSpan.right

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s : PushoutCocone f g
H : IsColimit s
rw : h ≫ f ≫ s.inl = (h ≫ g) ≫ s.inr
rw₁ : h ≫ f ≫ s.inl = h ≫ g ≫ s.inr
rw₂ rw₃ : h ≫ g ≫ s.inr = h ≫ g ≫ s.inr
⊢ (h ≫ f) ≫ s.inl = (h ≫ g) ≫ s.inr

Tactic:
rw [Category.assoc, Category.assoc, s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s : PushoutCocone f g
H : IsColimit s
create :
  (s_1 : PushoutCocone (h ≫ f) (h ≫ g)) →
    { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s.inl s.inr ⋯) ⟶ s_1.pt //
      inl (mk s.inl s.inr ⋯) ≫ l = s_1.inl ∧
        inr (mk s.inl s.inr ⋯) ≫ l = s_1.inr ∧
          ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s.inl s.inr ⋯) ⟶ s_1.pt},
            inl (mk s.inl s.inr ⋯) ≫ m = s_1.inl → inr (mk s.inl s.inr ⋯) ≫ m = s_1.inr → m = l }
⊢ IsColimit (F := span (h ≫ f) (h ≫ g)) (mk s.inl s.inr ⋯)

Tactic:
apply PushoutCocone.isColimitAux'

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitAux'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s_1 : PushoutCocone f g
H : IsColimit s_1
s : PushoutCocone (h ≫ f) (h ≫ g)
⊢ h ≫ f ≫ s.inl = h ≫ g ≫ s.inr

Tactic:
simpa using s.condition

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s_1 : PushoutCocone f g
H : IsColimit s_1
s : PushoutCocone (h ≫ f) (h ≫ g)
create :
  (l : s_1.pt ⟶ s.pt) →
    (h₁ : s_1.inl ≫ l = s.inl) →
      (h₂ : s_1.inr ≫ l = s.inr) →
        { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt //
          inl (mk s_1.inl s_1.inr ⋯) ≫ l = s.inl ∧
            inr (mk s_1.inl s_1.inr ⋯) ≫ l = s.inr ∧
              ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt},
                inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl → inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr → m = l }
⊢ { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt //
    inl (mk s_1.inl s_1.inr ⋯) ≫ l = s.inl ∧
      inr (mk s_1.inl s_1.inr ⋯) ≫ l = s.inr ∧
        ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt},
          inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl → inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr → m = l }

Tactic:
rcases PushoutCocone.IsColimit.desc' H s.inl s.inr
      ((cancel_epi h).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩

Premises used: CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Limits.PushoutCocone.IsColimit.desc', Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s_1 : PushoutCocone f g
H : IsColimit s_1
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s_1.pt ⟶ s.pt
h₁ : s_1.inl ≫ l = s.inl
h₂ : s_1.inr ≫ l = s.inr
create :
  ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt},
    inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl → inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr → m = l
⊢ { l : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt //
    inl (mk s_1.inl s_1.inr ⋯) ≫ l = s.inl ∧
      inr (mk s_1.inl s_1.inr ⋯) ≫ l = s.inr ∧
        ∀ {m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt},
          inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl → inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr → m = l }

Tactic:
refine ⟨l, h₁, h₂, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s_1 : PushoutCocone f g
H : IsColimit s_1
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s_1.pt ⟶ s.pt
h₁ : s_1.inl ≫ l = s.inl
h₂ : s_1.inr ≫ l = s.inr
m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt
hm₁ : inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl
hm₂ : inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr
⊢ m = l

Tactic:
(PushoutCocone.IsColimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext, CategoryTheory.Limits.WidePushoutShape.wideSpan, Eq.symm, CategoryTheory.Limits.span, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Y
g_1 : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
s_1 : PushoutCocone f g
H : IsColimit s_1
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s_1.pt ⟶ s.pt
h₁ : s_1.inl ≫ l = s.inl
h₂ : s_1.inr ≫ l = s.inr
m : Cocone.pt (F := span (h ≫ f) (h ≫ g)) (mk s_1.inl s_1.inr ⋯) ⟶ s.pt
hm₁ : inl (mk s_1.inl s_1.inr ⋯) ≫ m = s.inl
hm₂ : inr (mk s_1.inl s_1.inr ⋯) ≫ m = s.inr
⊢ m = l

Tactic:
exact (PushoutCocone.IsColimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
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
inst_2 : Epi g
⊢ Epi (Y := pushout f g) (inl f g)

Tactic:
PushoutCocone.epi_inl_of_is_pushout_of_epi (colimit.isColimit _)

Premises used: CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
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
inst_2 : Epi f
⊢ Epi (Y := pushout f g) (inr f g)

Tactic:
PushoutCocone.epi_inr_of_is_pushout_of_epi (colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
W_1 X_1 Y_1 Z_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasBinaryCoproduct.{v_1, u_1} Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h :
  Eq (α := coprod.{v_1, u_1} Y Z ⟶ W) (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁)
    (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂)
h₀ : pushout.inl f g ≫ i₁ = pushout.inl f g ≫ i₂
h₁ : pushout.inr f g ≫ i₁ = pushout.inr f g ≫ i₂
⊢ i₁ = i₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
W_1 X_1 Y_1 Z_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasBinaryCoproduct.{v_1, u_1} Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h :
  Eq (α := coprod.{v_1, u_1} Y Z ⟶ W) (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁)
    (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂)
⊢ pushout.inl f g ≫ i₁ = pushout.inl f g ≫ i₂

Tactic:
simpa using congrArg (fun f => coprod.inl ≫ f) h

Premises used: congrArg, CategoryTheory.Limits.coprod.inl, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
W_1 X_1 Y_1 Z_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasBinaryCoproduct.{v_1, u_1} Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h :
  Eq (α := coprod.{v_1, u_1} Y Z ⟶ W) (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁)
    (coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂)
⊢ pushout.inr f g ≫ i₁ = pushout.inr f g ≫ i₂

Tactic:
simpa using congrArg (fun f => coprod.inr ≫ f) h

Premises used: congrArg, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.coprod.inr