mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ((P q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
← assoc,

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ (((P q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1)) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ PInfty.f (n + 1) = 0

Tactic:
rw [PInfty_f, σ_comp_P_eq_zero X i]
  simp only [le_add_iff_nonneg_left, zero_le]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : θ.unop ≫ factorThruImage (θ'.unop ≫ A.e) ≫ image.ι (θ'.unop ≫ A.e) = (θ' ≫ θ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ

Tactic:
← assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e) = (θ' ≫ θ).unop ≫ A.e
⊢ colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ'' A) { as := A } ≫ Obj.map K θ' ≫ Obj.map K θ
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Tactic:
← assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ ((s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k) ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e' = cast hu hv e ↔ e' ≍ e

Tactic:
rw [eq_comm, Hom.cast_eq_iff_heq]
  exact ⟨HEq.symm, HEq.symm⟩

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v : U
p : Path u v
hzero : p.length = 0
⊢ Path.cast ⋯ ⋯ p = nil

Tactic:
cases p

Goal state after:
case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : nil.length = 0
⊢ Path.cast ⋯ ⋯ nil = nil

case cons
U : Type u_1
inst✝ : Quiver U
u v b✝ : U
a✝¹ : Path u b✝
a✝ : b✝ ⟶ v
hzero : (a✝¹.cons a✝).length = 0
⊢ Path.cast ⋯ ⋯ (a✝¹.cons a✝) = nil
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : Path { as := x }.as { as := y }.as
⊢ (map f).map (Path.Homotopic.Quotient.mk p) ≫ ⟦H.evalAt { as := y }.as⟧ =
    ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map (Path.Homotopic.Quotient.mk p)

Tactic:
simp only [map_map, Path.Homotopic.Quotient.mk''_eq_mk, comp_eq,
      ← Path.Homotopic.Quotient.mk_map, ← Path.Homotopic.Quotient.mk_trans]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : Path { as := x }.as { as := y }.as
⊢ Path.Homotopic.Quotient.mk ((p.map (⋯ : Continuous ⇑f)).trans (H.evalAt y)) =
    Path.Homotopic.Quotient.mk ((H.evalAt x).trans (p.map (⋯ : Continuous ⇑g)))
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case mk.mk
X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x₀ y₀ : X
x₁ y₁ : Y
motive : Homotopic.Quotient x₀ y₀ → Homotopic.Quotient x₁ y₁ → Prop
mk : ∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (Quotient.mk a) (Quotient.mk b)
a : Path x₀ y₀
b : Path x₁ y₁
⊢ motive (Quot.mk (⇑(Homotopic.setoid x₀ y₀)) a) (Quot.mk (⇑(Homotopic.setoid x₁ y₁)) b)

Tactic:
| mk b =>

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y✝ : C
inst✝¹ : IsCofibrant X
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this✝ : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
this : IsIso (L.map i)
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
← Function.Bijective.of_comp_iff _
      (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence Y i)

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y✝ : C
inst✝¹ : IsCofibrant X
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this✝ : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
this : IsIso (L.map i)
⊢ Function.Bijective (rightHomotopyClassToHom L ∘ fun g ↦ g.precomp i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ∂Δ[n]

Tactic:
rw [boundary_eq_iSup]
  exact le_iSup (fun (i : Fin (n +1)) ↦ stdSimplex.face {i}ᶜ) i

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ stdSimplex.face S ≤ Λ[n + 1, j] ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ

Tactic:
by
  rw [subcomplex_le_horn_iff, stdSimplex.face_le_face_iff, ← not_iff_not]
  simp only [Decidable.not_not, ne_eq, not_and_or]
  refine ⟨fun h ↦ ?_, by aesop⟩
  rw [← Finset.compl_subset_compl, compl_compl,
    Finset.subset_singleton_iff, Finset.compl_eq_empty_iff] at h
  grind [eq_compl_comm]

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

Goal state before:
pp: n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
x : Δ[n + 1].obj m
hx : x ∈ ∂Δ[n + 1].obj m
⊢ (ConcreteCategory.hom (f.app m)).toFun ⟨x, hx⟩ = (ConcreteCategory.hom (g.app m)).toFun ⟨x, hx⟩

Tactic:
simp only [boundary_eq_iSup, stdSimplex.face_singleton_compl, Subfunctor.iSup_obj,
    Set.mem_iUnion, Subcomplex.mem_ofSimplex_obj_iff, op_unop] at hx

Goal state after:
n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
x : Δ[n + 1].obj m
hx✝ : x ∈ ∂Δ[n + 1].obj m
hx : ∃ i f, (ConcreteCategory.hom (Δ[n + 1].map f.op)) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) = x
⊢ (ConcreteCategory.hom (f.app m)).toFun ⟨x, hx✝⟩ = (ConcreteCategory.hom (g.app m)).toFun ⟨x, hx✝⟩
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mk.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x✝ : Pushout f g
x₂ : X₂
⊢ (ConcreteCategory.hom m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
    (ConcreteCategory.hom
          (↾Quot.lift
              (fun x ↦
                match x with
                | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
                | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
              ⋯)).toFun
      (Quot.mk (Rel f g) (Sum.inr x₂))

Tactic:
· exact ConcreteCategory.congr_hom h₂ x₂

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
hf : Fibration f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f

Tactic:
by
  rw [fibration_iff] at hf
  exact hf _ (horn_ι_mem_J _ _)

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

Goal state before:
pp: case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).succ

Tactic:
· exact q.arrow_tgt 0

Goal state after:
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
k : Fin (m + 1)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op)) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f))

Tactic:
rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality]

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)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op)) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (ConcreteCategory.hom (X.map (tr (mkOfSucc k) ⋯ ⋯).op ≫ σ.app (op { obj := ⦋1⦌, property := ⋯ })))
      (sx.spineToSimplex (m + 1) ⋯ f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n✝ n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (spineToSimplex h (X.spine (n + 1) s)) =
    (ConcreteCategory.hom (SimplicialObject.δ X 0)) s

Tactic:
rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h1 : (f ≫ 𝟙 b✝) ≫ g = f ≫ 𝟙 b✝ ≫ g
h2 : 𝟙 b✝ ≫ g = g
h3 : f ≫ 𝟙 b✝ = f
⊢ (eqToIso h1).hom ≫ hComp (𝟙 f) (eqToIso h2).hom = hComp (eqToIso h3).hom (𝟙 g)

Tactic:
revert h1 h2 h3

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
⊢ ∀ (h1 : (f ≫ 𝟙 b✝) ≫ g = f ≫ 𝟙 b✝ ≫ g) (h2 : 𝟙 b✝ ≫ g = g) (h3 : f ≫ 𝟙 b✝ = f),
    (eqToIso h1).hom ≫ hComp (𝟙 f) (eqToIso h2).hom = hComp (eqToIso h3).hom (𝟙 g)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base κ

Tactic:
exact ((id_comp _).trans (comp_id _)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base η

Tactic:
exact ((id_comp _).trans (comp_id _)).symm

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₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ F.obj (P ⟶[V] Q) ◁ μ F (Q ⟶[V] R) (R ⟶[V] S) ≫
      μ F (P ⟶[V] Q) ((Q ⟶[V] R) ⊗ R ⟶[V] S) ≫ F.map ((P ⟶[V] Q) ◁ eComp V Q R S) ≫ F.map (eComp V P Q S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)

Tactic:
MonoidalCategory.whiskerLeft_comp,

Goal state after:
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
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ F.obj (P ⟶[V] Q) ◁ μ F (Q ⟶[V] R) (R ⟶[V] S) ≫
      μ F (P ⟶[V] Q) ((Q ⟶[V] R) ⊗ R ⟶[V] S) ≫ F.map ((P ⟶[V] Q) ◁ eComp V Q R S) ≫ F.map (eComp V P Q S) =
    (F.obj (P ⟶[V] Q) ◁ μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.obj (P ⟶[V] Q) ◁ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ⊤.prod T ⊓ S.prod ⊤ = S.prod T

Tactic:
by
    ext n ⟨x, y⟩
    change _ ∧ _ ↔ _
    simp [prod, Set.prod, Membership.mem, Set.Mem, Set.ofPred]
    tauto

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

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ (ConcreteCategory.hom
        (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).map
          (Hom.tr (SimplexCategory.δ 1) Truncated.Path₁._proof_1 Truncated.Path₁._proof_5).op))
      ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x) =
    (ConcreteCategory.hom
        (s.π.app
          (StructuredArrow.mk
            (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i.castSucc).op)))
      x

Tactic:
let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶
        strArrowMk₂ (⦋0⦌.const _ i.castSucc) :=
          StructuredArrow.homMk (Hom.tr (δ 1)).op
          (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
      exact ConcreteCategory.congr_hom (s.w φ) x

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

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : V.HomotopyCategory ⥤ D
φ : (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀ ⦃x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x✝¹ x✝ : V.HomotopyCategory
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ φ x✝.1.as = φ x✝¹.1.as ≫ G.map f

Tactic:
by
    have : MorphismProperty.naturalityProperty (fun (x : V.HomotopyCategory) ↦ φ _) = ⊤ :=
      morphismProperty_eq_top (fun e ↦ hφ e)
    exact this.symm.le f (by simp)

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

Goal state before:
pp: P : SimplexCategoryGenRel → Sort u_1
H : (n : ℕ) → P (mk n)
x : SimplexCategoryGenRel
⊢ P x

Tactic:
exact H x.len

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

Goal state before:
pp: L : List ℕ
m₁ m₂ : ℕ
hL : IsAdmissible m₂ L
hk : m₂ + L.length = m₁
j : ℕ
hj : j < m₁ + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j

Tactic:
induction L generalizing m₁ m₂ with

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 0

Tactic:
by
  simpa [toMk₁_apply]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 1

Tactic:
by
  simpa [toMk₁_apply]

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

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {t | ∃ v, t = {v}}

Tactic:
by
          constructor
          · rw [hv]; exact Finset.singleton_nonempty _
          · intro t hts ht
            cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
            | inl h => exact (ht.ne_empty h).elim
            | inr h => exact ⟨v, h⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
⊢ ∀ k ∈ ⇑f '' I.I, { as := f i.as }.as ≤ k

Tactic:
rintro _ ⟨k, hk, rfl⟩

Goal state after:
J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ { as := f i.as }.as ≤ f k
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
⊢ ∀ k ∈ ⇑f '' I.I, k ≤ { as := f j.as }.as

Tactic:
rintro _ ⟨k, hk, rfl⟩

Goal state after:
J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ f k ≤ { as := f j.as }.as
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)

Tactic:
simp only [eqToHom_toOrderHom, SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : AugmentedSimplexCategory
⊢ 𝟙 x ⊗ₘ 𝟙 y = 𝟙 (x ⊗ y)

Tactic:
by
  ext
  · simpa [inl, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (𝟙 x) (WithInitial.starInitial.to y) (𝟙 x) (𝟙 y))
  · simpa [inr, MonoidalCategoryStruct.whiskerLeft, MonoidalCategoryStruct.whiskerRight] using
      (tensorHom_comp_tensorHom (WithInitial.starInitial.to x) (𝟙 y) (𝟙 x) (𝟙 y))

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
this : Mono (yonedaEquiv.symm ((ConcreteCategory.hom (f.app (op ⦋n⦌))) x))
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)

Tactic:
rw [← SSet.yonedaEquiv_symm_comp] at this

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
this : Mono (yonedaEquiv.symm x ≫ f)
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)
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)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    ((-1) ^ n * (-1) ^ n) • H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 2))

Tactic:
rw [← pow_add, (Even.add_self n).neg_one_pow, one_smul]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{max ?u.47 w, w, w} J
this : IsFiltered J
f : ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app i)) xi

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{max ?u.47 w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)
hf :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app j)) f₁ =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app j)) f₂
⊢ ∃ k f,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op Y)).map f)) f₁ =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op Y)).map f)) f₂

Tactic:
· obtain ⟨i, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ hc (h.r ≫ f)
      exact ⟨i, h.i ≫ g, by simp [hg]⟩

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)
hf :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app j)) f₁ =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app j)) f₂
⊢ ∃ k f,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op Y)).map f)) f₁ =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op Y)).map f)) f₂