mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: a b : SimplexCategory
f g : a ⟶ b
h : f = g
x : Fin (a.len + 1)
⊢ (Hom.toOrderHom f) x = (Hom.toOrderHom g) x

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategory
i : Fin (y.len + 1)
⊢ Monotone fun x ↦ i

Tactic:
by

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

Goal state before:
pp: ⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌

Tactic:
by

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

Goal state before:
pp: n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const ⦋0⦌ 0 ≫ ⦋0⦌.const m i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd := of ↑(⇑(ConcreteCategory.hom f) '' ⊤)
e : X ⟶ I := ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom f) x, ⋯⟩, monotone' := ⋯ }
m : I ⟶ Y := ofHom { toFun := fun y ↦ ↑y, monotone' := ⋯ }
⊢ Epi e

Tactic:
by

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

Goal state before:
pp: n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
by

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: X Y : NonemptyFinLinOrd
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
by

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

Goal state before:
pp: n : SimplexCategory
f : ⦋0⦌ ⟶ n
⊢ f = ⦋0⦌.const n ((Hom.toOrderHom f) 0)

Tactic:
by

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

Goal state before:
pp: n : SimplexCategory
f : n ⟶ ⦋0⦌
⊢ f = n.const ⦋0⦌ 0

Tactic:
by

Goal state after:
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
inst✝ : Abelian D
⊢ IsIdempotentComplete D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ P = Q

Tactic:
by

Goal state after:
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
⊢ P.p ≫ 0 ≫ Q.p = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ f.f ≫ Q.p = f.f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f ≫ Q.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q R : Karoubi C
g : Q.Hom R
f : P.Hom Q
⊢ P.p ≫ (f.f ≫ g.f) ≫ R.p = f.f ≫ g.f

Tactic:
by

Goal state after:
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'
h : ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
by

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

Goal state before:
pp: n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
h1 : (toOrderHom f) 1 = (toOrderHom g) 1
⊢ f = g

Tactic:
by

Goal state after:
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 ≫ P.p ≫ P.p = P.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
by

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
by

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
this : 1 ≤ 0
⊢ ¬1 ≤ 0

Tactic:
by

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
⊢ (∃ a, f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ j ≤ j

Tactic:
by

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ j < n + 1

Tactic:
by

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ j + l < n + 1

Tactic:
by

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

Goal state before:
pp: ⊢ mkOfSucc 0 = 𝟙 ⦋1⦌

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
by

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑i + j < n + 1

Tactic:
by

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i i' : Fin (l + 1)
hii' : i ≤ i'
⊢ (fun i ↦ ⟨↑i + j, ⋯⟩) i ≤ (fun i ↦ ⟨↑i + j, ⋯⟩) i'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ { X := X, p := 𝟙 X, idem := ⋯ }.X = X

Tactic:
by

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ⦋0⦌.const ⦋l⦌ i ≫ subinterval j l hjl = ⦋0⦌.const ⦋n⦌ ⟨j + ↑i, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
h : P = Q
⊢ (eqToHom h).f = P.p ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin l
⊢ mkOfSucc i ≫ subinterval j l hjl = mkOfSucc ⟨j + ↑i, ⋯⟩

Tactic:
by

Goal state after:
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 := X✝, p := 𝟙 X✝, idem := ⋯ }.p ≫ f ≫ { X := Y✝, p := 𝟙 Y✝, idem := ⋯ }.p = f

Tactic:
by

Goal state after:
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'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom

Tactic:
by

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ diag l ≫ subinterval j l hjl = intervalEdge j l hjl

Tactic:
by

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

Goal state before:
pp: Δ : SimplexCategory
f g : Δ ⟶ ⦋0⦌
⊢ f = g

Tactic:
by

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

Goal state before:
pp: f : ⦋0⦌ ⟶ ⦋0⦌
⊢ f = 𝟙 ⦋0⦌

Tactic:
by

Goal state after:
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
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategory
h : x = y
⊢ Hom.toOrderHom (eqToHom h) = (Fin.castOrderIso ⋯).toOrderEmbedding.toOrderHom

Tactic:
by

Goal state after:
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'
⊢ ε.inverse.map p ≫ ε.inverse.map p = ε.inverse.map p

Tactic:
by

Goal state after:
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
⊢ P.p ≫ (-f.f) ≫ Q.p = -f.f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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
⊢ AddCommGroup (P ⟶ Q)

Tactic:
by

Goal state after:
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 ⟶ P
hp : p.f ≫ p.f = p.f
⊢ { X := P.X, p := p.f, idem := hp }.p ≫ p.f ≫ P.p = p.f

Tactic:
by

Goal state after:
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 ⟶ P
hp : p.f ≫ p.f = p.f
⊢ P.p ≫ p.f ≫ { X := P.X, p := p.f, idem := hp }.p = p.f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete (Karoubi C)

Tactic:
by

Goal state after:
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
⊢ IsIdempotentComplete D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ ((toKaroubi C).obj Y).p ≫ i ≫ P.p = i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ P.p ≫ e ≫ ((toKaroubi C).obj Y).p = e

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
⊢ (toKaroubi C).essImage P

Tactic:
by

Goal state after:
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 ≫ P.p ≫ { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p = P.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p ≫ P.p ≫ P.p = P.p

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p ≫ f.f ≫ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }.p = f.f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ } ⟶ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f ≫ Q.decompId_i = P.decompId_i ≫ { f := f.f, comm := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ P.decompId_p ≫ f = { f := f.f, comm := ⋯ } ≫ Q.decompId_p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ p.op ≫ p.op = p.op

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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)
j j' : J
φ : j ⟶ j'
⊢ (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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 :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ Y.map x✝ ≫ equalizer.ι (𝟙 (F.obj x✝¹)) (p.app x✝¹) = equalizer.ι (𝟙 (F.obj x✝²)) (p.app x✝²) ≫ F.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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 :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
i : Y ⟶ F := { app := fun j ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
j : J
⊢ p.app j ≫ 𝟙 (F.obj j) = p.app j ≫ p.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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 :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
i : Y ⟶ F := { app := fun j ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
j j' : J
φ : j ⟶ j'
⊢ (F.map φ ≫ equalizer.lift (p.app j') ⋯) ≫ equalizer.ι (𝟙 (F.obj j')) (p.app j') =
    (equalizer.lift (p.app j) ⋯ ≫ Y.map φ) ≫ equalizer.ι (𝟙 (F.obj j')) (p.app j')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i'

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ δ i ≫ δ j = δ (j.pred ⋯) ≫ δ i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ j = j'

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ (i.castLT ⋯) ≫ δ j.succ = δ j ≫ δ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ δ i ≫ δ j = δ i ≫ δ i.succ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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
⊢ IsIdempotentComplete (J ⥤ C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
⊢ { X := P.X.obj j, p := P.p.app j, idem := ⋯ }.p ≫
      (P.p.app j ≫ P.X.map φ) ≫ { X := P.X.obj j', p := P.p.app j', idem := ⋯ }.p =
    P.p.app j ≫ P.X.map φ

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ Q.X.map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
⊢ P.p ≫ { app := fun j ↦ (f.app j).f, naturality := ⋯ } ≫ Q.p = { app := fun j ↦ (f.app j).f, naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: 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
X✝ Y✝ : Karoubi (J ⥤ C)
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (karoubiFunctorCategoryEmbedding J C).map a₁✝ = (karoubiFunctorCategoryEmbedding J C).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
⊢ toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C = (Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)

Tactic:
by

Goal state after: