awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
Q : MorphismProperty.{v, u} C
inst_2 : Q.RespectsIso
E : Equivalence.{v, v_1, u, u_1} C D
⊢ Q.inverseImage E.inverse = Q.map E.functor

Tactic:
inverseImage_equivalence_inverse_eq_map_functor Q E.symm

Premises used: CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v_1, u_1} D
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F.asEquivalence.inverse).map F = P
erw₁ : P.map (F.asEquivalence.inverse ⋙ F) = P
erw₂ : P.map (𝟭 D) = P
erw₃ erw₄ : P = P
⊢ (P.inverseImage F).map F = P

Tactic:
erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]

Premises used: CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor, CategoryTheory.MorphismProperty.map_id, CategoryTheory.MorphismProperty.map_map, CategoryTheory.MorphismProperty.map_eq_of_iso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
P : MorphismProperty.{v, u} C
inst_2 : P.RespectsIso
F : Functor.{v, v_1, u, u_1} C D
inst_3 : F.IsEquivalence
erw : (P.map F).map F.asEquivalence.inverse = P
erw₁ : P.map (F ⋙ F.asEquivalence.inverse) = P
erw₂ : P.map (𝟭 C) = P
erw₃ erw₄ : P = P
⊢ (P.map F).inverseImage F = P

Tactic:
erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
    P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]

Premises used: CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor, CategoryTheory.MorphismProperty.map_id, CategoryTheory.Equivalence.unitIso, CategoryTheory.MorphismProperty.map_map, CategoryTheory.MorphismProperty.map_eq_of_iso, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.map, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f ↔ IsIso f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ monomorphisms C f ↔ Mono f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ epimorphisms C f ↔ Epi f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
hf : IsIso f
⊢ isomorphisms C f

Tactic:
hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
hf : Mono f
⊢ monomorphisms C f

Tactic:
hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
hf : Epi f
⊢ epimorphisms C f

Tactic:
hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := MorphismProperty.{v, u} Cᵒᵖ) (op (isomorphisms C)) (isomorphisms Cᵒᵖ)

Tactic:
op_isomorphisms _

Premises used: CategoryTheory.MorphismProperty.op_isomorphisms
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
hprecomp :
  ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
hpostcomp :
  ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y),
    MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
⊢ RespectsIso.{v, u} (MorphismProperty.monomorphisms C)

Tactic:
apply RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
h : Mono f
⊢ Mono (e.hom ≫ f)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
h : Mono f
⊢ Mono (f ≫ e.hom)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
hprecomp :
  ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)
hpostcomp :
  ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
⊢ RespectsIso.{v, u} (MorphismProperty.epimorphisms C)

Tactic:
apply RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
h : Epi f
⊢ Epi (e.hom ≫ f)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
h : Epi f
⊢ Epi (f ≫ e.hom)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
hprecomp :
  ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)
hpostcomp :
  ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)
⊢ RespectsIso.{v, u} (MorphismProperty.isomorphisms C)

Tactic:
apply RespectsIso.mk

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
h : IsIso f
⊢ IsIso (e.hom ≫ f)

Tactic:
IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
h : IsIso f
⊢ IsIso (e.hom ≫ f)

Tactic:
exact IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
h : IsIso f
⊢ IsIso (f ≫ e.hom)

Tactic:
IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
h : IsIso f
⊢ IsIso (f ≫ e.hom)

Tactic:
exact IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
α : F ⟶ G
X Y : C
e : X ≅ Y
⊢ (F.mapIso e).hom ≫ (Arrow.mk (α.app Y)).hom = (Arrow.mk (α.app X)).hom ≫ (G.mapIso e).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
T : Type u_3
inst_1 : Category.{v_3, u_3} T
P : MorphismProperty.{v_3, u_3} T
inst_2 : P.RespectsIso
L : Functor.{v_1, v_3, u_1, u_3} A T
X : T
f g : CostructuredArrow L X
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
P.comma_iso_iff e

Premises used: CategoryTheory.MorphismProperty.comma_iso_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
T : Type u_3
inst_1 : Category.{v_3, u_3} T
P : MorphismProperty.{v_3, u_3} T
inst_2 : P.RespectsIso
L : Functor.{v_1, v_3, u_1, u_3} A T
X : T
f g : StructuredArrow X L
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
P.comma_iso_iff e

Premises used: CategoryTheory.MorphismProperty.comma_iso_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
P : MorphismProperty.{v_3, u_3} T
inst_1 : P.RespectsIso
X : T
f g : Over.{v_3, u_3} X
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
P.comma_iso_iff e

Premises used: CategoryTheory.MorphismProperty.comma_iso_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
P : MorphismProperty.{v_3, u_3} T
inst_1 : P.RespectsIso
X : T
f g : Under.{v_3, u_3} X
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
P.comma_iso_iff e

Premises used: CategoryTheory.MorphismProperty.comma_iso_iff
-- 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
W : MorphismProperty.{v_3, u_3} T
Y : Comma L R
⊢ commaObj L R W Y ↔ W Y.hom

Tactic:
.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.commaObj
-- 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
W : MorphismProperty.{v_3, u_3} T
X_1 : T
inst_3 : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
rwa : W Y.hom
rwa₁ : W (L.map e.hom.left ≫ Y.hom)
rwa₂ : W (X.hom ≫ R.map e.hom.right)
rwa₃ rwa₄ rwa₅ rwa₆ : W X.hom
⊢ commaObj L R W Y

Tactic:
rwa [commaObj_iff, ← W.cancel_left_of_respectsIso (L.map e.hom.left), e.hom.w,
      W.cancel_right_of_respectsIso]

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.Functor.map, CategoryTheory.CommaMorphism.left, CategoryTheory.MorphismProperty.commaObj_iff, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
T : Type u_3
inst_1 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
W : MorphismProperty.{v_3, u_3} T
X : T
Y : CostructuredArrow L X
⊢ costructuredArrowObj L W Y ↔ W Y.hom

Tactic:
.rfl

Premises used: CategoryTheory.MorphismProperty.costructuredArrowObj, Iff.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
W : MorphismProperty.{v_3, u_3} T
X : T
inst_3 : W.RespectsIso
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := CostructuredArrow L X) (costructuredArrowObj L W)

Tactic:
inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms

Premises used: _private.0.CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCostructuredArrowCostructuredArrowObjOfRespectsIso._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
B : Type u_2
inst : Category.{v_2, u_2} B
T : Type u_3
inst_1 : Category.{v_3, u_3} T
R : Functor.{v_2, v_3, u_2, u_3} B T
W : MorphismProperty.{v_3, u_3} T
X : T
Y : StructuredArrow X R
⊢ structuredArrowObj R W Y ↔ W Y.hom

Tactic:
.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.structuredArrowObj
-- 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
W : MorphismProperty.{v_3, u_3} T
X : T
inst_3 : W.RespectsIso
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := StructuredArrow X L) (structuredArrowObj L W)

Tactic:
inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms

Premises used: _private.0.CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsStructuredArrowStructuredArrowObjOfRespectsIso._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
⊢ W.over = W.inverseImage (Over.forget X)

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.over, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
Y Z : Over.{v_3, u_3} X
f : Y ⟶ Z
⊢ W.over f ↔ W (Over.Hom.left f)

Tactic:
.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.over
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
⊢ W.under = W.inverseImage (Under.forget X)

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.under, CategoryTheory.MorphismProperty.inverseImage, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
Y Z : Under.{v_3, u_3} X
f : Y ⟶ Z
⊢ W.under f ↔ W (Under.Hom.right f)

Tactic:
.rfl

Premises used: CategoryTheory.MorphismProperty.under, Iff.rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
Y : Over.{v_3, u_3} X
⊢ W.overObj Y ↔ W Y.hom

Tactic:
.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.overObj
-- 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
W : MorphismProperty.{v_3, u_3} T
X : T
inst_3 : W.RespectsIso
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := Over.{v_3, u_3} X) W.overObj

Tactic:
inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms

Premises used: _private.0.CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
Y : Under.{v_3, u_3} X
⊢ W.underObj Y ↔ W Y.hom

Tactic:
.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.underObj
-- 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
W : MorphismProperty.{v_3, u_3} T
X : T
inst_3 : W.RespectsIso
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := Under.{v_3, u_3} X) W.underObj

Tactic:
inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms

Premises used: _private.0.CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsUnderUnderObjOfRespectsIso._proof_1
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
⊢ ObjectProperty.inverseImage (ObjectProperty.op W.overObj) (Equivalence.functor (Under.opEquivOpOver X)) =
    W.op.underObj

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.MorphismProperty.underObj, CategoryTheory.MorphismProperty.overObj, CategoryTheory.MorphismProperty.op, CategoryTheory.ObjectProperty.op, CategoryTheory.ObjectProperty.inverseImage, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Comma
Goal:
T : Type u_3
inst : Category.{v_3, u_3} T
W : MorphismProperty.{v_3, u_3} T
X : T
⊢ ObjectProperty.inverseImage (ObjectProperty.op W.underObj) (Equivalence.functor (Over.opEquivOpUnder X)) =
    W.op.overObj

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.MorphismProperty.underObj, CategoryTheory.MorphismProperty.overObj, CategoryTheory.MorphismProperty.op, CategoryTheory.ObjectProperty.op, CategoryTheory.ObjectProperty.inverseImage, 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
X Y : MorphismProperty.Comma L R P Q W
f : CommaMorphism (X.toComma (P := P) (Q := Q) (W := W)) (Y.toComma (P := P) (Q := Q) (W := W))
hf : Q f.left
hg : W f.right
⊢ (mk (P := P) (Q := Q) (W := W) f hf hg).hom (P := P) (Q := Q) (W := W) = f

Tactic:
rfl

Premises used: 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
X Y : MorphismProperty.Comma L R P Q W
f : X.Hom (P := P) (Q := Q) (W := W) Y
⊢ f.hom (P := P) (Q := Q) (W := W).left = f.toCommaMorphism (P := P) (Q := Q) (W := W).left

Tactic:
rfl

Premises used: 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
X Y : MorphismProperty.Comma L R P Q W
f : X.Hom (P := P) (Q := Q) (W := W) Y
⊢ f.hom (P := P) (Q := Q) (W := W).right = f.toCommaMorphism (P := P) (Q := Q) (W := W).right

Tactic:
rfl

Premises used: 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
⊢ f.toCommaMorphism (P := P) (Q := Q) (W := W) = Hom.hom (P := P) (Q := Q) (W := W) f

Tactic:
rfl

Premises used: 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 g : X ⟶ Y
h : hom (P := P) (Q := Q) (W := W) f = hom (P := P) (Q := Q) (W := W) g
⊢ f = g

Tactic:
Comma.Hom.ext
  (congrArg CommaMorphism.left h)
  (congrArg CommaMorphism.right h)

Premises used: congrArg, CategoryTheory.CommaMorphism.right, CategoryTheory.CommaMorphism.left, CategoryTheory.MorphismProperty.Comma.Hom.ext
-- 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
⊢ Hom.hom (P := P) (Q := Q) (W := W) (𝟙 X) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))

Tactic:
rfl

Premises used: 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 Z : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (P := P) (Q := Q) (W := W) (f ≫ g) =
    Hom.hom (P := P) (Q := Q) (W := W) f ≫ Hom.hom (P := P) (Q := Q) (W := W) g

Tactic:
rfl

Premises used: 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 Z : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).toCommaMorphism (P := P) (Q := Q) (W := W).left =
    f.toCommaMorphism (P := P) (Q := Q) (W := W).left ≫ g.toCommaMorphism (P := P) (Q := Q) (W := W).left

Tactic:
rfl

Premises used: 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 Z : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).toCommaMorphism (P := P) (Q := Q) (W := W).right =
    f.toCommaMorphism (P := P) (Q := Q) (W := W).right ≫ g.toCommaMorphism (P := P) (Q := Q) (W := W).right

Tactic:
rfl

Premises used: 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
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
out :
  ∃ (inv : Y ⟶ X),
    homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ inv = 𝟙 X ∧
      inv ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i = 𝟙 Y
⊢ IsIso (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i)

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 :
  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)
⊢ ∃ (inv : Y ⟶ X),
    homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i ≫ inv = 𝟙 X ∧
      inv ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i = 𝟙 Y

Tactic:
use homFromCommaOfIsIso (inv i)

Premises used: CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso, CategoryTheory.inv