mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h₁ : IsPullback t l r b
inst✝ : Mono r
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃ → x₃ = y₃
⊢ r ≫ 𝟙 X₄ = r

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
x✝¹ : ↑(Y.nonDegenerate n)
x✝ : ↑x✝¹ ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ n < n + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h₁ : IsPullback t l r b
inst✝ : Mono r
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃ → x₃ = y₃
⊢ b ≫ 𝟙 X₄ = b

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ d ≤ d + 1

Tactic:
by simp

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

Goal state before:
pp: ⊢ 3 ≠ 1

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ 1 < 3

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ 1 < 2

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) s ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
hs : s ∉ ∂Δ[d].obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (stdSimplex.objEquiv s)) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) s

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ 0 < 1

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ 0 ∈ {1}ᶜ

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ 2 ∈ {1}ᶜ

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ 3 ∈ {1}ᶜ

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ι₀ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₀ ∧ ι₂ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₂ ∧ ι₃ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₃

Tactic:
by simp

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

Goal state before:
pp: ⊢ 3 ≠ 2

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ 2 < 3

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
inst✝ : Mono i
⊢ ⋯.functor.obj ⊥ = Subcomplex.range i

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
s : X.N
⊢ ¬IsMax s.dim

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
s : X.N
⊢ s.simplex ∉ Set.range ⇑(ConcreteCategory.hom (⊥.ι.app (op ⦋s.dim⦌)))

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ 1 < 2

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ 0 < 2

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ 0 ∈ {2}ᶜ

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ 1 ∈ {2}ᶜ

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ 3 ∈ {2}ᶜ

Tactic:
by simp

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

Goal state before:
pp: case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ (X.spine 0 ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x)).vertex 0 =
    ((X.spine (0 + 1) x).interval 1 0 ⋯).vertex 0

Tactic:
simp [spine, Path.vertex, Truncated.Path.vertex,
      Truncated.spine, Path.interval, Truncated.Path.interval,
      Truncated.Hom.tr, ← SimplexCategory.δ_zero_eq_const]

Goal state after:
case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ (ConcreteCategory.hom (𝟙 (((truncation 1).obj X).obj (op { obj := ⦋0⦌, property := ⋯ }))))
      ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) =
    (ConcreteCategory.hom (((truncation 2).obj X).map (ObjectProperty.homMk (δ 0)).op)) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ 0 < i.succ.castSucc

Tactic:
by simp

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

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₀ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₀ ∧ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁ ∧ ι₃ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₃

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∀ (j : Fin (n + 2 + 1)), (stdSimplex.spineId (n + 2)).vertex j ∈ Λ[n + 2, i].obj (op ⦋0⦌)

Tactic:
by simp

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ 0 < i.succ.castSucc

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X : C
a : A.obj X
Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom ((coyoneda.rightOp.map f).unop.app Y)) (𝟙 (Opposite.unop (Opposite.op Y))) = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝⁵ : Category.{v', u'} V
inst✝⁴ : MonoidalCategory V
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : EnrichedOrdinaryCategory V C
D : Type u''
inst✝¹ : Category.{v'', u''} D
inst✝ : EnrichedOrdinaryCategory V D
X : ForgetEnrichment V D
⊢ (eHomEquiv V)
      ((equivFunctor V D).map
          ((NatIso.ofComponents (fun X ↦ Iso.refl ((𝟭 (ForgetEnrichment V D)).obj X)) ⋯).hom.app X) ≫
        (NatIso.ofComponents (fun X ↦ Iso.refl ((equivInverse V D ⋙ equivFunctor V D).obj X)) ⋯).hom.app
          ((equivFunctor V D).obj X)) =
    (eHomEquiv V) (𝟙 ((equivFunctor V D).obj X))

Tactic:
by simp

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

Goal state before:
pp: K : SSet
φ : 𝟙_ SSet ⟶ K
⊢ (fun x ↦
        { app := fun Δ ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) x,
          naturality := ⋯ })
      ((fun φ ↦ (ConcreteCategory.hom (φ.app (Opposite.op ⦋0⦌))) PUnit.unit) φ) =
    φ

Tactic:
ext Δ ⟨⟩
    dsimp [-Monoidal.tensorUnit_obj]
    rw [← NatTrans.naturality_apply]
    rfl

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

Goal state before:
pp: K : SSet
x : K _⦋0⦌
⊢ (fun φ ↦ (ConcreteCategory.hom (φ.app (Opposite.op ⦋0⦌))) PUnit.unit)
      ((fun x ↦
          { app := fun Δ ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) x,
            naturality := ⋯ })
        x) =
    x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
U : C
⊢ (α_ X.fst Y.fst Z.fst).hom ▷ U ≫ ((X.tensorObj (Y.tensorObj Z)).snd.β U).hom =
    (((X.tensorObj Y).tensorObj Z).snd.β U).hom ≫ U ◁ (α_ X.fst Y.fst Z.fst).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
U : C
⊢ (λ_ X.fst).hom ▷ U ≫ (X.snd.β U).hom = ((tensorUnit.tensorObj X).snd.β U).hom ≫ U ◁ (λ_ X.fst).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
U : C
⊢ (ρ_ X.fst).hom ▷ U ≫ (X.snd.β U).hom = ((X.tensorObj tensorUnit).snd.β U).hom ≫ U ◁ (ρ_ X.fst).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
⊢ ∀ {X Y : TransportEnrichment F (ForgetEnrichment V D)} (f : X ⟶ Y),
    (𝟭 (TransportEnrichment F (ForgetEnrichment V D))).map f ≫
        (Iso.refl ((𝟭 (TransportEnrichment F (ForgetEnrichment V D))).obj Y)).hom =
      (Iso.refl ((𝟭 (TransportEnrichment F (ForgetEnrichment V D))).obj X)).hom ≫
        (forgetEnrichmentEquivFunctor F D e h ⋙ forgetEnrichmentEquivInverse F D e h).map f

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : FreeRefl V
f : x ⟶ y
⊢ motive f

Tactic:
induction x using induction with | _ x
    induction y using induction with | _ y
    obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f
    induction f with
    | nil => simpa using! id x
    | cons _ f h => simpa using! comp_homMk _ f h

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

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
⊢ W ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: case comp_homMk
V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x✝ y✝ : FreeRefl V
x y z : V
f✝ : mk x ⟶ mk y
g : y ⟶ z
h : f✝ = homMk default
⊢ f✝ ≫ homMk g = homMk default

Tactic:
| @comp_homMk x y z _ g h =>

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

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
v : V
⊢ (toFreeRefl V ⋙rq (lift F).toReflPrefunctor).obj v = F.obj v

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F : V ⥤rq D
⊢ ∀ (X Y : V) (f : X ⟶ Y), (toFreeRefl V ⋙rq (lift F).toReflPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (F.map f))

Tactic:
by simp

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 : V
⊢ FreeRefl.homMk (F.map (𝟙rq v)) = 𝟙 (FreeRefl.mk (F.obj v))

Tactic:
by simp

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
⊢ ∀ (v : ↑X),
    (freeReflMap (𝟙 X)).toCatHom.toFunctor.obj (FreeRefl.mk v) = (𝟙 (of (FreeRefl ↑X))).toFunctor.obj (FreeRefl.mk v)

Tactic:
by simp

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
⊢ ∀ {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 simp

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 simp

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 simp

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 simp

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 simp

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:
obtain ⟨f, rfl, rfl⟩ := f
      dsimp [ofNerve₂, ReflQuiv.isoOfEquiv, ReflQuiv.isoOfQuivIso,
        Quiv.isoOfEquiv, nerveHomEquiv_apply]
      simp only [comp_id, id_comp]
      rfl

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 })
⊢ (quotientFunctor V).map (Cat.FreeRefl.homMk (Edge.id x)) = 𝟙 (mk x)

Tactic:
← OneTruncation₂.reflQuiver_id,

Goal state after:
V : Truncated 2
x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ (quotientFunctor V).map (Cat.FreeRefl.homMk (𝟙rq x)) = 𝟙 (mk x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

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

Tactic:
by simp

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 simp

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 simp

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
F G : V.HomotopyCategory ⥤ D
φ : (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀ ⦃x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x✝¹ x✝ : V.HomotopyCategory
f : x✝¹ ⟶ x✝
this : (MorphismProperty.naturalityProperty fun x ↦ φ x.1.as) = ⊤
⊢ ⊤ f

Tactic:
by simp

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

Goal state before:
pp: V W x✝ : Truncated 2
⊢ ∀ (x : x✝.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })),
    (mapHomotopyCategory (𝟙 x✝)).toCatHom.toFunctor.obj (HomotopyCategory.mk x) =
      (𝟙 (Cat.of x✝.HomotopyCategory)).toFunctor.obj (HomotopyCategory.mk x)

Tactic:
by simp

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

Goal state before:
pp: V W X✝ Y✝ Z✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ∀ (x : X✝.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })),
    (mapHomotopyCategory (x✝¹ ≫ x✝)).toCatHom.toFunctor.obj (HomotopyCategory.mk x) =
      ((mapHomotopyCategory x✝¹).toCatHom ≫ (mapHomotopyCategory x✝).toCatHom).toFunctor.obj (HomotopyCategory.mk x)

Tactic:
by simp

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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
⊢ ⟨i, ⋯⟩ ≤ ⟨i + k, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
this : ∀ {X Y : C} (e : X ≅ Y), r.deg X ≤ r.deg Y
⊢ r.deg X = r.deg Y

Tactic:
exact le_antisymm (this e) (this e.symm)

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ 𝟙 X ≫ e.hom = e.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ e.hom ≫ 𝟙 Y = e.hom

Tactic:
by simp

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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
⊢ ⟨i, ⋯⟩ ≤ ⟨i + k, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: ⊢ generators.multiplicativeClosure ≤ ⊤

Tactic:
by simp

Goal state after: