awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q W : MorphismProperty.{v_1, u_1} C
Z_1 X_1 Y_1 A_1 : C
f_1 : Z_1 ⟶ X_1
g_1 : Z_1 ⟶ Y_1
inl_1 : X_1 ⟶ A_1
inr_1 : Y_1 ⟶ A_1
inst_1 : Q.IsStableUnderCobaseChange
inst_2 : P.HasOfPostcompProperty Q
inst_3 : P.RespectsLeft Q
X Y Z A : C
f : X ⟶ Y
g : X ⟶ Z
inl : Y ⟶ A
inr : Z ⟶ A
h : IsPushout f g inl inr
hf : Q f
hinl : P inl
⊢ P g
have apply : P (g ≫ inr)
Tactic: apply P.of_postcomp (W' := Q) g inr (Q.of_isPushout h.flip hf)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Descent (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q W : MorphismProperty.{v_1, u_1} C
Z_1 X_1 Y_1 A_1 : C
f_1 : Z_1 ⟶ X_1
g_1 : Z_1 ⟶ Y_1
inl_1 : X_1 ⟶ A_1
inr_1 : Y_1 ⟶ A_1
inst_1 : Q.IsStableUnderCobaseChange
inst_2 : P.HasOfPostcompProperty Q
inst_3 : P.RespectsLeft Q
X Y Z A : C
f : X ⟶ Y
g : X ⟶ Z
inl : Y ⟶ A
inr : Z ⟶ A
h : IsPushout f g inl inr
hf : Q f
hinl : P inl
⊢ P (g ≫ inr)
have rw : P (f ≫ inl)
Tactic: rw [← h.1.1]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
⊢ W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂
have mp : W₁.comp W₂ = ⊤ → W₁.HasFactorization W₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
mp : W₁.comp W₂ = ⊤ → W₁.HasFactorization W₂
⊢ W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂
have mpr : W₁.HasFactorization W₂ → W₁.comp W₂ = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
h : W₁.comp W₂ = ⊤
⊢ W₁.HasFactorization W₂
have mp : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (W₁.MapFactorizationData W₂ f)
Tactic: refine ⟨fun f => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
h : W₁.comp W₂ = ⊤
X Y : C
f : X ⟶ Y
⊢ Nonempty (W₁.MapFactorizationData W₂ f)
have this : W₁.comp W₂ f
Tactic: have : W₁.comp W₂ f := by simp only [h, top_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
h : W₁.HasFactorization W₂
⊢ W₁.comp W₂ = ⊤
have mpr : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W₁.comp W₂ f ↔ ⊤ f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
h : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f ↔ ⊤ f
have mpr : W₁.comp W₂ f
Tactic: simp only [top_apply, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
f : Arrow.{v_1, u_1} C
⊢ data.i (W₁ := W₁) (W₂ := W₂).app f ≫ data.p (W₁ := W₁) (W₂ := W₂).app f = f.hom
have rw : (data.i (W₁ := W₁) (W₂ := W₂) ≫ data.p (W₁ := W₁) (W₂ := W₂)).app f = f.hom
Tactic: rw [← NatTrans.comp_app, fac, Arrow.leftToRight_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
f : Arrow.{v_1, u_1} C
rw : (data.i (W₁ := W₁) (W₂ := W₂) ≫ data.p (W₁ := W₁) (W₂ := W₂)).app f = f.hom
⊢ data.i (W₁ := W₁) (W₂ := W₂).app f ≫ data.p (W₁ := W₁) (W₂ := W₂).app f = f.hom
have rw₁ : NatTrans.app Arrow.leftToRight f = f.hom
Tactic: rw [← NatTrans.comp_app, fac, Arrow.leftToRight_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
f : Arrow.{v_1, u_1} C
rw : (data.i (W₁ := W₁) (W₂ := W₂) ≫ data.p (W₁ := W₁) (W₂ := W₂)).app f = f.hom
rw₁ : NatTrans.app Arrow.leftToRight f = f.hom
⊢ data.i (W₁ := W₁) (W₂ := W₂).app f ≫ data.p (W₁ := W₁) (W₂ := W₂).app f = f.hom
have rw₂ : f.hom = f.hom
Tactic: rw [← NatTrans.comp_app, fac, Arrow.leftToRight_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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.map (𝟙 j)) (f.right.map (𝟙 j)) ⋯) =
    𝟙 ((data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
have rw : data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map (𝟙 j)) (f.right.map (𝟙 j)) sorry) =
  data.mapZ (W₁ := W₁) (W₂ := W₂) (𝟙 (Arrow.mk (f.hom.app j)))
Tactic: rw [← data.mapZ_id (f.hom.app j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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.map (𝟙 j)) (f.right.map (𝟙 j)) ⋯) =
    data.mapZ (W₁ := W₁) (W₂ := W₂) (𝟙 (Arrow.mk (f.hom.app j)))
have e_φ : f.left.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).left
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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
e_φ : f.left.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).left
⊢ data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map (𝟙 j)) (f.right.map (𝟙 j)) ⋯) =
    data.mapZ (W₁ := W₁) (W₂ := W₂) (𝟙 (Arrow.mk (f.hom.app j)))
have e_φ₁ : f.right.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).right
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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)
X Y Z_1 : J
x : X ⟶ Y
x_1 : Y ⟶ Z_1
⊢ Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app X)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app Z_1)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map (x ≫ x_1)) (f.right.map (x ≫ x_1)) ⋯))
    (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app Y)).Z (W₁ := W₁) (W₂ := W₂))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map x) (f.right.map x) ⋯))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map x_1) (f.right.map x_1) ⋯)))
have rw : Eq (α :=
  (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app X)).Z (W₁ := W₁) (W₂ := W₂) ⟶
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app Z_1)).Z (W₁ := W₁) (W₂ := W₂))
  (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map (x ≫ x_1)) (f.right.map (x ≫ x_1)) sorry))
  (data.mapZ (W₁ := W₁) (W₂ := W₂)
    (CategoryStruct.comp (Y := Arrow.mk (f.hom.app Y)) (Arrow.homMk (f.left.map x) (f.right.map x) sorry)
      (Arrow.homMk (f.left.map x_1) (f.right.map x_1) sorry)))
Tactic: rw [← data.mapZ_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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)
X Y Z_1 : J
x : X ⟶ Y
x_1 : Y ⟶ Z_1
⊢ Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app X)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app Z_1)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map (x ≫ x_1)) (f.right.map (x ≫ x_1)) ⋯))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (CategoryStruct.comp (Y := Arrow.mk (f.hom.app Y)) (Arrow.homMk (f.left.map x) (f.right.map x) ⋯)
        (Arrow.homMk (f.left.map x_1) (f.right.map x_1) ⋯)))
have e_φ : f.left.map (x ≫ x_1) =
  CategoryStruct.comp (Y := (Arrow.mk (f.hom.app Y)).left)
    (CommaMorphism.left (Arrow.homMk (f.left.map x) (f.right.map x) sorry))
    (CommaMorphism.left (Arrow.homMk (f.left.map x_1) (f.right.map x_1) sorry))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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)
X Y Z_1 : J
x : X ⟶ Y
x_1 : Y ⟶ Z_1
e_φ :
  f.left.map (x ≫ x_1) =
    CategoryStruct.comp (Y := (Arrow.mk (f.hom.app Y)).left)
      (CommaMorphism.left (Arrow.homMk (f.left.map x) (f.right.map x) ⋯))
      (CommaMorphism.left (Arrow.homMk (f.left.map x_1) (f.right.map x_1) ⋯))
⊢ Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app X)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app Z_1)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (f.left.map (x ≫ x_1)) (f.right.map (x ≫ x_1)) ⋯))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (CategoryStruct.comp (Y := Arrow.mk (f.hom.app Y)) (Arrow.homMk (f.left.map x) (f.right.map x) ⋯)
        (Arrow.homMk (f.left.map x_1) (f.right.map x_1) ⋯)))
have e_φ₁ : f.right.map (x ≫ x_1) =
  CategoryStruct.comp (Y := (Arrow.mk (f.hom.app Y)).right)
    (CommaMorphism.right (Arrow.homMk (f.left.map x) (f.right.map x) sorry))
    (CommaMorphism.right (Arrow.homMk (f.left.map x_1) (f.right.map x_1) sorry))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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 (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app x)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app x_1)).Z (W₁ := W₁) (W₂ := W₂))
    (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app x_1)).Z (W₁ := W₁) (W₂ := W₂))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (X.left.map x_2) (X.right.map x_2) ⋯))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) ⋯)))
    (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app x)).Z (W₁ := W₁) (W₂ := W₂))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) ⋯))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) ⋯)))
have rw : Eq (α :=
  (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app x)).Z (W₁ := W₁) (W₂ := W₂) ⟶
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app x_1)).Z (W₁ := W₁) (W₂ := W₂))
  (data.mapZ (W₁ := W₁) (W₂ := W₂)
    (CategoryStruct.comp (Y := Arrow.mk (X.hom.app x_1)) (Arrow.homMk (X.left.map x_2) (X.right.map x_2) sorry)
      (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) sorry)))
  (data.mapZ (W₁ := W₁) (W₂ := W₂)
    (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app x))
      (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) sorry)
      (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) sorry)))
Tactic: rw [← data.mapZ_comp, ← data.mapZ_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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 (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app x)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app x_1)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (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) ⋯)))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (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) ⋯)))
have e_φ : Eq.{v_1 + 1} (α := Arrow.mk (X.hom.app x) ⟶ Arrow.mk (Y.hom.app x_1))
  (CategoryStruct.comp (Y := Arrow.mk (X.hom.app x_1)) (Arrow.homMk (X.left.map x_2) (X.right.map x_2) sorry)
    (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) sorry))
  (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app x))
    (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) sorry)
    (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) sorry))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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) ⟶ Arrow.mk (Y.hom.app x_1))
    (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) ⋯))
    (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) ⋯))
have e_φ : 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) sorry)
      (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) sorry)))
  (Arrow.Hom.left
    (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app x))
      (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) sorry)
      (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) sorry)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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
e_φ :
  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) ⋯)))
⊢ Eq.{v_1 + 1} (α := Arrow.mk (X.hom.app x) ⟶ Arrow.mk (Y.hom.app x_1))
    (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) ⋯))
    (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) ⋯))
have e_φ₁ : 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) sorry)
      (Arrow.homMk ((Arrow.Hom.left τ).app x_1) ((Arrow.Hom.right τ).app x_1) sorry)))
  (Arrow.Hom.right
    (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app x))
      (Arrow.homMk ((Arrow.Hom.left τ).app x) ((Arrow.Hom.right τ).app x) sorry)
      (Arrow.homMk (Y.left.map x_2) (Y.right.map x_2) sorry)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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)
⊢ 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 := ⋯ })
have 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 φ) sorry),
          map_id := sorry, map_comp := sorry }
        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 φ) sorry),
          map_id := sorry, map_comp := sorry }
        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) sorry),
        naturality := sorry }
      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 φ) sorry),
          map_id := sorry, map_comp := sorry })
      j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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
⊢ 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)
have w : data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) sorry) =
  𝟙 ((data.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
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.factorizationData (W₁ := W₁) (W₂ := W₂) (f.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
have w : data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) sorry) =
  data.mapZ (W₁ := W₁) (W₂ := W₂) (𝟙 (Arrow.mk (f.hom.app j)))
Tactic: rw [← data.mapZ_id]