mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
⊢ j ≥ max N N2 → padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
hj

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑(p - 1)‖ = 1

Tactic:
norm_natCast_eq_one_iff

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ p.Coprime (p - 1)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)
      rw [PadicSeq.val_eq_iff_norm_eq hf hg]
      exact PadicSeq.norm_equiv h

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
⊢ ⟦f⟧ ≠ 0 → ‖⟦f⟧‖ = ↑p ^ (-valuation ⟦f⟧)

Tactic:
intro hf

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ‖⟦f⟧‖ = ↑p ^ (-valuation ⟦f⟧)
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)
j : Fin (n + 1)
⊢ j ∈ {i | ↑i < q} →
    (((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
        (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
      0

Tactic:
hj

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)
j : Fin (n + 1)
hj : j ∈ {i | ↑i < q}
⊢ (((P ↑j).f (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ f.app Δ = s.φ f (unop A.fst).len ≫ Y.map A.e.op

Tactic:
by
  simp only [cofan_inj_eq_assoc, φ, assoc]
  rw [NatTrans.naturality]

Goal state after:
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 : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ ((s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ PInfty.f i) ≫ K[X].d i j =
    ((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⦌)) ≫ PInfty.f j

Tactic:
rw [assoc, assoc, assoc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty,
              HomologicalComplex.Hom.comm]

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ 𝟭 (SingleObj M) = e.toMonoidHom.toFunctor ⋙ e.symm.toMonoidHom.toFunctor

Tactic:
rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ (MonoidHom.id M).toFunctor = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ e.symm.toMonoidHom.toFunctor ⋙ e.toMonoidHom.toFunctor = 𝟭 (SingleObj N)

Tactic:
rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
⊢ (e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = (MonoidHom.id N).toFunctor
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as

Tactic:
apply Prod.ext <;> simp <;> rfl

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

Goal state before:
pp: case mpr
Y : Type u_2
inst✝ : TopologicalSpace Y
hpc : PathConnectedSpace Y
x y : Y
p₁ p₂ : Path x y
hloops : ∀ (x : Y) (γ : Path x x), ⟦γ⟧ = ⟦Path.refl x⟧
h : Path.Homotopic.Quotient.trans ⟦p₁⟧ (Path.Homotopic.Quotient.symm ⟦p₂⟧) = Path.Homotopic.Quotient.refl x
⊢ mk p₁ = mk p₂

Tactic:
calc ⟦p₁⟧
      _ = trans (trans ⟦p₁⟧ (symm ⟦p₂⟧)) ⟦p₂⟧ := by simp
      _ = ⟦p₂⟧ := by grind

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence (toHoCat.map { hom := HoCat.pResolutionObj X.obj })

Tactic:
weakEquivalence_toHoCat_map_iff,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence { hom := HoCat.pResolutionObj X.obj }
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject C) f

Tactic:
by rwa [weakEquivalence_iff] at hf

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
g : BifibrantObject.toHoCat.obj X.bifibrantResolutionObj ⟶ BifibrantObject.toHoCat.obj Y
f : X.bifibrantResolutionObj ⟶ Y
h :
  toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map f) =
    toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map g
⊢ BifibrantObject.toHoCat.map f = g

Tactic:
obtain ⟨g, rfl⟩ := BifibrantObject.toHoCat.map_surjective g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject C
f g : X.bifibrantResolutionObj ⟶ Y
h :
  toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map f) =
    toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map g)
⊢ BifibrantObject.toHoCat.map f = BifibrantObject.toHoCat.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence (toHoCat.map X.iBifibrantResolutionObj)

Tactic:
weakEquivalence_toHoCat_map_iff,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
X Y : Over S
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Cofibration (Over.Hom.left f)

Tactic:
by
  rwa [← cofibrations_over_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
⊢ x ∈
      {x |
        ∃ (hx : x ∈ A.obj U✝), (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩} →
    x ∈
      ⇑(ConcreteCategory.hom (F₁.map φ)) ⁻¹'
        {x |
          ∃ (hx : x ∈ A.obj V✝), (ConcreteCategory.hom (f.app V✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app V✝)) ⟨x, hx⟩}

Tactic:
rintro ⟨hx, h⟩
    exact ⟨A.map _ hx,
      (NatTrans.naturality_apply f φ ⟨x, hx⟩).trans (Eq.trans (by rw [h])
        (NatTrans.naturality_apply g φ ⟨x, hx⟩).symm)⟩

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

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
k : Fin (n + 1)
hk : k ∉ {i, a, b}
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)

Tactic:
simp only [mem_insert, mem_singleton, not_or] at hk

Goal state after:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
k : Fin (n + 1)
hk : ¬k = i ∧ ¬k = a ∧ ¬k = b
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)
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
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✝⟩

Tactic:
obtain ⟨i, ⟨y, rfl⟩⟩ := hx

Goal state after:
n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
i : Fin (n + 1 + 1)
y : unop m ⟶ ⦋n⦌
hx : (ConcreteCategory.hom (Δ[n + 1].map y.op)) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ∈ ∂Δ[n + 1].obj m
⊢ (ConcreteCategory.hom (f.app m)).toFun
      ⟨(ConcreteCategory.hom (Δ[n + 1].map y.op)) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)), hx⟩ =
    (ConcreteCategory.hom (g.app m)).toFun
      ⟨(ConcreteCategory.hom (Δ[n + 1].map y.op)) (stdSimplex.objEquiv.symm (SimplexCategory.δ i)), hx⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
j : Fin (n + 1 + 1)
⊢ ¬j = i → yonedaEquiv (stdSimplex.δ j) ∈ (Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌)

Tactic:
hj

Goal state after:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
j : Fin (n + 1 + 1)
hj : ¬j = i
⊢ yonedaEquiv (stdSimplex.δ j) ∈ (Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij = faceι i j hij

Tactic:
by
  rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} j).hom, Iso.hom_inv_id_assoc]
  rfl

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

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
⊢ ∀ (h : j ≠ i),
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h) =
      (ConcreteCategory.hom ((Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
hj

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj) =
    (ConcreteCategory.hom ((Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

Tactic:
rw [horn_eq_iSup, iSup_le_iff]

Goal state after:
case a
⊢ ∀ (i : ↑{0}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

Tactic:
rw [horn_eq_iSup, iSup_le_iff]

Goal state after:
case a
⊢ ∀ (i : ↑{1}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

Tactic:
rw [horn_eq_iSup, iSup_le_iff]

Goal state after:
case a
⊢ ∀ (i : ↑{2}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
⊢ ∀ (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k),
    (stdSimplex.δ (k.pred ⋯) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g

Tactic:
hj

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
hj : j ≠ i
⊢ ∀ (hk : k ≠ i) (hjk : j < k), (stdSimplex.δ (k.pred ⋯) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

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

Tactic:
hj

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

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (stdSimplex.objEquiv.symm (SimplexCategory.δ j)))

Tactic:
Equiv.apply_symm_apply,

Goal state after:
case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc = stdSimplex.objEquiv.symm (mkOfSucc k ≫ SimplexCategory.δ j)
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (stdSimplex.objEquiv.symm (SimplexCategory.δ j)))

Tactic:
Equiv.apply_symm_apply,

Goal state after:
case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ = stdSimplex.objEquiv.symm (mkOfSucc k ≫ SimplexCategory.δ j)
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
φ : X ⟶ Y
⊢ F.map φ ≫ ((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 φ

Tactic:
rw [← (f.app X (PUnit.unit)).naturality φ]

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 Y : C
φ : X ⟶ Y
⊢ F.map φ ≫ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    F.map φ ≫
      ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y
        ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map φ)) (𝟙 (Opposite.unop (Opposite.op X))))
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
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F ⟶ G
h : ∀ (X : C), α.out.app X = β.out.app X
⊢ α = β

Tactic:
by
  rcases α with ⟨α⟩
  rcases β with ⟨β⟩
  congr
  ext
  apply h

Goal state after:
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 : ForgetEnrichment W (TransportEnrichment F D)
⊢ (e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X))
      ((e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)).symm (eId W (ForgetEnrichment.to W X))) =
    (e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) (eId V (ForgetEnrichment.to W X))

Tactic:
Equiv.apply_symm_apply,

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 : ForgetEnrichment W (TransportEnrichment F D)
⊢ eId W (ForgetEnrichment.to W X) =
    (e (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W X)) (eId V (ForgetEnrichment.to W X))
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✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝))
      ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W (f ≫ g))) =
    (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝))
      ((λ_ (𝟙_ V)).inv ≫
        ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
            (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
          eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))

Tactic:
Equiv.apply_symm_apply,

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✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homTo W (f ≫ g) =
    (e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Z✝))
      ((λ_ (𝟙_ V)).inv ≫
        ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
            (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g)) ≫
          eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: case mk.mk.mk
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
W✝ X✝ Y✝ Z✝ : A.HomotopyCategory₂
f✝ : W✝ ⟶ X✝
f : Edge W✝.pt X✝.pt
g✝ : X✝ ⟶ Y✝
g : Edge X✝.pt Y✝.pt
h✝ : Y✝ ⟶ Z✝
h : Edge Y✝.pt Z✝.pt
⊢ (Quot.mk (⇑(instSetoidEdge W✝.pt X✝.pt)) f ≫ Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) g) ≫
      Quot.mk (⇑(instSetoidEdge Y✝.pt Z✝.pt)) h =
    Quot.mk (⇑(instSetoidEdge W✝.pt X✝.pt)) f ≫
      Quot.mk (⇑(instSetoidEdge X✝.pt Y✝.pt)) g ≫ Quot.mk (⇑(instSetoidEdge Y✝.pt Z✝.pt)) h

Tactic:
exact (Quasicategory₂.fill31 (compStruct f g) (compStruct g h)
      (compStruct _ _)).some.homotopyCategory₂_fac

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

Goal state before:
pp: V W : Truncated 2
f : V ⟶ W
⊢ ∀ (x y : Cat.FreeRefl (OneTruncation₂ V)) (f₁ f₂ : x ⟶ y),
    OneTruncation₂.HoRel₂ V f₁ f₂ →
      (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map f₁ =
        (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map f₂

Tactic:
by
      rintro _ _ _ _ ⟨h⟩
      exact CategoryTheory.Quotient.sound _ ⟨h.map f⟩

Goal state after: