awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.CodescendsAlong Q
inst_3 : HasPushout f g
hf : Q f
⊢ P (Y := pushout f g) (pushout.inl f g) ↔ P g

Tactic:
iff_of_isPushout (.of_hasPushout f g) hf

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.iff_of_isPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
inst_1 : P.CodescendsAlong Q
inst_2 : HasPushout f g
hg : Q g
hinr : P (Y := pushout f g) (pushout.inr f g)
⊢ P f

Tactic:
of_isPushout_of_codescendsAlong (IsPushout.of_hasPushout f g).flip hg hinr

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.of_isPushout_of_codescendsAlong, CategoryTheory.IsPushout.flip
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
inst_1 : P.IsStableUnderCobaseChange
inst_2 : P.CodescendsAlong Q
inst_3 : HasPushout f g
hg : Q g
⊢ P (Y := pushout f g) (pushout.inr f g) ↔ P f

Tactic:
iff_of_isPushout (IsPushout.of_hasPushout f g).flip hg

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MorphismProperty.iff_of_isPushout, CategoryTheory.IsPushout.flip
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst_2 : HasPushout f g], Q f → P (Y := pushout f g) (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
have : ∀ (this : HasPushout f g), P g
⊢ P g

Tactic:
have : HasPushout f g := h.hasPushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst_2 : HasPushout f g], Q f → P (Y := pushout f g) (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
apply : P (Y := pushout f g) (pushout.inl f g)
⊢ P g

Tactic:
apply H hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst_2 : HasPushout f g], Q f → P (Y := pushout f g) (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
this : HasPushout f g
rwa : P (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.inv h.isoPushout))
rwa₁ rwa₂ rwa₃ rwa₄ : P inl
⊢ P (Y := pushout f g) (pushout.inl f g)

Tactic:
rwa [← P.cancel_right_of_respectsIso _ h.isoPushout.inv, h.inl_isoPushout_inv]

Premises used: CategoryTheory.IsPushout.isoPushout, CategoryTheory.IsPushout.inl_isoPushout_inv, CategoryTheory.Iso.inv, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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
apply : P (g ≫ inr)
⊢ P g

Tactic:
apply P.of_postcomp (W' := Q) g inr (Q.of_isPushout h.flip hf)

Premises used: CategoryTheory.MorphismProperty.of_isPushout, CategoryTheory.IsPushout.flip, CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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
rw : P (f ≫ inl)
⊢ P (g ≫ inr)

Tactic:
rw [← h.1.1]

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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 (f ≫ inl)

Tactic:
RespectsLeft.precomp _ hf _ hinl

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Descent
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 (f ≫ inl)

Tactic:
exact RespectsLeft.precomp _ hf _ hinl

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp
-- 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
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
hf : W₁.MapFactorizationData W₂ f
⊢ Quiver.Hom.unop (hf.p (W₁ := W₁) (W₂ := W₂).op ≫ hf.i (W₁ := W₁) (W₂ := W₂).op) = f.op.unop

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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₂
mpr : W₁.HasFactorization W₂ → W₁.comp W₂ = ⊤
⊢ W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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₂

Tactic:
⟨fun f => ?_⟩

Premises used: CategoryTheory.MorphismProperty.HasFactorization.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
h : W₁.comp W₂ = ⊤
mp : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (W₁.MapFactorizationData W₂ f)
⊢ W₁.HasFactorization W₂

Tactic:
refine ⟨fun f => ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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
⊢ W₁.comp W₂ f

Tactic:
simp only [h, top_apply]

Premises used: CategoryTheory.MorphismProperty.top_apply
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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
⊢ W₁.comp W₂ f

Tactic:
have : W₁.comp W₂ f := by simp only [h, top_apply]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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
this : W₁.comp W₂ f
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Tactic:
⟨this.some⟩

Premises used: Nonempty.some, Nonempty.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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
this : W₁.comp W₂ f
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Tactic:
exact ⟨this.some⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
h : W₁.HasFactorization W₂
mpr : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W₁.comp W₂ f ↔ ⊤ f
⊢ W₁.comp W₂ = ⊤

Tactic:
ext X Y f
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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
mpr : W₁.comp W₂ f
⊢ W₁.comp W₂ f ↔ ⊤ f

Tactic:
simp only [top_apply, iff_true]

Premises used: iff_true, CategoryTheory.MorphismProperty.top_apply
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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

Tactic:
⟨factorizationData W₁ W₂ f⟩

Premises used: CategoryTheory.MorphismProperty.factorizationData, Nonempty.intro, CategoryTheory.MorphismProperty.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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

Tactic:
exact ⟨factorizationData W₁ W₂ f⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
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
rw₂ rw₃ : f.hom = f.hom
⊢ data.i (W₁ := W₁) (W₂ := W₂).app f ≫ data.p (W₁ := W₁) (W₂ := W₂).app f = f.hom

Tactic:
rw [← NatTrans.comp_app, fac, Arrow.leftToRight_app]

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac, CategoryTheory.Arrow.leftToRight_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
φ : Arrow.mk f ⟶ Arrow.mk g
⊢ (data.factorizationData (W₁ := W₁) (W₂ := W₂) f).i (W₁ := W₁) (W₂ := W₂) ≫ data.mapZ (W₁ := W₁) (W₂ := W₂) φ =
    Arrow.Hom.left φ ≫ (data.factorizationData (W₁ := W₁) (W₂ := W₂) g).i (W₁ := W₁) (W₂ := W₂)

Tactic:
(data.i.naturality φ).symm

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ, CategoryTheory.MorphismProperty.FunctorialFactorizationData.i, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
φ : Arrow.mk f ⟶ Arrow.mk g
⊢ data.mapZ (W₁ := W₁) (W₂ := W₂) φ ≫ (data.factorizationData (W₁ := W₁) (W₂ := W₂) g).p (W₁ := W₁) (W₂ := W₂) =
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) f).p (W₁ := W₁) (W₂ := W₂) ≫ Arrow.Hom.right φ

Tactic:
data.p.naturality φ

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ, CategoryTheory.NatTrans.naturality, CategoryTheory.MorphismProperty.FunctorialFactorizationData.p
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
X Y : C
f : X ⟶ Y
⊢ data.mapZ (W₁ := W₁) (W₂ := W₂) (𝟙 (Arrow.mk f)) =
    𝟙 ((data.factorizationData (W₁ := W₁) (W₂ := W₂) f).Z (W₁ := W₁) (W₂ := W₂))

Tactic:
data.Z.map_id _

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ, CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Factorization
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
φ : Arrow.mk f ⟶ Arrow.mk g
X'' Y'' : C
h : X'' ⟶ Y''
ψ : Arrow.mk g ⟶ Arrow.mk h
⊢ data.mapZ (W₁ := W₁) (W₂ := W₂) (φ ≫ ψ) = data.mapZ (W₁ := W₁) (W₂ := W₂) φ ≫ data.mapZ (W₁ := W₁) (W₂ := W₂) ψ

Tactic:
data.Z.map_comp _ _

Premises used: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ, CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z, CategoryTheory.Functor.map_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
f : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
j : J
rw :
  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)))
⊢ 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₂))

Tactic:
rw [← data.mapZ_id (f.hom.app j)]

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.NatTrans.app, 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
e_φ : f.left.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).left
e_φ₁ : f.right.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).right
⊢ 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)))

Tactic:
congr
-- 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
⊢ f.left.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).left

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)
j : J
⊢ f.right.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).right

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)
X Y Z_1 : J
x : X ⟶ Y
x_1 : Y ⟶ Z_1
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)) ⋯))
    (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) ⋯)))
⊢ 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) ⋯)))

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
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) ⋯))
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) ⋯))
      (CommaMorphism.right (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) ⋯)))

Tactic:
congr
-- 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)
X Y Z_1 : J
x : X ⟶ Y
x_1 : Y ⟶ Z_1
⊢ 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) ⋯))

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)
X Y Z_1 : J
x : X ⟶ Y
x_1 : Y ⟶ Z_1
⊢ 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) ⋯))
      (CommaMorphism.right (Arrow.homMk (f.left.map x_1) (f.right.map x_1) ⋯))

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
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) ⋯)
        (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) ⋯)))
⊢ 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) ⋯)))

Tactic:
rw [← data.mapZ_comp, ← 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 : 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) ⟶ 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) ⋯))
⊢ 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) ⋯)))

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 : 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) ⋯)))
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) ⋯)
        (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) ⋯)))
⊢ 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) ⋯))

Tactic:
ext