awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
hprecomp : P (Y := pullback.diagonalObj (e.hom ≫ f)) (pullback.diagonal (e.hom ≫ f))
hprecomp₁ :
  P (Y := pullback.diagonalObj (e.hom ≫ f))
    (CategoryStruct.comp (Y := pullback.diagonalObj e.hom) (pullback.diagonal e.hom)
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (e.hom ≫ f) (e.hom ≫ f)) (Z := pullback.diagonalObj f) (pullback.diagonal f)
          (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIdIso e.hom e.hom f))
        (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))))
hprecomp₂ :
  P (X := pullback.diagonalObj e.hom) (Y := pullback.diagonalObj (e.hom ≫ f))
    (CategoryStruct.comp (Y :=
      pullback (Y := pullback (e.hom ≫ f) (e.hom ≫ f)) (Z := pullback.diagonalObj f) (pullback.diagonal f)
        (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))
      (Iso.inv (pullbackDiagonalMapIdIso e.hom e.hom f))
      (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯)))
hprecomp₃ :
  P (X :=
    pullback (Y := pullback (e.hom ≫ f) (e.hom ≫ f)) (Z := pullback.diagonalObj f) (pullback.diagonal f)
      (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))
    (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))
hprecomp₄ :
  P (X :=
    pullback (Y := pullback (e.hom ≫ f) (e.hom ≫ f)) (Z := pullback.diagonalObj f) (pullback.diagonal f)
      (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))
    (Y := pullback f f)
    (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯) ≫
      pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯)
hprecomp₅ :
  P (X :=
    pullback (Y := pullback (e.hom ≫ f) (e.hom ≫ f)) (Z := pullback.diagonalObj f) (pullback.diagonal f)
      (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))
    (Y := pullback f f)
    (pullback.fst (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯) ≫
      pullback.diagonal f)
hprecomp₆ hprecomp₇ hprecomp₈ hprecomp₉ : P (Y := pullback f f) (pullback.diagonal f)
⊢ P.diagonal (e.hom ≫ f)

Tactic:
rwa [diagonal_iff, pullback.diagonal_comp, P.cancel_left_of_respectsIso,
      P.cancel_left_of_respectsIso, ← P.cancel_right_of_respectsIso _
        (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)),
      ← pullback.condition, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, CategoryTheory.Limits.pullback.diagonal_comp, CategoryTheory.MorphismProperty.diagonal_iff, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Limits.pullback.condition, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
hpostcomp : P (Y := pullback.diagonalObj (f ≫ e.hom)) (pullback.diagonal (f ≫ e.hom))
⊢ P.diagonal (f ≫ e.hom)

Tactic:
delta diagonal
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
hpostcomp :
  P (Y := pullback.diagonalObj (f ≫ e.hom))
    (CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f)
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (f ≫ e.hom) (f ≫ e.hom)) (Z := pullback.diagonalObj e.hom) (pullback.diagonal e.hom)
          (pullback.map (f ≫ e.hom) (f ≫ e.hom) e.hom e.hom f f (𝟙 Z) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIdIso f f e.hom))
        (pullback.snd (pullback.diagonal e.hom) (pullback.map (f ≫ e.hom) (f ≫ e.hom) e.hom e.hom f f (𝟙 Z) ⋯ ⋯))))
hpostcomp₁ hpostcomp₂ hpostcomp₃ hpostcomp₄ : P (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ P (Y := pullback.diagonalObj (f ≫ e.hom)) (pullback.diagonal (f ≫ e.hom))

Tactic:
rwa [pullback.diagonal_comp, P.cancel_right_of_respectsIso]

Premises used: CategoryTheory.Limits.pullback.diagonal_comp, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderComposition
inst_3 : P.RespectsIso
inst_4 : P.IsStableUnderBaseChange
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
h₁ : P.diagonal x
h₂ : P.diagonal x_1
rw :
  P (Y := pullback.diagonalObj (x ≫ x_1))
    (CategoryStruct.comp (Y := pullback.diagonalObj x) (pullback.diagonal x)
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (x ≫ x_1) (x ≫ x_1)) (Z := pullback.diagonalObj x_1) (pullback.diagonal x_1)
          (pullback.map (x ≫ x_1) (x ≫ x_1) x_1 x_1 x x (𝟙 Z) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIdIso x x x_1))
        (pullback.snd (pullback.diagonal x_1) (pullback.map (x ≫ x_1) (x ≫ x_1) x_1 x_1 x x (𝟙 Z) ⋯ ⋯))))
⊢ P.diagonal (x ≫ x_1)

Tactic:
rw [diagonal_iff, pullback.diagonal_comp]

Premises used: CategoryTheory.Limits.pullback.diagonal_comp, CategoryTheory.MorphismProperty.diagonal_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderComposition
inst_3 : P.RespectsIso
inst_4 : P.IsStableUnderBaseChange
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
h₁ : P.diagonal x
h₂ : P.diagonal x_1
⊢ P (X := pullback.diagonalObj x) (Y := pullback.diagonalObj (x ≫ x_1))
    (CategoryStruct.comp (Y :=
      pullback (Y := pullback (x ≫ x_1) (x ≫ x_1)) (Z := pullback.diagonalObj x_1) (pullback.diagonal x_1)
        (pullback.map (x ≫ x_1) (x ≫ x_1) x_1 x_1 x x (𝟙 Z) ⋯ ⋯))
      (Iso.inv (pullbackDiagonalMapIdIso x x x_1))
      (pullback.snd (pullback.diagonal x_1) (pullback.map (x ≫ x_1) (x ≫ x_1) x_1 x_1 x x (𝟙 Z) ⋯ ⋯)))

Tactic:
simpa only [cancel_left_of_respectsIso] using P.pullback_snd _ _ h₂

Premises used: CategoryTheory.MorphismProperty.pullback_snd, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderComposition
inst_3 : P.RespectsIso
inst_4 : P.IsStableUnderBaseChange
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
h₁ : P.diagonal x
h₂ : P.diagonal x_1
⊢ P (Y := pullback.diagonalObj (x ≫ x_1))
    (CategoryStruct.comp (Y := pullback.diagonalObj x) (pullback.diagonal x)
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (x ≫ x_1) (x ≫ x_1)) (Z := pullback.diagonalObj x_1) (pullback.diagonal x_1)
          (pullback.map (x ≫ x_1) (x ≫ x_1) x_1 x_1 x x (𝟙 Z) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIdIso x x x_1))
        (pullback.snd (pullback.diagonal x_1) (pullback.map (x ≫ x_1) (x ≫ x_1) x_1 x_1 x x (𝟙 Z) ⋯ ⋯))))

Tactic:
exact P.comp_mem _ _ h₁
      (by simpa only [cancel_left_of_respectsIso] using P.pullback_snd _ _ h₂)

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_4 : HasPullback f g
h : P.diagonal g
rw :
  P (X := pullback (Over.mk g).hom f) (Y :=
    ((Over.pullback f).obj (Over.mk (Y := pullback g g) (pullback.snd g g ≫ g))).left)
    (Over.Hom.left ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)))
⊢ P.diagonal (X := pullback f g) (pullback.fst f g)

Tactic:
rw [diagonal_iff, diagonal_pullback_fst, P.cancel_left_of_respectsIso,
        P.cancel_right_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.diagonal_iff, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso, CategoryTheory.Limits.diagonal_pullback_fst
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_4 : HasPullback f g
h : P.diagonal g
⊢ P (X := (Over.mk g).left) (Y := (Over.mk (Y := pullback g g) (pullback.snd g g ≫ g)).left)
    (Over.Hom.left (Over.homMk (pullback.diagonal g) ⋯))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_4 : HasPullback f g
h : P.diagonal g
⊢ P (X := pullback (Over.mk g).hom f) (Y :=
    ((Over.pullback f).obj (Over.mk (Y := pullback g g) (pullback.snd g g ≫ g))).left)
    (Over.Hom.left ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)))

Tactic:
exact P.overPullbackMap f _ (by simpa)

Premises used: CategoryTheory.MorphismProperty.overPullbackMap
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} C) (diagonal (isomorphisms C)) (monomorphisms C)

Tactic:
ext _ _ fun _ _ _ ↦ pullback.isIso_diagonal_iff _

Premises used: CategoryTheory.Limits.pullback.isIso_diagonal_iff, CategoryTheory.MorphismProperty.ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
⊢ P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal

Tactic:
⟨fun hP X Y f hf ↦ ?_, fun hP ↦ ⟨fun {Y X S} g f hf hcomp ↦ ?_⟩⟩

Premises used: CategoryTheory.MorphismProperty.HasOfPostcompProperty.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
refine_1 : ∀ (hP : P.HasOfPostcompProperty Q) (X Y : C) (f : X ⟶ Y) (hf : Q f), P.diagonal f
refine_2 : ∀ (hP : Q ≤ P.diagonal) {Y X S : C} (g : Y ⟶ X) (f : X ⟶ S) (hf : Q f) (hcomp : P (g ≫ f)), P g
⊢ P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal

Tactic:
refine ⟨fun hP X Y f hf ↦ ?_, fun hP ↦ ⟨fun {Y X S} g f hf hcomp ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : P.HasOfPostcompProperty Q
X Y : C
f : X ⟶ Y
hf : Q f
⊢ P (CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.fst f f))

Tactic:
simpa using P.id_mem X

Premises used: CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : P.HasOfPostcompProperty Q
X Y : C
f : X ⟶ Y
hf : Q f
⊢ P.diagonal f

Tactic:
exact hP.of_postcomp _ _ (Q.pullback_fst _ _ hf) (by simpa using P.id_mem X)

Premises used: CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_postcomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
⊢ 𝟙 Y ≫ g ≫ f = g ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
⊢ g = gr ≫ pullback.snd (g ≫ f) f

Tactic:
simp [gr]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
refine_2 : ∀ (this : g = gr ≫ pullback.snd (g ≫ f) f), P g
⊢ P g

Tactic:
have : g = gr ≫ pullback.snd _ _ := by simp [gr]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
refine_2 : P (gr ≫ pullback.snd (g ≫ f) f)
⊢ P g

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
refine_2 : P gr
refine_2₁ : P (X := pullback (g ≫ f) f) (pullback.snd (g ≫ f) f)
⊢ P (gr ≫ pullback.snd (g ≫ f) f)

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
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P gr

Tactic:
P.of_isPullback (pullback_lift_diagonal_isPullback g f) (hP _ hf)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.pullback_lift_diagonal_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P gr

Tactic:
exact P.of_isPullback (pullback_lift_diagonal_isPullback g f) (hP _ hf)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.pullback_lift_diagonal_isPullback
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (X := pullback (g ≫ f) f) (pullback.snd (g ≫ f) f)

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
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.IsMultiplicative
Q : MorphismProperty.{v, u} C
inst_4 : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (X := pullback (g ≫ f) f) (pullback.snd (g ≫ f) f)

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
hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)
hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)
⊢ P.universally.RespectsIso

Tactic:
apply RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
rw : i₁ = (i₁ ≫ e.hom) ≫ e.inv
rw₁ : i₁ = i₁ ≫ e.hom ≫ e.inv
rw₂ : i₁ = i₁ ≫ 𝟙 X
rw₃ rw₄ : i₁ = i₁
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv

Tactic:
rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
hprecomp : ∀ (this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv), P f'
⊢ P f'

Tactic:
have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv :=
      IsPullback.of_horiz_isIso
        ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ IsPullback f' (i₁ ≫ e.hom) i₂ f

Tactic:
simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.IsPullback.paste_horiz, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
this : IsPullback (𝟙 X') (i₁ ≫ e.hom) i₁ e.inv
⊢ P f'

Tactic:
exact hf _ _ _
      (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
hpostcomp : ∀ (this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv), P f'
⊢ P f'

Tactic:
have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv :=
      IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ IsPullback f' i₁ (i₂ ≫ e.inv) f

Tactic:
simpa only [Category.assoc, Iso.hom_inv_id,
      Category.comp_id, Category.comp_id] using H.paste_horiz this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ e.hom)
this : IsPullback (𝟙 Z') i₂ (i₂ ≫ e.inv) e.inv
⊢ P f'

Tactic:
exact hf _ _ _ (by simpa only [Category.assoc, Iso.hom_inv_id,
      Category.comp_id, Category.comp_id] using H.paste_horiz this)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
have : ∀ (this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'), P f'
⊢ P f'

Tactic:
have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'
rw :
  ∀
    (H_1 :
      IsPullback (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g)) i₁ i₂
        (f ≫ g))
    (this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'),
    P (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g))
⊢ P f'

Tactic:
rw [← this] at H ⊢
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H_1 : IsPullback f' i₁ i₂ (f ≫ g)
H :
  IsPullback (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g)) i₁ i₂ (f ≫ g)
this : CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g) = f'
apply : P (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯)
⊢ P (CategoryStruct.comp (Y := pullback i₂ g) (pullback.lift f' (i₁ ≫ f) ⋯) (pullback.fst i₂ g))

Tactic:
apply P.comp_mem _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _)

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.IsPullback.of_hasPullback