awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst_2 : HasPushout v₂₂ f
H : P g
inst_3 : HasPushout (v₂₂ ≫ g) f
⊢ P (X := pushout v₂₂ f) (Y := pushout (v₂₂ ≫ g) f)
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)

Tactic:
IsStableUnderCobaseChangeAlong.of_isPushout (f' := pushout.inl (v₂₂ ≫ g) f)
    (f := pushout.inl v₂₂ f) ?_ H

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.of_isPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst_2 : HasPushout v₂₂ f
H : P g
inst_3 : HasPushout (v₂₂ ≫ g) f
refine :
  IsPushout (X := pushout v₂₂ f) (P := pushout (v₂₂ ≫ g) f) (pushout.inl v₂₂ f) g
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯) (pushout.inl (v₂₂ ≫ g) f)
⊢ P (X := pushout v₂₂ f) (Y := pushout (v₂₂ ≫ g) f)
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)

Tactic:
refine IsStableUnderCobaseChangeAlong.of_isPushout (f' := pushout.inl (v₂₂ ≫ g) f)
    (f := pushout.inl v₂₂ f) ?_ H

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.of_isPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst_2 : HasPushout v₂₂ f
H : P g
inst_3 : HasPushout (v₂₂ ≫ g) f
⊢ Eq (α := Y ⟶ pushout (v₂₂ ≫ g) f)
    (CategoryStruct.comp (Y := pushout v₂₂ f) (pushout.inl v₂₂ f)
      (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯))
    (g ≫ pushout.inl (v₂₂ ≫ g) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst_2 : HasPushout v₂₂ f
H : P g
inst_3 : HasPushout (v₂₂ ≫ g) f
refine :
  IsPushout (P := pushout (v₂₂ ≫ g) f) f (v₂₂ ≫ g)
    (CategoryStruct.comp (Y := pushout v₂₂ f) (pushout.inr v₂₂ f)
      (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯))
    (pushout.inl (v₂₂ ≫ g) f)
⊢ IsPushout (X := pushout v₂₂ f) (P := pushout (v₂₂ ≫ g) f) (pushout.inl v₂₂ f) g
    (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯) (pushout.inl (v₂₂ ≫ g) f)

Tactic:
refine IsPushout.of_top ?_ (by simp) (IsPushout.of_hasPushout v₂₂ f).flip

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.IsPushout.of_top, CategoryTheory.IsPushout.flip
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst_2 : HasPushout v₂₂ f
H : P g
inst_3 : HasPushout (v₂₂ ≫ g) f
⊢ IsPushout (P := pushout (v₂₂ ≫ g) f) f (v₂₂ ≫ g)
    (CategoryStruct.comp (Y := pushout v₂₂ f) (pushout.inr v₂₂ f)
      (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯))
    (pushout.inl (v₂₂ ≫ g) f)

Tactic:
simpa using (IsPushout.of_hasPushout (v₂₂ ≫ g) f).flip

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.IsPushout.flip, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
S S' : C
f : S' ⟶ S
inst_2 : HasPushoutsAlong f
X Y : Under.{v, u} S'
g : X ⟶ Y
H : P (Under.Hom.right g)
⊢ P (Under.Hom.right ((Under.pushout f).map g))

Tactic:
pushoutDesc_inl_inr f g.w.symm H

Premises used: CategoryTheory.MorphismProperty.pushoutDesc_inl_inr, CategoryTheory.Under.Hom.w, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.desc, Eq.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
⊢ f ≫ i₁ = 𝟙 S ≫ f'

Tactic:
simp [e₁]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
⊢ g ≫ i₂ = 𝟙 S ≫ g'

Tactic:
simp [e₂]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
have :
  ∀ (this : HasPushoutsAlong (Under.mk g').hom),
    P (X := pushout f g) (Y := pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
⊢ P (X := pushout f g) (Y := pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Tactic:
have : HasPushoutsAlong (Under.mk g').hom := by cat_disch
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ f ≫ i₁ = 𝟙 S ≫ f'

Tactic:
simp [e₁]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ g ≫ i₂ = 𝟙 S ≫ g'

Tactic:
simp [e₂]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
h₀ :
  Eq (α := X ⟶ pushout f' g')
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
      ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))))
h₃ :
  Eq (α := Y ⟶ pushout f' g')
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
      ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))))
⊢ Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ Eq (α := X ⟶ pushout f' g')
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
      ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ Eq (α := Y ⟶ pushout f' g')
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
      ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
        Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this : HasPushoutsAlong (Under.mk g').hom
⊢ Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))

Tactic:
have : pushout.map f g f' g' i₁ i₂ (𝟙 _) (by simp [e₁]) (by simp [e₂]) =
      ((pushoutSymmetry _ _).hom ≫
        ((Under.pushout f).map (Under.homMk _ e₂.symm : Under.mk g ⟶ Under.mk g')).right) ≫
        (pushoutSymmetry _ _).hom ≫
        ((Under.pushout g').map (Under.homMk _ e₁.symm : Under.mk f ⟶ Under.mk f')).right := by
    ext <;> simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
rw :
  P (X := pushout f g) (Y := pushout f' g')
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout f g) (Y := pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
hf :
  P (X := pushout f g) (Y := ((Under.pushout f).obj (Under.mk g')).right)
    (Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))
hg :
  P (X := ((Under.pushout f).obj (Under.mk g')).right) (Y := pushout f' g')
    (Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout f g) (Y := pushout f' g')
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))

Tactic:
apply P.comp_mem

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
hf :
  P (X := pushout (Under.mk g).hom f) (Y := ((Under.pushout f).obj (Under.mk g')).right)
    (Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))
⊢ P (X := pushout f g) (Y := ((Under.pushout f).obj (Under.mk g')).right)
    (Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))

Tactic:
rw [P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
hg :
  P (X := pushout f (Under.mk g').hom) (Y := pushout f' g')
    (Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)) :
      ((Under.pushout g').obj (Under.mk f)).right ⟶ ((Under.pushout g').obj (Under.mk f')).right)
⊢ P (X := ((Under.pushout f).obj (Under.mk g')).right) (Y := pushout f' g')
    (Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))

Tactic:
rw [P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout (Under.mk g).hom f) (Y := ((Under.pushout f).obj (Under.mk g')).right)
    (Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))

Tactic:
underPushoutMap _ _ h₂

Premises used: CategoryTheory.MorphismProperty.underPushoutMap, CategoryTheory.Limits.colimit
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout f (Under.mk g').hom) (Y := pushout f' g')
    (Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)) :
      ((Under.pushout g').obj (Under.mk f)).right ⟶ ((Under.pushout g').obj (Under.mk f')).right)

Tactic:
underPushoutMap _ _ h₁

Premises used: CategoryTheory.MorphismProperty.underPushoutMap, CategoryTheory.Limits.colimit
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst_3 : HasPushoutsAlong f
inst_4 : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
this_1 : HasPushoutsAlong (Under.mk g').hom
this :
  Eq (α := pushout f g ⟶ pushout f' g') (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pushoutSymmetry f (Under.mk g).hom) ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      Iso.hom (pushoutSymmetry (Under.mk g').hom f) ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
⊢ P (X := pushout (Under.mk g).hom f) (Y := ((Under.pushout f).obj (Under.mk g')).right)
    (Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯)))

Tactic:
exacts [underPushoutMap _ _ h₂, underPushoutMap _ _ h₁]

Premises used: CategoryTheory.MorphismProperty.underPushoutMap
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
rw : g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (inv (pushout.inl (f ≫ g) f))
rw₁ : Eq (α := Y ⟶ pushout (f ≫ g) f) (g ≫ pushout.inl (f ≫ g) f) (pushout.inr (f ≫ g) f)
rw₂ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) (f ≫ pushout.inr (f ≫ g) f)
rw₃ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) ((f ≫ g) ≫ pushout.inl (f ≫ g) f)
rw₄ rw₅ : Eq (α := X ⟶ pushout (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f) (f ≫ g ≫ pushout.inl (f ≫ g) f)
⊢ g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))

Tactic:
rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.condition, CategoryTheory.asIso_inv, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
have :
  ∀
    (this :
      g =
        CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))),
    P g
⊢ P g

Tactic:
have : g = pushout.inr (f ≫ g) f ≫ (asIso (pushout.inl (f ≫ g) f)).inv := by
      rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
this :
  g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
rw : P (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f)
⊢ P g

Tactic:
rw [this, cancel_right_of_respectsIso (P := P)]

Premises used: CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
this :
  g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
⊢ P (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f)

Tactic:
P.pushout_inr _ _ hcomp

Premises used: CategoryTheory.MorphismProperty.pushout_inr
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
this :
  g = CategoryStruct.comp (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f) (Iso.inv (asIso (pushout.inl (f ≫ g) f)))
⊢ P (Y := pushout (f ≫ g) f) (pushout.inr (f ≫ g) f)

Tactic:
exact P.pushout_inr _ _ hcomp

Premises used: CategoryTheory.MorphismProperty.pushout_inr
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
j : J
⊢ φ ≫ c₂.π.app j = h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } ≫ c₂.π.app j

Tactic:
simp [hφ]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
obtain :
  ∀ (hφ : ∀ (j : J), h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } ≫ c₂.π.app j = c₁.π.app j ≫ f.app j),
    limitsOfShape.{v, u, v_1, u_1} W J (X := c₁.pt)
      (h₂.lift { pt := c₁.pt, π := c₁.π ≫ f } : { pt := c₁.pt, π := c₁.π ≫ f : Cone X₂ }.pt ⟶ c₂.pt)
⊢ limitsOfShape.{v, u, v_1, u_1} W J φ

Tactic:
obtain rfl : φ = h₂.lift (Cone.mk _ (c₁.π ≫ f)) := h₂.hom_ext (fun j ↦ by simp [hφ])

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Cone.mk, CategoryTheory.Limits.IsLimit.lift, rfl