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

Goal state before:
pp: case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
⊢ b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

Tactic:
hb

Goal state after:
case pos.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : A.EqId
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
dsimp at h

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : A = Splitting.IndexSet.id (op ⦋j⦌)
⊢ Φ.f (unop A.fst).len ≫ (S₂.s.cofan (op ⦋j⦌)).inj A ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ Φ.f j ≫ 𝟙 (S₂.s.N j) =
    (S₁.s.cofan (op ⦋j⦌)).inj (Splitting.IndexSet.id (op ⦋j⦌)) ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
rw [comp_id, Splitting.cofan_inj_πSummand_eq_id_assoc]

Goal state after:
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
⊢ ∀ (X : SimplicialObject C), IsIso (Γ₂N₁.natTrans.app X)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ IsIso (Γ₂N₁.natTrans.app X)
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
X : SimplicialObject C
⊢ IsIso (Γ₂N₁.natTrans.app X)

Tactic:
rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ IsIso ((Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X))
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ∀ {x y : C(X, Y)}, x.Homotopic y → y.Homotopic x

Tactic:
apply symm

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set X
⊢ ∀ {x y : C(X, Y)}, x.HomotopicRel y S → y.HomotopicRel x S

Tactic:
apply symm

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ (F.eval x.1).extend (2 * ↑x.2) = (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩

Tactic:
exact Path.extend_apply _ _

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ (G.eval x.1).extend (2 * ↑x.2 - 1) = (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩

Tactic:
exact Path.extend_apply _ _

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
this✝ : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map f)

Tactic:
adj.unit_naturality

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
this✝ : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = f ≫ adj.unit.app Y
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: t : ↑I
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I

Tactic:
split_ifs <;> constructor

Goal state after:
case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ 2 * ↑t

case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ≤ 1

case neg.left
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1

case neg.right
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 1
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
⊢ ∀ (X : C₁), IsIso ((Functor.whiskerRight adj.unit W.Q).app X)

Tactic:
intro X

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
X : C₁
⊢ IsIso ((Functor.whiskerRight adj.unit W.Q).app X)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: t : ↑I
⊢ (if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I

Tactic:
split_ifs <;> constructor

Goal state after:
case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 0 ≤ 2 * ↑t

case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ≤ 1

case pos.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ ↑t + 1 / 4

case pos.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ≤ 1

case neg.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * (↑t + 1)

case neg.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ≤ 1
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
⊢ ∀ (X : CofibrantObject C), IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).app X)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
X : CofibrantObject C
⊢ IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).app X)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
⊢ ∀ (X : C), IsIso ((HoCat.resolutionCompToLocalizationNatTrans L).app X)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
X : C
⊢ IsIso ((HoCat.resolutionCompToLocalizationNatTrans L).app X)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ ∀ (x y : CofibrantObject C) (f₁ f₂ : x ⟶ y),
    homRel C f₁ f₂ → bifibrantResolution'.map f₁ = bifibrantResolution'.map f₂

Tactic:
intro X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ ∀ (y : CofibrantObject C) (f₁ f₂ : X ⟶ y), homRel C f₁ f₂ → bifibrantResolution'.map f₁ = bifibrantResolution'.map f₂
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ (weakEquivalences (HoCat C)).IsInvertedBy HoCat.bifibrantResolution

Tactic:
intro X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ ∀ ⦃Y : HoCat C⦄ (f : X ⟶ Y), weakEquivalences (HoCat C) f → IsIso (HoCat.bifibrantResolution.map f)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case left
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.left l) z

Tactic:
exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z, by rw [ιColimitType_map]⟩

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

Goal state before:
pp: case succ
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[n + 1].obj (op ⦋m⦌)

Tactic:
obtain ⟨i, q, rfl⟩ := SimplexCategory.eq_comp_δ_of_not_surjective f (fun hf ↦ by
      rw [← SimplexCategory.epi_iff_surjective] at hf
      have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
      lia)

Goal state after:
case succ
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm (q ≫ SimplexCategory.δ i) ∈ ∂Δ[n + 1].obj (op ⦋m⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
n : ℕ
⊢ monomorphisms SSet ∂Δ[n].ι

Tactic:
exact monomorphisms.infer_property _

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

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

Tactic:
exact monomorphisms.infer_property _

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

Goal state before:
pp: X : SSet
d n : ℕ
h : d < n
⊢ (X.skeleton n).obj (op ⦋d⦌) = ⊤

Tactic:
rw [← top_le_iff]
  intro x _
  exact mem_skeleton _ _ h

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

Goal state before:
pp: X : SSet
i : ℕ
x : X _⦋i⦌
n : ℕ
hi : i < n
⊢ Subcomplex.ofSimplex x ≤ X.skeleton n

Tactic:
by
  simpa using X.mem_skeleton x hi

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

Goal state before:
pp: case inr.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₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) y₂)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom r) y₂

