mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x✝ : G₀
⊢ (fst G₀ H₀) ((inl G₀ H₀) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x✝ : H₀
⊢ (snd G₀ H₀) ((inr G₀ H₀) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝¹ : GroupWithZero G₀
inst✝ : GroupWithZero H₀
x✝ : G₀
⊢ (fst G₀ H₀) ((inl G₀ H₀) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝¹ : GroupWithZero G₀
inst✝ : GroupWithZero H₀
x✝ : H₀
⊢ (snd G₀ H₀) ((inr G₀ H₀) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : MulZeroOneClass G
inst✝ : MulZeroOneClass H
f : G →*₀ H
⊢ f 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
⊢ ⟨f 0, ⋯⟩ ≠ ⟨f 1, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: H : Type u_2
inst✝ : CommGroupWithZero H
x✝ : H
⊢ x✝ ∈ MonoidHom.mker MonoidWithZero.inverse ↔ x✝ ∈ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 = 1 ∨ 1 < f 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
⊢ 1 ≠ 1 → 1 < f 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
⊢ f 1 = ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ (if h : f 0 = 0 then 0 else ↑⟨Units.mk0 (f 0) h, ⋯⟩) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case h
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ (restrict₀ f) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
⊢ f 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
⊢ f 1 * ↑1 = f 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ ⦋0⦌.len ≤ n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ r s : A
hr : f r ≠ 0
hs : f s ≠ 0
⊢ ↑(Units.mk0 (f r) hr) ∈ range ⇑f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ r s : A
hr : f r ≠ 0
hs : f s ≠ 0
⊢ ↑(Units.mk0 (f s) hs) ∈ range ⇑f

Tactic:
simp

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

Goal state before:
pp: X : FinPartOrd
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

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

Goal state before:
pp: X Y Z : FinPartOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

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

Goal state before:
pp: X : LinOrd
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

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

Goal state before:
pp: X Y Z : LinOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

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

Goal state before:
pp: X Y : LinOrd
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

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

Goal state before:
pp: X Y : LinOrd
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ ((h.hom ≫ h.inv) { down := a }).down = a

Tactic:
simp

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (𝟙 X { down := a }).down = a
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ ((h.inv ≫ h.hom) { down := a }).down = a

Tactic:
simp

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (𝟙 Y { down := a }).down = a
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X✝ Y✝ : Skeleton
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : incl.map a₁✝ = incl.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by
    simpa using TypeCat.homEquiv.symm.injective (InducedCategory.homEquiv.symm.injective h)

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

Goal state before:
pp: X : NonemptyFinLinOrd
x : ↑X.toLinOrd
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

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

Goal state before:
pp: X Y Z : NonemptyFinLinOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toLinOrd
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ i.succ ∈ Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ 0 ∈ Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ =
    0

Tactic:
factorThru_right,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
      ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0)
      ⋯ =
    0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ 0 ∈ Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ i ∈ Finset.univ

Tactic:
simp

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

Goal state before:
pp: case refine_2
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ ofHom { toFun := φ, monotone' := ?refine_1 } ≫ f = 𝟙 Y

Tactic:
ext b

Goal state after:
case refine_2
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
b : ↑Y.toLinOrd
⊢ (LinOrd.Hom.hom (ofHom { toFun := φ, monotone' := ?refine_1 } ≫ f).hom) b = (LinOrd.Hom.hom (𝟙 Y).hom) b
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:
simp

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

Goal state before:
pp: 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'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv

Tactic:
simp

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:
simp

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        0) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        0)

Tactic:
simp

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + j = j + ↑i✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        1) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        1)

Tactic:
simp

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + 1 + j = j + ↑i✝ + 1
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => 0
                  | 1 => Fin.last l,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        0) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j, ⋯⟩
                | 1 => ⟨j + l, ⋯⟩,
              monotone' := ⋯ }))
        0)

Tactic:
simp

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => 0
                  | 1 => Fin.last l,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        1) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j, ⋯⟩
                | 1 => ⟨j + l, ⋯⟩,
              monotone' := ⋯ }))
        1)

Tactic:
simp

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ l + j = j + l
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:
coe_p,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ P.p ≫ P.p ≫ 𝟙 P.X = P.p
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:
coe_p,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ 𝟙 P.X ≫ P.p ≫ P.p = P.p
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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

Tactic:
simp

Goal state after:
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

Tactic:
simp

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

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j

Tactic:
simp

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

Goal state before:
pp: case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j

Tactic:
simp

Goal state after:
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ False
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 Y : J ⥤ C
f : X ⟶ Y
j : J
⊢ (((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f).app j).f =
    ((eqToHom ⋯ ≫ ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯).app j).f

Tactic:
simp

Goal state after:
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
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro j

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
⊢ ∀ (Y : J) (f : j ⟶ Y),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
      eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯
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 φ).f =
    (eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map φ ≫ eqToHom ⋯).f

Tactic:
simp

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.pred ⋯) = j

Tactic:
simp

Goal state after:
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ j - 1 = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j, ⋯⟩
⊢ ↑(⟨j, ⋯⟩.castPred ⋯) = j

Tactic:
simp

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.pred ⋯) = j

Tactic:
simp

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ ↑(⟨j + 1, ⋯⟩.castPred ⋯) = j

Tactic:
simp

Goal state after:
case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < ⦋n⦌.len + 1
h✝¹ : ¬⟨j, ⋯⟩ < ⟨i + 1, ⋯⟩
h✝ : ¬⟨i, ⋯⟩ < ⟨j + 1, ⋯⟩
⊢ False
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_obj.h_obj
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
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1

Tactic:
intro j

Goal state after:
case h_obj.h_obj
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
⊢ ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj j =
    (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
simp

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

Goal state before:
pp: case cast.zero
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ j.predAbove (i.castSucc.predAbove (Fin.castSucc 0)) = i.predAbove (j.succ.predAbove (Fin.castSucc 0))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ (X.augment X₀ f w).hom.app (op ⦋0⦌) = f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ ∀ (a : Fin (i + 1)), (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑a.succ • X.δ a.succ) = 0

Tactic:
intro j

Goal state after:
case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
j : Fin (i + 1)
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑j.succ • X.δ j.succ) = 0
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match 0 with
      | 0 => (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow
      | n.succ =>
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯) ≫
      (match 0 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow

Tactic:
simp

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

Goal state before:
pp: 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

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n✝ : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 =
    (match n✝ + 1 with
      | 0 => (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow
      | n.succ =>
        (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
          ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯) ≫
      (match n✝ + 1 with
        | 0 => ⊤
        | n.succ => Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X ^⦋0⦌
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ (X.augment X₀ f w).hom.app ⦋0⦌ = f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Augmented C
⊢ X.rightOp.leftOp.right = X.right

Tactic:
simp

Goal state after: