mathlib-initiative/mathlib-tactics huggingface dataset:
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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        ((λ_ (𝟙_ V)).hom ▷ X'' ⟶[V] Y) ≫
          (((eHomEquiv V) f' ≫ (λ_ (X' ⟶[V] X'')).inv) ▷ X'' ⟶[V] Y) ≫
            (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
              (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (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:
← comp_whiskerRight_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 ≫
      (((λ_ (𝟙_ V)).inv ≫ (λ_ (𝟙_ V)).hom) ▷ X'' ⟶[V] Y) ≫
        (((eHomEquiv V) f' ≫ (λ_ (X' ⟶[V] X'')).inv) ▷ X'' ⟶[V] Y) ≫
          (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
            (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (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
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' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        ((λ_ (X' ⟶[V] Y)).inv ▷ Y ⟶[V] Y') ≫
          (((eHomEquiv V) f ▷ X' ⟶[V] Y) ▷ Y ⟶[V] Y') ≫ (eComp V X X' Y ▷ Y ⟶[V] Y') ≫ eComp V X Y Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y'

Tactic:
← comp_whiskerRight_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' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (ρ_ (X' ⟶[V] Y)).inv ≫
      (X' ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        (((λ_ (X' ⟶[V] Y)).inv ≫ (eHomEquiv V) f ▷ X' ⟶[V] Y) ▷ Y ⟶[V] Y') ≫
          (eComp V X X' Y ▷ Y ⟶[V] Y') ≫ eComp V X Y Y' =
    (λ_ (X' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫
        eComp V X X' Y ≫ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y 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✝
⊢ Function.Injective (ForgetEnrichment.homTo W)

Tactic:
intro f g w

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.homTo W f = ForgetEnrichment.homTo W g
⊢ f = g
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
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
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 (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ⊗ₘ Functor.LaxMonoidal.ε F) ≫
          (F.map (ForgetEnrichment.homTo V f) ⊗ₘ F.map (ForgetEnrichment.homTo V g)) ≫
            eComp W (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝)) =
    ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X✝ Y✝ Z✝)

Tactic:
tensorHom_comp_tensorHom_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
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
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 (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝)) =
    ForgetEnrichment.homOf W
      ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X✝ Y✝ Z✝)
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
fac fac' : W₁.MapFactorizationData W₂ f
⊢ ∃ (h : fac.Z = fac'.Z), fac.i = fac'.i ≫ eqToHom ⋯ ∧ fac.p = eqToHom h ≫ fac'.p

Tactic:
have := r.subsingleton_mapFactorizationData f
  obtain rfl : fac = fac' := Subsingleton.elim _ _
  simp

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

Goal state before:
pp: x y : OneTruncation₂ ((truncation 2).obj Δ[0])
x✝ : x ⟶ y
⊢ x✝ = ⋯ ▸ ⋯ ▸ 𝟙rq default

Tactic:
let : Subsingleton (((truncation 2).obj Δ[0]).obj (.op ⦋1⦌2)) :=
      inferInstanceAs (Subsingleton (ULift.{_, 0} (⦋1⦌ ⟶ ⦋0⦌)))
    ext
    exact this.allEq _ _

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

Goal state before:
pp: case succ
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'

Goal state after:
case succ.inl
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
h : δ i' ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

case succ.inr
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
j : Fin (n + 1)
j' : Fin (n + 2)
h : δ i' ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X✝ Y✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Truncated 2
⊢ hoFunctor₂.map x✝¹ ▷ hoFunctor₂.obj x✝ ≫ (iso Y✝ x✝).symm.hom = (iso X✝ x✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ▷ x✝)

Tactic:
by ext; apply mapHomotopyCategory_prod_id_comp_inverse

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

Goal state before:
pp: 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)
⊢ (X.spine 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 =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)).vertex k

Tactic:
dsimp% show op f = f.op from rfl

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)
⊢ (X.spine i
          ((ConcreteCategory.hom (X.map f.op))
            (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 =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ (ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z ∈
      (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1)))).nonDegenerate n ↔
    Function.Injective ⇑(objEquiv z)

Tactic:
PartialOrder.mem_nerve_nonDegenerate_iff_injective,

Goal state after:
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ Function.Injective ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj ↔
    Function.Injective ⇑(objEquiv z)
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0

Tactic:
let γ₄ (i : Fin (n + 1)) := (i.castSucc.succ, i.castSucc)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
j : ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
c : f.Cell j
⊢ range c.map ≤ f.filtration (Order.succ j)

Tactic:
by simpa using f.subcomplex_le_filtration c (Order.lt_succ _)

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs hs'✝ =
        Cell.type₂ f c

Tactic:
rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply] at hs

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ J x, P.colimitsOfShape J X
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
J : Type w
w✝ : Category.{w', w} J
p : P.ColimitOfShape J Y
φ : (j : J) → p.diag.obj j ⟶ X
hφ : ∀ (j : J), (fun f ↦ f ≫ i) (φ j) = p.ι.app j
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ p.diag.map f ≫ φ j₂ = φ j₁ ≫ ((Functor.const J).obj X).map f

Tactic:
by simp [← cancel_mono i, hφ]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable

Goal state before:
pp: C : Type u
hC : Category.{v, u} C
inst✝ : IsAccessibleCategory.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X

Tactic:
by
  obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal C
  obtain ⟨_, _, h⟩ := HasCardinalFilteredGenerator.exists_generator C κ
  apply h.presentable

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

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (f.mapN (Cell.type₂ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₂ f c)).dim

Tactic:
rw [f.mapN_type₂]

Goal state after:
case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ { dim := (↑c.s).dim, simplex := (↑c.s).simplex }.simplex ∈
    X.nonDegenerate { dim := (↑c.s).dim, simplex := (↑c.s).simplex }.dim
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

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₂
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 f₂ ⟶ Arrow.mk sq₁₃.π
⊢ (fun α ↦
        Arrow.homMk (adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α))
          (⋯.lift (adj₂.homEquiv (sq₁₂.inr ≫ Arrow.Hom.left α)) (adj₂.homEquiv (Arrow.Hom.right α)) ⋯) ⋯)
      ((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)) ⋯)
        β) =
    β

Tactic:
by
    ext
    · simp
    · apply sq₁₃.isPullback.hom_ext <;> simp

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₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₂ : Arrow C₂
⊢ adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)) ≫
      (G.obj (op (unop (op X₁)).left)).map ((F.leibnizPushout.obj X₁).obj X₂).hom =
    adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right)) ≫
      (G.map (unop (op X₁)).hom.op).app ((F.leibnizPushout.obj X₁).obj X₂).right

Tactic:
by simp [← homEquiv_naturality_one, ← homEquiv_naturality_three]

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

Goal state before:
pp: X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f✝ g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f' g' : RelativeMorphism B C ψ
h : f'.Homotopy g'
f : RelativeMorphism A B φ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ A.ι ▷ Δ[1] ≫ f.map ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι

Tactic:
← comp_whiskerRight_assoc,

Goal state after:
X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f✝ g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f' g' : RelativeMorphism B C ψ
h : f'.Homotopy g'
f : RelativeMorphism A B φ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ (A.ι ≫ f.map) ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι
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 + 2)
n : ℕ
⊢ (pairing k n).IsRegular

Tactic:
by
  by_cases! hk : k = Fin.last (m + 1)
  · subst hk
    dsimp only [pairing]
    rw [dif_pos rfl]
    infer_instance
  · obtain ⟨k, rfl⟩ := Fin.eq_castSucc_of_ne_last hk
    rw [pairing_castSucc]
    infer_instance

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

Goal state before:
pp: case fst
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
          ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
        (ConcreteCategory.hom (σ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.succ)).1 =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)),
        stdSimplex.objMk₁ j.castSucc.castSucc.succ).1

Tactic:
simp [← SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
      rfl

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

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y u t : X.N
h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)
⊢ t.subcomplex ≤ u.subcomplex

Tactic:
Subcomplex.ofSimplex_le_iff

Goal state after:
X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y u t : X.N
h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)
⊢ t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)
Module: Mathlib.Analysis.Convex.Contractible

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : s.Nonempty
⊢ ContractibleSpace ↑s

Tactic:
by
  refine
    (contractible_iff_id_nullhomotopic s).2 ⟨⟨x, h.mem hne⟩,
      ⟨⟨⟨fun p ↦ ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), ?_⟩, ?_⟩, fun x ↦ by simp, fun x ↦ by simp⟩⟩⟩
  · exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _)
  · fun_prop

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
i : ι
⊢ #↑(f i) ≤ #α

Tactic:
exact mk_set_le (f i)

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
⊢ ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y

Tactic:
intro z

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
z : E
⊢ dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y