Tactic:
obtain ⟨x₁, rfl, rfl⟩ := exists_of_isPullback h₂ y₂ x₃ eq.symm
    rw [w]

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

Goal state before:
pp: case a.left
X : SSet
n : ℕ
⊢ X.skeleton n ≤ X.skeleton (n + 1)

pp: case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)

Tactic:
· exact X.skeleton.monotone (by simp)

Goal state after:
case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
y : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : x ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
h : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) ⟨x, hx⟩) = ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y)
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = ⟨x, hx⟩ ∧ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = y

Tactic:
dsimp at h

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
y : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : x ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
h : x = ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y)
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = ⟨x, hx⟩ ∧ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
x : (MultispanShape.ofLinearOrder ↑{1}ᶜ).L
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst x ≫
      match (MultispanShape.ofLinearOrder ↑{1}ᶜ).fst x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => ⋯.elim
        | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd x ≫
      match (MultispanShape.ofLinearOrder ↑{1}ᶜ).snd x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => ⋯.elim
        | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
dsimp at x ⊢

Goal state after:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
x : ↑{x | x.1 < x.2}
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑x).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑x).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
x : (MultispanShape.ofLinearOrder ↑{2}ᶜ).L
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst x ≫
      match (MultispanShape.ofLinearOrder ↑{2}ᶜ).fst x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
        | 2, hi => ⋯.elim
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd x ≫
      match (MultispanShape.ofLinearOrder ↑{2}ᶜ).snd x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
        | 2, hi => ⋯.elim
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
dsimp at x ⊢

Goal state after:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
x : ↑{x | x.1 < x.2}
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑x).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑x).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).vertex i =
    ((X.spine m hₘ Δ).interval j l h).vertex i

pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).arrow i =
    ((X.spine m hₘ Δ).interval j l h).arrow i

Tactic:
· dsimp only [spine_vertex, Path.interval]
    rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp,
      const_subinterval_eq]

Goal state after:
case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).arrow i =
    ((X.spine m hₘ Δ).interval j l h).arrow i
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
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (Y.map (mkOfSucc k).op)) (sy.spineToSimplex (f.map σ)) =
    (ConcreteCategory.hom (σ.app (Opposite.op ⦋1⦌)))
      ((ConcreteCategory.hom (X.map (mkOfSucc k).op)) (sx.spineToSimplex f))

Tactic:
spineToSimplex_arrow,

Goal state after:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (f.map σ).arrow k =
    (ConcreteCategory.hom (σ.app (Opposite.op ⦋1⦌)))
      ((ConcreteCategory.hom (X.map (mkOfSucc k).op)) (sx.spineToSimplex f))
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
k : Fin (n + 1)
⊢ (f.map σ).arrow k =
    (ConcreteCategory.hom (σ.app (Opposite.op ⦋1⦌)))
      ((ConcreteCategory.hom (X.map (mkOfSucc k).op)) (sx.spineToSimplex f))

Tactic:
spineToSimplex_arrow,

Goal state after:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (f.map σ).arrow k = (ConcreteCategory.hom (σ.app (Opposite.op ⦋1⦌))) (f.arrow k)
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'
⊢ CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 (homEquiv h) ≫ Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
conv => enter [2, 1]; exact ((id_comp _).trans (comp_id _)).symm

Goal state after:
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'
⊢ CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 (homEquiv h) ≫ Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    F.map f_1 ≫ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
      ((ConcreteCategory.hom (f.app X)) PUnit.unit).app X (𝟙 (Opposite.unop (Opposite.op X))) ≫ G.map f_1

Tactic:
intro X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X : C
⊢ ∀ ⦃Y : C⦄ (f_1 : X ⟶ Y),
    F.map f_1 ≫ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
      ((ConcreteCategory.hom (f.app X)) PUnit.unit).app X (𝟙 (Opposite.unop (Opposite.op X))) ≫ G.map f_1
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ∀ {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), tensorHom f g = whiskerRight f X₂ ≫ Y₁.whiskerLeft g

Tactic:
by intros; ext; simp [tensorHom_def]

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

Goal state before:
pp: X : Truncated 2
x₁ y₁ x₂ y₂ : OneTruncation₂ X
f : x₁ ⟶ y₁
hx : x₁ = x₂
hy : y₁ = y₂
⊢ (Quiver.homOfEq f hx hy).edge = f.edge

Tactic:
subst hx hy
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
fac fac' : W₁.MapFactorizationData W₂ f
this : Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ fac.Z = fac'.Z

Tactic:
obtain rfl : fac = fac' := Subsingleton.elim _ _

Goal state after:
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 : W₁.MapFactorizationData W₂ f
this : Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ fac.Z = fac.Z