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

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

Tactic:
ext k

Goal state after:
case h
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
⊢ ((sx.spineEquiv (n + 1))
          ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)))).arrow
      k =
    ((sx.spineEquiv (n + 1)) ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj))).arrow k
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
⊢ (sy.spineEquiv (m + 1) ⋯) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (sy.spineEquiv (m + 1) ⋯)
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f))

Tactic:
ext k

Goal state after:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ ((sy.spineEquiv (m + 1) ⋯) (sy.spineToSimplex (m + 1) ⋯ (f.map σ))).arrow k =
    ((sy.spineEquiv (m + 1) ⋯)
          ((ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      k
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ (sy.spineEquiv (n + 1)) (sy.spineToSimplex (f.map σ)) =
    (sy.spineEquiv (n + 1)) ((ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f))

Tactic:
ext k

Goal state after:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ ((sy.spineEquiv (n + 1)) (sy.spineToSimplex (f.map σ))).arrow k =
    ((sy.spineEquiv (n + 1)) ((ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f))).arrow k
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' ▷ X'' ⟶[V] Y) ≫
        (λ_ ((X' ⟶[V] X'') ⊗ X'' ⟶[V] Y)).inv ≫
          (eHomEquiv V) f ▷ ((X' ⟶[V] X'') ⊗ X'' ⟶[V] Y) ≫ (X ⟶[V] X') ◁ eComp V X' X'' 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:
← whisker_exchange_assoc,

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
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        (λ_ ((X' ⟶[V] X'') ⊗ X'' ⟶[V] Y)).inv ≫
          𝟙_ V ◁ eComp V X' X'' Y ≫ ((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 ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y
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)) =
    Functor.LaxMonoidal.ε F ≫
      (ρ_ (F.obj (𝟙_ V))).inv ≫
        F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
          Functor.LaxMonoidal.μ F (𝟙_ V) (𝟙_ V) ≫ F.map ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) g) ≫ F.map (eComp V X✝ Y✝ Z✝)

Tactic:
Functor.LaxMonoidal.right_unitality_inv_assoc,

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)) =
    Functor.LaxMonoidal.ε F ≫
      F.map (ρ_ (𝟙_ V)).inv ≫ F.map ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) g) ≫ F.map (eComp V X✝ Y✝ Z✝)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
f : X✝ ⟶ Y✝
⊢ (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
induction f using hom_induction with
    | id => exact le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _)
    | comp_homMk _ _ h =>
      exact comp_mem _ _ _ h (le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _))

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
x✝³ x✝² : C₁
g : x✝³ ⟶ x✝²
x✝¹ : C₃
x✝ : C₂
⊢ ((X✝.flip₂₃.map g ≫
              { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝²).app Z).app Y, naturality := ⋯ }, naturality := ⋯ }).app
          x✝¹).app
      x✝ =
    (({ app := fun Y ↦ { app := fun Z ↦ ((f.app x✝³).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } ≫
              Y✝.flip₂₃.map g).app
          x✝¹).app
      x✝

Tactic:
simp only [flip₂₃_obj_obj_obj, NatTrans.comp_app, flip₂₃_map_app_app]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
x✝³ x✝² : C₁
g : x✝³ ⟶ x✝²
x✝¹ : C₃
x✝ : C₂
⊢ ((X✝.map g).app x✝).app x✝¹ ≫ ((f.app x✝²).app x✝).app x✝¹ =
    ((f.app x✝³).app x✝).app x✝¹ ≫ ((Y✝.map g).app x✝).app x✝¹
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f : Edge x y
g : Edge y z
h : Edge x z
fac : ⟦f.comp g⟧ = ⟦h⟧
⊢ f.CompStruct g h

Tactic:
Quotient.eq_iff_equiv

Goal state after:
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f : Edge x y
g : Edge y z
h : Edge x z
fac : f.comp g ≈ h
⊢ f.CompStruct g h
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case of_comp.inr
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
z✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
g : mk n✝ ⟶ z✝
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (σ i ≫ g)

Tactic:
simpa using! (σ_comp g i hrec)

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

Goal state before:
pp: case cons
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + (a :: t).length = m₂
⊢ standardσ L₁ h ≫ standardσ (a :: t) h' = standardσ (a :: t ++ L₁) ⋯

Tactic:
dsimp at h' ⊢

Goal state after:
case cons
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₂
⊢ standardσ L₁ h ≫ standardσ t ⋯ ≫ σ ↑a = standardσ (t ++ L₁) ⋯ ≫ σ ↑a
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

Goal state after:
n m : SemiSimplexCategory
f : n ⟶ m
Z✝ : SemiSimplexCategory
g₁ g₂ : Z✝ ⟶ n
h : g₁ ≫ f = g₂ ≫ f
⊢ toSimplexCategory.map g₁ = toSimplexCategory.map g₂
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case refine_1
α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsLowerSet s
a : α
x : a ∈ Subtype.val '' s
⊢ P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val '' s

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
⊢ b ∈ s

Tactic:
· obtain ⟨a, ma, rfl⟩ := x
    exact ⟨a.2, fun b x y ↦ by simpa [h (show ⟨b, y⟩ ≤ a by exact x) ma]⟩

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
⊢ b ∈ s
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
⊢ (sx.spineEquiv i)
      ((ConcreteCategory.hom (X.map (op f)))
        (sx.spineToSimplex
          { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
            arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
            arrow_src := ⋯, arrow_tgt := ⋯ })) =
    (sx.spineEquiv i) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)

Tactic:
ext k

Goal state after:
case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ ((sx.spineEquiv i)
          ((ConcreteCategory.hom (X.map (op f)))
            (sx.spineToSimplex
              { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
                arrow := fun i ↦
                  (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
                arrow_src := ⋯, arrow_tgt := ⋯ }))).vertex
      k =
    ((sx.spineEquiv i) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)).vertex k

case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin i
⊢ ((sx.spineEquiv i)
          ((ConcreteCategory.hom (X.map (op f)))
            (sx.spineToSimplex
              { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
                arrow := fun i ↦
                  (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
                arrow_src := ⋯, arrow_tgt := ⋯ }))).arrow
      k =
    ((sx.spineEquiv i) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)).arrow k
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ

Tactic:
Fin.succAbove_of_le_castSucc _ _ h,

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ j.succ < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Goal state before:
pp: X₁ X₂ X₃ X₄ : SSet
inst✝¹ : X₁.Finite
inst✝ : X₂.Finite
d₁ : ℕ
h✝ : X₁.HasDimensionLT d₁
⊢ (X₁ ⊗ X₂).Finite

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

Goal state after:
X₁ X₂ X₃ X₄ : SSet
inst✝¹ : X₁.Finite
inst✝ : X₂.Finite
d₁ : ℕ
h✝¹ : X₁.HasDimensionLT d₁
d₂ : ℕ
h✝ : X₂.HasDimensionLT d₂
⊢ (X₁ ⊗ X₂).Finite
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
⊢ y =
    (Types.isLimitEquivSections (hc cX.pt))
      ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))

Tactic:
ext k

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
k : K
⊢ ↑y k =
    ↑((Types.isLimitEquivSections (hc cX.pt))
          ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s)))
      k
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ P.colimitsCardinalClosure κ (coequalizer φ₁ φ₂)

Tactic:
apply ObjectProperty.prop_colimit

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι := ⋯
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C := ⋯
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ ∀ (j_1 : WalkingParallelPair), P.colimitsCardinalClosure κ ((parallelPair φ₁ φ₂).obj j_1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions.rlp.llp Λ[n, i].ι

Tactic:
exact le_llp_rlp _ _ (horn_ι_mem_innerHornInclusions h0 hn)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ (α_ A Z W).hom ≫ f ▷ (Z ⊗ W) ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)

Tactic:
← whisker_exchange_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ (α_ A Z W).hom ≫ A ◁ h ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : l.succ ≤ i
⊢ (x.cast hd).simplex.1 l.succ ≤ (x.cast hd).simplex.1 i

Tactic:
exact stdSimplex.monotone_apply _ hi

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: 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₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Arrow.Hom.left
      ((fun β ↦
          Arrow.homMk
            (⋯.desc (adj₂.homEquiv.symm (Arrow.Hom.left β)) (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.fst)) ⋯)
            (adj₂.homEquiv.symm (Arrow.Hom.right β ≫ sq₁₃.snd)) ⋯)
        ((fun α ↦
            Arrow.homMk (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α))
              (⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ⋯)
          α)) =
    Arrow.Hom.left α

Tactic:
apply sq₁₂.isPushout.hom_ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X : Arrow C
I : C
i : IsInitial I
W : C
this✝ : IsIso (I ◁ X.hom)
this : IsPushout (i.to W ▷ X.left) (I ◁ X.hom) (𝟙 (W ⊗ X.left)) ((i.ofIso (mulZero i).symm).to (W ⊗ X.left))
⊢ pushout.inl (((curriedTensor C).map (Arrow.mk (i.to W)).hom).app X.left)
        (((curriedTensor C).obj (Arrow.mk (i.to W)).left).map X.hom) ≫
      this.isoPushout.symm.hom ≫ W ◁ X.hom =
    pushout.inl (((curriedTensor C).map (Arrow.mk (i.to W)).hom).app X.left)
        (((curriedTensor C).obj (Arrow.mk (i.to W)).left).map X.hom) ≫
      (ofHasPushout (curriedTensor C) (Arrow.mk (i.to W)).hom X.hom).ι ≫
        (Iso.refl (((curriedTensor C).obj (Arrow.mk (i.to W)).right).obj X.right)).hom

Tactic:
simp [pushout.inl_desc]

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

Goal state before:
pp: case inl
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₂
hf : Mono (SimplexCategory.δ it.castSucc)
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map (SimplexCategory.δ it.castSucc).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:
refine (h₁ (hs.δ_injective ht ?_)).elim
      rw [Subcomplex.N.ext_iff, N.ext_iff, S.ext_iff']
      exact ⟨rfl, hδ.symm⟩

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] 0)) (stdSimplex.objMk₁ 1)).2
      k =
    ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x).2 k

Tactic:
· rw [stdSimplex.δ_objMk₁_of_lt _ _ (by tauto)]
      rfl

Goal state after: