mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case mk.zero
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
hm : ⦋0⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋0⦌, property := hm })
fac : SimplexCategory.δ 0 ≫ SimplexCategory.σ 0 = 𝟙 ⦋0⦌
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋0⦌, property := hm }))).toFun x

Tactic:
simpa using

Goal state after:
case mk.zero
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
hm : ⦋0⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋0⦌, property := hm })
fac : SimplexCategory.δ 0 ≫ SimplexCategory.σ 0 = 𝟙 ⦋0⦌
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋0⦌, property := hm }))) x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋0⦌, property := hm }))) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i.castSucc) ⋯ h).op)) Δ

Tactic:
simp [← δ_one_mkOfSucc, tr_comp]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X : C
f : (coyoneda.obj (op (𝟙_ C))).obj X
⊢ (ConcreteCategory.hom (ρ_ ((coyoneda.obj (op (𝟙_ C))).obj X)).hom).toFun (f, PUnit.unit) =
    (ConcreteCategory.hom
          ((𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun x ↦ 𝟙 (unop (op (𝟙_ C)))) ≫
            (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (ρ_ X).hom)).toFun
      (f, PUnit.unit)

Tactic:
simp [unitors_inv_equal]

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

Goal state before:
pp: case succ.refine_2.inr
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯)).arrow i.succ = p.arrow i.succ

Tactic:
simpa using

Goal state after:
case succ.refine_2.inr
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ↑(hn (p.interval 1 n ⋯)) = (p.interval 1 n ⋯).arrow i
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫ ((eHomEquiv V) (f ≫ f') ▷ X'' ⟶[V] Y) ≫ eComp V X X'' Y =
    ((λ_ (X'' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫ eComp V X' X'' Y) ≫
      (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y

Tactic:
rw [assoc, assoc, eHomEquiv_comp, comp_whiskerRight_assoc, comp_whiskerRight_assoc, ← e_assoc',
    tensorHom_def', comp_whiskerRight_assoc, id_whiskerLeft, comp_whiskerRight_assoc,
    ← comp_whiskerRight_assoc, Iso.inv_hom_id, id_whiskerRight_assoc,
    comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc,
    ← associator_inv_naturality_left_assoc, Iso.inv_hom_id_assoc,
    ← whisker_exchange_assoc, id_whiskerLeft_assoc, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
X Y : C
⊢ F_map X Y = G_map X Y

Tactic:
simpa using

Goal state after:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
X Y : C
⊢ F_map X Y = G_map X Y
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
⊢ f = g

Tactic:
simpa using

Goal state after:
case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
⊢ f = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : Category.{u, u} C
F G : X ⟶ (truncation 2).obj (nerve C)
h : map F = map G
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })
f : Truncated.Edge x₀ x₁
⊢ (ConcreteCategory.hom (F.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (G.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge

Tactic:
simpa using

Goal state after:
X : Truncated 2
C : Type u
inst✝ : Category.{u, u} C
F G : X ⟶ (truncation 2).obj (nerve C)
h : map F = map G
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })
f : Truncated.Edge x₀ x₁
⊢ (ConcreteCategory.hom (F.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (G.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hf : W₂.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hf : W₂.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hf : W₁.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hf : W₁.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
⊢ r.degHom f ≤ r.deg X

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
⊢ r.degHom f ≤ r.deg X
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
⊢ r.degHom f ≤ r.deg Y

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
⊢ r.degHom f ≤ r.deg Y
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : r.degHom f = r.deg X✝
X Y : C
i : X✝ ⟶ Y✝
hi : W₂ i
h : r.degHom f = r.deg X✝
hp : W₁ (𝟙 X✝)
fac : 𝟙 X✝ ≫ i = f
⊢ i = f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : r.degHom f = r.deg X✝
X Y : C
i : X✝ ⟶ Y✝
hi : W₂ i
h : r.degHom f = r.deg X✝
hp : W₁ (𝟙 X✝)
fac : 𝟙 X✝ ≫ i = f
⊢ i = f
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : r.degHom f = r.deg Y✝
X Y : C
p : X✝ ⟶ Y✝
hp : W₁ p
h : r.degHom f = r.deg Y✝
hi : W₂ (𝟙 Y✝)
fac : p ≫ 𝟙 Y✝ = f
⊢ p = f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : r.degHom f = r.deg Y✝
X Y : C
p : X✝ ⟶ Y✝
hp : W₁ p
h : r.degHom f = r.deg Y✝
hi : W₂ (𝟙 Y✝)
fac : p ≫ 𝟙 Y✝ = f
⊢ p = f
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.degHom e.hom ≤ r.deg Y

Tactic:
simpa using

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.degHom e.hom ≤ r.deg Y
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.deg Y ≤ r.degHom e.hom

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.deg Y ≤ r.degHom e.hom
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i = 𝟙 (mk n)

Tactic:
cases i using Fin.lastCases

Goal state after:
case last
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) (Fin.last (n + 1)) = 𝟙 (mk n)

case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i✝.castSucc = 𝟙 (mk n)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case zero.comp_of.inl
i : Fin (0 + 1)
X Y : SimplexCategoryGenRel
k : Fin (0 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simpa using

Goal state after:
case zero.comp_of.inl
i : Fin (0 + 1)
X Y : SimplexCategoryGenRel
k : Fin (0 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, P_δ m ∧ P_σ e ∧ δ k ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.comp_of.inl
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simpa using

Goal state after:
case succ.comp_of.inl
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, P_δ m ∧ P_σ e ∧ δ k ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)

Tactic:
obtain ⟨z, e, m, he, hm, fac⟩ := exists_P_σ_P_δ_factorization f

Goal state after:
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
z : SimplexCategoryGenRel
e : X✝ ⟶ z
m : z ⟶ Y✝
he : P_σ e
hm : P_δ m
fac : f = e ≫ m
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := ⋯
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
⊢ ↑(Fin.ofNat (m₂ + 1) a) = ↑a₀

Tactic:
simpa using

Goal state after:
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
⊢ a < m₂ + 1
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
ha₀ : Fin.ofNat (m₂ + 1) a = a₀
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) ⋯))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j

Tactic:
simpa using

Goal state after:
case cons
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
ha₀ : Fin.ofNat (m₂ + 1) a = a₀
⊢ ↑(a₀.predAbove ((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩)) =
    if a < ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) then
      ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) - 1
    else ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ (mkNatTrans (fun y ↦ homMk (e₀₁.tensor (Edge.id y))) ⋯ ≫ mkNatTrans (fun y ↦ homMk (e₁₂.tensor (Edge.id y))) ⋯).app
      (mk y) =
    (mkNatTrans (fun y ↦ homMk (e₀₂.tensor (Edge.id y))) ⋯).app (mk y)

Tactic:
simpa using

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (e₀₁.tensor (Edge.id y)) ≫ homMk (e₁₂.tensor (Edge.id y)) = homMk (e₀₂.tensor (Edge.id y))
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case refine_2
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelUpperSet (Subtype.val '' s) P
a b : { x // P x }
x : a ≤ b
y : a ∈ s
ma : ↑a ∈ Subtype.val '' s
⊢ b ∈ s

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelUpperSet (Subtype.val '' s) P
a b : { x // P x }
x : a ≤ b
y : a ∈ s
ma : ↑a ∈ Subtype.val '' s
⊢ b ∈ s
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case refine_2
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelLowerSet (Subtype.val '' s) P
a b : { x // P x }
x : b ≤ a
y : a ∈ s
ma : ↑a ∈ Subtype.val '' s
⊢ b ∈ s

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelLowerSet (Subtype.val '' s) P
a b : { x // P x }
x : b ≤ a
y : a ∈ s
ma : ↑a ∈ Subtype.val '' s
⊢ b ∈ s
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
s : Set (PreAbstractSimplicialComplex ι)
x✝¹ : Finset ι
x✝ : x✝¹ ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}
hx : x✝¹ ∈ ⋂ K ∈ s, K.faces
hn : x✝¹ ∈ {t | t.Nonempty}
⊢ x✝¹.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x✝¹ → b.Nonempty → b ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}

Tactic:
by
        grind [IsRelLowerSet.mem_of_le, isRelLowerSet_faces, mem_iInter]

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
hi : i < y
this : x ≤ (f i).castSucc
⊢ y ≤ i

Tactic:
simpa using

Goal state after:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
hi : i < y
this : x ≤ (f i).castSucc
⊢ y ≤ i
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
this : i < y
⊢ x ≤ (f i).castSucc

Tactic:
simpa using

Goal state after:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ i < y, (f i).castSucc < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
this : i < y
⊢ x ≤ (f i).castSucc