awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.toCommaMorphism (P := P) (Q := Q) (W := W).left = g.toCommaMorphism (P := P) (Q := Q) (W := W).left
hr : f.toCommaMorphism (P := P) (Q := Q) (W := W).right = g.toCommaMorphism (P := P) (Q := Q) (W := W).right
h : (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).left
h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).right
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.toCommaMorphism (P := P) (Q := Q) (W := W).left = g.toCommaMorphism (P := P) (Q := Q) (W := W).left
hr : f.toCommaMorphism (P := P) (Q := Q) (W := W).right = g.toCommaMorphism (P := P) (Q := Q) (W := W).right
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).left

Tactic:
hl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.toCommaMorphism (P := P) (Q := Q) (W := W).left = g.toCommaMorphism (P := P) (Q := Q) (W := W).left
hr : f.toCommaMorphism (P := P) (Q := Q) (W := W).right = g.toCommaMorphism (P := P) (Q := Q) (W := W).right
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).left

Tactic:
exact hl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.toCommaMorphism (P := P) (Q := Q) (W := W).left = g.toCommaMorphism (P := P) (Q := Q) (W := W).left
hr : f.toCommaMorphism (P := P) (Q := Q) (W := W).right = g.toCommaMorphism (P := P) (Q := Q) (W := W).right
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).right

Tactic:
hr
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.toCommaMorphism (P := P) (Q := Q) (W := W).left = g.toCommaMorphism (P := P) (Q := Q) (W := W).left
hr : f.toCommaMorphism (P := P) (Q := Q) (W := W).right = g.toCommaMorphism (P := P) (Q := Q) (W := W).right
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).right

Tactic:
exact hr
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f : A ⟶ B
⊢ f.toCommaMorphism (P := P) (Q := Q) (W := W).left ≫ B.toComma (P := P) (Q := Q) (W := W).hom =
    A.toComma (P := P) (Q := Q) (W := W).hom ≫ f.toCommaMorphism (P := P) (Q := Q) (W := W).right

Tactic:
f.w

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
P' Q' W' : MorphismProperty.{v_1, u_1} T
inst_3 : Q'.IsMultiplicative
inst_4 : W'.IsMultiplicative
hPP' : P ≤ P'
hQQ' : Q ≤ Q'
hWW' : W ≤ W'
Y : P.Arrow Q W
⊢ (Functor.obj (changeProp (P := P) (Q := Q) (W := W) (P' := P') (Q' := Q') (W' := W') hPP' hQQ' hWW') Y).toComma (P :=
        P') (Q := Q') (W := W').left =
    Y.toComma (P := P) (Q := Q) (W := W).left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
P' Q' W' : MorphismProperty.{v_1, u_1} T
inst_3 : Q'.IsMultiplicative
inst_4 : W'.IsMultiplicative
hPP' : P ≤ P'
hQQ' : Q ≤ Q'
hWW' : W ≤ W'
Y : P.Arrow Q W
⊢ (Functor.obj (changeProp (P := P) (Q := Q) (W := W) (P' := P') (Q' := Q') (W' := W') hPP' hQQ' hWW') Y).toComma (P :=
        P') (Q := Q') (W := W').right =
    Y.toComma (P := P) (Q := Q) (W := W).right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
P' Q' W' : MorphismProperty.{v_1, u_1} T
inst_3 : Q'.IsMultiplicative
inst_4 : W'.IsMultiplicative
hPP' : P ≤ P'
hQQ' : Q ≤ Q'
hWW' : W ≤ W'
Y : P.Arrow Q W
⊢ (Functor.obj (changeProp (P := P) (Q := Q) (W := W) (P' := P') (Q' := Q') (W' := W') hPP' hQQ' hWW') Y).toComma (P :=
        P') (Q := Q') (W := W').hom =
    Y.toComma (P := P) (Q := Q) (W := W).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
⊢ Functor.Faithful (Over.forget P Q X)

Tactic:
inferInstanceAs <| (Comma.forget _ _ _ _ _).Faithful

Premises used: _private.0.CategoryTheory.MorphismProperty.instFaithfulOverOverForget._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
⊢ Functor.Full (C := P.Over ⊤ X) (Over.forget P ⊤ X)

Tactic:
inferInstanceAs <| (Comma.forget _ _ _ _ _).Full

Premises used: _private.0.CategoryTheory.MorphismProperty.instFullOverTopOverForget._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f : A ⟶ B
⊢ Functor.map (Over.forget P Q X ⋙ CategoryTheory.Over.forget X) f = f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left
h₂ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).right
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left

Tactic:
h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f : A ⟶ B
⊢ f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left ≫ B.toComma (P := P) (Q := Q) (W := ⊤).hom =
    A.toComma (P := P) (Q := Q) (W := ⊤).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
P' Q' : MorphismProperty.{v_1, u_1} T
inst_2 : Q'.IsMultiplicative
hPP' : P ≤ P'
hQQ' : Q ≤ Q'
Y : P.Over Q X
⊢ (Functor.obj (changeProp (P := P) (Q := Q) X (P' := P') (Q' := Q') hPP' hQQ') Y).toComma (P := P') (Q := Q') (W :=
        ⊤).left =
    Y.toComma (P := P) (Q := Q) (W := ⊤).left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
P' Q' : MorphismProperty.{v_1, u_1} T
inst_2 : Q'.IsMultiplicative
hPP' : P ≤ P'
hQQ' : Q ≤ Q'
Y : P.Over Q X
⊢ (Functor.obj (changeProp (P := P) (Q := Q) X (P' := P') (Q' := Q') hPP' hQQ') Y).toComma (P := P') (Q := Q') (W :=
        ⊤).hom =
    Y.toComma (P := P) (Q := Q) (W := ⊤).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
⊢ Functor.Faithful (Under.forget P Q X)

Tactic:
inferInstanceAs <| (Comma.forget _ _ _ _ _).Faithful

Premises used: _private.0.CategoryTheory.MorphismProperty.instFaithfulUnderUnderForget._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
⊢ Functor.Full (C := P.Under ⊤ X) (Under.forget P ⊤ X)

Tactic:
inferInstanceAs <| (Comma.forget _ _ _ _ _).Full

Premises used: _private.0.CategoryTheory.MorphismProperty.instFullUnderTopUnderForget._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f : A ⟶ B
⊢ Functor.map (Under.forget P Q X ⋙ CategoryTheory.Under.forget X) f =
    f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right = g.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right
h₁ : (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).left = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).left
h₂ : (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).right = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).right
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right = g.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right
⊢ (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).left = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right = g.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right
⊢ (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).right = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).right

Tactic:
h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right = g.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right
⊢ (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).right = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).right

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f : A ⟶ B
⊢ A.toComma (P := P) (Q := ⊤) (W := Q).hom ≫ f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right =
    B.toComma (P := P) (Q := ⊤) (W := Q).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left
h₂ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).right
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
⊢ (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).right

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
A B : P.CostructuredArrow Q F X
f : A.toComma (P := P) (Q := Q) (W := ⊤).left ≅ B.toComma (P := P) (Q := Q) (W := ⊤).left
hf : Q f.hom
hf' : Q f.inv
w : F.map f.hom ≫ B.toComma (P := P) (Q := Q) (W := ⊤).hom = A.toComma (P := P) (Q := Q) (W := ⊤).hom
⊢ F.map f.inv ≫ A.toComma (P := P) (Q := Q) (W := ⊤).hom = B.toComma (P := P) (Q := Q) (W := ⊤).hom

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Faithful
map_injective :
  autoParam
    (∀ {X_1 Y : P.CostructuredArrow ⊤ F X}, Function.Injective (α := X_1 ⟶ Y) (CostructuredArrow.toOver P F X).map)
    Functor.Faithful.map_injective._autoParam
⊢ (CostructuredArrow.toOver P F X).Faithful

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Faithful
A B : P.CostructuredArrow ⊤ F X
f g : A ⟶ B
hfg : (CostructuredArrow.toOver P F X).map f = (CostructuredArrow.toOver P F X).map g
⊢ f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
F.map_injective congr($(hfg).left)

Premises used: congrArg, id, CategoryTheory.CommaMorphism.left, CategoryTheory.Functor.map_injective, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Faithful
A B : P.CostructuredArrow ⊤ F X
f g : A ⟶ B
hfg : (CostructuredArrow.toOver P F X).map f = (CostructuredArrow.toOver P F X).map g
⊢ f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
exact F.map_injective congr($(hfg).left)

Premises used: congrArg, id, CategoryTheory.CommaMorphism.left, CategoryTheory.Functor.map_injective, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
map_surjective :
  ∀ {X_1 Y : P.CostructuredArrow ⊤ F X}, Function.Surjective (α := X_1 ⟶ Y) (CostructuredArrow.toOver P F X).map
