mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
i : J.R
⊢ ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).ι.app (WalkingMultispan.right i) ≫
      (Iso.refl ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).pt).hom =
    (c.map F).ι.app (WalkingMultispan.right i)

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
i : J.R
⊢ ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).ι.app (WalkingMultispan.right i) ≫
      (Iso.refl ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).pt).hom =
    (c.map F).ι.app (WalkingMultispan.right i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
⊢ ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i}

Tactic:
;

Goal state after:
n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
⊢ ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
k : Fin (⦋n⦌.len + 1)
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤

Tactic:
;

Goal state after:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
this : ∀ (j : Fin (n + 1)), j ≠ i → j ∈ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
k : Fin (⦋n⦌.len + 1)
⊢ k ∈ Finset.image ⇑(SimplexCategory.Hom.toOrderHom f) ⊤ ∪ {i} ↔ k ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ U i ⊓ U j = U j ⊓ U i

Tactic:
inf_comm

Goal state after:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ U j ⊓ U i = U j ⊓ U i
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ x₁ ∈ V i₁ i₂

Tactic:
;

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ x₁ ∈ V i₁ i₂
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ x₁ ∈ U i₁ ⊓ U i₂

Tactic:
;

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ x₁ ∈ U i₁ ⊓ U i₂
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ x₁ ∈ V i₁ i₂

Tactic:
;

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ x₁ ∈ V i₁ i₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : {j}ᶜᶜ.card = 1
h : ¬stdSimplex.face {j}ᶜ ≤ A
⊢ False

Tactic:
;

Goal state after:
n : ℕ
A : Δ[n + 1].Subcomplex
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : {j}ᶜᶜ.card = 1
h : ¬stdSimplex.face {j}ᶜ ≤ A
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ x₁ ∈ U i₁ ⊓ U i₂

Tactic:
;

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ x₁ ∈ U i₁ ⊓ U i₂
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case refine_1
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : (MultispanShape.prod ι).R
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ c.multispanIndex.right i₁
x₂ : X
h₂ : x₂ ∈ c.multispanIndex.right i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₂, h₂⟩
⊢ (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) ⟨x₂, h₂⟩

Tactic:
dsimp at i₁ i₂ h₁ h₂
    obtain rfl : x₁ = x₂ := by simpa using h
    have eq₁ := e.ιColimitType_map (WalkingMultispan.Hom.fst (J := .prod ι) ⟨i₁, i₂⟩)
      ⟨x₁, by dsimp; rw [c.eq_inf]; exact ⟨h₁, h₂⟩⟩
    have eq₂ := e.ιColimitType_map (WalkingMultispan.Hom.snd (J := .prod ι) ⟨i₁, i₂⟩)
      ⟨x₁, by dsimp; rw [c.eq_inf]; exact ⟨h₁, h₂⟩⟩
    dsimp [e] at eq₁ eq₂
    rw [eq₁, eq₂]

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

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst✝ : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ U i ⊓ U j = U j ⊓ U i

Tactic:
inf_comm

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst✝ : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ U j ⊓ U i = U j ⊓ U i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Mono (Subcomplex.homOfLE ⋯)

Tactic:
;

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ Mono (Subcomplex.homOfLE ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 ≤ n

Tactic:
;

Goal state after:
n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ 2 ≤ n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_2.inl
⊢ ∀ {i : Fin (2 + 1)} (j : Fin 2), 0 < ↑i → ↑i < 2 → #{i, j.castSucc, j.succ} ≤ 2

Tactic:
;

Goal state after:
case refine_2.inl
⊢ ∀ {i : Fin (2 + 1)} (j : Fin 2), 0 < ↑i → ↑i < 2 → #{i, j.castSucc, j.succ} ≤ 2
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₃ ⟶ X₄
b : X₂ ⟶ X₄
sq : IsPushout l t r b
ht : Mono t
⊢ Mono r

Tactic:
exact Limits.Types.pushoutCocone_inr_mono_of_isColimit sq.flip.isColimit

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

Goal state before:
pp: case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.mk (Rel f g) x)) = Quot.mk (Rel f g) x

Tactic:
;

Goal state after:
case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.mk (Rel f g) x)) = Quot.mk (Rel f g) x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout' f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.mk (Rel' f g) x)) = Quot.mk (Rel' f g) x

Tactic:
;

Goal state after:
case mk
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x✝ : Pushout' f g
x : X₁ ⊕ X₂
⊢ Quot.lift (Quot.mk (Rel' f g)) ⋯ (Quot.lift (Quot.mk (Rel f g)) ⋯ (Quot.mk (Rel' f g) x)) = Quot.mk (Rel' f g) x
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 : IsPushout t l r b
x : (span t l).obj none
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom (t ≫ r)) x

Tactic:
;

Goal state after:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x : (span t l).obj none
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom (t ≫ r)) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
inst✝ : X.IsStrictSegal
d : ℕ
hd : ⦋d + 1⦌.len ≤ n + 1
x y : X.obj (op { obj := ⦋d + 1⦌, property := hd })
h :
  ∀ (i : Fin (d + 1)),
    (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ hd).op)) x =
      (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ hd).op)) y
i : Fin (d + 1)
⊢ (X.spine (d + 1) hd x).arrow i = (X.spine (d + 1) hd y).arrow i

Tactic:
;

Goal state after:
n : ℕ
X : Truncated (n + 1)
inst✝ : X.IsStrictSegal
d : ℕ
hd : ⦋d + 1⦌.len ≤ n + 1
x y : X.obj (op { obj := ⦋d + 1⦌, property := hd })
h :
  ∀ (i : Fin (d + 1)),
    (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ hd).op)) x =
      (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ hd).op)) y
i : Fin (d + 1)
⊢ (X.spine (d + 1) hd x).arrow i = (X.spine (d + 1) hd y).arrow i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).vertex
      i =
    f.vertex i.castSucc

Tactic:
rw [spine_vertex, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    SimplexCategory.const_comp, spineToSimplex_vertex]

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j)) i) = f.vertex i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).vertex
      i =
    f.vertex i.succ

Tactic:
rw [spine_vertex, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    SimplexCategory.const_comp, spineToSimplex_vertex]

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j)) i) = f.vertex i.succ
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₀

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 0).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
  exact (horn.isColimit 2).fac _ (.right ⟨0, by simp⟩)

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

Goal state before:
pp: case hᵥ.«0»
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
⊢ f.vertex ((fun i ↦ i) ⟨0, ⋯⟩) = g.vertex ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
;

Goal state after:
case hᵥ.«0»
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
⊢ f.vertex ((fun i ↦ i) ⟨0, ⋯⟩) = g.vertex ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
X✝ : ↑chosenTerminal
⊢ ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).obj X✝ = x✝.obj X✝

Tactic:
;

Goal state after:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
X✝ : ↑chosenTerminal
⊢ ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).obj X✝ = x✝.obj X✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝⁴ : BinaryFan X Y
x✝³ : x✝⁴.pt ⟶ of (↑X × ↑Y)
h1 : x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝⁴.fst
h2 : x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝⁴.snd
x✝² x✝¹ : ↑x✝⁴.pt
x✝ : x✝² ⟶ x✝¹
⊢ x✝³.toFunctor.map x✝ ≍ Prod.mkHom (x✝⁴.fst.toFunctor.map x✝) (x✝⁴.snd.toFunctor.map x✝)

Tactic:
;

Goal state after:
X Y : Cat
x✝⁴ : BinaryFan X Y
x✝³ : x✝⁴.pt ⟶ of (↑X × ↑Y)
h1 : x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝⁴.fst
h2 : x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝⁴.snd
x✝² x✝¹ : ↑x✝⁴.pt
x✝ : x✝² ⟶ x✝¹
⊢ x✝³.toFunctor.map x✝ ≍ Prod.mkHom (x✝⁴.fst.toFunctor.map x✝) (x✝⁴.snd.toFunctor.map x✝)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝⁴ : BinaryFan X Y
x✝³ : x✝⁴.pt ⟶ of (↑X × ↑Y)
h1 : x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝⁴.fst
h2 : x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝⁴.snd
x✝² x✝¹ : ↑x✝⁴.pt
x✝ : x✝² ⟶ x✝¹
⊢ x✝³.toFunctor.map x✝ ≍
    Prod.mkHom ((x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom).toFunctor.map x✝) ((x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom).toFunctor.map x✝)

Tactic:
;

Goal state after:
X Y : Cat
x✝⁴ : BinaryFan X Y
x✝³ : x✝⁴.pt ⟶ of (↑X × ↑Y)
h1 : x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝⁴.fst
h2 : x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝⁴.snd
x✝² x✝¹ : ↑x✝⁴.pt
x✝ : x✝² ⟶ x✝¹
⊢ x✝³.toFunctor.map x✝ ≍
    Prod.mkHom ((x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom).toFunctor.map x✝) ((x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom).toFunctor.map x✝)
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : (coyoneda.obj (op (𝟙_ C))).obj Z
f : (coyoneda.obj (op (𝟙_ C))).obj X
g : (coyoneda.obj (op (𝟙_ C))).obj Y
⊢ (ConcreteCategory.hom
          (((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
            (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom)).toFun
      ((f, g), h) =
    (ConcreteCategory.hom
          ((α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y)
                ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
            (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
              ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2))).toFun
      ((f, g), h)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : (coyoneda.obj (op (𝟙_ C))).obj Z
f : (coyoneda.obj (op (𝟙_ C))).obj X
g : (coyoneda.obj (op (𝟙_ C))).obj Y
⊢ (ConcreteCategory.hom
          (((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
            (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom)).toFun
      ((f, g), h) =
    (ConcreteCategory.hom
          ((α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y)
                ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
            (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
              ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2))).toFun
      ((f, g), h)
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g) ⊗ₘ h)) ≫ (α_ X Y Z).hom =
    (λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (g ⊗ₘ h))

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g) ⊗ₘ h)) ≫ (α_ X Y Z).hom =
    (λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (g ⊗ₘ h))
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X : C
⊢ (ρ_ ((coyoneda.obj (op (𝟙_ C))).obj X)).hom =
    (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun x ↦ 𝟙 (unop (op (𝟙_ C)))) ≫
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (ρ_ X).hom

Tactic:
ext ⟨f, ⟨⟩⟩
      simp [unitors_inv_equal]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case refl
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯

Tactic:
;

Goal state after:
case refl
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g g' : b ⟶ c
β : g = g'
⊢ hComp (eqToHom ⋯) (eqToHom β) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: case refl.refl
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯

Tactic:
;

Goal state after:
case refl.refl
C : Type u_1
inst✝ : EnrichedCategory Cat C
a b c : CatEnriched C
f : a ⟶ b
g : b ⟶ c
⊢ hComp (eqToHom ⋯) (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
h1 : (f ≫ g) ≫ h = f ≫ g ≫ h
h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i
h3 : (g ≫ h) ≫ i = g ≫ h ≫ i
h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
⊢ hComp (eqToIso h1).hom (𝟙 i) ≫ (eqToIso h2).hom ≫ hComp (𝟙 f) (eqToIso h3).hom = (eqToIso h4).hom ≫ (eqToIso pf✝).hom

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
h1 : (f ≫ g) ≫ h = f ≫ g ≫ h
h2 : (f ≫ g ≫ h) ≫ i = f ≫ (g ≫ h) ≫ i
h3 : (g ≫ h) ≫ i = g ≫ h ≫ i
h4 : ((f ≫ g) ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
⊢ hComp (eqToIso h1).hom (𝟙 i) ≫ (eqToIso h2).hom ≫ hComp (𝟙 f) (eqToIso h3).hom = (eqToIso h4).hom ≫ (eqToIso pf✝).hom