mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) → ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ (Hom.toOrderHom (subinterval j l hjl)) i = ⟨j + ↑i, ⋯⟩

Tactic:
ext

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑((Hom.toOrderHom (subinterval j l hjl)) i) = ↑⟨j + ↑i, ⋯⟩
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ f + g + h' = f + (g + h')

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ (f + g + h').f = (f + (g + h')).f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ 0 + f = f

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (0 + f).f = f.f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ f + 0 = f

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (f + 0).f = f.f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ -f + f = 0

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ (-f + f).f = Karoubi.Hom.f 0
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f + g = g + f

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ (f + g).f = (g + f).f
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom

Tactic:
use ε.functor.obj Y, ε.functor.map i, ε.functor.map e

Goal state after:
case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom

Tactic:
constructor

Goal state after:
case h.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)

case h.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C ↔ IsIdempotentComplete D

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ (𝟙 P).f = (P.decompId_i ≫ P.decompId_p).f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ (toKaroubi C).map P.p = P.decompId_p ≫ P.decompId_i

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (P.decompId_p ≫ P.decompId_i).f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ g = h

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ g.f = h.f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g = h

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g.f = h.f
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y) ∧ i.unop ≫ e.unop = p

Tactic:
constructor

Goal state after:
case h.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y)

case h.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ ↔ IsIdempotentComplete C

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ → IsIdempotentComplete C

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
⊢ i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
constructor

Goal state after:
case h.left
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
⊢ i ≫ e = 𝟙 Y

case h.right
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : J ⥤ C := ⋯
i : Y ⟶ F := ⋯
e : F ⟶ Y := ⋯
⊢ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ =
    eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯

Tactic:
ext

Goal state after:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
j j' : J
φ : j ⟶ j'
⊢ (((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map φ).f =
    (eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯).f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ (k.pred ⋯).castSucc < i

Tactic:
Fin.castSucc_lt_iff_succ_le,

Goal state after:
case inl.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ (k.pred ⋯).succ ≤ i
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
⊢ f.app = g.app

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
x✝ : SimplexCategoryᵒᵖ
⊢ f.app x✝ = g.app x✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ)) x)

Tactic:
fin_cases x

Goal state after:
case «0»
n : ℕ
i : Fin n
⊢ ↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ)) ((fun i ↦ i) ⟨0, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc)) x)

Tactic:
fin_cases x

Goal state after:
case «0»
n : ℕ
i : Fin n
⊢ ↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc)) ((fun i ↦ i) ⟨0, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) x)

Tactic:
fin_cases x

Goal state after:
case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) x)) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)

Tactic:
fin_cases x

Goal state after:
case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩))) =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩))) =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
      { left := ((whiskering C D).obj F).obj (drop.obj Y✝), right := F.obj (point.obj Y✝),
          hom := whiskerRight Y✝.hom F ≫ (constComp SimplexCategoryᵒᵖ Y✝.right F).hom }.hom =
    { left := ((whiskering C D).obj F).obj (drop.obj X✝), right := F.obj (point.obj X✝),
          hom := whiskerRight X✝.hom F ≫ (constComp SimplexCategoryᵒᵖ X✝.right F).hom }.hom ≫
      (const D).map (F.map η.right)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
          { left := ((whiskering C D).obj F).obj (drop.obj Y✝), right := F.obj (point.obj Y✝),
              hom := whiskerRight Y✝.hom F ≫ (constComp SimplexCategoryᵒᵖ Y✝.right F).hom }.hom).app
      n✝ =
    ({ left := ((whiskering C D).obj F).obj (drop.obj X✝), right := F.obj (point.obj X✝),
              hom := whiskerRight X✝.hom F ≫ (constComp SimplexCategoryᵒᵖ X✝.right F).hom }.hom ≫
          (const D).map (F.map η.right)).app
      n✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝¹ ≫ x✝), right := (x✝¹ ≫ x✝).app (point.obj A), w := ⋯ },
      naturality := ⋯ } =
    { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
        naturality := ⋯ } ≫
      { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝, right := x✝.app (point.obj A), w := ⋯ }, naturality := ⋯ }

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
n✝ : SimplexCategoryᵒᵖ
⊢ ({ app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝² ≫ x✝¹), right := (x✝² ≫ x✝¹).app (point.obj A), w := ⋯ },
                naturality := ⋯ }.app
            x✝).left.app
      n✝ =
    (({ app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝², right := x✝².app (point.obj A), w := ⋯ },
                  naturality := ⋯ } ≫
                { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
                  naturality := ⋯ }).app
            x✝).left.app
      n✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
⊢ ({ app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝² ≫ x✝¹), right := (x✝² ≫ x✝¹).app (point.obj A), w := ⋯ },
            naturality := ⋯ }.app
        x✝).right =
    (({ app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝², right := x✝².app (point.obj A), w := ⋯ },
              naturality := ⋯ } ≫
            { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
              naturality := ⋯ }).app
        x✝).right
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) x)

Tactic:
fin_cases x

Goal state after:
case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
⊢ f.app = g.app

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
x✝ : SimplexCategory
⊢ f.app x✝ = g.app x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (const D).map (F.map η.left) ≫
      { left := F.obj (point.obj Y✝), right := ((whiskering C D).obj F).obj (drop.obj Y✝),
          hom := (constComp SimplexCategory (point.obj Y✝) F).inv ≫ whiskerRight Y✝.hom F }.hom =
    { left := F.obj (point.obj X✝), right := ((whiskering C D).obj F).obj (drop.obj X✝),
          hom := (constComp SimplexCategory (point.obj X✝) F).inv ≫ whiskerRight X✝.hom F }.hom ≫
      (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ ((const D).map (F.map η.left) ≫
          { left := F.obj (point.obj Y✝), right := ((whiskering C D).obj F).obj (drop.obj Y✝),
              hom := (constComp SimplexCategory (point.obj Y✝) F).inv ≫ whiskerRight Y✝.hom F }.hom).app
      n✝ =
    ({ left := F.obj (point.obj X✝), right := ((whiskering C D).obj F).obj (drop.obj X✝),
              hom := (constComp SimplexCategory (point.obj X✝) F).inv ≫ whiskerRight X✝.hom F }.hom ≫
          (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F)).app
      n✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ (whiskeringObj C D X✝).map f ≫ { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ } =
    { left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫ (whiskeringObj C D Y✝).map f

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ ((whiskeringObj C D X✝).map f ≫ { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ }).left =
    ({ left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫
        (whiskeringObj C D Y✝).map f).left

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
n✝ : SimplexCategory
⊢ ((whiskeringObj C D X✝).map f ≫
            { left := η.app (point.obj x✝), right := whiskerLeft (drop.obj x✝) η, w := ⋯ }).right.app
      n✝ =
    ({ left := η.app (point.obj x✝¹), right := whiskerLeft (drop.obj x✝¹) η, w := ⋯ } ≫
            (whiskeringObj C D Y✝).map f).right.app
      n✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X = Y

Tactic:
ext

Goal state after:
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X.len = Y.len
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
⊢ InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) ≫
      InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) =
    𝟙 (skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌)

Tactic:
ext

Goal state after:
X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
x✝ : ↑(skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌).toLinOrd
⊢ (LinOrd.Hom.hom
        (InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) ≫
            InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 })).hom)
      x✝ =
    (LinOrd.Hom.hom (𝟙 (skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌)).hom) x✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
⊢ InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) ≫
      InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) =
    𝟙 X

Tactic:
ext

Goal state after:
X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
x✝ : ↑X.toLinOrd
⊢ (LinOrd.Hom.hom
        (InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) ≫
            InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ })).hom)
      x✝ =
    (LinOrd.Hom.hom (𝟙 X).hom) x✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (δ₀Iter (i + 1) h)) k = (ConcreteCategory.hom (δ 0 ≫ δ₀Iter i ⋯)) k

Tactic:
ext

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter (i + 1) h)) k) = ↑((ConcreteCategory.hom (δ 0 ≫ δ₀Iter i ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (δ₀Iter i hi ≫ δ j)) k = (ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k

Tactic:
ext

Goal state after:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter i hi ≫ δ j)) k) = ↑((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)