awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
x_1 : Arrow.{v₂, u₂} C₂
w :
  Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right) =
    Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right)
w₁ :
  Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right) =
    Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right)
⊢ Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
            whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
        x_1) =
    Arrow.Hom.right
      ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
            (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
        x_1)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
x_1 : Arrow.{v₂, u₂} C₂
⊢ Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right) =
    Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1) ≫
      pullback.fst ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right)

Tactic:
simp [← homEquiv_naturality_one, ← homEquiv_naturality_three]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
inst_3 : HasPullbacks.{v₂, u₂} C₂
inst_4 : HasPushouts.{v₃, u₃} C₃
X₁ Y₁ : Arrow.{v₁, u₁} C₁
x : X₁ ⟶ Y₁
x_1 : Arrow.{v₂, u₂} C₂
⊢ Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ X₁) ≫
              whiskerRight (F.leibnizPushout.map x) (G.leibnizPullback.obj (op X₁))).app
          x_1) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right) =
    Arrow.Hom.right
        ((Adjunction.unit (LeibnizAdjunction.adj F G adj₂ Y₁) ≫
              (F.leibnizPushout.obj Y₁).whiskerLeft (G.leibnizPullback.map x.op)).app
          x_1) ≫
      pullback.snd ((G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj Y₁).obj x_1).hom)
        ((G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj Y₁).obj x_1).right)

Tactic:
simp [← homEquiv_naturality_one, ← homEquiv_naturality_three]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
⊢ sq.IsPullback ↔ Nonempty (IsLimit sq.pullbackCone)

Tactic:
⟨fun h ↦ ⟨h.isLimit⟩, fun h ↦ { w := sq.fac, isLimit' := h }⟩

Premises used: CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro, CategoryTheory.Square.fac, Iff.intro, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
⊢ sq.IsPushout ↔ Nonempty (IsColimit sq.pushoutCocone)

Tactic:
⟨fun h ↦ ⟨h.isColimit⟩, fun h ↦ { w := sq.fac, isColimit' := h }⟩

Premises used: CategoryTheory.IsPushout.mk, CategoryTheory.CommSq.mk, Nonempty.intro, CategoryTheory.Square.fac, Iff.intro, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : IsLimit sq.pullbackCone
⊢ sq.IsPullback

Tactic:
sq.isPullback_iff.2 ⟨h⟩

Premises used: Iff.mpr, CategoryTheory.Square.isPullback_iff, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : IsColimit sq.pushoutCocone
⊢ sq.IsPushout

Tactic:
sq.isPushout_iff.2 ⟨h⟩

Premises used: Iff.mpr, Nonempty.intro, CategoryTheory.Square.isPushout_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₂.IsPullback

Tactic:
CategoryTheory.IsPullback.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_

Premises used: CategoryTheory.Square.evaluation₃, CategoryTheory.IsPullback.of_iso, CategoryTheory.Square.evaluation₁, CategoryTheory.Square.evaluation₂, CategoryTheory.Square.IsPullback, CategoryTheory.Square.evaluation₄, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
refine_2 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
refine_3 :
  Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)
refine_4 :
  Eq (α := sq₁.X₃ ⟶ sq₂.X₄) (sq₁.f₃₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₃ e) ≫ sq₂.f₃₄)
⊢ sq₂.IsPullback

Tactic:
refine CategoryTheory.IsPullback.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_

Premises used: CategoryTheory.Square.evaluation₃, CategoryTheory.IsPullback.of_iso, CategoryTheory.Square.evaluation₁, CategoryTheory.Square.evaluation₂, CategoryTheory.Square.evaluation₄, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₃ ⟶ sq₂.X₄) (sq₁.f₃₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₃ e) ≫ sq₂.f₃₄)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
e : sq₁ ≅ sq₂
⊢ sq₁.IsPullback ↔ sq₂.IsPullback

Tactic:
⟨fun h ↦ h.of_iso e, fun h ↦ h.of_iso e.symm⟩

Premises used: CategoryTheory.Square.IsPullback.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₂.IsPushout

Tactic:
CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_

Premises used: CategoryTheory.Square.evaluation₃, CategoryTheory.Square.IsPushout, CategoryTheory.Square.evaluation₁, CategoryTheory.IsPushout.of_iso, CategoryTheory.Square.evaluation₂, CategoryTheory.Square.evaluation₄, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
refine_1 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)
refine_2 :
  Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)
refine_3 :
  Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)
refine_4 :
  Eq (α := sq₁.X₃ ⟶ sq₂.X₄) (sq₁.f₃₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₃ e) ≫ sq₂.f₃₄)
⊢ sq₂.IsPushout

Tactic:
refine CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_

Premises used: CategoryTheory.Square.evaluation₃, CategoryTheory.Square.evaluation₁, CategoryTheory.IsPushout.of_iso, CategoryTheory.Square.evaluation₂, CategoryTheory.Square.evaluation₄, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₁ ⟶ sq₂.X₂) (sq₁.f₁₂ ≫ Iso.hom (Functor.mapIso evaluation₂ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₁ ⟶ sq₂.X₃) (sq₁.f₁₃ ≫ Iso.hom (Functor.mapIso evaluation₃ e))
    (Iso.hom (Functor.mapIso evaluation₁ e) ≫ sq₂.f₁₃)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₂ ⟶ sq₂.X₄) (sq₁.f₂₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₂ e) ≫ sq₂.f₂₄)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ Eq (α := sq₁.X₃ ⟶ sq₂.X₄) (sq₁.f₃₄ ≫ Iso.hom (Functor.mapIso evaluation₄ e))
    (Iso.hom (Functor.mapIso evaluation₃ e) ≫ sq₂.f₃₄)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
e : sq₁ ≅ sq₂
⊢ sq₁.IsPushout ↔ sq₂.IsPushout

Tactic:
⟨fun h ↦ h.of_iso e, fun h ↦ h.of_iso e.symm⟩

Premises used: CategoryTheory.Square.IsPushout.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
⊢ sq.op.IsPullback

Tactic:
CategoryTheory.IsPushout.op h.flip

Premises used: Quiver.Hom.op, CategoryTheory.IsPushout.flip, CategoryTheory.Square.IsPullback, CategoryTheory.IsPushout.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} Cᵒᵖ
h : sq.IsPushout
⊢ sq.unop.IsPullback

Tactic:
CategoryTheory.IsPushout.unop h.flip

Premises used: Quiver.Hom.unop, CategoryTheory.IsPushout.unop, CategoryTheory.IsPushout.flip, CategoryTheory.Square.IsPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
⊢ sq.op.IsPushout

Tactic:
CategoryTheory.IsPullback.op h.flip

Premises used: CategoryTheory.IsPullback.op, Quiver.Hom.op, CategoryTheory.Square.IsPushout, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} Cᵒᵖ
h : sq.IsPullback
⊢ sq.unop.IsPushout

Tactic:
CategoryTheory.IsPullback.unop h.flip

Premises used: Quiver.Hom.unop, CategoryTheory.Square.IsPushout, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
⊢ sq.flip.IsPullback

Tactic:
CategoryTheory.IsPullback.flip h

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.Square.IsPullback
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
inst_1 : Mono sq.f₂₄
⊢ MorphismProperty.monomorphisms C sq.f₂₄

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
inst_1 dsimp : Mono sq.f₃₄
⊢ Mono sq.flip.f₂₄

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
inst_1 : Mono sq.f₃₄
⊢ Mono sq.f₃₄

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
inst_1 : Mono sq.f₃₄
⊢ Mono sq.flip.f₂₄

Tactic:
have : Mono sq.flip.f₂₄ := by dsimp; infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
inst_1 : Mono sq.f₃₄
this : Mono sq.flip.f₂₄
⊢ Mono sq.f₁₂

Tactic:
h.flip.mono_f₁₃

Premises used: CategoryTheory.Square.IsPullback.flip, CategoryTheory.Square.IsPullback.mono_f₁₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPullback
inst_1 : Mono sq.f₃₄
this : Mono sq.flip.f₂₄
⊢ Mono sq.f₁₂

Tactic:
exact h.flip.mono_f₁₃

Premises used: CategoryTheory.Square.IsPullback.flip, CategoryTheory.Square.IsPullback.mono_f₁₃
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
⊢ sq.flip.IsPushout

Tactic:
CategoryTheory.IsPushout.flip h

Premises used: CategoryTheory.Square.IsPushout, CategoryTheory.IsPushout.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
inst_1 : Epi sq.f₁₃
⊢ MorphismProperty.epimorphisms C sq.f₁₃

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
inst_1 dsimp : Epi sq.f₁₂
⊢ Epi sq.flip.f₁₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
inst_1 : Epi sq.f₁₂
⊢ Epi sq.f₁₂

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
inst_1 : Epi sq.f₁₂
⊢ Epi sq.flip.f₁₃

Tactic:
have : Epi sq.flip.f₁₃ := by dsimp; infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
inst_1 : Epi sq.f₁₂
this : Epi sq.flip.f₁₃
⊢ Epi sq.f₃₄

Tactic:
h.flip.epi_f₂₄

Premises used: CategoryTheory.Square.IsPushout.epi_f₂₄, CategoryTheory.Square.IsPushout.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
h : sq.IsPushout
inst_1 : Epi sq.f₁₂
this : Epi sq.flip.f₁₃
⊢ Epi sq.f₃₄

Tactic:
exact h.flip.epi_f₂₄

Premises used: CategoryTheory.Square.IsPushout.epi_f₂₄, CategoryTheory.Square.IsPushout.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
⊢ ∃ (s : B ⟶ A), s ≫ f = 𝟙 B ∧ s ≫ g = 𝟙 B

Tactic:
IsReflexivePair.common_section'

Premises used: CategoryTheory.IsReflexivePair.common_section'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsCoreflexivePair f g
⊢ ∃ (s : B ⟶ A), f ≫ s = 𝟙 A ∧ g ≫ s = 𝟙 A

Tactic:
IsCoreflexivePair.common_retraction'

Premises used: CategoryTheory.IsCoreflexivePair.common_retraction'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
sf : s ≫ f = 𝟙 B
sg : s ≫ g = 𝟙 B
⊢ IsReflexivePair f g

Tactic:
⟨⟨s, sf, sg⟩⟩

Premises used: And.intro, CategoryTheory.IsReflexivePair.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
s : B ⟶ A
fs : f ≫ s = 𝟙 A
gs : g ≫ s = 𝟙 A
⊢ IsCoreflexivePair f g

Tactic:
⟨⟨s, fs, gs⟩⟩

Premises used: CategoryTheory.IsCoreflexivePair.mk, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
⊢ commonSection f g ≫ f = 𝟙 B

Tactic:
(IsReflexivePair.common_section f g).choose_spec.1

Premises used: Exists.choose_spec, CategoryTheory.commonSection, CategoryTheory.IsReflexivePair.common_section, And.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
⊢ commonSection f g ≫ g = 𝟙 B

Tactic:
(IsReflexivePair.common_section f g).choose_spec.2

Premises used: Exists.choose_spec, CategoryTheory.commonSection, CategoryTheory.IsReflexivePair.common_section, And.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsCoreflexivePair f g
⊢ f ≫ commonRetraction f g = 𝟙 A

Tactic:
(IsCoreflexivePair.common_retraction f g).choose_spec.1

Premises used: Exists.choose_spec, CategoryTheory.IsCoreflexivePair.common_retraction, CategoryTheory.commonRetraction, And.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsCoreflexivePair f g
⊢ g ≫ commonRetraction f g = 𝟙 A

Tactic:
(IsCoreflexivePair.common_retraction f g).choose_spec.2

Premises used: Exists.choose_spec, CategoryTheory.IsCoreflexivePair.common_retraction, CategoryTheory.commonRetraction, And.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B R : C
f g : R ⟶ A
q : A ⟶ B
h : IsKernelPair q f g
⊢ IsReflexivePair f g

Tactic:
IsReflexivePair.mk' _ (h.lift' _ _ rfl).2.1 (h.lift' _ _ _).2.2

Premises used: CategoryTheory.IsReflexivePair.mk', And.right, And.left, CategoryTheory.IsKernelPair.lift', rfl, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsReflexivePair f g
⊢ IsReflexivePair g f

Tactic:
IsReflexivePair.mk' _ (section_comp_right f g) (section_comp_left f g)

Premises used: CategoryTheory.section_comp_right, CategoryTheory.IsReflexivePair.mk', CategoryTheory.section_comp_left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
f g : A ⟶ B
inst_1 : IsCoreflexivePair f g
⊢ IsCoreflexivePair g f

Tactic:
IsCoreflexivePair.mk' _ (right_comp_retraction f g) (left_comp_retraction f g)

Premises used: CategoryTheory.right_comp_retraction, CategoryTheory.IsCoreflexivePair.mk', CategoryTheory.left_comp_retraction
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B_1 : C
f g : A ⟶ B_1
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v, u₂, u} D C
adj : F ⊣ G
B : D
rw : F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) B)))
⊢ F.map (adj.unit.app (G.obj B)) ≫ F.map (G.map (adj.counit.app B)) =
    𝟙 (F.obj (G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) B)))

Tactic:
rw [← F.map_comp, adj.right_triangle_components]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B_1 : C
f g : A ⟶ B_1
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v, u₂, u} D C
adj : F ⊣ G
B : D
⊢ F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) B)))

Tactic:
apply F.map_id

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasReflexiveCoequalizers.{v, u} C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
this : IsReflexivePair f g := ⋯
⊢ HasCoequalizer f g

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoreflexiveEqualizers.{v, u} C
A B : C
f g : A ⟶ B
r : B ⟶ A
fr : f ≫ r = 𝟙 A
gr : g ≫ r = 𝟙 A
this : IsCoreflexivePair f g := ⋯
⊢ HasEqualizer f g

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A_1 B_1 : C
f_1 g_1 : A_1 ⟶ B_1
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v, u₂, u} D C
adj : F ⊣ G
inst_2 : HasCoequalizers.{v, u} C
A B : C
f g : A ⟶ B
h : IsReflexivePair f g
⊢ HasCoequalizer f g

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A_1 B_1 : C
f_1 g_1 : A_1 ⟶ B_1
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v, u₂, u} D C
adj : F ⊣ G
inst_2 : HasEqualizers.{v, u} C
A B : C
f g : A ⟶ B
h : IsCoreflexivePair f g
⊢ HasEqualizer f g

Tactic:
infer_instance