awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
h :
  Eq (α := X ⟶ X)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) (𝟙 X)
h₁ :
  Eq (α := Y ⟶ Y)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)
⊢ Eq (α := X ⟶ X)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i))
      (𝟙 X) ∧
    Eq (α := Y ⟶ Y)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
h :
  Hom.hom (P := P) (Q := Q) (W := W)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) =
    Hom.hom (P := P) (Q := Q) (W := W) (𝟙 X)
⊢ Eq (α := X ⟶ X)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) (𝟙 X)

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
h :
  Hom.hom (P := P) (Q := Q) (W := W)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) =
    Hom.hom (P := P) (Q := Q) (W := W) (𝟙 Y)
⊢ Eq (α := Y ⟶ Y)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
⊢ Hom.hom (P := P) (Q := Q) (W := W)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i)) =
    Hom.hom (P := P) (Q := Q) (W := W) (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
⊢ Hom.hom (P := P) (Q := Q) (W := W)
      (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) =
    Hom.hom (P := P) (Q := Q) (W := W) (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst_5 : IsIso f
⊢ IsIso (Hom.hom (P := P) (Q := Q) (W := W) f)

Tactic:
(forget L R P Q W).map_isIso f

Premises used: CategoryTheory.MorphismProperty.Comma.forget, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X ⟶ Y
inst_7 : IsIso (Hom.hom (P := P) (Q := Q) (W := W) i)
⊢ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (Hom.hom (P := P) (Q := Q) (W := W) i) = i

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst_5 : IsIso f
hom_inv_id :
  Hom.hom (P := P) (Q := Q) (W := W) f ≫ Hom.hom (P := P) (Q := Q) (W := W) (inv f) =
    𝟙 (X.toComma (P := P) (Q := Q) (W := W))
⊢ Hom.hom (P := P) (Q := Q) (W := W) (inv f) = inv (Hom.hom (P := P) (Q := Q) (W := W) f)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst_5 : IsIso f
hom_inv_id : Hom.hom (P := P) (Q := Q) (W := W) (f ≫ inv f) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
hom_inv_id₁ : Hom.hom (P := P) (Q := Q) (W := W) (𝟙 X) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
hom_inv_id₂ hom_inv_id₃ : 𝟙 (X.toComma (P := P) (Q := Q) (W := W)) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
⊢ Hom.hom (P := P) (Q := Q) (W := W) f ≫ Hom.hom (P := P) (Q := Q) (W := W) (inv f) =
    𝟙 (X.toComma (P := P) (Q := Q) (W := W))

Tactic:
rw [← comp_hom, IsIso.hom_inv_id, id_hom]

Premises used: CategoryTheory.MorphismProperty.Comma.id_hom, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.MorphismProperty.Comma.comp_hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
A_1 B_1 : MorphismProperty.Comma L R P Q W
f : A_1 ⟶ B_1
hf : IsIso (Hom.hom (P := P) (Q := Q) (W := W) f)
rw : IsIso (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (Hom.hom (P := P) (Q := Q) (W := W) f))
⊢ IsIso f

Tactic:
rw [← hom_homFromCommaOfIsIso f]

Premises used: CategoryTheory.MorphismProperty.Comma.hom_homFromCommaOfIsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
A_1 B_1 : MorphismProperty.Comma L R P Q W
f : A_1 ⟶ B_1
hf : IsIso (Hom.hom (P := P) (Q := Q) (W := W) f)
⊢ IsIso (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (Hom.hom (P := P) (Q := Q) (W := W) f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
⊢ Functor.Full (C := MorphismProperty.Comma L R P ⊤ ⊤) (forget L R P ⊤ ⊤)

Tactic:
Functor.FullyFaithful.full (forgetFullyFaithful L R P)

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.MorphismProperty.Comma.forgetFullyFaithful
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
rw rw₁ : Y.toComma (P := P) (Q := Q) (W := W).left = Y.toComma (P := P) (Q := Q) (W := W).left
⊢ X.toComma (P := P) (Q := Q) (W := W).left = Y.toComma (P := P) (Q := Q) (W := W).left

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
subst : CommaMorphism.left (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom ⋯)) = eqToHom ⋯
⊢ CommaMorphism.left (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom h)) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ CommaMorphism.left (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom ⋯)) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
rw rw₁ : Y.toComma (P := P) (Q := Q) (W := W).right = Y.toComma (P := P) (Q := Q) (W := W).right
⊢ X.toComma (P := P) (Q := Q) (W := W).right = Y.toComma (P := P) (Q := Q) (W := W).right

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
subst : CommaMorphism.right (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom ⋯)) = eqToHom ⋯
⊢ CommaMorphism.right (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom h)) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ CommaMorphism.right (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom ⋯)) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P_1 : MorphismProperty.{v_3, u_3} T
Q_1 : MorphismProperty.{v_1, u_1} A
W_1 : MorphismProperty.{v_2, u_2} B
inst_3 : Q_1.IsMultiplicative
inst_4 : W_1.IsMultiplicative
P P' : MorphismProperty.{v_3, u_3} T
Q Q' : MorphismProperty.{v_1, u_1} A
W W' : MorphismProperty.{v_2, u_2} B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst_5 : Q.IsMultiplicative
inst_6 : Q'.IsMultiplicative
inst_7 : W.IsMultiplicative
inst_8 : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) X ⟶
      Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) Y)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) f)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) g)
h₁ : Hom.hom (P := P) (Q := Q) (W := W) f = Hom.hom (P := P) (Q := Q) (W := W) g
⊢ f = g

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P_1 : MorphismProperty.{v_3, u_3} T
Q_1 : MorphismProperty.{v_1, u_1} A
W_1 : MorphismProperty.{v_2, u_2} B
inst_3 : Q_1.IsMultiplicative
inst_4 : W_1.IsMultiplicative
P P' : MorphismProperty.{v_3, u_3} T
Q Q' : MorphismProperty.{v_1, u_1} A
W W' : MorphismProperty.{v_2, u_2} B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst_5 : Q.IsMultiplicative
inst_6 : Q'.IsMultiplicative
inst_7 : W.IsMultiplicative
inst_8 : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) X ⟶
      Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) Y)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) f)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) g)
⊢ Hom.hom (P := P) (Q := Q) (W := W) f = Hom.hom (P := P) (Q := Q) (W := W) g

Tactic:
congr($(h).hom)

Premises used: congrArg, id, CategoryTheory.MorphismProperty.Comma.Hom.hom
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P_1 : MorphismProperty.{v_3, u_3} T
Q_1 : MorphismProperty.{v_1, u_1} A
W_1 : MorphismProperty.{v_2, u_2} B
inst_3 : Q_1.IsMultiplicative
inst_4 : W_1.IsMultiplicative
P P' : MorphismProperty.{v_3, u_3} T
Q Q' : MorphismProperty.{v_1, u_1} A
W W' : MorphismProperty.{v_2, u_2} B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst_5 : Q.IsMultiplicative
inst_6 : Q'.IsMultiplicative
inst_7 : W.IsMultiplicative
inst_8 : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) X ⟶
      Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) Y)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) f)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) g)
⊢ Hom.hom (P := P) (Q := Q) (W := W) f = Hom.hom (P := P) (Q := Q) (W := W) g

Tactic:
exact congr($(h).hom)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P_1 : MorphismProperty.{v_3, u_3} T
Q_1 : MorphismProperty.{v_1, u_1} A
W_1 : MorphismProperty.{v_2, u_2} B
inst_3 : Q_1.IsMultiplicative
inst_4 : W_1.IsMultiplicative
P P' : MorphismProperty.{v_3, u_3} T
Q Q' : MorphismProperty.{v_1, u_1} A
W W' : MorphismProperty.{v_2, u_2} B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst_5 : Q.IsMultiplicative
inst_6 : Q'.IsMultiplicative
inst_7 : W.IsMultiplicative
inst_8 : W'.IsMultiplicative
⊢ Functor.Full (C := MorphismProperty.Comma L R P Q W)
    (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q) (W := W) (W' := W) hP ⋯ ⋯)

Tactic:
(fullyFaithfulChangeProp ..).full

Premises used: CategoryTheory.MorphismProperty.Comma.fullyFaithfulChangeProp, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
L₁ L₂ L₃ : Functor.{v_1, v_3, u_1, u_3} A T
R₁ R₂ R₃ : Functor.{v_2, v_3, u_2, u_3} B T
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X : MorphismProperty.Comma L R P Q W
⊢ P (NatTrans.app (𝟙 L) X.toComma (P := P) (Q := Q) (W := W).left ≫ X.toComma (P := P) (Q := Q) (W := W).hom)

Tactic:
simpa using X.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
L₁ L₂ L₃ : Functor.{v_1, v_3, u_1, u_3} A T
R₁ R₂ R₃ : Functor.{v_2, v_3, u_2, u_3} B T
inst_5 : P.RespectsIso
inst_6 : Q.RespectsIso
inst_7 : W.RespectsIso
e : L₁ ≅ L₂
X : MorphismProperty.Comma L₁ R P Q W
⊢ P (NatTrans.app (𝟙 L₁) X.toComma (P := P) (Q := Q) (W := W).left ≫ X.toComma (P := P) (Q := Q) (W := W).hom)

Tactic:
simpa using X.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
L₁ L₂ L₃ : Functor.{v_1, v_3, u_1, u_3} A T
R₁ R₂ R₃ : Functor.{v_2, v_3, u_2, u_3} B T
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X : MorphismProperty.Comma L R P Q W
⊢ P (X.toComma (P := P) (Q := Q) (W := W).hom ≫ NatTrans.app (𝟙 R) X.toComma (P := P) (Q := Q) (W := W).right)

Tactic:
simpa using X.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
L₁ L₂ L₃ : Functor.{v_1, v_3, u_1, u_3} A T
R₁ R₂ R₃ : Functor.{v_2, v_3, u_2, u_3} B T
inst_5 : P.RespectsIso
inst_6 : Q.RespectsIso
inst_7 : W.RespectsIso
e : R₁ ≅ R₂
X : MorphismProperty.Comma L R₁ P Q W
⊢ P (X.toComma (P := P) (Q := Q) (W := W).hom ≫ NatTrans.app (𝟙 R₁) X.toComma (P := P) (Q := Q) (W := W).right)

Tactic:
simpa using X.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- 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
⊢ Functor.Faithful (Arrow.forget P Q W)

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

Premises used: _private.0.CategoryTheory.MorphismProperty.instFaithfulArrowArrowForget._proof_1
-- 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
⊢ Functor.Full (C := P.Arrow ⊤ ⊤) (Arrow.forget P ⊤ ⊤)

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

Premises used: _private.0.CategoryTheory.MorphismProperty.instFullArrowTopArrowForget._proof_1
-- 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
⊢ Functor.map (Arrow.forget P Q W ⋙ Arrow.leftFunc) f = f.toCommaMorphism (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
A B : P.Arrow Q W
f : A ⟶ B
⊢ Functor.map (Arrow.forget P Q W ⋙ Arrow.rightFunc) f = f.toCommaMorphism (P := P) (Q := Q) (W := W).right

Tactic:
rfl

Premises used: rfl