awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ (pushoutCoconeOfRightIso f g).inr = inv g ≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ (pushoutCoconeOfRightIso f g).ι.app none = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ (pushoutCoconeOfRightIso f g).ι.app left = 𝟙 ((span f g).obj left)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ (pushoutCoconeOfRightIso f g).ι.app right = inv g ≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
s : PushoutCocone f g
⊢ (pushoutCoconeOfRightIso f g).inl ≫ s.inl = s.inl ∧
    (pushoutCoconeOfRightIso f g).inr ≫ s.inl = s.inr ∧
      ∀ {m : (pushoutCoconeOfRightIso f g).pt ⟶ s.pt},
        (pushoutCoconeOfRightIso f g).inl ≫ m = s.inl → (pushoutCoconeOfRightIso f g).inr ≫ m = s.inr → m = s.inl

Tactic:
simp [← s.condition]

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

Tactic:
⟨⟨⟨_, pushoutCoconeOfRightIsoIsLimit f g⟩⟩⟩

Premises used: CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (𝟙 Y) (inv g ≫ f) ⋯) = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
refine : pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = 𝟙 (pushout f g)
⊢ IsIso (Y := pushout f g) (pushout.inl f g)

Tactic:
refine ⟨⟨pushout.desc (𝟙 _) (inv g ≫ f) (by simp), by simp, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
h₀ :
  CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g) =
    pushout.inl f g ≫ 𝟙 (pushout f g)
h₁ :
  CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g) =
    pushout.inr f g ≫ 𝟙 (pushout f g)
⊢ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = 𝟙 (pushout f g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g) =
    pushout.inl f g ≫ 𝟙 (pushout f g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g) =
    pushout.inr f g ≫ 𝟙 (pushout f g)

Tactic:
simp [pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
rw : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = f
rw₁ : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inl f g)) = f
rw₂ : f ≫ 𝟙 Y = f
rw₃ rw₄ : f = f
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = inv g ≫ f

Tactic:
rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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

Tactic:
⟨fun {W} h k i => IsLimit.hom_ext ht ?_ i⟩

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, CategoryTheory.Mono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono f
refine : ∀ {W : C} (h k : W ⟶ t.pt) (i : h ≫ t.snd = k ≫ t.snd), h ≫ t.fst = k ≫ t.fst
⊢ Mono t.snd

Tactic:
refine ⟨fun {W} h k i => IsLimit.hom_ext ht ?_ i⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
rw : h ≫ t.snd ≫ g = k ≫ t.snd ≫ g
⊢ h ≫ t.fst = k ≫ t.fst

Tactic:
rw [← cancel_mono f, Category.assoc, Category.assoc, condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.snd ≫ g = k ≫ t.snd ≫ g

Tactic:
apply reassoc_of% i
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono g
⊢ Mono t.fst

Tactic:
⟨fun {W} h k i => IsLimit.hom_ext ht i ?_⟩

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, CategoryTheory.Mono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono g
refine : ∀ {W : C} (h k : W ⟶ t.pt) (i : h ≫ t.fst = k ≫ t.fst), h ≫ t.snd = k ≫ t.snd
⊢ Mono t.fst

Tactic:
refine ⟨fun {W} h k i => IsLimit.hom_ext ht i ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
rw : h ≫ t.fst ≫ f = k ≫ t.fst ≫ f
⊢ h ≫ t.snd = k ≫ t.snd

Tactic:
rw [← cancel_mono g, Category.assoc, Category.assoc, ← condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.fst ≫ f = k ≫ t.fst ≫ f

Tactic:
apply reassoc_of% i
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst_1 : Mono f
s : PullbackCone f f
rw : ((fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X) ≫ f = s.snd ≫ f
rw₁ : (fun (s : PullbackCone f f) ↦ s.fst) s ≫ f = s.snd ≫ f
rw₂ rw₃ : s.snd ≫ f = s.snd ≫ f
⊢ (fun (s : PullbackCone f f) ↦ s.fst) s ≫ 𝟙 X = s.snd

Tactic:
rw [← cancel_mono f, Category.comp_id, s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst_1 : Mono f
s : PullbackCone f f
m : s.pt ⟶ X
m₁ : m ≫ 𝟙 X = s.fst
h : m ≫ 𝟙 X = s.snd
⊢ m = (fun (s : PullbackCone f f) ↦ s.fst) 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 : IsLimit.{0, v, 0, u} (F := cospan f f) (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
g h : Z ⟶ X
eq : g ≫ f = h ≫ f
rcases :
  ∀ (val : Z ⟶ Cone.pt.{0, v, 0, u} (F := cospan f f) (mk (𝟙 X) (𝟙 X) ⋯))
    (eq : (val ≫ fst (mk (𝟙 X) (𝟙 X) ⋯)) ≫ f = (val ≫ snd (mk (𝟙 X) (𝟙 X) ⋯)) ≫ f),
    val ≫ fst (mk (𝟙 X) (𝟙 X) ⋯) = val ≫ snd (mk (𝟙 X) (𝟙 X) ⋯)
⊢ g = h

Tactic:
rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift', rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit.{0, v, 0, u} (F := cospan f f) (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
val : Z ⟶ Cone.pt.{0, v, 0, u} (F := cospan f f) (mk (𝟙 X) (𝟙 X) ⋯)
eq : (val ≫ fst (mk (𝟙 X) (𝟙 X) ⋯)) ≫ f = (val ≫ snd (mk (𝟙 X) (𝟙 X) ⋯)) ≫ f
⊢ val ≫ fst (mk (𝟙 X) (𝟙 X) ⋯) = val ≫ snd (mk (𝟙 X) (𝟙 X) ⋯)

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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
⊢ (s.fst ≫ x) ≫ h = (s.snd ≫ y) ≫ h

Tactic:
simp only [Category.assoc, hxh, hyh, s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
rw : (t.fst ≫ x) ≫ h = (t.snd ≫ y) ≫ h
⊢ t.fst ≫ x ≫ h = t.snd ≫ y ≫ h

Tactic:
rw [← Category.assoc, ← 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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
⊢ (t.fst ≫ x) ≫ h = (t.snd ≫ y) ≫ h

Tactic:
apply congrArg (· ≫ h) t.condition

Premises used: CategoryTheory.Limits.PullbackCone.condition, congrArg, 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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
rw : t.fst ≫ x ≫ h = t.snd ≫ g
rw₁ : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
rw₂ rw₃ : t.snd ≫ y ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ f = t.snd ≫ g

Tactic:
rw [← hxh, ← hyh, this]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ fst (mk s.fst s.snd ⋯) = t.fst
hr' : m ≫ snd (mk s.fst s.snd ⋯) = t.snd
h₀ : m ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst
h₁ : m ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
⊢ m = hs.lift (mk t.fst t.snd ⋯)

Tactic:
apply PullbackCone.IsLimit.hom_ext hs

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
h₀ : t.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst
⊢ m ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

Tactic:
simp only [hr, 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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
h₁ : t.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
⊢ m ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd

Tactic:
simp only [hr, 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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
h₀ : hs.lift (mk t.fst t.snd ⋯) ≫ s.fst = t.fst
⊢ t.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
h₁ : hs.lift (mk t.fst t.snd ⋯) ≫ s.snd = t.snd
⊢ t.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd

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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
⊢ hs.lift (mk t.fst t.snd ⋯) ≫ s.fst = t.fst

Tactic:
hs.fac _ WalkingCospan.left

Premises used: CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.cospan, CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
⊢ hs.lift (mk t.fst t.snd ⋯) ≫ s.snd = t.snd

Tactic:
hs.fac _ WalkingCospan.right

Premises used: CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.cospan, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst_1 : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m : t.pt ⟶ Cone.pt (F := cospan x y) (mk s.fst s.snd ⋯)
hr : m ≫ s.fst = t.fst
hr' : m ≫ s.snd = t.snd
⊢ hs.lift (mk t.fst t.snd ⋯) ≫ s.fst = t.fst

Tactic:
exacts [hs.fac _ WalkingCospan.left, hs.fac _ WalkingCospan.right]

Premises used: CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s : PullbackCone f g
H : IsLimit s
rw : (s.fst ≫ f) ≫ i = s.snd ≫ g ≫ i
rw₁ : (s.fst ≫ f) ≫ i = (s.snd ≫ g) ≫ i
rw₂ rw₃ : (s.snd ≫ g) ≫ i = (s.snd ≫ g) ≫ i
⊢ s.fst ≫ f ≫ i = s.snd ≫ g ≫ i

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s : PullbackCone f g
H : IsLimit s
create :
  (s_1 : PullbackCone (f ≫ i) (g ≫ i)) →
    { l : s_1.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s.fst s.snd ⋯) //
      l ≫ fst (mk s.fst s.snd ⋯) = s_1.fst ∧
        l ≫ snd (mk s.fst s.snd ⋯) = s_1.snd ∧
          ∀ {m : s_1.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s.fst s.snd ⋯)},
            m ≫ fst (mk s.fst s.snd ⋯) = s_1.fst → m ≫ snd (mk s.fst s.snd ⋯) = s_1.snd → m = l }
⊢ IsLimit (F := cospan (f ≫ i) (g ≫ i)) (mk s.fst s.snd ⋯)

Tactic:
apply PullbackCone.isLimitAux'

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s_1 : PullbackCone f g
H : IsLimit s_1
s : PullbackCone (f ≫ i) (g ≫ i)
⊢ (s.fst ≫ f) ≫ i = (s.snd ≫ g) ≫ i

Tactic:
simpa using s.condition

Premises used: CategoryTheory.Limits.PullbackCone.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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s_1 : PullbackCone f g
H : IsLimit s_1
s : PullbackCone (f ≫ i) (g ≫ i)
create :
  (l : s.pt ⟶ s_1.pt) →
    (h₁ : l ≫ s_1.fst = s.fst) →
      (h₂ : l ≫ s_1.snd = s.snd) →
        { l : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯) //
          l ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst ∧
            l ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd ∧
              ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)},
                m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst → m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd → m = l }
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯) //
    l ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst ∧
      l ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)},
          m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst → m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd → m = l }

Tactic:
rcases PullbackCone.IsLimit.lift' H s.fst s.snd
      ((cancel_mono i).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.cancel_mono, CategoryTheory.Limits.PullbackCone.IsLimit.lift', Iff.mp, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s_1 : PullbackCone f g
H : IsLimit s_1
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s_1.pt
h₁ : l ≫ s_1.fst = s.fst
h₂ : l ≫ s_1.snd = s.snd
create :
  ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)},
    m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst → m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd → m = l
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯) //
    l ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst ∧
      l ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)},
          m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst → m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd → 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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s_1 : PullbackCone f g
H : IsLimit s_1
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s_1.pt
h₁ : l ≫ s_1.fst = s.fst
h₂ : l ≫ s_1.snd = s.snd
m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)
hm₁ : m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst
hm₂ : m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd
⊢ m = l

Tactic:
(PullbackCone.IsLimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

Premises used: CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, CategoryTheory.Limits.cospan, Eq.symm, 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 ⟶ Z
g_1 : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst_1 : Mono i
s_1 : PullbackCone f g
H : IsLimit s_1
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s_1.pt
h₁ : l ≫ s_1.fst = s.fst
h₂ : l ≫ s_1.snd = s.snd
m : s.pt ⟶ Cone.pt (F := cospan (f ≫ i) (g ≫ i)) (mk s_1.fst s_1.snd ⋯)
hm₁ : m ≫ fst (mk s_1.fst s_1.snd ⋯) = s.fst
hm₂ : m ≫ snd (mk s_1.fst s_1.snd ⋯) = s.snd
⊢ m = l

Tactic:
exact (PullbackCone.IsLimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.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 ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
inst_2 : Mono g
⊢ Mono (X := pullback f g) (fst f g)

Tactic:
PullbackCone.mono_fst_of_is_pullback_of_mono (limit.isLimit _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit
-- 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 ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
inst_2 : Mono f
⊢ Mono (X := pullback f g) (snd f g)

Tactic:
PullbackCone.mono_snd_of_is_pullback_of_mono (limit.isLimit _)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono
-- 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 ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h :
  Eq (α := W ⟶ prod.{v_1, u_1} X Y) (i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
    (i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
h₀ : i₁ ≫ pullback.fst f g = i₂ ≫ pullback.fst f g
h₁ : i₁ ≫ pullback.snd f g = i₂ ≫ pullback.snd f g
⊢ 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 ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h :
  Eq (α := W ⟶ prod.{v_1, u_1} X Y) (i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
    (i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
⊢ i₁ ≫ pullback.fst f g = i₂ ≫ pullback.fst f g

Tactic:
simpa using congrArg (fun f => f ≫ prod.fst) h

Premises used: congrArg, CategoryTheory.Limits.prod.fst, 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 ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasBinaryProduct.{v_1, u_1} X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h :
  Eq (α := W ⟶ prod.{v_1, u_1} X Y) (i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
    (i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g))
⊢ i₁ ≫ pullback.snd f g = i₂ ≫ pullback.snd f g

Tactic:
simpa using congrArg (fun f => f ≫ prod.snd) h

Premises used: congrArg, CategoryTheory.Limits.prod.snd, CategoryTheory.CategoryStruct.comp