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

Goal state before:
pp: case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ f ≫ ∑ j with ↑j < n + 1, ((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
Preadditive.comp_sum,

Goal state after:
case mp.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : f ≫ PInfty.f (n + 1) = 0
h' : f ≫ QInfty.f (n + 1) = f
⊢ ∑ j with ↑j < n + 1, f ≫ ((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ f ≫ ∑ j, (s.πSummand j ≫ (s.cofan (op ⦋n⦌)).inj j) ≫ PInfty.f n = 0

Tactic:
Preadditive.comp_sum,

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h : f ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = 0
⊢ ∑ j, f ≫ (s.πSummand j ≫ (s.cofan (op ⦋n⦌)).inj j) ≫ PInfty.f n = 0
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)) ≫
      Preadditive.DoldKan.equivalence.unitIso.hom.app ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫
        Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    (𝟙 (N₁ ⋙ Γ₂)).app X

Tactic:
Preadditive.DoldKan.equivalence_unitIso,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)) ≫
      Γ₂N₂.hom.app ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫
        Preadditive.DoldKan.equivalence.inverse.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    (𝟙 (N₁ ⋙ Γ₂)).app X
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
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      K[X].d i j ≫
        ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
          (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0

Tactic:
Preadditive.comp_sum,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j k : ℕ
x✝¹ : (ComplexShape.down ℕ).Rel i j
x✝ : (ComplexShape.down ℕ).Rel j k
eq :
  K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) +
      ∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        K[X].d i j ≫ (s.πSummand j_1 ≫ (s.cofan (op ⦋j⦌)).inj j_1) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫
      K[X].d i j ≫
        s.πSummand (IndexSet.id (op ⦋j⦌)) ≫
          (s.cofan (op ⦋j⦌)).inj (IndexSet.id (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)

Tactic:
ext n
  have eq₁ : (N₂Γ₂.inv.app (N₂.obj P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) ≫
      ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) := by
    simp only [N₂Γ₂_inv_app_f_f, N₂_obj_p_f, assoc]
  have eq₂ : ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) := by
    dsimp
    rw [PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₂N₂.natTrans_app_f_app]
    dsimp
    rw [Γ₂N₂ToKaroubiIso_hom_app, assoc, Splitting.ι_desc_assoc, assoc, assoc]
    dsimp [toKaroubi]
    rw [Splitting.ι_desc_assoc]
    simp [Splitting.IndexSet.e]
  simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_f, N₂_obj_p_f, assoc,
    eq₁, eq₂, PInfty_f_naturality_assoc, app_idem, PInfty_f_idem_assoc]

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
fst✝ : ↑TopPair.snd
snd✝ : ↑I
⊢ (ConcreteCategory.hom (map ▷ I ≫ Homotopy.h (F.fst.trans G.fst))) (fst✝, snd✝) =
    (ConcreteCategory.hom (Homotopy.h (F.snd.trans G.snd) ≫ map)) (fst✝, snd✝)

Tactic:
simp only [TopCat.comp_app, Homotopy.h_hom_apply, ContinuousMap.Homotopy.trans_apply]

Goal state after:
X✝ Y✝ X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
fst✝ : ↑TopPair.snd
snd✝ : ↑I
⊢ (if h : ↑(I.homeomorph ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).2) ≤ 1 / 2 then
      F.fst
        (⟨2 * ↑(I.homeomorph ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).2), ⋯⟩,
          ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).1)
    else
      G.fst
        (⟨2 * ↑(I.homeomorph ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).2) - 1, ⋯⟩,
          ((ConcreteCategory.hom (map ▷ I)) (fst✝, snd✝)).1)) =
    (ConcreteCategory.hom map)
      (if h : ↑(I.homeomorph snd✝) ≤ 1 / 2 then F.snd (⟨2 * ↑(I.homeomorph snd✝), ⋯⟩, fst✝)
      else G.snd (⟨2 * ↑(I.homeomorph snd✝) - 1, ⋯⟩, fst✝))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
simp only [simplyConnectedSpace_iff, equiv_punit_iff_unique,
    FundamentalGroupoid.nonempty_iff X, and_congr_right_iff, Nonempty.forall]
  intros
  exact ⟨fun h _ _ => h _ _, fun h _ _ => h _ _⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: case mp
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
hall : ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
⊢ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

Tactic:
exact ⟨hpc, fun x γ => hall γ (Path.refl x)⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ IsIso HoCat.adj.counit

Tactic:
by
  dsimp [HoCat.adj]
  infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
j : Fin (n + 1)
⊢ j ∈ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i}

Tactic:
apply Or.imp _ id (h j)

Goal state after:
n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
j : Fin (n + 1)
⊢ j ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) →
    j ∈ Set.range ⇑(stdSimplex.asOrderHom s)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case mpr.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
x : c.pt
⊢ ∃ a, d.multispan.descColimitType c a = x

Tactic:
obtain ⟨i, y, rfl⟩ := h₂ x
      exact ⟨d.multispan.ιColimitType (.right i) y, rfl⟩

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hS : Sᶜ = {j}
⊢ S = {j}ᶜ

Tactic:
by simp [← hS]

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
h : S = Finset.univ ∨ Sᶜ = {j}
⊢ S = Finset.univ ∨ S = {j}ᶜ

Tactic:
grind [eq_compl_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝))

Tactic:
symm
      apply Quot.sound
      apply Rel.inl_inr

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

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2} = Λ[2, 0]

Tactic:
apply le_antisymm

Goal state after:
case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2} ≤ Λ[2, 0]

case a
⊢ Λ[2, 0] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: ⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2} = Λ[2, 1]

Tactic:
apply le_antisymm

Goal state after:
case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 1]

case a
⊢ Λ[2, 1] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d : ℕ
x : ↑(X.nonDegenerate d)
n : ℕ
h : ↑x ∈ (X.skeleton n).obj (op ⦋d⦌)
⊢ d < n

Tactic:
obtain ⟨x, hx⟩ := x

Goal state after:
X : SSet
d n : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
h : ↑⟨x, hx⟩ ∈ (X.skeleton n).obj (op ⦋d⦌)
⊢ d < n
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl.inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₂ y₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) y₂)
⊢ (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom r) y₂

Tactic:
obtain rfl : x₂ = y₂ := hr' eq

Goal state after:
case inl.inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) x₂)
⊢ (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom r) x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.skeleton (n + 1) = X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
apply le_antisymm

Goal state after:
case a
X : SSet
n : ℕ
⊢ X.skeleton (n + 1) ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: ⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} = Λ[2, 2]

Tactic:
apply le_antisymm

Goal state after:
case a
⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 2]

case a
⊢ Λ[2, 2] ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
⊢ t ≫ r = l ≫ b

Tactic:
simp only [← cancel_mono k, Category.assoc, facr, facb, h₁.w]

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton (n + 1) =
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
apply le_antisymm

Goal state after:
case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton (n + 1) ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
c : Cell i d
s : Δ[d] _⦋n⦌
hy :
  (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) s ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
hs : s ∉ ∂Δ[d].obj (op ⦋n⦌)
⊢ Epi (stdSimplex.objEquiv s)

Tactic:
simpa [SimplexCategory.epi_iff_surjective, boundary] using! hs

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

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

Tactic:
obtain _ | m := m

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

case mk.succ
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m + 1⦌, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
⊢ (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₂.simplex

Tactic:
rwa [← c₁.b_app_ι_app_objEquiv_symm_val f₁, ← c₂.b_app_ι_app_objEquiv_symm_val f₂]

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

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1⦌
⊢ X.spine m ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1) x).interval 1 m ⋯

Tactic:
obtain _ | m := m

Goal state after:
case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ X.spine 0 ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (0 + 1) x).interval 1 0 ⋯

case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯
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
D : Type u''
inst✝¹ : Category.{v'', u''} D
inst✝ : EnrichedOrdinaryCategory V D
X : ForgetEnrichment V D
⊢ (eHomEquiv V).symm (homTo V (𝟙 X)) = 𝟙 («to» V X)

Tactic:
by rw [ForgetEnrichment.homTo_id, ← eHomEquiv_id, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
C : Type u
inst✝ : Category.{max u v, u} C
⊢ adj.homEquiv (of V) (Cat.of C) = (Cat.Hom.equivFunctor (Cat.freeRefl.obj (of V)) (Cat.of C)).trans adj.homEquiv

Tactic:
ext F
  apply Adjunction.homEquiv_unit

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

Goal state before:
pp: case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
· obtain ⟨i', rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)
    rw [Fin.castSucc_lt_castSucc_iff] at h
    obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
    rw [← Fin.le_castSucc_iff] at h
    exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_le h]⟩

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

Goal state before:
pp: case «0»
i' : Fin 2
⊢ δ i' ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Tactic:
fin_cases i'

Goal state after:
case «0».«0»
⊢ δ ((fun i ↦ i) ⟨0, ⋯⟩) ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

case «0».«1»
⊢ δ ((fun i ↦ i) ⟨1, ⋯⟩) ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

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

Tactic:
simp only [List.length_cons] at hk
    subst hk
    set a₀ := hL.head
    have aux (t : Fin (m₂ + 2)) :
        (a₀.predAbove t : ℕ) = if a < ↑t then (t : ℕ) - 1 else ↑t := by
      simp only [Fin.predAbove, a₀]
      split_ifs with h₁ h₂ h₂
      · rfl
      · simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁; grind
      · simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val, not_lt] at h₁; grind
      · rfl
    have := h_rec _ _ hL.of_cons (by grind) hj
    have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
    simpa only [toSimplexCategory_obj_mk, SimplexCategory.len_mk, standardσ_cons, Functor.map_comp,
      toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategory.mkHom,
      SimplexCategory.comp_toOrderHom, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe,
      Function.comp_apply, Fin.predAboveOrderHom_coe, simplicialEvalσ, ha₀, ← this] using aux _

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)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin (n + 1)
⊢ (X.spine n ((ConcreteCategory.hom m) x)).vertex i =
    Path.vertex
      { 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 := ⋯ }
      i

pp: case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom m) x)).arrow i =
    Path.arrow
      { 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 := ⋯ }
      i

Tactic:
· exact ConcreteCategory.congr_hom (hm (StructuredArrow.mk
        (Y := op ⦋0⦌2) (⦋0⦌.const ⦋n⦌ i).op)) x

Goal state after:
case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
i : Fin n
⊢ (X.spine n ((ConcreteCategory.hom m) x)).arrow i =
    Path.arrow
      { 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 := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : ↑P.I
y : ↑P.II
⊢ ↑x ≠ ↑y

Tactic:
obtain ⟨x, hx⟩ := x

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
x : A.N
hx : x ∈ P.I
⊢ ↑⟨x, hx⟩ ≠ ↑y