awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
⊢ IsPushout f g inl inr ↔ IsPushout g f inr inl

Tactic:
⟨flip, flip⟩

Premises used: CategoryTheory.IsPushout.flip, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
⊢ IsPullback.{v₁, u₁} (C := Cᵒᵖ) (P := Opposite.op P) (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op Z)
    inr.op inl.op g.op f.op

Tactic:
IsPullback.of_isLimit
    (IsLimit.ofIsoLimit
      (Limits.PushoutCocone.isColimitEquivIsLimitOp h.flip.cocone h.flip.isColimit)
      h.toCommSq.flip.coconeOp)

Premises used: Quiver.Hom.op, CategoryTheory.IsPushout.cocone, CategoryTheory.IsPullback.of_isLimit, CategoryTheory.CommSq.flip, CategoryTheory.CommSq.coconeOp, CategoryTheory.IsPushout.flip, CategoryTheory.IsPushout.toCommSq, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe, CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : Cᵒᵖ
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout.{v₁, u₁} (C := Cᵒᵖ) (Z := Z) (X := X) (Y := Y) (P := P) f g inl inr
⊢ IsPullback inr.unop inl.unop g.unop f.unop

Tactic:
IsPullback.of_isLimit
    (IsLimit.ofIsoLimit
      (Limits.PushoutCocone.isColimitEquivIsLimitUnop h.flip.cocone h.flip.isColimit)
      h.toCommSq.flip.coconeUnop)

Premises used: CategoryTheory.IsPushout.cocone, Quiver.Hom.unop, CategoryTheory.IsPullback.of_isLimit, CategoryTheory.CommSq.flip, CategoryTheory.CommSq.coconeUnop, CategoryTheory.IsPushout.flip, CategoryTheory.IsPushout.toCommSq, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe, CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
⊢ IsPullback.{v₁, u₁} (C := Cᵒᵖ) (P := Opposite.op P) (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op Z)
      inr.op inl.op g.op f.op ↔
    IsPushout f g inl inr

Tactic:
⟨fun h ↦ h.unop, fun h ↦ h.op⟩

Premises used: Iff.intro, CategoryTheory.IsPullback.unop, CategoryTheory.IsPushout.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z P : Cᵒᵖ
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
⊢ IsPullback inr.unop inl.unop g.unop f.unop ↔
    IsPushout.{v₁, u₁} (C := Cᵒᵖ) (Z := Z) (X := X) (Y := Y) (P := P) f g inl inr

Tactic:
⟨fun h ↦ h.op, fun h ↦ h.unop⟩

Premises used: CategoryTheory.IsPullback.op, CategoryTheory.IsPushout.unop, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
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
⊢ IsPushout.{v₁, u₁} (C := Cᵒᵖ) (Z := Opposite.op Z) (X := Opposite.op Y) (Y := Opposite.op X) (P := Opposite.op P) g.op
      f.op snd.op fst.op ↔
    IsPullback fst snd f g

Tactic:
⟨fun h ↦ h.unop, fun h ↦ h.op⟩

Premises used: CategoryTheory.IsPullback.op, CategoryTheory.IsPushout.unop, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
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
⊢ IsPushout g.unop f.unop snd.unop fst.unop ↔
    IsPullback.{v₁, u₁} (C := Cᵒᵖ) (P := P) (X := X) (Y := Y) (Z := Z) fst snd f g

Tactic:
⟨fun h ↦ h.op, fun h ↦ h.unop⟩

Premises used: Iff.intro, CategoryTheory.IsPullback.unop, CategoryTheory.IsPushout.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasKernel t
inst_3 : HasKernel b
sq : IsPullback t l r b
⊢ Eq (α := kernel b ⟶ X₄) (0 ≫ r) (kernel.ι b ≫ b)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasKernel t
inst_3 : HasKernel b
sq : IsPullback t l r b
⊢ Eq (α := kernel b ⟶ X₂) (sq.lift 0 (kernel.ι b) ⋯ ≫ t) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasKernel t
inst_3 : HasKernel b
sq : IsPullback t l r b
h :
  CategoryStruct.comp (Y := equalizer t 0)
      (CategoryStruct.comp (Y := kernel b) (kernel.map t b l r ⋯) (kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯))
      (equalizer.ι t 0) =
    𝟙 (kernel t) ≫ equalizer.ι t 0
⊢ CategoryStruct.comp (Y := kernel b) (kernel.map t b l r ⋯) (kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) = 𝟙 (kernel t)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasKernel t
inst_3 : HasKernel b
sq : IsPullback t l r b
⊢ CategoryStruct.comp (Y := equalizer t 0)
      (CategoryStruct.comp (Y := kernel b) (kernel.map t b l r ⋯) (kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯))
      (equalizer.ι t 0) =
    𝟙 (kernel t) ≫ equalizer.ι t 0

Tactic:
exact sq.hom_ext (by cat_disch) (by cat_disch)

Premises used: CategoryTheory.IsPullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasCokernel t
inst_3 : HasCokernel b
sq : IsPushout t l r b
⊢ Eq (α := X₁ ⟶ cokernel t) (t ≫ cokernel.π t) (l ≫ 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasCokernel t
inst_3 : HasCokernel b
sq : IsPushout t l r b
⊢ Eq (α := X₃ ⟶ cokernel t) (b ≫ sq.desc (cokernel.π t) 0 ⋯) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasCokernel t
inst_3 : HasCokernel b
sq : IsPushout t l r b
h :
  CategoryStruct.comp (Y := coequalizer b 0) (coequalizer.π b 0)
      (CategoryStruct.comp (Y := cokernel t) (cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯)
        (cokernel.map t b l r ⋯)) =
    coequalizer.π b 0 ≫ 𝟙 (cokernel b)
⊢ CategoryStruct.comp (Y := cokernel t) (cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯) (cokernel.map t b l r ⋯) =
    𝟙 (cokernel b)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasCokernel t
inst_3 : HasCokernel b
sq : IsPushout t l r b
⊢ CategoryStruct.comp (Y := coequalizer b 0) (coequalizer.π b 0)
      (CategoryStruct.comp (Y := cokernel t) (cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯)
        (cokernel.map t b l r ⋯)) =
    coequalizer.π b 0 ≫ 𝟙 (cokernel b)

Tactic:
exact sq.hom_ext (by cat_disch) (by cat_disch)

Premises used: CategoryTheory.IsPushout.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ (g ≫ inv f) ≫ f = 𝟙 Y ≫ 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ (pullbackConeOfLeftIso f g).pt = Y

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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ (pullbackConeOfLeftIso f g).fst = g ≫ inv 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ (pullbackConeOfLeftIso f g).snd = 𝟙 (pullbackConeOfLeftIso f g).pt

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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ (pullbackConeOfLeftIso f g).π.app none = 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ (pullbackConeOfLeftIso f g).π.app left = g ≫ inv 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ (pullbackConeOfLeftIso f g).π.app right =
    𝟙 (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) (pullbackConeOfLeftIso f g).pt) right)

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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
s : PullbackCone f g
⊢ s.snd ≫ (pullbackConeOfLeftIso f g).fst = s.fst ∧
    s.snd ≫ (pullbackConeOfLeftIso f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfLeftIso f g).pt},
        m ≫ (pullbackConeOfLeftIso f g).fst = s.fst → m ≫ (pullbackConeOfLeftIso f g).snd = s.snd → m = s.snd

Tactic:
simp [← s.condition_assoc]

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

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

Premises used: Nonempty.intro, CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ CategoryStruct.comp (Y := pullback f g) (pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) (pullback.snd f g) = 𝟙 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
refine : pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ = 𝟙 (pullback f g)
⊢ IsIso (X := pullback f g) (pullback.snd f g)

Tactic:
refine ⟨⟨pullback.lift (g ≫ inv 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
h₀ :
  CategoryStruct.comp (Y := pullback f g) (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) (pullback.fst f g) =
    𝟙 (pullback f g) ≫ pullback.fst f g
h₁ :
  CategoryStruct.comp (Y := pullback f g) (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) (pullback.snd f g) =
    𝟙 (pullback f g) ≫ pullback.snd f g
⊢ pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ = 𝟙 (pullback 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ CategoryStruct.comp (Y := pullback f g) (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) (pullback.fst f g) =
    𝟙 (pullback f g) ≫ pullback.fst f g

Tactic:
simp [← pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ CategoryStruct.comp (Y := pullback f g) (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) (pullback.snd f g) =
    𝟙 (pullback f g) ≫ pullback.snd 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
rw : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.snd f g ≫ g ≫ inv f)
rw₁ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g ≫ f ≫ inv f)
rw₂ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g ≫ 𝟙 X)
rw₃ rw₄ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g)
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.snd f g)) (pullback.fst f g) = g ≫ inv f

Tactic:
rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ 𝟙 X ≫ f = (f ≫ inv g) ≫ 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ (pullbackConeOfRightIso f g).pt = X

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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ (pullbackConeOfRightIso f g).fst = 𝟙 (pullbackConeOfRightIso f g).pt

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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ (pullbackConeOfRightIso f g).snd = f ≫ inv g

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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ (pullbackConeOfRightIso 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ (pullbackConeOfRightIso f g).π.app left =
    𝟙 (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingCospan) (pullbackConeOfRightIso f g).pt) 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ (pullbackConeOfRightIso f g).π.app right = f ≫ inv g

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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
s : PullbackCone f g
⊢ s.fst ≫ (pullbackConeOfRightIso f g).fst = s.fst ∧
    s.fst ≫ (pullbackConeOfRightIso f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfRightIso f g).pt},
        m ≫ (pullbackConeOfRightIso f g).fst = s.fst → m ≫ (pullbackConeOfRightIso f g).snd = s.snd → m = s.fst

Tactic:
simp [s.condition_assoc]

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

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

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pullback f g) (pullback.lift (𝟙 X) (f ≫ inv g) ⋯) (pullback.fst f g) = 𝟙 X

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

Tactic:
refine ⟨⟨pullback.lift (𝟙 _) (f ≫ inv g) (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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
h₀ :
  CategoryStruct.comp (Y := pullback f g) (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) (pullback.fst f g) =
    𝟙 (pullback f g) ≫ pullback.fst f g
h₁ :
  CategoryStruct.comp (Y := pullback f g) (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) (pullback.snd f g) =
    𝟙 (pullback f g) ≫ pullback.snd f g
⊢ pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯ = 𝟙 (pullback 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pullback f g) (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) (pullback.fst f g) =
    𝟙 (pullback f g) ≫ pullback.fst 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 ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pullback f g) (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) (pullback.snd f g) =
    𝟙 (pullback f g) ≫ pullback.snd f g

Tactic:
simp [pullback.condition_assoc]

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

Tactic:
rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.IsIso.hom_inv_id
-- 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 f
⊢ f ≫ inv f ≫ g = g ≫ 𝟙 Z

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 f
⊢ (pushoutCoconeOfLeftIso f g).pt = Z

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 f
⊢ (pushoutCoconeOfLeftIso f g).inl = inv f ≫ g

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 f
⊢ (pushoutCoconeOfLeftIso f g).inr = 𝟙 Z

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 f
⊢ (pushoutCoconeOfLeftIso f g).ι.app none = 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 f
⊢ (pushoutCoconeOfLeftIso f g).ι.app left = inv f ≫ g

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 f
⊢ (pushoutCoconeOfLeftIso f g).ι.app right = 𝟙 ((span f g).obj right)

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 f
s : PushoutCocone f g
⊢ (pushoutCoconeOfLeftIso f g).inl ≫ s.inr = s.inl ∧
    (pushoutCoconeOfLeftIso f g).inr ≫ s.inr = s.inr ∧
      ∀ {m : (pushoutCoconeOfLeftIso f g).pt ⟶ s.pt},
        (pushoutCoconeOfLeftIso f g).inl ≫ m = s.inl → (pushoutCoconeOfLeftIso f g).inr ≫ m = s.inr → m = s.inr

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 f
⊢ HasPushout f g

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

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

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 f
refine : pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = 𝟙 (pushout f g)
⊢ IsIso (Y := pushout f g) (pushout.inr f g)

Tactic:
refine ⟨⟨pushout.desc (inv f ≫ g) (𝟙 _) (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 f
h₀ :
  CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g) =
    pushout.inl f g ≫ 𝟙 (pushout f g)
h₁ :
  CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g) =
    pushout.inr f g ≫ 𝟙 (pushout f g)
⊢ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr 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 f
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g) =
    pushout.inl 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 f
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g) =
    pushout.inr 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 f
rw : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = g
rw₁ : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inr f g)) = g
rw₂ : g ≫ 𝟙 Z = g
rw₃ rw₄ : g = g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = inv f ≫ g

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.Iso
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ f ≫ 𝟙 Y = g ≫ inv g ≫ 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).pt = Y

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).inl = 𝟙 Y

Tactic:
rfl

Premises used: rfl