awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso fst
inst_2 : Mono g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (fun (s : PullbackCone f g) ↦ s.fst ≫ inv fst) s ≫ snd = s.snd

Tactic:
simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono, CategoryTheory.CommSq.w, CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso fst
inst_2 : IsIso g
sq : CommSq fst snd f g
⊢ IsPullback fst snd f g

Tactic:
of_horiz_isIso_mono sq

Premises used: CategoryTheory.IsPullback.of_horiz_isIso_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
rw : e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₁ : fst ≫ e₂.hom ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₂ : fst ≫ f ≫ e₄.hom = e₁.hom ≫ snd' ≫ g'
rw₃ : fst ≫ f ≫ e₄.hom = snd ≫ e₃.hom ≫ g'
rw₄ : fst ≫ f ≫ e₄.hom = snd ≫ g ≫ e₄.hom
rw₅ rw₆ : snd ≫ g ≫ e₄.hom = snd ≫ g ≫ e₄.hom
⊢ fst' ≫ f' = snd' ≫ g'

Tactic:
rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, h.w_assoc]

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_1 :
  h.cone.fst =
    e₁.hom ≫ PullbackCone.fst ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))
refine_2 :
  h.cone.snd =
    e₁.hom ≫ PullbackCone.snd ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))
⊢ h.cone ≅ (Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯)

Tactic:
refine PullbackCone.ext e₁ ?_ ?_

Premises used: CategoryTheory.Limits.PullbackCone.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_1 : fst = e₁.hom ≫ fst' ≫ e₂.inv
⊢ h.cone.fst =
    e₁.hom ≫ PullbackCone.fst ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))

Tactic:
change fst = e₁.hom ≫ fst' ≫ e₂.inv

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_1 : fst = fst ≫ e₂.hom ≫ e₂.inv
refine_1₁ : fst = fst ≫ 𝟙 X
refine_1₂ refine_1₃ : fst = fst
⊢ fst = e₁.hom ≫ fst' ≫ e₂.inv

Tactic:
rw [← reassoc_of% commfst, e₂.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_2 : snd = e₁.hom ≫ snd' ≫ e₃.inv
⊢ h.cone.snd =
    e₁.hom ≫ PullbackCone.snd ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))

Tactic:
change snd = e₁.hom ≫ snd' ≫ e₃.inv

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_2 : snd = snd ≫ e₃.hom ≫ e₃.inv
refine_2₁ : snd = snd ≫ 𝟙 Y
refine_2₂ refine_2₃ : snd = snd
⊢ snd = e₁.hom ≫ snd' ≫ e₃.inv

Tactic:
rw [← reassoc_of% commsnd, e₃.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
commfst₁ : fst ≫ e₂.symm.hom = e₁.symm.hom ≫ fst'
commsnd₁ : snd ≫ e₃.symm.hom = e₁.symm.hom ≫ snd'
commf₁ : f ≫ e₄.symm.hom = e₂.symm.hom ≫ f'
commg₁ : g ≫ e₄.symm.hom = e₃.symm.hom ≫ g'
⊢ IsPullback fst' snd' f' g'

Tactic:
apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm

Premises used: CategoryTheory.IsPullback.of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ fst ≫ e₂.symm.hom = e₁.symm.hom ≫ fst'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commfst, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ snd ≫ e₃.symm.hom = e₁.symm.hom ≫ snd'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commsnd, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ f ≫ e₄.symm.hom = e₂.symm.hom ≫ f'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commf, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ g ≫ e₄.symm.hom = e₃.symm.hom ≫ g'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y : C
fst snd : P ⟶ X
f : X ⟶ Y
h : IsPullback fst snd f f
inst : Mono f
⊢ IsIso fst

Tactic:
h.cone.isIso_fst_of_mono_of_isLimit h.isLimit

Premises used: CategoryTheory.Limits.PullbackCone.isIso_fst_of_mono_of_isLimit, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y : C
fst snd : P ⟶ X
f : X ⟶ Y
h : IsPullback fst snd f f
inst : Mono f
⊢ IsIso snd

Tactic:
h.cone.isIso_snd_of_mono_of_isLimit h.isLimit

Premises used: CategoryTheory.Limits.PullbackCone.isIso_snd_of_mono_of_isLimit, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Mono g
right_cancellation : ∀ {Z : C} (g h : Z ⟶ P), g ≫ fst = h ≫ fst → g = h
⊢ Mono fst

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Mono g
W : C
fst' snd' : W ⟶ P
heq : fst' ≫ fst = snd' ≫ fst
⊢ fst' ≫ snd = snd' ≫ snd

Tactic:
simp [← cancel_mono g, ← h.w, reassoc_of% heq]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Mono g
W : C
fst' snd' : W ⟶ P
heq : fst' ≫ fst = snd' ≫ fst
⊢ fst' = snd'

Tactic:
exact h.hom_ext heq (by simp [← cancel_mono g, ← h.w, reassoc_of% heq])

Premises used: CategoryTheory.IsPullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Mono f
⊢ Mono snd

Tactic:
h.flip.mono_fst_of_mono

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.mono_fst_of_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
⊢ HasPullback f g

Tactic:
have := h.hasPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
this : HasPullback f g
rw : IsIso (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g))
⊢ IsIso fst