⊢ (CostructuredArrow.toOver P F X).Full

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ ∃ (a : A ⟶ B), (CostructuredArrow.toOver P F X).map a = f

Tactic:
⟨CostructuredArrow.homMk (F.preimage f.left) trivial ?_, ?_⟩

Premises used: CategoryTheory.Functor.preimage, trivial, CategoryTheory.MorphismProperty.CostructuredArrow.homMk, CategoryTheory.CommaMorphism.left, Exists.intro, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
map_surjective :
  F.map (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) ≫ B.toComma (P := P) (Q := ⊤) (W := ⊤).hom =
    A.toComma (P := P) (Q := ⊤) (W := ⊤).hom
map_surjective₁ :
  (CostructuredArrow.toOver P F X).map
      (CostructuredArrow.homMk (P := P) (Q := ⊤) (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) trivial
        ⋯) =
    f
⊢ ∃ (a : A ⟶ B), (CostructuredArrow.toOver P F X).map a = f

Tactic:
refine ⟨CostructuredArrow.homMk (F.preimage f.left) trivial ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ F.map (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) ≫ B.toComma (P := P) (Q := ⊤) (W := ⊤).hom =
    A.toComma (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
simpa using f.w

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
map_surjective :
  ((CostructuredArrow.toOver P F X).map
            (CostructuredArrow.homMk (P := P) (Q := ⊤) (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left)
              trivial ⋯)).toCommaMorphism
        (P := P) (Q := ⊤) (W := ⊤).left =
    f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ (CostructuredArrow.toOver P F X).map
      (CostructuredArrow.homMk (P := P) (Q := ⊤) (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) trivial
        ⋯) =
    f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ ((CostructuredArrow.toOver P F X).map
            (CostructuredArrow.homMk (P := P) (Q := ⊤) (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left)
              trivial ⋯)).toCommaMorphism
        (P := P) (Q := ⊤) (W := ⊤).left =
    f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C_1 : Type u_1
D : Type u_2
inst : Category.{?u.349276, u_1} C_1
inst_1 : Category.{?u.349280, u_2} D
P : MorphismProperty D
Q : MorphismProperty C_1
inst_2 : Q.IsMultiplicative
F : C_1 ⥤ D
X_1 : D
C : Type u_3
inst_3 : Category.{v_1, u_3} C
W₁ W₂ : MorphismProperty.{v_1, u_3} C
inst_4 : W₁.HasFactorization W₂
S : C
X Y : Over.{v_1, u_3} S
f : X ⟶ Y
hf : W₁.MapFactorizationData W₂ (Over.Hom.left f) := W₁.factorizationData W₂ (Over.Hom.left f)
⊢ Nonempty (MapFactorizationData W₁.over W₂.over f)

Tactic:
⟨{
      Z := .mk (hf.p ≫ Y.hom)
      i := CategoryTheory.Over.homMk hf.i
      p := CategoryTheory.Over.homMk hf.p
      hi := hf.hi
      hp := hf.hp
    }⟩

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.p, CategoryTheory.Over.mk, CategoryTheory.MorphismProperty.MapFactorizationData.mk, Nonempty.intro, CategoryTheory.Over.homMk, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.MapFactorizationData.hi, CategoryTheory.Over.hom, CategoryTheory.MorphismProperty.MapFactorizationData.hp, CategoryTheory.MorphismProperty.MapFactorizationData.i
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
C_1 : Type u_1
D : Type u_2
inst : Category.{?u.349276, u_1} C_1
inst_1 : Category.{?u.349280, u_2} D
P : MorphismProperty D
Q : MorphismProperty C_1
inst_2 : Q.IsMultiplicative
F : C_1 ⥤ D
X_1 : D
C : Type u_3
inst_3 : Category.{v_1, u_3} C
W₁ W₂ : MorphismProperty.{v_1, u_3} C
inst_4 : W₁.HasFactorization W₂
S : C
X Y : Over.{v_1, u_3} S
f : X ⟶ Y
hf : W₁.MapFactorizationData W₂ (Over.Hom.left f) := W₁.factorizationData W₂ (Over.Hom.left f)
⊢ Nonempty (MapFactorizationData W₁.over W₂.over f)

Tactic:
exact ⟨{
      Z := .mk (hf.p ≫ Y.hom)
      i := CategoryTheory.Over.homMk hf.i
      p := CategoryTheory.Over.homMk hf.p
      hi := hf.hi
      hp := hf.hp
    }⟩