mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' univ ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
rw [this, image_union, union_subset_iff]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f)) ∧
    v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
hj : f (v i) < 1
⊢ (v i)⁻¹ ∈ Submonoid.closure (v '' {i | 1 < f (v i)})

Tactic:
exact Submonoid.subset_closure ⟨i⁻¹, by simpa [hi']⟩

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
by 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:
by 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:
by 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:
by 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 : ℕ
⊢ 0 ∈ Finset.univ

Tactic:
by 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:
by 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 : ℕ
⊢ ((normalizedMooreComplex C).obj X).d (n + 1) n = objD X n

Tactic:
by
  simp [-objD, -obj_X]

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

Goal state after:
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:
dsimp [subinterval]

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑i + j = 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 : P ⟶ Q
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f

Tactic:
add_comp,

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

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:
simpa only [comp_id] using! (congr_app hp j).symm

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
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (X.left.δ 0 + -X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
add_comp,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ X.left.δ 0 ≫ X.hom.app (op ⦋0⦌) + (-X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0
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:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.δ i ≫ X.δ j = X.δ (j.pred ⋯) ≫ X.δ i.castSucc

Tactic:
by
  dsimp [δ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_δ' H]

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:
by 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:
by 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.leftOp.rightOp.left = X.left

Tactic:
by simp

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)
⊢ 0 ≤ i

Tactic:
by simp

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)
⊢ 0 ≤ j.castSucc

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ ↑0 < 1

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ Fin.castSucc 0

Tactic:
by simp

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

Goal state before:
pp: case h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ ∃ θ', θ = σ (x.castPred ⋯) ≫ θ'

Tactic:
apply eq_σ_comp_of_not_injective'

Goal state after:
case h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc = (Hom.toOrderHom θ) (x.castPred ⋯).succ
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 → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ 0 ≤ j'

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
U V : Cᵒᵖ
g : U ⟶ V
f : X ⟶ U
⊢ (ConcreteCategory.hom (F.map (f ≫ g))) x = (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map f)) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
⊢ (ConcreteCategory.hom (F.map (𝟙 X))) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (ConcreteCategory.hom (F'.map (𝟙 X))) ((ConcreteCategory.hom (f.app X)) x) = (ConcreteCategory.hom (f.app X)) x

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X✝ Y✝ : SimplexCategoryᵒᵖ
g : X✝ ⟶ Y✝
⊢ ∀ (j : Fin ((Opposite.unop Y✝).len + 1)),
    WidePullback.π (fun x ↦ f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) j) ≫ f.hom = WidePullback.base fun x ↦ f.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePullback f✝.right (fun x ↦ f✝.left) fun x ↦ f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
inst✝ : ∀ (n : ℕ), HasWidePullback g.right (fun x ↦ g.left) fun x ↦ g.hom
F : f ⟶ g
n : SimplexCategoryᵒᵖ
j : Fin ((Opposite.unop n).len + 1)
⊢ (WidePullback.π (fun x ↦ f.hom) j ≫ Hom.left F) ≫ g.hom = (WidePullback.base fun x ↦ f.hom) ≫ Hom.right F

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin ((Opposite.unop x).len + 1)
⊢ (X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ≫ F.hom = X.hom.app x ≫ Arrow.Hom.right G

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : X.S
⊢ (fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.inv.app (Opposite.op ⦋s.dim⦌))) s.simplex })
      ((fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋s.dim⦌))) s.simplex }) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : Y.S
⊢ (fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋s.dim⦌))) s.simplex })
      ((fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.inv.app (Opposite.op ⦋s.dim⦌))) s.simplex }) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
⊢ x ∈ X.nonDegenerate 0

Tactic:
by simp

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
⊢ x = (ConcreteCategory.hom (X.map (𝟙 ⦋0⦌).op)) ↑⟨x, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
⊢ x = (ConcreteCategory.hom (X.map (𝟙 ⦋n + 1⦌).op)) ↑⟨x, hx⟩

Tactic:
by simp

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

Goal state before:
pp: X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ ∀ (X : SimplexCategoryᵒᵖ), IsIso (f.app X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map f.op)) x

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (range f).preimage f ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.toImage f) ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: X : SSet
⊢ ⨆ s, s.subcomplex ≤ ⊤

Tactic:
by simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∀ s ∈ ∅, s < 0

Tactic:
by simp

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ φ (N.mk x hx) ∈ Finset.image φ ⊤

Tactic:
by simp

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

Goal state before:
pp: X : SSet
x : X.S
y : X.N
h : y.subcomplex = x.subcomplex
⊢ x.toN.subcomplex = x.subcomplex

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a : Fin (n + 1)
⊢ i.succAboveOrderEmb a ∈ {i}ᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
hj✝ : j ∈ {0}ᶜ
hj : ¬j = 0
⊢ (fun a ↦ ⟨(succAboveOrderEmb 0) a, ⋯⟩) (j.pred hj) = ⟨j, hj✝⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
⊢ a ∈ {a, b}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
⊢ b ∈ {a, b}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ a ∈ {a, b, c}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ b ∈ {a, b, c}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ c ∈ {a, b, c}

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
α : Type u
inst✝ : Preorder α
e : α ≃o Fin (n + 1)
X✝ : SimplexCategory
F : Fin (X✝.len + 1) ⥤ Fin (⦋n⦌.len + 1)
x : Fin (X✝.len + 1)
⊢ ((fun F ↦ F ⋙ ⋯.functor) ((fun F ↦ F ⋙ ⋯.functor) F)).obj x = F.obj x

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
α : Type u
inst✝ : Preorder α
e : α ≃o Fin (n + 1)
X✝ : SimplexCategory
F : (nerve α).obj (op X✝)
x : Fin ((unop (op X✝)).len + 1)
⊢ ((fun F ↦ F ⋙ ⋯.functor) ((fun F ↦ F ⋙ ⋯.functor) F)).obj x = F.obj x

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ nerveEquiv x = ComposableArrows.left e.edge

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.right e.edge = nerveEquiv y

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
f : nerveEquiv x ⟶ nerveEquiv y
⊢ (fun e ↦ eqToHom ⋯ ≫ ComposableArrows.hom e.edge ≫ eqToHom ⋯) ((fun f ↦ Edge.mk (ComposableArrows.mk₁ f) ⋯ ⋯) f) = f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ x = nerveEquiv (nerveEquiv.symm x)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ nerveEquiv (nerveEquiv.symm y) = y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even (n + 1)
⊢ n + 1 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroObject V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ (truncate.obj C).d 1 0 ≫ C.d 1 0 = 0

Tactic:
by simp

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

Goal state before:
pp: n : SimplexCategory
m : SimplexCategoryᵒᵖ
a b : (stdSimplex.obj n).obj m
⊢ objEquiv a = objEquiv b ↔ a = b

Tactic:
by simp

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

Goal state before:
pp: X : SSet
n : SimplexCategory
inst✝ : DecidableEq (X.obj (op n))
a b : stdSimplex.obj n ⟶ X
⊢ yonedaEquiv a = yonedaEquiv b ↔ a = b

Tactic:
by simp

Goal state after: