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.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
hf :
  P (X := pullback (Over.mk g).hom (Over.mk f).hom) (Y := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left)
    (Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))
⊢ P (X := pullback f g) (Y := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left)
    (Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
      Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.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.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
hg :
  P (X := pullback (Over.mk f).hom (Over.mk g').hom) (Y := pullback f' g')
    (Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      ((Over.pullback g').obj (Over.mk f)).left ⟶ ((Over.pullback g').obj (Over.mk f')).left)
⊢ P (X := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left) (Y := pullback f' g')
    (Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left ⟶ ((Over.pullback g').obj (Over.mk f')).left)

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.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
⊢ P (X := pullback (Over.mk g).hom (Over.mk f).hom) (Y := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left)
    (Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))

Tactic:
overPullbackMap _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂

Premises used: CategoryTheory.Over.homMk, CategoryTheory.MorphismProperty.overPullbackMap, CategoryTheory.Limits.limit, Eq.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
⊢ P (X := pullback (Over.mk f).hom (Over.mk g').hom) (Y := pullback f' g')
    (Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)) :
      ((Over.pullback g').obj (Over.mk f)).left ⟶ ((Over.pullback g').obj (Over.mk f')).left)

Tactic:
overPullbackMap _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁

Premises used: CategoryTheory.Over.homMk, CategoryTheory.MorphismProperty.overPullbackMap, CategoryTheory.Limits.limit, Eq.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.IsStableUnderComposition
S X X' Y Y' : C
f : X ⟶ S
inst_3 : HasPullbacksAlong f
g : Y ⟶ S
f' : X' ⟶ S
g' : Y' ⟶ S
i₁ : X ⟶ X'
inst_4 : HasPullbacksAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f = i₁ ≫ f'
e₂ : g = i₂ ≫ g'
this_1 : HasPullbacksAlong (Over.mk f).hom
this :
  Eq (α := pullback f g ⟶ pullback f' g') (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
    ((Iso.hom (pullbackSymmetry (Over.mk f).hom (Over.mk g).hom) ≫
        Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯))) ≫
      Iso.hom (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom) ≫
        Over.Hom.left ((Over.pullback g').map (Over.homMk i₁ ⋯)))
⊢ P (X := pullback (Over.mk g).hom (Over.mk f).hom) (Y := ((Over.pullback (Over.mk f).hom).obj (Over.mk g')).left)
    (Over.Hom.left ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)))

Tactic:
exacts [overPullbackMap _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂,
    overPullbackMap _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁]

Premises used: CategoryTheory.Over.homMk, CategoryTheory.MorphismProperty.overPullbackMap, Eq.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
⊢ f = CategoryStruct.comp (Y := pullback (f ≫ g) g) (Iso.inv (asIso (pullback.fst (f ≫ g) g))) (pullback.snd (f ≫ g) g)

Tactic:
simp [← cancel_mono g, pullback.condition]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
have :
  ∀
    (this :
      f =
        CategoryStruct.comp (Y := pullback (f ≫ g) g) (Iso.inv (asIso (pullback.fst (f ≫ g) g)))
          (pullback.snd (f ≫ g) g)),
    P f
⊢ P f

Tactic:
have : f = (asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g := by
      simp [← cancel_mono g, pullback.condition]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
this :
  f = CategoryStruct.comp (Y := pullback (f ≫ g) g) (Iso.inv (asIso (pullback.fst (f ≫ g) g))) (pullback.snd (f ≫ g) g)
rw : P (X := pullback (f ≫ g) g) (pullback.snd (f ≫ g) g)
⊢ P f

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

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.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
this :
  f = CategoryStruct.comp (Y := pullback (f ≫ g) g) (Iso.inv (asIso (pullback.fst (f ≫ g) g))) (pullback.snd (f ≫ g) g)
⊢ P (X := pullback (f ≫ g) g) (pullback.snd (f ≫ g) g)

Tactic:
P.pullback_snd _ _ hcomp

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
this :
  f = CategoryStruct.comp (Y := pullback (f ≫ g) g) (Iso.inv (asIso (pullback.fst (f ≫ g) g))) (pullback.snd (f ≫ g) g)
⊢ P (X := pullback (f ≫ g) g) (pullback.snd (f ≫ g) g)

Tactic:
exact P.pullback_snd _ _ hcomp

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
mp : P.IsStableUnderCobaseChange → P.pushouts ≤ P
mpr : P.pushouts ≤ P → P.IsStableUnderCobaseChange
⊢ P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderCobaseChange
mp : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P.pushouts f → P f
⊢ P.pushouts ≤ P

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderCobaseChange
X : C
mp : ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.pushouts f → P f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.pushouts f → P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderCobaseChange
X Y : C
mp : ∀ (f : X ⟶ Y), P.pushouts f → P f
⊢ ∀ (f : X ⟶ Y), P.pushouts f → P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderCobaseChange
X Y : C
f : X ⟶ Y
mp : ∀ (w w_1 : C) (w_2 : w ⟶ w_1) (w_3 : w ⟶ X) (w_4 : w_1 ⟶ Y) (h₁ : P w_2) (h₂ : IsPushout w_3 w_2 f w_4), P f
⊢ P.pushouts f → P f

Tactic:
⟨_, _, _, _, _, h₁, h₂⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderCobaseChange
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
w_3 : w ⟶ X
w_4 : w_1 ⟶ Y
h₁ : P w_2
h₂ : IsPushout w_3 w_2 f w_4
⊢ P f

Tactic:
of_isPushout h₂ h₁

Premises used: CategoryTheory.MorphismProperty.of_isPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.IsStableUnderCobaseChange
X Y : C
f : X ⟶ Y
w w_1 : C
w_2 : w ⟶ w_1
w_3 : w ⟶ X
w_4 : w_1 ⟶ Y
h₁ : P w_2
h₂ : IsPushout w_3 w_2 f w_4
⊢ P f

Tactic:
exact of_isPushout h₂ h₁

Premises used: CategoryTheory.MorphismProperty.of_isPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
mpr :
  ∀ {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ P.IsStableUnderCobaseChange

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A : C
mpr : ∀ {A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ ∀ {A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' : C
mpr : ∀ {B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ ∀ {B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' B : C
mpr : ∀ {B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ ∀ {B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' B B' : C
mpr : ∀ {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ ∀ {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' B B' : C
f : A ⟶ A'
mpr : ∀ {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ ∀ {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
mpr : ∀ {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ ∀ {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
mpr : ∀ {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'
⊢ ∀ {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f), P f'

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
h₁ : IsPushout g f f' g'
h₂ : P f
⊢ P f'

Tactic:
h _ ⟨_, _, _, _, _, h₂, h₁⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h : P.pushouts ≤ P
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
h₁ : IsPushout g f f' g'
h₂ : P f
⊢ P f'

Tactic:
exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 rwa rwa₁ rwa₂ rwa₃ : P.IsStableUnderCobaseChange
⊢ P.pushouts ≤ P

Tactic:
rwa [← isStableUnderCobaseChange_iff_pushouts_le]

Premises used: CategoryTheory.MorphismProperty.isStableUnderCobaseChange_iff_pushouts_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderCobaseChange
mp : P.pushouts ≤ Q → P ≤ Q
mpr : P ≤ Q → P.pushouts ≤ Q
⊢ P.pushouts ≤ Q ↔ P ≤ Q

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q → P ≤ Q

Tactic:
le_trans P.le_pushouts

Premises used: CategoryTheory.MorphismProperty.le_pushouts, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q → P ≤ Q

Tactic:
exact le_trans P.le_pushouts

Premises used: CategoryTheory.MorphismProperty.le_pushouts, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderCobaseChange
h : P ≤ Q
⊢ P.pushouts ≤ Q

Tactic:
le_trans (pushouts_monotone h) pushouts_le

Premises used: CategoryTheory.MorphismProperty.pushouts_le, CategoryTheory.MorphismProperty.pushouts_monotone, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderCobaseChange
h : P ≤ Q
⊢ P.pushouts ≤ Q

Tactic:
exact le_trans (pushouts_monotone h) pushouts_le

Premises used: CategoryTheory.MorphismProperty.pushouts_le, CategoryTheory.MorphismProperty.pushouts_monotone, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst_2 : HasPushout f g], P f → P (Y := pushout f g) (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
haveI : ∀ (this : HasPushout f g), P f'
⊢ P f'

Tactic:
haveI : HasPushout f g := sq.flip.hasPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst_2 : HasPushout f g], P f → P (Y := pushout f g) (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
rw : P (Y := pushout f g) (pushout.inr f g)
⊢ P f'

Tactic:
rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]

Premises used: CategoryTheory.IsPushout.flip, CategoryTheory.IsPushout.inr_isoPushout_hom, CategoryTheory.Iso.hom, 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.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst_2 : HasPushout f g], P f → P (Y := pushout f g) (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P (Y := pushout f g) (pushout.inr f g)

Tactic:
hP₂ _ _ _ f g hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst_2 : HasPushout f g], P f → P (Y := pushout f g) (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P (Y := pushout f g) (pushout.inr f g)

Tactic:
exact hP₂ _ _ _ f g hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    P f → ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr
⊢ P.IsStableUnderCobaseChange

Tactic:
.mk' fun X Y S f g _ hg ↦ ?_

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk'
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    P f → ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr
refine : ∀ (X Y S : C) (f : X ⟶ S) (g : X ⟶ Y) (x : HasPushout f g) (hg : P f), P (Y := pushout f g) (pushout.inr f g)
⊢ P.IsStableUnderCobaseChange

Tactic:
refine .mk' fun X Y S f g _ hg ↦ ?_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    P f → ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr
X Y S : C
f : X ⟶ S
g : X ⟶ Y
h : HasPushout f g
hg : P f
obtain :
  ∀ (T : C) (inl : S ⟶ T) (inr : Y ⟶ T) (h_1 : IsPushout f g inl inr) (hinl : P inr),
    P (Y := pushout f g) (pushout.inr f g)
⊢ P (Y := pushout f g) (pushout.inr f g)

Tactic:
obtain ⟨T, inl, inr, h, hinl⟩ := H f g hg
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
H :
  ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    P f → ∃ (T : C) (inl : X ⟶ T) (inr : Y ⟶ T), IsPushout f g inl inr ∧ P inr
X Y S : C
f : X ⟶ S
g : X ⟶ Y
h_1 : HasPushout f g
hg : P f
T : C
inl : S ⟶ T
inr : Y ⟶ T
h : IsPushout f g inl inr
hinl : P inr
rwa : P (Y := pushout f g) (inr ≫ Iso.hom h.isoPushout)
rwa₁ rwa₂ rwa₃ rwa₄ : P inr
⊢ P (Y := pushout f g) (pushout.inr f g)

Tactic:
rwa [← h.inr_isoPushout_hom, P.cancel_right_of_respectsIso]

Premises used: CategoryTheory.IsPushout.inr_isoPushout_hom, 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
⊢ P.RespectsIso

Tactic:
RespectsIso.of_respects_arrow_iso _ fun _ _ e ↦
    of_isPushout (IsPushout.of_horiz_isIso (CommSq.mk e.hom.w))

Premises used: CategoryTheory.IsPushout.of_horiz_isIso, CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_isPushout, CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso, CategoryTheory.CommSq.mk, CategoryTheory.Arrow.Hom.w, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A B A' : C
f : A ⟶ A'
g : A ⟶ B
inst_1 : HasPushout f g
inst_2 : P.IsStableUnderCobaseChangeAlong f
H : P g
⊢ P (Y := pushout f g) (pushout.inl f g)

Tactic:
IsStableUnderCobaseChangeAlong.of_isPushout (IsPushout.of_hasPushout f g) H

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.of_isPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
A B A' : C
f : A ⟶ A'
g : A ⟶ B
inst_1 : HasPushout f g
inst_2 : P.IsStableUnderCobaseChangeAlong g
H : P f
⊢ P (Y := pushout f g) (pushout.inr f g)

Tactic:
IsStableUnderCobaseChangeAlong.of_isPushout (IsPushout.of_hasPushout f g).flip H

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.of_isPushout, 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 ⟶ X
v₂₂ : S ⟶ Y
g : Y ⟶ X
hv₁₂ : v₁₂ = v₂₂ ≫ g
inst_2 : HasPushout v₁₂ f
inst_3 : HasPushout v₂₂ f
H : P g
⊢ Eq (α := S ⟶ pushout v₁₂ f) (v₂₂ ≫ g ≫ pushout.inl v₁₂ f) (f ≫ pushout.inr v₁₂ f)

Tactic:
simp [pushout.condition, ← reassoc_of% hv₁₂]

Premises used: CategoryTheory.Limits.pushout.condition
-- 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 ⟶ X
v₂₂ : S ⟶ Y
g : Y ⟶ X
hv₁₂ : v₁₂ = v₂₂ ≫ g
inst_2 : HasPushout v₁₂ f
inst_3 : HasPushout v₂₂ f
H : P g
subst :
  ∀ [inst_4 : 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) ⋯)
⊢ P (X := pushout v₂₂ f) (Y := pushout v₁₂ f) (pushout.desc (g ≫ pushout.inl v₁₂ f) (pushout.inr v₁₂ f) ⋯)

Tactic:
subst hv₁₂