Tactic:
rw [← h.isoPullback_hom_fst]

Premises used: CategoryTheory.IsPullback.isoPullback_hom_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
this : HasPullback f g
⊢ IsIso (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso f
⊢ IsIso snd

Tactic:
h.flip.isIso_fst_of_isIso

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.isIso_fst_of_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₁₁ v₁₁ v₁₂ h₂₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
⊢ IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁

Tactic:
of_isLimit (pasteHorizIsPullback rfl t.isLimit s.isLimit)

Premises used: CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Limits.pasteHorizIsPullback, rfl, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₁ v₁₁ v₁₂ h₂₁
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)

Tactic:
(paste_vert s.flip t.flip).flip

Premises used: CategoryTheory.IsPullback.paste_vert, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁
p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
⊢ IsPullback h₁₁ v₁₁ v₁₂ h₂₁

Tactic:
of_isLimit (leftSquareIsPullback (PullbackCone.mk h₁₁ _ p) rfl t.isLimit s.isLimit)

Premises used: CategoryTheory.Limits.leftSquareIsPullback, CategoryTheory.IsPullback.of_isLimit, CategoryTheory.Limits.PullbackCone.mk, rfl, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ IsPullback h₁₁ v₁₁ v₁₂ h₂₁

Tactic:
(of_bot s.flip p.symm t.flip).flip

Premises used: CategoryTheory.IsPullback.of_bot, CategoryTheory.IsPullback.flip, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁
⊢ IsPullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ ↔ IsPullback h₁₁ v₁₁ v₁₂ h₂₁

Tactic:
⟨fun h => h.of_bot e s, fun h => h.paste_vert s⟩

Premises used: CategoryTheory.IsPullback.of_bot, CategoryTheory.IsPullback.paste_vert, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
e : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁
⊢ IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ IsPullback h₁₁ v₁₁ v₁₂ h₂₁

Tactic:
⟨fun h => h.of_right e s, fun h => h.paste_horiz s⟩

Premises used: Iff.intro, CategoryTheory.IsPullback.of_right, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
h₁₃ : X₁₁ ⟶ X₁₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
rw : v₁₁ ≫ h₂₁ ≫ h₂₂ = (v₁₁ ≫ h₂₁) ≫ h₂₂
rw₁ rw₂ : v₁₁ ≫ h₂₁ ≫ h₂₂ = v₁₁ ≫ h₂₁ ≫ h₂₂
⊢ h₁₃ ≫ v₁₃ = (v₁₁ ≫ h₂₁) ≫ h₂₂

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
h₁₃ : X₁₁ ⟶ X₁₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ IsPullback (t.lift h₁₃ (v₁₁ ≫ h₂₁) ⋯) v₁₁ v₁₂ h₂₁

Tactic:
of_right ((t.lift_fst _ _ _) ▸ s) (t.lift_snd _ _ _) t

Premises used: CategoryTheory.IsPullback.lift_snd, CategoryTheory.IsPullback.of_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₃₁ : X₁₁ ⟶ X₃₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
rw : h₁₁ ≫ v₁₂ ≫ v₂₂ = v₃₁ ≫ h₃₁
rw₁ rw₂ : v₃₁ ≫ h₃₁ = v₃₁ ≫ h₃₁
⊢ (h₁₁ ≫ v₁₂) ≫ v₂₂ = v₃₁ ≫ h₃₁

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₃₁ : X₁₁ ⟶ X₃₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
⊢ h₁₁ ≫ v₁₂ = t.lift (h₁₁ ≫ v₁₂) v₃₁ ⋯ ≫ h₂₁

Tactic:
simp only [lift_fst]

Premises used: CategoryTheory.IsPullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullbacksAlong f
h : P ⟶ Y
⊢ HasPullback (Y := pullback g f) h (pullback.fst g f)

Tactic:
IsPullback.hasPullback (IsPullback.of_bot' (IsPullback.of_hasPullback (h ≫ g) f)
    (IsPullback.of_hasPullback g f))

Premises used: CategoryTheory.IsPullback.of_bot', CategoryTheory.IsPullback.hasPullback, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso snd
inst_2 : Mono f
sq : CommSq fst snd f g
⊢ IsPullback fst snd f g

Tactic:
IsPullback.flip (of_horiz_isIso_mono sq.flip)

Premises used: CategoryTheory.CommSq.flip, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_horiz_isIso_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso snd
inst_2 : IsIso f
sq : CommSq fst snd f g
⊢ IsPullback fst snd f g

Tactic:
of_vert_isIso_mono sq

Premises used: CategoryTheory.IsPullback.of_vert_isIso_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
refine_1 :
  CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.fst
refine_2 :
  CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.snd
refine_3 :
  ∀
    {m :
      s.pt ⟶
        Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
          (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)},
    m ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst →
      m ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.snd →
        m = prod.lift s.fst (s.snd ≫ prod.snd)
⊢ { l :
    s.pt ⟶
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) //
    l ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst ∧
      l ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.snd ∧
        ∀
          {m :
            s.pt ⟶
              Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
                (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)},
          m ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst →
            m ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) =
                s.snd →
              m = l }

Tactic:
refine ⟨prod.lift s.fst (s.snd ≫ prod.snd), ?_, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.fst

Tactic:
simp