mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ ∀ {v w : ↑X} (f : v ⟶ w),
    (freeReflMap (𝟙 X)).toCatHom.toFunctor.map (FreeRefl.homMk f) =
      eqToHom ⋯ ≫ (𝟙 (of (FreeRefl ↑X))).toFunctor.map (FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ (freeReflMap (𝟙 X)).toCatHom = 𝟙 (of (FreeRefl ↑X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (v : ↑X),
    (freeReflMap (f ≫ g)).toCatHom.toFunctor.obj (FreeRefl.mk v) =
      ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor.obj (FreeRefl.mk v)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {v w : ↑X} (f_1 : v ⟶ w),
    (freeReflMap (f ≫ g)).toCatHom.toFunctor.map (FreeRefl.homMk f_1) =
      eqToHom ⋯ ≫ ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor.map (FreeRefl.homMk f_1) ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ (freeReflMap (f ≫ g)).toCatHom = (freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor.obj =
    ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor.obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ∀ (a b : ↑(Quiv.of ↑v)) (e : a ⟶ b),
    ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor.map e.toPath =
      eqToHom ⋯ ≫ ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor.map e.toPath ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ (ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom =
    (FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : ReflQuiver W
inst✝² : ReflQuiver V
C : Type u_3
D : Type u_4
inst✝¹ : Category.{v_1, u_3} C
inst✝ : Category.{v_2, u_4} D
F : Cat.FreeRefl V ⥤ C
⊢ ∀ (v : V),
    (Cat.FreeRefl.lift ((fun F ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F)).obj (Cat.FreeRefl.mk v) =
      F.obj (Cat.FreeRefl.mk v)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : ReflQuiver W
inst✝² : ReflQuiver V
C : Type u_3
D : Type u_4
inst✝¹ : Category.{v_1, u_3} C
inst✝ : Category.{v_2, u_4} D
F : Cat.FreeRefl V ⥤ C
⊢ ∀ {v w : V} (f : v ⟶ w),
    (Cat.FreeRefl.lift ((fun F ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F)).map (Cat.FreeRefl.homMk f) =
      eqToHom ⋯ ≫ F.map (Cat.FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝² : ReflQuiver W
inst✝¹ : ReflQuiver V
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : V ⥤rq W
G : W ⥤rq C
⊢ ∀ (v : V),
    (homEquiv.symm (F ⋙rq G)).obj (Cat.FreeRefl.mk v) = (Cat.freeReflMap F ⋙ homEquiv.symm G).obj (Cat.FreeRefl.mk v)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝² : ReflQuiver W
inst✝¹ : ReflQuiver V
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : V ⥤rq W
G : W ⥤rq C
⊢ ∀ {v w : V} (f : v ⟶ w),
    (homEquiv.symm (F ⋙rq G)).map (Cat.FreeRefl.homMk f) =
      eqToHom ⋯ ≫ (Cat.freeReflMap F ⋙ homEquiv.symm G).map (Cat.FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: X'✝ X✝ : ReflQuiv
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ forget.obj Y✝
⊢ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X'✝) Y✝).trans adj.homEquiv).symm (x✝¹ ≫ x✝) =
    Cat.freeRefl.map x✝¹ ≫ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X✝) Y✝).trans adj.homEquiv).symm x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
C : Type u
inst✝ : Category.{max u v, u} C
⊢ adj.homEquiv (of V) (Cat.of C) = (Cat.Hom.equivFunctor (Cat.freeRefl.obj (of V)) (Cat.of C)).trans adj.homEquiv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: C : Type u
inst✝ : Category.{max u v, u} C
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (Cat.FreeRefl.quotientFunctor C ⋙ (adj.counit.app (Cat.of C)).toFunctor).map f.toPath =
    eqToHom ⋯ ≫ (pathComposition C).map f.toPath ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
        (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ (ConcreteCategory.hom
        (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).map
          (Hom.tr (SimplexCategory.δ 1) Truncated.Path₁._proof_1 Truncated.Path₁._proof_5).op))
      ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x) =
    (ConcreteCategory.hom
        (s.π.app
          (StructuredArrow.mk
            (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i.castSucc).op)))
      x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
        (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ (ConcreteCategory.hom
        (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).map
          (Hom.tr (SimplexCategory.δ 0) Truncated.Path₁._proof_1 Truncated.Path₁._proof_5).op))
      ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x) =
    (ConcreteCategory.hom
        (s.π.app
          (StructuredArrow.mk
            (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i.succ).op)))
      x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i < n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc ⟨i, hi⟩).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) fac_aux₁._proof_1))) x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ i < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ j < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ Truncated.Edge.map (𝟙rq x) f = 𝟙rq ((ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := _proof_1 }))) x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X : Truncated 2
x₁ y₁ x₂ y₂ : OneTruncation₂ X
f : x₁ ⟶ y₁
hx : x₁ = x₂
hy : y₁ = y₂
⊢ (Quiver.homOfEq f hx hy).edge = f.edge

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : Category.{u, u} C
F G : X ⟶ (truncation 2).obj (nerve C)
h : map F = map G
f : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom (F.app (op { obj := ⦋1⦌, property := ⋯ }))) f =
    (ConcreteCategory.hom (G.app (op { obj := ⦋1⦌, property := ⋯ }))) f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
⊢ ∀ (X : ↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X✝)),
    ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫ (ofNerve₂ ↑Y✝).hom).obj X =
      ((ofNerve₂ ↑X✝).hom ≫ ReflQuiv.forget.map F).obj X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
⊢ ⟨i, ⋯⟩ ≤ ⟨i, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
x y : ↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X✝)
f : x ⟶ y
⊢ ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫ (ofNerve₂ ↑Y✝).hom).map f =
    Eq.recOn ⋯ (Eq.recOn ⋯ (((ofNerve₂ ↑X✝).hom ≫ ReflQuiv.forget.map F).map f))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
V : Cᵒᵖ ⥤ Type w
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
γ : X ⟶ Z
φ : (fun X ↦ X) (V.obj (op Z))
⊢ α ≫ β = γ →
    (ConcreteCategory.hom (V.map α.op)) ((ConcreteCategory.hom (V.map β.op)) φ) = (ConcreteCategory.hom (V.map γ.op)) φ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ι0₂._proof_3 })
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
⊢ Function.Surjective mk

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
h : x.as.as = y.as.as
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
motive : V.HomotopyCategory → Prop
h : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), motive (mk x)
x : V.HomotopyCategory
⊢ motive x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₀ y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge y₀ y₁
h : e.edge = e'.edge
⊢ x₀ = y₀

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
⊢ (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1).hom ≫ (inclusion 2).op.map (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op =
    (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ x₁ = y₁

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e e' : Edge x₀ x₁
h : e.edge = e'.edge
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₀ y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge y₀ y₁
h : e.edge = e'.edge
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e')

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (Edge.id x) = 𝟙 (mk x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ homMk e₀₁ ≫ homMk e₁₂ = homMk e₀₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_4} C₃
inst✝ : Category.{v_9, u_9} E
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.hom.app F).app X₁).app X₂).app X₃ = 𝟙 (((((𝟭 (C₁ ⥤ C₂ ⥤ C₃ ⥤ E)).obj F).obj X₁).obj X₂).obj X₃)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x y
⊢ morphismPropertyHomMk V (homMk e)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
⊢ morphismPropertyHomMk V = (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_4} C₃
inst✝ : Category.{v_9, u_9} E
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ =
    𝟙 (((((currying₃.functor ⋙ currying₃.inverse).obj F).obj X₁).obj X₂).obj X₃)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ ⊤ f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x ⟶ y
x✝ : ⊤ f
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
X : C₃
Y : C₂
x✝¹ x✝ : C₁
g : x✝¹ ⟶ x✝
⊢ ((X✝.flip₁₃.obj X).obj Y).map g ≫ ((f.app x✝).app Y).app X =
    ((f.app x✝¹).app Y).app X ≫ ((Y✝.flip₁₃.obj X).obj Y).map g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ W ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ ⊤ ≤ W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
X : C₁
Y : C₃
x✝¹ x✝ : C₂
g : x✝¹ ⟶ x✝
⊢ ((X✝.flip₂₃.obj X).obj Y).map g ≫ ((f.app X).app x✝).app Y =
    ((f.app X).app x✝¹).app Y ≫ ((Y✝.flip₂₃.obj X).obj Y).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
x✝¹ x✝ : C₁
g : x✝¹ ⟶ x✝
⊢ X✝.flip₂₃.map g ≫ { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝¹).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } ≫ Y✝.flip₂₃.map g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
⊢ ∀ (x y : Cat.FreeRefl (OneTruncation₂ V)) (f₁ f₂ : x ⟶ y),
    OneTruncation₂.HoRel₂ V f₁ f₂ →
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map f₁ =
        (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map f₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
⊢ ∀ (x y : Cat.FreeRefl (OneTruncation₂ V)) (f₁ f₂ : x ⟶ y),
    OneTruncation₂.HoRel₂ V f₁ f₂ →
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map f₁ =
        (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map f₂

Tactic:
by
      rintro _ _ _ _ ⟨h⟩
      simp only [Functor.map_comp]
      convert! map_comp h <;> apply Cat.FreeRefl.lift'_map

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : HomotopicL f g
⊢ HomotopicL g f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hfg : HomotopicL f g
hgh : HomotopicL g h
⊢ HomotopicL f h

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : HomotopicR f g
⊢ HomotopicR g f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hfg : HomotopicR f g
hgh : HomotopicR g h
⊢ HomotopicR f h

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
h : HomotopicL f g
⊢ HomotopicR f g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
h : HomotopicR f g
⊢ HomotopicL f g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hf : HomotopicL f f'
hg : HomotopicL g g'
⊢ HomotopicL h h'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f : Edge x y
g : Edge y z
h : Edge x z
fac : homMk f ≫ homMk g = homMk h
⊢ f.CompStruct g h

Tactic:
by

Goal state after: