awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
rw : 𝟙 ((quotientFunctor V).obj (Cat.FreeRefl.mk x)) = 𝟙 (mk x)
⊢ homMk (Edge.id x) = 𝟙 (mk x)

Tactic:
rw [homMk, ← OneTruncation₂.reflQuiver_id, Cat.FreeRefl.homMk_id,
    CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.Cat.FreeRefl.homMk_id, SSet.OneTruncation₂.reflQuiver_id, CategoryTheory.Functor.map_id, SSet.Truncated.HomotopyCategory.homMk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ 𝟙 ((quotientFunctor V).obj (Cat.FreeRefl.mk x)) = 𝟙 (mk x)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ 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:
simpa [homMk] using CategoryTheory.Quotient.sound _
    (OneTruncation₂.HoRel₂.of_compStruct h)

Premises used: SSet.OneTruncation₂.HoRel₂.of_compStruct, SSet.Truncated.HomotopyCategory.homMk, CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x y
⊢ ∃ (i :
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) ×
      (y :
        V.obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
              OneTruncation₂._proof_1))) ×
        Edge x y),
    Arrow.mk (homMk e) =
      Arrow.mk
        (homMk
          (i.snd (β :=
                fun
                  (x :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ×
                  Edge x y).snd
            (β :=
            fun
              (y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            Edge
              (i.fst (β :=
                fun
                  (x :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ×
                  Edge x y))
              y)))

Tactic:
⟨⟨x, y, e⟩, rfl⟩

Premises used: Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x y
⊢ ∃ (i :
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) ×
      (y :
        V.obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
              OneTruncation₂._proof_1))) ×
        Edge x y),
    Arrow.mk (homMk e) =
      Arrow.mk
        (homMk
          (i.snd (β :=
                fun
                  (x :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ×
                  Edge x y).snd
            (β :=
            fun
              (y :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            Edge
              (i.fst (β :=
                fun
                  (x :
                    V.obj
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (y :
                  V.obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ×
                  Edge x y))
              y)))

Tactic:
exact ⟨⟨x, y, e⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
h :
  ∀ ⦃X Y : V.HomotopyCategory⦄ (f : X ⟶ Y),
    morphismPropertyHomMk V f ↔
      MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f
⊢ morphismPropertyHomMk V =
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)

Tactic:
ext _ _ f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
X Y : V.HomotopyCategory
f : X ⟶ Y
h :
  morphismPropertyHomMk V f →
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f
h₁ :
  MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f →
    morphismPropertyHomMk V f
⊢ morphismPropertyHomMk V f ↔
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
X Y : V.HomotopyCategory
i :
  (x :
    V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))) ×
    (y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) ×
      Edge x y
⊢ MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)
    (homMk
      (i.snd (β :=
            fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ×
              Edge x y).snd
        (β :=
        fun
          (y :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ↦
        Edge
          (i.fst (β :=
            fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ×
              Edge x y))
          y)))

Tactic:
MorphismProperty.map_mem_strictMap _ _ _ ⟨_⟩

Premises used: CategoryTheory.MorphismProperty.map_mem_strictMap, CategoryTheory.MorphismProperty.ofHoms.mk, SSet.Truncated.HomotopyCategory.homMk, SSet.Truncated.HomotopyCategory.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
X Y : V.HomotopyCategory
i :
  (x :
    V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))) ×
    (y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) ×
      Edge x y
⊢ MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)
    (homMk
      (i.snd (β :=
            fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ×
              Edge x y).snd
        (β :=
        fun
          (y :
            V.obj
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))) ↦
        Edge
          (i.fst (β :=
            fun
              (x :
                V.obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (y :
              V.obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ×
              Edge x y))
          y)))

Tactic:
exact MorphismProperty.map_mem_strictMap _ _ _ ⟨_⟩

Premises used: CategoryTheory.MorphismProperty.map_mem_strictMap
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
X_1 Y_1 : V.HomotopyCategory
X Y : Cat.FreeRefl (OneTruncation₂ V)
fst fst_1 : OneTruncation₂ V
e : fst ⟶ fst_1
⊢ morphismPropertyHomMk V (X :=
    (quotientFunctor V).obj
      (Cat.FreeRefl.mk
        (Sigma.fst (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
          (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
            (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e)))))
    (Y :=
    (quotientFunctor V).obj
      (Cat.FreeRefl.mk
        (Sigma.fst (β := fun (y : OneTruncation₂ V) ↦
          Sigma.fst (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
              (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
                (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e)) ⟶
            y)
          (Sigma.snd (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
            (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
              (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e))))))
    ((quotientFunctor V).map
      (Cat.FreeRefl.homMk
        (Sigma.snd (β := fun (y : OneTruncation₂ V) ↦
          Sigma.fst (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
              (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
                (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e)) ⟶
            y)
          (Sigma.snd (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
            (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
              (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e))))))

Tactic:
morphismPropertyHomMk_of_edge e

Premises used: SSet.Truncated.HomotopyCategory.homMk, SSet.Truncated.HomotopyCategory.mk, SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_of_edge
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
X_1 Y_1 : V.HomotopyCategory
X Y : Cat.FreeRefl (OneTruncation₂ V)
fst fst_1 : OneTruncation₂ V
e : fst ⟶ fst_1
⊢ morphismPropertyHomMk V (X :=
    (quotientFunctor V).obj
      (Cat.FreeRefl.mk
        (Sigma.fst (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
          (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
            (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e)))))
    (Y :=
    (quotientFunctor V).obj
      (Cat.FreeRefl.mk
        (Sigma.fst (β := fun (y : OneTruncation₂ V) ↦
          Sigma.fst (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
              (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
                (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e)) ⟶
            y)
          (Sigma.snd (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
            (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
              (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e))))))
    ((quotientFunctor V).map
      (Cat.FreeRefl.homMk
        (Sigma.snd (β := fun (y : OneTruncation₂ V) ↦
          Sigma.fst (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
              (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
                (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e)) ⟶
            y)
          (Sigma.snd (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y))
            (Sigma.mk (β := fun (x : OneTruncation₂ V) ↦ (y : OneTruncation₂ V) × (x ⟶ y)) fst
              (Sigma.mk (β := fun (y : OneTruncation₂ V) ↦ fst ⟶ y) fst_1 e))))))

Tactic:
exact morphismPropertyHomMk_of_edge e

Premises used: SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_of_edge
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x ⟶ y
h : ⊤ f
obtain :
  ∀ (f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)),
    ⊤ ((quotientFunctor V).map f) → (morphismPropertyHomMk V).multiplicativeClosure ((quotientFunctor V).map f)
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f

Premises used: SSet.Truncated.HomotopyCategory.quotientFunctor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
rw :
  (strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)).multiplicativeClosure
    ((quotientFunctor V).map f)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ((quotientFunctor V).map f)

Tactic:
rw [morphismPropertyHomMk_eq_strictMap]

Premises used: SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
⊢ (strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)).multiplicativeClosure
    ((quotientFunctor V).map f)

Tactic:
strictMap_multiplicativeClosure_le _ _ _ ?_

Premises used: CategoryTheory.MorphismProperty.strictMap_multiplicativeClosure_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
refine :
  strictMap (multiplicativeClosure (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V))) (quotientFunctor V)
    ((quotientFunctor V).map f)
⊢ (strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)).multiplicativeClosure
    ((quotientFunctor V).map f)

Tactic:
refine strictMap_multiplicativeClosure_le _ _ _ ?_

Premises used: CategoryTheory.MorphismProperty.strictMap_multiplicativeClosure_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
rw : strictMap ⊤ (quotientFunctor V) ((quotientFunctor V).map f)
⊢ strictMap (multiplicativeClosure (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V))) (quotientFunctor V)
    ((quotientFunctor V).map f)

Tactic:
rw [Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk]

Premises used: CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
⊢ ⊤ f

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
⊢ strictMap ⊤ (quotientFunctor V) ((quotientFunctor V).map f)

Tactic:
exact map_mem_strictMap _ _ _ (by simp)

Premises used: CategoryTheory.MorphismProperty.map_mem_strictMap
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst : W.IsMultiplicative
hW :
  ∀
    {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    (e : Edge x y), W (homMk e)
⊢ W ≤ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst : W.IsMultiplicative
hW :
  ∀
    {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    (e : Edge x y), W (homMk e)
rw : morphismPropertyHomMk V ≤ W
⊢ ⊤ ≤ W

Tactic:
rw [← multiplicativeClosure_morphismPropertyHomMk,
      MorphismProperty.multiplicativeClosure_le_iff]

Premises used: SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk, CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
obj :
  V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)) →
    D
map :
  {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))} →
    Edge x y → (obj x ⟶ obj y)
map_id :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀
    {x₀ x₁ x₂ :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ 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)
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ map e₀₁ ≫ map e₁₂ = map e₀₂

Tactic:
map_comp h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
obj :
  V.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)) →
    D
map :
  {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))} →
    Edge x y → (obj x ⟶ obj y)
map_id :
  ∀
    (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀
    {x₀ x₁ x₂ :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ 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)
x₀ x₁ x₂ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
e_1 :
  (Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) ⟶
      Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
        (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
        (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₂)) =
    (obj x₀ ⟶ obj x₂)
e_3 :
  Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
      (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₀) =
    obj x₀
e_4 :
  Functor.obj.{u, v_1, u, u_1} (C := Cat.FreeRefl (OneTruncation₂ V))
      (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (Functor.obj (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) x₁) =
    obj x₁
⊢ CategoryTheory.Functor.map (Cat.FreeRefl.lift' obj (fun {v w : OneTruncation₂ V} (f : v ⟶ w) ↦ map f) map_id)
      (CategoryTheory.Functor.map (Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)) (Quiver.Hom.toPath e₀₁)) =
    map e₀₁

Tactic:
apply Cat.FreeRefl.lift'_map

Premises used: CategoryTheory.Cat.FreeRefl.lift'_map