mathlib-initiative/mathlib-tactics huggingface dataset:
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)})
⊢ ∀ x ∈ v '' {i | 1 < f (v i)}, x = 1 ∨ 1 < f x

Tactic:
grind

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

Goal state before:
pp: case inl
ι✝ : 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)
y : G
x✝² : y ∈ closure (v '' s)
hy : y ≠ 1 → 1 < f y
x✝¹ : 1 ∈ closure (v '' s)
hx : 1 ≠ 1 → 1 < f 1
x✝ : 1 * y ≠ 1
⊢ 1 < f (1 * y)

Tactic:
grind

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

Goal state before:
pp: case inr.inl
ι✝ : 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)
x : G
x✝² : x ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hx' : x ≠ 1
x✝¹ : 1 ∈ closure (v '' s)
hy : 1 ≠ 1 → 1 < f 1
x✝ : x * 1 ≠ 1
⊢ 1 < f (x * 1)

Tactic:
grind

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

Goal state before:
pp: case refine_2.a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ u⁻¹ ∈ f.valueGroup

pp: case a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ v ∈ f.valueGroup

Tactic:
· apply inv_mem_valueGroup
      use a

Goal state after:
case a
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ v ∈ f.valueGroup
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case none
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
⊢ none = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mpr
X : FintypeCat
⊢ homMk id = 𝟙 X

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mpr
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
⊢ homMk (g ∘ f) = homMk f ≫ homMk g

Tactic:
rfl

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
⊢ (𝟙 X { down := a }).down = a

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

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

Tactic:
rfl

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

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
x✝² x✝¹ : ULift.{u, 0} (Fin 1)
x✝ : x✝² ≤ x✝¹
⊢ (fun x ↦ a₁) x✝² ≤ (fun x ↦ a₁) x✝¹

Tactic:
rfl

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

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
x✝² x✝¹ : ULift.{u, 0} (Fin 1)
x✝ : x✝² ≤ x✝¹
⊢ (fun x ↦ a₂) x✝² ≤ (fun x ↦ a₂) x✝¹

Tactic:
rfl

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

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }

Tactic:
rfl

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

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }

Tactic:
rfl

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

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : (LinOrd.Hom.hom f.hom) a < m
h₂ : (LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 0 } = { down := 0 }

Tactic:
rfl

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

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : (LinOrd.Hom.hom f.hom) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 0 } = { down := 1 }

Tactic:
rfl

Goal state after:
case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : (LinOrd.Hom.hom f.hom) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 0 } = { down := 1 }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : ¬(LinOrd.Hom.hom f.hom) a < m
h₂ : (LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 1 } = { down := 0 }

Tactic:
rfl

Goal state after:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : ¬(LinOrd.Hom.hom f.hom) a < m
h₂ : (LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 1 } = { down := 0 }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : ¬(LinOrd.Hom.hom f.hom) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom) a ≤ m
⊢ { down := 1 } = { down := 1 }

Tactic:
rfl

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 m ((Hom.toOrderHom (⦋0⦌.const m i)) 0)

Tactic:
rfl

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

Goal state before:
pp: n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) 0) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) 0)

Tactic:
rfl

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

Goal state before:
pp: case h
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 : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'

Tactic:
grind

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0))) 0

Tactic:
rfl

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 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0))) 0

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: 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' := ε.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
⊢ ε.counit.app X' ≫ p ≫ ε.counitInv.app X' = φ.inv ≫ p ≫ φ.hom

Tactic:
rfl

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

Goal state before:
pp: 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
⊢ (𝟙 Y).unop = 𝟙 (unop Y)

Tactic:
rfl

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

Goal state before:
pp: 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
⊢ p.op.unop = p

Tactic:
rfl

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
⊢ δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i

Tactic:
rfl

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'
h : (P.p ≫ P.p).app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
rw [NatTrans.comp_app] at h

Goal state after:
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'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
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
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

Tactic:
rfl

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

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

Tactic:
by
  ext k : 3
  dsimp [δ, σ]
  rcases le_or_gt k i with (hik | hik)
  · rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hik)]
    rcases le_or_gt k (j.castSucc) with (hjk | hjk)
    · rw [Fin.predAbove_of_le_castSucc _ _
      (Fin.castSucc_le_castSucc_iff.mpr hjk), Fin.castPred_castSucc,
      Fin.predAbove_of_le_castSucc _ _ hjk, Fin.succAbove_of_castSucc_lt, Fin.castSucc_castPred]
      rw [Fin.castSucc_castPred]
      exact hjk.trans_lt H
    · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hjk),
      Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_pred_eq_pred_castSucc]
      rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]
  · rw [Fin.succAbove_of_le_castSucc _ _ (Fin.succ_le_castSucc_iff.mpr hik)]
    have hjk := H.trans hik
    rw [Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.predAbove_of_castSucc_lt _ _
      (Fin.castSucc_lt_succ_iff.mpr hjk.le),
    Fin.pred_succ, Fin.succAbove_of_le_castSucc, Fin.succ_pred]
    rwa [Fin.le_castSucc_pred_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
j : ℕ
⊢ ∑ x, (-1) ^ ↑x • F.map (X.δ x) = ∑ i, (-1) ^ ↑i • (((SimplicialObject.whiskering C D).obj F).obj X).δ i

Tactic:
rfl

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

Goal state before:
pp: 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, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
n : ℕ
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X n =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X n

Tactic:
rfl

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

Goal state before:
pp: 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, ⋯⟩))

Tactic:
rfl

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
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ∑ x, (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f =
    ∑ x, (-1) ^ ↑x • P.p.app (op ⦋n + 1⦌) ≫ P.X.δ x

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case «0»
n : ℕ
i : Fin n
⊢ ↑i.castSucc.castSucc = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 0)

Tactic:
rfl

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

Goal state before:
pp: case «1»
n : ℕ
i : Fin n
⊢ ↑i.succ.succ = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Tactic:
rfl

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 0

Tactic:
rfl

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 0

Tactic:
rfl

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 0

Tactic:
rfl

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 : CosimplicialObject C
n : ℕ
⊢ ∑ i, (-1) ^ ↑i • X.δ i = ∑ i, (-1) ^ ↑i • (((cosimplicialSimplicialEquiv C).functor.obj (op X)).δ i).unop

Tactic:
rfl

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
rw [e0, e1] at this
    exact Not.elim (by decide) this

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 0
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
rw [e0, e1] at this
    exact Not.elim (by decide) this

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
rw [e0, e1] at this
    exact Not.elim (by decide) this

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

Goal state before:
pp: i n m : ℕ
hi : n + i = m
x✝¹ x✝ : Fin (⦋n⦌.len + 1)
⊢ x✝¹ ≤ x✝ → (fun j ↦ ⟨↑j + i, ⋯⟩) x✝¹ ≤ (fun j ↦ ⟨↑j + i, ⋯⟩) x✝

Tactic:
grind

Goal state after:
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)
⊢ j ≤ ⟨↑k + i, ⋯⟩.castSucc

Tactic:
grind

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

Goal state before:
pp: j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ ↑i' = ↑i.succ + j

Tactic:
grind

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

Goal state before:
pp: x : SimplexCategory
e : x ≅ x
⊢ e = Iso.refl x

Tactic:
have h : (Finset.univ : Finset (Fin (x.len + 1))).card = x.len + 1 := Finset.card_fin (x.len + 1)

Goal state after:
x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
⊢ e = Iso.refl x
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ j.castSucc < ⟨↑k + (i + 1), ⋯⟩

Tactic:
grind

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

Goal state before:
pp: case succ.zero
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
j : Fin (0 + 1)
hi' : n + (i + 1) = 0
hj' : ↑j = ↑j' + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
grind

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

Goal state before:
pp: i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : ↑j.succ = ↑j' + (i + 1)
⊢ ↑j = ↑j' + i

Tactic:
grind

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

Goal state before:
pp: case neg
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter (i + 1) h)) k) =
    ↑((ConcreteCategory.hom (σ 0)) ((ConcreteCategory.hom (σ₀Iter i ⋯)) k))

Tactic:
· rw [σ₀Iter_coe_eq_of_ge .., coe_σ,
      Fin.predAbove_of_castSucc_lt _ _ ?_, Fin.val_pred,
      σ₀Iter_coe_eq_of_ge .., Nat.sub_add_eq]
    rw [Fin.lt_def, Fin.castSucc_zero, σ₀Iter_coe_eq_of_ge ..,
      Fin.coe_ofNat_eq_mod, Nat.zero_mod]
    lia

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

Goal state before:
pp: case succ
i : ℕ
hi' : ∀ {n m : ℕ} (h : n + i = m), σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h
n m : ℕ
h : n + (i + 1) = m
⊢ σ₀Iter (i + 1 + 1) ⋯ = σ 0 ≫ σ₀Iter (i + 1) h

Tactic:
| succ i hi' =>

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

Goal state before:
pp: j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ ↑i = ↑i'.succ + j

Tactic:
grind

Goal state after: