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

Goal state before:
pp: case h.inr.inr.zero
X : SSet
sx : X.StrictSegal
i : Fin (0 + 3)
σ₀ : Λ[0 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (0 + 2)
j : Fin (0 + 3)
hj : j ≠ i
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, i].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
fin_cases i

Goal state after:
case h.inr.inr.zero.«0»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨0, ⋯⟩
hₙ : (fun i ↦ i) ⟨0, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨0, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨0, ⋯⟩) j hj)

case h.inr.inr.zero.«1»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨1, ⋯⟩
hₙ : (fun i ↦ i) ⟨1, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨1, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨1, ⋯⟩) j hj)

case h.inr.inr.zero.«2»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨2, ⋯⟩
hₙ : (fun i ↦ i) ⟨2, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨2, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨2, ⋯⟩) j hj)
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
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    (λ_ (𝟙_ W)).inv ≫
      (Functor.LaxMonoidal.ε F ⊗ₘ Functor.LaxMonoidal.ε F) ≫
        (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫ eComp W X✝ Y✝ Z✝

Tactic:
eComp_eq,

Goal state after:
V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    (λ_ (𝟙_ W)).inv ≫
      (Functor.LaxMonoidal.ε F ⊗ₘ Functor.LaxMonoidal.ε F) ≫
        (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
          Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
β : F ⟶ G
α : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α }.out.app X = β.out.app X
⊢ { out := α } = β

Tactic:
rcases β with ⟨β⟩

Goal state after:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α }.out.app X = { out := β }.out.app X
⊢ { out := α } = { out := β }
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
⊢ (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f) =
    ((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z)

Tactic:
ext ⟨f, g⟩

Goal state after:
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
f : X ⟶[Type v] Y
g : Y ⟶[Type v] Z
⊢ (ConcreteCategory.hom (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f)).toFun (f, g) =
    (ConcreteCategory.hom
          (((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z))).toFun
      (f, g)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ f.f ▷ Y.fst ▷ U ≫ ((X₂.tensorObj Y).snd.β U).hom = ((X₁.tensorObj Y).snd.β U).hom ≫ U ◁ f.f ▷ Y.fst

Tactic:
dsimp only [tensorObj_fst, tensorObj_snd_β, Iso.trans_hom, whiskerLeftIso_hom,
    Iso.symm_hom, whiskerRightIso_hom]
  calc
    _ = 𝟙 _ ⊗≫
      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (HalfBraiding.β Y.snd U).hom) ⊗≫
        (HalfBraiding.β X₂.snd U).hom ▷ Y.fst ⊗≫ 𝟙 _ := by monoidal
    _ = 𝟙 _ ⊗≫
      X₁.fst ◁ (HalfBraiding.β Y.snd U).hom ⊗≫
        (f.f ▷ U ≫ (HalfBraiding.β X₂.snd U).hom) ▷ Y.fst ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; monoidal
    _ = _ := by rw [f.comm]; monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (α_ X.fst Y.fst Z.fst).hom ≫ (α_ X Y Z).inv.f = 𝟙 ((X ⊗ Y) ⊗ Z).fst

Tactic:
← associator_hom_f,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y Z : Center C
⊢ (α_ X Y Z).hom.f ≫ (α_ X Y Z).inv.f = 𝟙 ((X ⊗ Y) ⊗ Z).fst
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : V
f : x ⟶ y
⊢ motive ((quotientFunctor V).map f)

Tactic:
induction f with

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

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x ⟶ y
x✝ : ⊤ f
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f
    rw [morphismPropertyHomMk_eq_strictMap]
    refine strictMap_multiplicativeClosure_le _ _ _ ?_
    rw [Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk]
    exact map_mem_strictMap _ _ _ (by simp)

Goal state after:
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
w✝ : C
f₁ : X ⟶ w✝
f₂ : w✝ ⟶ Y
left✝¹ : W₁ f₁
left✝ : W₂ f₂
h_fac : f₁ ≫ f₂ = f
h_deg : r.degHom f = r.deg w✝
⊢ r.degHom (f₁ ≫ f₂ ≫ g) ≤ r.deg w✝

Tactic:
exact r.degHom_le f₁ (f₂ ≫ g)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: i : Fin 1
i' : Fin 2
⊢ δ i' ≫ σ i = 𝟙 (mk 0)

Tactic:
fin_cases i

Goal state after:
case «0»
i' : Fin 2
⊢ δ i' ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f = e ≫ m

Tactic:
induction f with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L : List ℕ
j : ℕ
hj : ∀ k ∈ L, j ≤ k
⊢ simplicialEvalσ L j = j

Tactic:
induction L with

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case of
x y : SimplexCategoryGenRel
f✝ : x ⟶ y
x✝ y✝ : SimplexCategoryGenRel
f : x✝ ⟶ y✝
hf : degeneracies f
⊢ ∃ L m b, ∃ (h₁ : mk m = y✝) (h₂ : x✝ = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ f = standardσ L ⋯

Tactic:
cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]

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

Goal state before:
pp: n m : SemiSimplexCategory
f : n ⟶ m
Z✝ : SemiSimplexCategory
g₁ g₂ : Z✝ ⟶ n
h : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
apply toSimplexCategory.map_injective
    simp only [← cancel_mono (toSimplexCategory.map f), ← Functor.map_comp, h]

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
by
  cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
by
  cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
i : SimplexCategoryᵒᵖ
⊢ ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (𝟙 i).unop).uliftMap) =
    𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C)

Tactic:
by
    ext
    change EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) _ = _
    rw [SimplicialThickening.functor_id]
    rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
y : ↑P.II
hy : P.p y = ⟨x, h⟩
⊢ x = ↑(P.p y)

Tactic:
by rw [hy]

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ pullback.fst i b ≫ i = pullback.snd i b ≫ b

Tactic:
pullback.condition

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ pullback.snd i b ≫ b = pullback.snd i b ≫ b
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsDense
Y : D
⊢ F.isDenseAt Y

Tactic:
exact ⟨F.denseAt Y⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: A : SSet
⊢ (A ⟹ ⊤_ SSet).Quasicategory

Tactic:
have : IsIso (terminal.from ((ihom A).obj (⊤_ _))) :=
    isIso_of_isTerminal (IsTerminal.isTerminalObj _ _ terminalIsTerminal)
      terminalIsTerminal _

Goal state after:
A : SSet
this : IsIso (terminal.from (A ⟹ ⊤_ SSet))
⊢ (A ⟹ ⊤_ SSet).Quasicategory
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ φ x hd ((min x hd).castSucc.succAbove i) = (objEquiv (x.cast hd).simplex) i

Tactic:
φ_succAbove

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ (objEquiv (x.cast hd).simplex) i = (objEquiv (x.cast hd).simplex) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: A : SSet
⊢ (A ⟹ ⊤_ SSet).KanComplex

Tactic:
have : IsIso (terminal.from ((ihom A).obj (⊤_ _))) :=
    isIso_of_isTerminal (IsTerminal.isTerminalObj _ _ terminalIsTerminal)
      terminalIsTerminal _

Goal state after:
A : SSet
this : IsIso (terminal.from (A ⟹ ⊤_ SSet))
⊢ (A ⟹ ⊤_ SSet).KanComplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.zero
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hd : x.dim = 0
i : Fin (0 + 1)
hx : IsIndex x ⋯ i
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
fin_cases i

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd.1998712541._hygCtx._hyg.462.«0»
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hd : x.dim = 0
hx : IsIndex x ⋯ ((fun i ↦ i) ⟨0, ⋯⟩)
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
⊢ ∀ (a b : X _⦋0⦌), π₀Rel a b → f a = f b

Tactic:
rintro x y ⟨e⟩; exact hf e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (𝟭 C₃).map
        (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
apply PushoutObjObj.hom_ext

Goal state after:
case hₗ
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ sq₁₂.inl ≫
      (𝟭 C₃).map
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.map (Arrow.Hom.right sq)).app f₂.right)

case hᵣ
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ sq₁₂.inr ≫
      (𝟭 C₃).map
          (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
            ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.map (Arrow.Hom.right sq)).app f₂.right)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
f :
  ⦋((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).dim⦌ ⟶
    ⦋((pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).dim⦌
hf : Mono f
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map f.op))
      ((pairingCore k n).type₁
          { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).simplex =
    ((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).simplex
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }.x ⋯).card

Tactic:
dsimp at f hf

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
f : ⦋d⦌ ⟶ ⦋d + 1⦌
hf : Mono f
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map f.op))
      ((pairingCore k n).type₁
          { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).simplex =
    ((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).simplex
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }.x ⋯).card
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (𝟭 C₃).map
        (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
          ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.obj f₁.right).map (Arrow.Hom.right sq))

Tactic:
apply PushoutObjObj.hom_ext

Goal state after:
case hₗ
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ sq₁₂.inl ≫
      (𝟭 C₃).map
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inl ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.obj f₁.right).map (Arrow.Hom.right sq))

case hᵣ
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ sq₁₂.inr ≫
      (𝟭 C₃).map
          (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
            ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
        (Arrow.mk sq₁₂'.ι).hom =
    sq₁₂.inr ≫ (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.obj f₁.right).map (Arrow.Hom.right sq))
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case neg
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ ↑((SimplexCategory.Hom.toOrderHom (SimplexCategory.σ i)) j) + ↑1 = ↑j

Tactic:
change (i.predAbove j : ℕ) + 1 = _

Goal state after:
case neg
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ ↑(i.predAbove j) + 1 = ↑j
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case zero
X : SSet
x : X _⦋0⦌
f : X.PtSimplex 0 x
i : Fin 0
j : Fin (0 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x

Tactic:
fin_cases i

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ stdSimplex.σ i ≫ const x = const x

Tactic:
comp_const

Goal state after:
case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ const x = const x
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case zero
X : SSet
x : X _⦋0⦌
f : X.PtSimplex 0 x
i : Fin 0
j : Fin (0 + 1)
hj : i.castSucc.succ < j.succ
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x

Tactic:
fin_cases i

Goal state after: