awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q ↔ P ≤ Q
have mp : coproducts.{w, v, u} P ≤ Q → P ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : IsStableUnderCoproducts.{w, v, u} Q
mp : coproducts.{w, v, u} P ≤ Q → P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q ↔ P ≤ Q
have mpr : P ≤ Q → coproducts.{w, v, u} P ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
⊢ P.diagonal.RespectsIso
have hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.diagonal f → P.diagonal (e.hom ≫ f)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.diagonal f → P.diagonal (e.hom ≫ f)
⊢ P.diagonal.RespectsIso
have hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.diagonal f → P.diagonal (f ≫ e.hom)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ P.diagonal (e.hom ≫ f)
have hprecomp : P (Y := pullback.diagonalObj (e.hom ≫ f)) (pullback.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]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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))
⊢ P.diagonal (e.hom ≫ f)
have 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) sorry sorry))
      (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) sorry sorry))))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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) ⋯ ⋯))))
⊢ P.diagonal (e.hom ≫ f)
have 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) sorry sorry))
    (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) sorry sorry)))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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) ⋯ ⋯)))
⊢ P.diagonal (e.hom ≫ f)
have 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) sorry sorry))
  (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) sorry sorry))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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) ⋯ ⋯))
⊢ P.diagonal (e.hom ≫ f)
have 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) sorry sorry))
  (Y := pullback f f)
  (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) sorry sorry) ≫
    pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) sorry sorry)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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) ⋯ ⋯)
⊢ P.diagonal (e.hom ≫ f)
have 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) sorry sorry))
  (Y := pullback f f)
  (pullback.fst (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) sorry sorry) ≫
    pullback.diagonal 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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)
⊢ P.diagonal (e.hom ≫ f)
have hprecomp₆ : P (Y := pullback f f) (pullback.diagonal 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ P.diagonal (f ≫ e.hom)
have hpostcomp : P (Y := pullback.diagonalObj (f ≫ e.hom)) (pullback.diagonal (f ≫ e.hom))
Tactic: delta diagonal
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ P (Y := pullback.diagonalObj (f ≫ e.hom)) (pullback.diagonal (f ≫ e.hom))
have 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) sorry sorry))
      (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) sorry sorry))))
Tactic: rwa [pullback.diagonal_comp, P.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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) ⋯ ⋯))))
⊢ P (Y := pullback.diagonalObj (f ≫ e.hom)) (pullback.diagonal (f ≫ e.hom))
have hpostcomp₁ : P (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: rwa [pullback.diagonal_comp, P.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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.diagonal (x ≫ x_1)
have 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) sorry sorry))
      (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) sorry sorry))))
Tactic: rw [diagonal_iff, pullback.diagonal_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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.diagonal (X := pullback f g) (pullback.fst f g)
have 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) sorry)))
Tactic: rw [diagonal_iff, diagonal_pullback_fst, P.cancel_left_of_respectsIso,
        P.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
have refine_1 : ∀ (hP : P.HasOfPostcompProperty Q) (X Y : C) (f : X ⟶ Y) (hf : Q f), P.diagonal f
Tactic: refine ⟨fun hP X Y f hf ↦ ?_, fun hP ↦ ⟨fun {Y X S} g f hf hcomp ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal
have 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
Tactic: refine ⟨fun hP X Y f hf ↦ ?_, fun hP ↦ ⟨fun {Y X S} g f hf hcomp ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 ⋯
⊢ P g
have refine_2 : ∀ (this : g = gr ≫ pullback.snd (g ≫ f) f), P g
Tactic: have : g = gr ≫ pullback.snd _ _ := by simp [gr]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 g
have refine_2 : P (gr ≫ pullback.snd (g ≫ f) f)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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 ≫ pullback.snd (g ≫ f) f)
have refine_2 : P gr
Tactic: apply P.comp_mem
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ P (gr ≫ pullback.snd (g ≫ f) f)
have refine_2₁ : P (X := pullback (g ≫ f) f) (pullback.snd (g ≫ f) f)
Tactic: apply P.comp_mem
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
⊢ P.universally.RespectsIso
have hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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)
⊢ P.universally.RespectsIso
have hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)
Tactic: apply RespectsIso.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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)
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv
have rw : i₁ = (i₁ ≫ e.hom) ≫ e.inv
Tactic: rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv
have rw₁ : i₁ = i₁ ≫ e.hom ≫ e.inv
Tactic: rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Limits (goal)
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
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv
have rw₂ : i₁ = i₁ ≫ 𝟙 X
Tactic: rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]