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✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
rintro - ⟨i, hi : 1 < f (v i), rfl⟩

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : 1 < f (v i)
⊢ v i ∈ ↑(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
⊢ (snd G₀ H₀).comp (inl G₀ H₀) = 1

Tactic:
ext x

Goal state after:
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : G₀
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) x = 1 x
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
⊢ (fst G₀ H₀).comp (inr G₀ H₀) = 1

Tactic:
ext x

Goal state after:
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : H₀
⊢ ((fst G₀ H₀).comp (inr G₀ H₀)) x = 1 x
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Units.val '' ↑f.valueGroup = range ⇑f \ {0}

Tactic:
ext x

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ x ∈ Units.val '' ↑f.valueGroup ↔ x ∈ range ⇑f \ {0}
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_1.mem
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y x✝ : Bˣ
h : x✝ ∈ ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑x✝ = f x

Tactic:
obtain ⟨a, ha⟩ := h

Goal state after:
case refine_1.mem
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y x✝ : Bˣ
a : A
ha : f a = ↑x✝
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑x✝ = f x
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mp
X : FintypeCat
f : X.obj → X.obj
h : homMk f = 𝟙 X
⊢ f = id

Tactic:
ext x

Goal state after:
case mp
X : FintypeCat
f : X.obj → X.obj
h : homMk f = 𝟙 X
x : X.obj
⊢ f x = id x
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mpr
X : FintypeCat
f : X.obj → X.obj
⊢ f = id → homMk f = 𝟙 X

Tactic:
· rintro rfl
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mp
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h✝ : X.obj → Z.obj
h : homMk h✝ = homMk f ≫ homMk g
⊢ h✝ = g ∘ f

Tactic:
ext x

Goal state after:
case mp
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h✝ : X.obj → Z.obj
h : homMk h✝ = homMk f ≫ homMk g
x : X.obj
⊢ h✝ x = (g ∘ f) x
Module: Mathlib.CategoryTheory.FintypeCat

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

Tactic:
· rintro rfl
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X : FintypeCat
⊢ uSwitch.map
        ((NatIso.ofComponents (fun X ↦ (equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).symm)
                @uSwitchEquivalence._proof_2).hom.app
          X) ≫
      (NatIso.ofComponents (fun X ↦ equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv))
              @uSwitchEquivalence._proof_4).hom.app
        (uSwitch.obj X) =
    𝟙 (uSwitch.obj X)

Tactic:
ext x

Goal state after:
X : FintypeCat
x : (uSwitch.obj X).obj
⊢ (ConcreteCategory.hom
        (uSwitch.map
            ((NatIso.ofComponents (fun X ↦ (equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).symm)
                    @uSwitchEquivalence._proof_2).hom.app
              X) ≫
          (NatIso.ofComponents (fun X ↦ equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv))
                  @uSwitchEquivalence._proof_4).hom.app
            (uSwitch.obj X)))
      x =
    (ConcreteCategory.hom (𝟙 (uSwitch.obj X))) x
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: 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.1
h : φ b < φ b
this : b ≤ b
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasKernel p

Tactic:
have : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ HasKernel p
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 rw [h]

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:
ext x

Goal state after:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) x) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) x)
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 : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
⊢ (∃ a, f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
rw [e0, e1] at this

Goal state after:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
this : 1 ≤ 0
⊢ (∃ a, f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
simp [hp]

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

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

Tactic:
Fin.castPred_castSucc,

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ k = i.succAbove (k.castPred ⋯)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
Fin.castPred_castSucc,

Goal state after:
case inl.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ k = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove (k.succ.castSucc.castPred ⋯) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
Fin.castPred_castSucc,

Goal state after:
case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (j.succ.predAbove k.succ.castSucc)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (k.castSucc.castPred ⋯).succ

Tactic:
Fin.castPred_castSucc,

Goal state after:
case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove k.succ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ δ 0 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.succ

Tactic:
ext x

Goal state after:
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ)) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ δ 1 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.castSucc

Tactic:
ext x

Goal state after:
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc)) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
ext x

Goal state after:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
ext x

Goal state after:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ mkOfSucc i ≫ δ j = intervalEdge (↑i) 2 ⋯

Tactic:
ext x

Goal state after:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) x)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n m : ℕ
h : n = m
⊢ ⦋n⦌ = ⦋m⦌

Tactic:
by rw [h]

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

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : 1 ≤ 0
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a
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

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 0
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 0
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ (unop Y✝).rightOp.hom =
    (unop X✝).rightOp.hom ≫ (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)

Tactic:
ext x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ ((CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ (unop Y✝).rightOp.hom).app x =
    ((unop X✝).rightOp.hom ≫ (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)).app x
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

Goal state after:
f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ X✝.leftOp.hom =
    Y✝.leftOp.hom ≫ (SimplicialObject.const C).map f.left.unop

Tactic:
ext x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ X✝.leftOp.hom).app x =
    (Y✝.leftOp.hom ≫ (SimplicialObject.const C).map f.left.unop).app x
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) ⋯ ≫ σ 0 = σ 0 ≫ σ₀Iter (i + 1) h

Tactic:
hi' (by lia),

Goal state after:
case succ
i : ℕ
hi' : ∀ {n m : ℕ} (h : n + i = m), σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h
n m : ℕ
h : n + (i + 1) = m
⊢ (σ 0 ≫ σ₀Iter i ⋯) ≫ σ 0 = σ 0 ≫ σ₀Iter (i + 1) h
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
A : X.Subcomplex
n : ℕ
hd : d ≤ n
⊢ A.toSSet.degenerate n = ⊤

Tactic:
ext x

Goal state after:
X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
A : X.Subcomplex
n : ℕ
hd : d ≤ n
x : A.toSSet _⦋n⦌
⊢ x ∈ A.toSSet.degenerate n ↔ x ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
⊢ X.degenerate n = ⊤

Tactic:
ext x

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ x ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
⊢ X.degenerate 0 = ∅

Tactic:
ext x

Goal state after:
X : SSet
x : X _⦋0⦌
⊢ x ∈ X.degenerate 0 ↔ x ∈ ∅
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.degenerate (n + 1) = ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

Tactic:
ext x

Goal state after:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
⊢ x ∈ X.degenerate (n + 1) ↔ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

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

Tactic:
le_iff

Goal state after:
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
⊢ ∃ f_1,
    (ConcreteCategory.hom (X.map f_1.op)) { dim := n, simplex := x }.simplex =
      { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x }.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
x y : X.S
⊢ x ≤ y ↔ Nonempty (equivElements y ⟶ equivElements x)

Tactic:
le_iff

Goal state after:
X : SSet
x y : X.S
⊢ (∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) ↔ Nonempty (equivElements y ⟶ equivElements x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
⊢ (ConcreteCategory.hom (X.map (factorThruImage f).op)) ((ConcreteCategory.hom (X.map (image.ι f).op)) y) = ↑x

Tactic:
by
      rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy]

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

Goal state before:
pp: case inr
X : SSet
d : ℕ
y : X _⦋d⦌
hy hx : y ∈ X.nonDegenerate d
h : mk ↑⟨y, hx⟩ ⋯ < mk ↑⟨y, hy⟩ ⋯
w✝ : Mono (𝟙 ⦋(mk ↑⟨y, hx⟩ ⋯).dim⦌)
hf : (ConcreteCategory.hom (X.map (𝟙 ⦋(mk ↑⟨y, hx⟩ ⋯).dim⦌).op)) (mk ↑⟨y, hy⟩ ⋯).simplex = (mk ↑⟨y, hx⟩ ⋯).simplex
⊢ (mk ↑⟨y, hx⟩ ⋯).dim < (mk ↑⟨y, hy⟩ ⋯).dim

Tactic:
simp at h

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.degenerate n = ⊤

Tactic:
ext x

Goal state after:
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⦌
⊢ x ∈ X.degenerate n ↔ x ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
A : X.Subcomplex
⊢ A.toSSet.Finite

Tactic:
obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite

Goal state after:
X : SSet
inst✝ : X.Finite
A : X.Subcomplex
d : ℕ
h✝ : X.HasDimensionLT d
⊢ A.toSSet.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
⊢ Y.Finite

Tactic:
obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite

Goal state after:
X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
⊢ Y.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x : X.S
⊢ ∃ x_1, x_1.subcomplex = x.subcomplex

Tactic:
by
    obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
    obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x
    refine ⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩
    · simp only [Subcomplex.ofSimplex_le_iff]
      have := isSplitEpi_of_epi f
      have : Function.Injective (X.map f.op) := by
        rw [← mono_iff_injective]
        infer_instance
      refine ⟨(section_ f).op, this ?_⟩
      dsimp
      rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp,
        ← op_comp, ← op_comp, Category.assoc, IsSplitEpi.id, Category.comp_id]
    · simp only [Subcomplex.ofSimplex_le_iff]
      exact ⟨f.op, rfl⟩

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

Goal state before:
pp: case mp
X : SSet
A : X.Subcomplex
n : ℕ
h : A.toSSet.degenerate n = ⊤
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

Tactic:
ext x

Goal state after:
case mp
X : SSet
A : X.Subcomplex
n : ℕ
h : A.toSSet.degenerate n = ⊤
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ⊓ A.obj (op ⦋n⦌) ↔ x ∈ A.obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
⊢ A.toSSet.degenerate n = ⊤

Tactic:
ext x

Goal state after:
case mpr
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
x : A.toSSet _⦋n⦌
⊢ x ∈ A.toSSet.degenerate n ↔ x ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
by
    rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_one]
    simp

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, k with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
rcases k with (_ | _ | k)

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j 0
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j (0 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel j (k + 1 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n i : ℕ
hi : n + 1 ≤ i
⊢ Δ[n].degenerate i = ⊤

Tactic:
ext x

Goal state after:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
⊢ x ∈ Δ[n].degenerate i ↔ x ∈ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case left
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁✝ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂✝ : objEquiv.symm f₂ ∈ Δ[n].nonDegenerate m
h₁ : Function.Injective ⇑(Hom.toOrderHom f₁)
h₂ : Function.Injective ⇑(Hom.toOrderHom f₂)
h₃ : Finset.image (⇑(Hom.toOrderHom f₁)) univ = Finset.image (⇑(Hom.toOrderHom f₂)) univ
⊢ Set.range ⇑(Hom.toOrderHom f₁) = Set.range ⇑(Hom.toOrderHom f₂)

Tactic:
ext x

Goal state after:
case left
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁✝ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂✝ : objEquiv.symm f₂ ∈ Δ[n].nonDegenerate m
h₁ : Function.Injective ⇑(Hom.toOrderHom f₁)
h₂ : Function.Injective ⇑(Hom.toOrderHom f₂)
h₃ : Finset.image (⇑(Hom.toOrderHom f₁)) univ = Finset.image (⇑(Hom.toOrderHom f₂)) univ
x : Fin (n + 1)
⊢ x ∈ Set.range ⇑(Hom.toOrderHom f₁) ↔ x ∈ Set.range ⇑(Hom.toOrderHom f₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
⊢ Δ[n].nonDegenerate n = {objEquiv.symm (𝟙 (unop (op ⦋n⦌)))}

Tactic:
ext x

Goal state after:
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x ∈ Δ[n].nonDegenerate n ↔ x ∈ {objEquiv.symm (𝟙 (unop (op ⦋n⦌)))}
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
⊢ (↾fun f ↦
        objEquiv.symm
          (SimplexCategory.Hom.mk
            { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
      SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1 =
    Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫ ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0)

Tactic:
ext x

Goal state after:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
⊢ (ConcreteCategory.hom
          ((↾fun f ↦
              objEquiv.symm
                (SimplexCategory.Hom.mk
                  { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
            SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1)).toFun
      x =
    (ConcreteCategory.hom
          (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫ ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0))).toFun
      x
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ c.ε₂ c c (c.π c c (x✝², x✝¹), x✝) = c.ε₂ c c (x✝², c.π c c (x✝¹, x✝)) * c.ε₂ c c (x✝¹, x✝)

Tactic:
by dsimp; rw [ε_add]

Goal state after: