awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
τ : X ⟶ Y
x x_1 : J
x_2 : x ⟶ x_1
⊢ Eq.{v_1 + 1} (α := (Arrow.mk (X.hom.app x)).left ⟶ (Arrow.mk (Y.hom.app x_1)).left)
    (Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (X.hom.app x_1)) (Arrow.homMk (X.left.map x_2) (X.right.map x_2) ⋯)
        (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) ⋯)))
    (Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app x))
        (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) ⋯)
        (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) ⋯)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
τ : X ⟶ Y
x x_1 : J
x_2 : x ⟶ x_1
⊢ Eq.{v_1 + 1} (α := (Arrow.mk (X.hom.app x)).right ⟶ (Arrow.mk (Y.hom.app x_1)).right)
    (Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk (X.hom.app x_1)) (Arrow.homMk (X.left.map x_2) (X.right.map x_2) ⋯)
        (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) ⋯)))
    (Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app x))
        (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) ⋯)
        (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) ⋯)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
f : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
w :
  ∀ (j : J),
    Eq.{v_1 + 1} (α :=
      Quiver.Hom.{v_1, u_1} (V := C)
        (Functor.obj.{v_3, v_1, u_3, u_1}
          { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
            map := fun {X Y : J} (φ : X ⟶ Y) ↦
              data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
            map_id := ⋯, map_comp := ⋯ }
          j)
        (Functor.obj.{v_3, v_1, u_3, u_1}
          { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
            map := fun {X Y : J} (φ : X ⟶ Y) ↦
              data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
            map_id := ⋯, map_comp := ⋯ }
          j))
      (NatTrans.app
        {
          app := fun (j : J) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂)
              (Arrow.homMk ((Arrow.Hom.left (𝟙 f)).app j) ((Arrow.Hom.right (𝟙 f)).app j) ⋯),
          naturality := ⋯ }
        j)
      (NatTrans.app
        (𝟙
          { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
            map := fun {X Y : J} (φ : X ⟶ Y) ↦
              data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
            map_id := ⋯, map_comp := ⋯ })
        j)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_3, v_1, u_3, u_1} J C)
      { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
        map := fun {X Y : J} (φ : X ⟶ Y) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
        map_id := ⋯, map_comp := ⋯ }
      { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
        map := fun {X Y : J} (φ : X ⟶ Y) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
        map_id := ⋯, map_comp := ⋯ })
    {
      app := fun (j : J) ↦
        data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left (𝟙 f)).app j) ((Arrow.Hom.right (𝟙 f)).app j) ⋯),
      naturality := ⋯ }
    (𝟙
      { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
        map := fun {X Y : J} (φ : X ⟶ Y) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
        map_id := ⋯, map_comp := ⋯ })

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
f : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
j : J
w :
  data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) =
    𝟙 ((data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y : J} (φ : X ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        j)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y : J} (φ : X ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        j))
    (NatTrans.app
      {
        app := fun (j : J) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂)
            (Arrow.homMk ((Arrow.Hom.left (𝟙 f)).app j) ((Arrow.Hom.right (𝟙 f)).app j) ⋯),
        naturality := ⋯ }
      j)
    (NatTrans.app
      (𝟙
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y : J} (φ : X ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ })
      j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
f : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
j : J
w :
  data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) =
    data.mapZ (W₁ := W₁) (W₂ := W₂) (𝟙 (Arrow.mk (f.hom.app j)))
⊢ data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) =
    𝟙 ((data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))

Tactic:
rw [← data.mapZ_id]

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
f : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
j : J
⊢ data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) =
    data.mapZ (W₁ := W₁) (W₂ := W₂) (𝟙 (Arrow.mk (f.hom.app j)))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y Z_1 : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
f : X ⟶ Y
g : Y ⟶ Z_1
j : J
w :
  Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯))
    (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)))
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X_1 Y : J} (φ : X_1 ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (X.left.map φ) (X.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        j)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y : J} (φ : X ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Z_1.left.map φ) (Z_1.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        j))
    (NatTrans.app
      {
        app := fun (j : J) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂)
            (Arrow.homMk ((Arrow.Hom.left (f ≫ g)).app j) ((Arrow.Hom.right (f ≫ g)).app j) ⋯),
        naturality := ⋯ }
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y_1 : J} (φ : X ⟶ Y_1) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Y.left.map φ) (Y.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ })
        {
          app := fun (j : J) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯),
          naturality := ⋯ }
        {
          app := fun (j : J) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯),
          naturality := ⋯ })
      j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y Z_1 : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
f : X ⟶ Y
g : Y ⟶ Z_1
j : J
w :
  Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app j))
        (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯)
        (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)))
⊢ Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯))
    (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)))

Tactic:
rw [← data.mapZ_comp]

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y Z_1 : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
f : X ⟶ Y
g : Y ⟶ Z_1
j : J
⊢ Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app j))
        (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯)
        (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
inst_2 : W₁.HasFunctorialFactorization W₂
J : Type u_3
inst_3 : Category.{v_3, u_3} J
⊢ HasFunctorialFactorization (C := Functor.{v_3, v_1, u_3, u_1} J C) (W₁.functorCategory J) (W₂.functorCategory J)

Tactic:
⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩

Premises used: CategoryTheory.MorphismProperty.HasFunctorialFactorization.mk, CategoryTheory.MorphismProperty.functorialFactorizationData, Nonempty.intro, CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ F.map
      (CategoryStruct.comp (Y := F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂)))
        (F.preimage (h.i (W₁ := W₁) (W₂ := W₂) ≫ Iso.inv (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂)))))
        (F.preimage (Iso.hom (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))) ≫ h.p (W₁ := W₁) (W₂ := W₂)))) =
    F.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ W₁.inverseImage F (Y := F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂)))
    (F.preimage (h.i (W₁ := W₁) (W₂ := W₂) ≫ Iso.inv (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂)))))

Tactic:
(W₁.arrow_mk_iso_iff ?_).1 h.hi

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.MorphismProperty.MapFactorizationData.hi
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
refine :
  Arrow.mk (h.i (W₁ := W₁) (W₂ := W₂)) ≅
    Arrow.mk (Y := F.obj (F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂))))
      (F.map (F.preimage (h.i (W₁ := W₁) (W₂ := W₂) ≫ Iso.inv (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))))))
⊢ W₁.inverseImage F (Y := F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂)))
    (F.preimage (h.i (W₁ := W₁) (W₂ := W₂) ≫ Iso.inv (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂)))))

Tactic:
refine (W₁.arrow_mk_iso_iff ?_).1 h.hi

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.MorphismProperty.MapFactorizationData.hi
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ Arrow.mk (h.i (W₁ := W₁) (W₂ := W₂)) ≅
    Arrow.mk (Y := F.obj (F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂))))
      (F.map (F.preimage (h.i (W₁ := W₁) (W₂ := W₂) ≫ Iso.inv (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))))))

Tactic:
exact Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ W₂.inverseImage F (X := F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂)))
    (F.preimage (Iso.hom (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))) ≫ h.p (W₁ := W₁) (W₂ := W₂)))

Tactic:
(W₂.arrow_mk_iso_iff ?_).1 h.hp

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
refine :
  Arrow.mk (h.p (W₁ := W₁) (W₂ := W₂)) ≅
    Arrow.mk (X := F.obj (F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂))))
      (F.map (F.preimage (Iso.hom (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))) ≫ h.p (W₁ := W₁) (W₂ := W₂))))
⊢ W₂.inverseImage F (X := F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂)))
    (F.preimage (Iso.hom (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))) ≫ h.p (W₁ := W₁) (W₂ := W₂)))

Tactic:
refine (W₂.arrow_mk_iso_iff ?_).1 h.hp

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ Arrow.mk (h.p (W₁ := W₁) (W₂ := W₂)) ≅
    Arrow.mk (X := F.obj (F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂))))
      (F.map (F.preimage (Iso.hom (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))) ≫ h.p (W₁ := W₁) (W₂ := W₂))))

Tactic:
exact Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
K : Type u'
inst_1 : LinearOrder K
inst_2 : SuccOrder K
inst_3 : OrderBot K
inst_4 : WellFoundedLT K
inst_5 : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst_6 : Category.{v'', u''} J
inst_7 : HasIterationOfShape.{u', v, u} K C
X Y : Functor.{v'', v, u'', u} J C
f : X ⟶ Y
hf : TransfiniteCompositionOfShape (W.functorCategory J) K f
j : J
have :
  ∀
    (this :
      LE.le (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (W.functorCategory J)
        (W.inverseImage (Functor.obj (evaluation J C) j))),
    W (f.app j)
⊢ W (f.app j)

Tactic:
have : W.functorCategory J ≤ W.inverseImage ((evaluation _ _).obj j) := fun _ _ _ h ↦ h _
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
K : Type u'
inst_1 : LinearOrder K
inst_2 : SuccOrder K
inst_3 : OrderBot K
inst_4 : WellFoundedLT K
inst_5 : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst_6 : Category.{v'', u''} J
inst_7 : HasIterationOfShape.{u', v, u} K C
X Y : Functor.{v'', v, u'', u} J C
f : X ⟶ Y
hf : TransfiniteCompositionOfShape (W.functorCategory J) K f
j : J
this :
  LE.le (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (W.functorCategory J)
    (W.inverseImage (Functor.obj (evaluation J C) j))
⊢ W (f.app j)

Tactic:
W.transfiniteCompositionsOfShape_le K _ ⟨(hf.ofLE this).map⟩

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, Nonempty.intro, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLE
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
K : Type u'
inst_1 : LinearOrder K
inst_2 : SuccOrder K
inst_3 : OrderBot K
inst_4 : WellFoundedLT K
inst_5 : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst_6 : Category.{v'', u''} J
inst_7 : HasIterationOfShape.{u', v, u} K C
X Y : Functor.{v'', v, u'', u} J C
f : X ⟶ Y
hf : TransfiniteCompositionOfShape (W.functorCategory J) K f
j : J
this :
  LE.le (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (W.functorCategory J)
    (W.inverseImage (Functor.obj (evaluation J C) j))
⊢ W (f.app j)

Tactic:
exact W.transfiniteCompositionsOfShape_le K _ ⟨(hf.ofLE this).map⟩

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, Nonempty.intro, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLE
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
h :
  ∀ ⦃X Y : Functor.{v'', v, u'', u} J C⦄ (f : X ⟶ Y),
    functorCategory (isomorphisms C) J f ↔ isomorphisms (Functor.{v'', v, u'', u} J C) f
⊢ Eq (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (functorCategory (isomorphisms C) J)
    (isomorphisms (Functor.{v'', v, u'', u} J C))

Tactic:
ext _ _ f
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
X Y : Functor.{v'', v, u'', u} J C
f : X ⟶ Y
⊢ functorCategory (isomorphisms C) J f ↔ isomorphisms (Functor.{v'', v, u'', u} J C) f

Tactic:
simp only [functorCategory, isomorphisms.iff, NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.MorphismProperty.functorCategory
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
inst_2 : HasPullbacks.{v, u} C
h :
  ∀ ⦃X Y : Functor.{v'', v, u'', u} J C⦄ (f : X ⟶ Y),
    functorCategory (monomorphisms C) J f ↔ monomorphisms (Functor.{v'', v, u'', u} J C) f
⊢ Eq (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (functorCategory (monomorphisms C) J)
    (monomorphisms (Functor.{v'', v, u'', u} J C))

Tactic:
ext _ _ f
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
inst_2 : HasPullbacks.{v, u} C
X Y : Functor.{v'', v, u'', u} J C
f : X ⟶ Y
⊢ functorCategory (monomorphisms C) J f ↔ monomorphisms (Functor.{v'', v, u'', u} J C) f

Tactic:
simp only [functorCategory, monomorphisms.iff, NatTrans.mono_iff_mono_app]

Premises used: CategoryTheory.MorphismProperty.monomorphisms.iff, CategoryTheory.NatTrans.mono_iff_mono_app, CategoryTheory.MorphismProperty.functorCategory