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

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

Tactic:
fin_cases i
        dsimp at h hi
        rw [show q = 0 by lia]
        change X.σ 0 ≫ (P 1).f 1 = 0
        simp only [P_succ, HomologicalComplex.add_f_apply, comp_add,
          AlternatingFaceMapComplex.obj_d_eq, Hσ,
          HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl),
          comp_id]
        rw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm]
        dsimp [P_zero]
        rw [comp_id, Fin.sum_univ_two,
          Fin.sum_univ_succ, Fin.sum_univ_two]
        simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.val_succ,
          Fin.val_one, mul_neg, one_mul, neg_mul, neg_neg, id_comp, add_comp, comp_add, neg_comp,
          comp_neg, Fin.succ_zero_eq_one]
        rw [← Fin.castSucc_one, SimplicialObject.δ_comp_σ_self, ← Fin.castSucc_zero (n := 1),
          SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ, comp_id, ← Fin.castSucc_zero (n := 2),
          ← Fin.succ_zero_eq_one,
          SimplicialObject.δ_comp_σ_of_le X
            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
          ← Fin.castSucc_zero (n := 1), SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ_assoc]
        simp only [add_neg_cancel, add_zero, zero_add]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p)

Tactic:
dsimp [cofan]
  rw [assoc, ← X.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f (unop A.fst).len ≫ (S₂.s.cofan Δ).inj A

Tactic:
rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : Karoubi (Karoubi C)
f : X✝ ⟶ Y✝
⊢ { X := X✝.X.X, p := X✝.p.f, idem := ⋯ }.p ≫ f.f.f ≫ { X := Y✝.X.X, p := Y✝.p.f, idem := ⋯ }.p = f.f.f

Tactic:
by simpa only [hom_ext_iff] using! f.comm

Goal state after:
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 ≫ (∑ i with ↑i < n + 1, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev) ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
Preadditive.sum_comp,

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
⊢ 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
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 ≫ (∑ A, s.πSummand A ≫ (s.cofan (op ⦋n⦌)).inj A) ≫ PInfty.f n = 0

Tactic:
Preadditive.sum_comp,

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
⊢ f ≫ ∑ j, (s.πSummand j ≫ (s.cofan (op ⦋n⦌)).inj j) ≫ PInfty.f n = 0
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 ≫
        (∑ i ∈ {IndexSet.id (op ⦋j⦌)}ᶜ, s.πSummand i ≫ (s.cofan (op ⦋j⦌)).inj i) ≫
          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.sum_comp,

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⦌)) +
      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
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f Δ'.len ≫ X.map i.op

Tactic:
induction Δ' using SimplexCategory.rec with | _ n'
   =>  _ 

Goal state after:
case mk.mk
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f ⦋n'⦌.len ≫ X.map i.op
Module: Mathlib.Topology.Category.TopCat.Monoidal

Goal state before:
pp: ⊢ homeomorph 0 = 0

Tactic:
by simp [OfNat.ofNat]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Monoidal

Goal state before:
pp: ⊢ homeomorph 1 = 1

Tactic:
by simp [OfNat.ofNat]

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

Goal state before:
pp: case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl] -- Porting note: this ↓ `simp` didn't do this
    slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
    rfl

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

Goal state before:
pp: case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
          hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl] -- Porting note: this ↓ `simp` didn't do this
    slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
    rfl

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 : C
⊢ ∃ X', ∃ (_ : IsCofibrant X'), ∃ p, Fibration p ∧ WeakEquivalence p

Tactic:
have h := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C)
    (initial.to X)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (initial.to X)
⊢ ∃ X', ∃ (_ : IsCofibrant X'), ∃ p, Fibration p ∧ WeakEquivalence p
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
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

Tactic:
change toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map f) =
    toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g) at h

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.ιCofibrantObject.map f) =
    toHoCat.map (X.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g)
⊢ BifibrantObject.toHoCat.map f = BifibrantObject.toHoCat.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

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

Tactic:
by
  simp only [weakEquivalence_iff, weakEquivalences_over_def, MorphismProperty.over_iff]

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h₁ : ∂Δ[n] ≤ A
h₂ : A ≠ ⊤
⊢ A ≤ ∂Δ[n]

Tactic:
le_boundary_iff

Goal state after:
n : ℕ
A : Δ[n].Subcomplex
h₁ : ∂Δ[n] ≤ A
h₂ : A ≠ ⊤
⊢ A ≠ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

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

Tactic:
by
  simp [faceι]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hij : j ≠ i
⊢ faceι i j hij ≫ Λ[n, i].ι = (stdSimplex.face {j}ᶜ).ι

Tactic:
by
  simp [faceι]

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

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx : (ConcreteCategory.hom (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ ∂Δ[d].obj (op ⦋n⦌)

Tactic:
← c.preimage_map,

Goal state after:
case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx : (ConcreteCategory.hom (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ∀ (x₃ y₃ : evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d)),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
        (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) x₃ =
            (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) y₃ →
          x₃ = y₃

Tactic:
dsimp
      intro x₁ x₂ hx₁ hx₂ h
      obtain ⟨c₁, f₁, _, rfl⟩ := isPushout_aux x₁ hx₁
      obtain ⟨c₂, f₂, _, rfl⟩ := isPushout_aux x₂ hx₂
      rw [Subtype.ext_iff] at h
      replace h : Y.map f₁.op c₁.simplex = Y.map f₂.op c₂.simplex := by
        rwa [← c₁.b_app_ι_app_objEquiv_symm_val f₁, ← c₂.b_app_ι_app_objEquiv_symm_val f₂]
      obtain rfl : c₁ = c₂ := by
        ext
        exact Subtype.ext_iff.mp
          (Y.unique_nonDegenerate_simplex _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
            f₂ ⟨_, c₂.nonDegenerate⟩ h)
      obtain rfl : f₁ = f₂ :=
        Y.unique_nonDegenerate_map _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
          f₂ ⟨_, c₁.nonDegenerate⟩ h
      rfl

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ }))) (f.vertex i.castSucc)

Tactic:
by
    simp only [← f.arrow_src i]
    exact ConcreteCategory.congr_hom (σ.naturality (tr (δ 1)).op) _ |>.symm

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
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫ ((eHomEquiv V) (f ≫ f') ▷ X'' ⟶[V] Y) ≫ eComp V X X'' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y

Tactic:
eHomEquiv_comp,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      (((λ_ (𝟙_ V)).inv ≫ ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) f') ≫ eComp V X X' X'') ▷ X'' ⟶[V] Y) ≫ eComp V X X'' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) (g ≫ g') ≫ eComp V X Y Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
eHomEquiv_comp,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ ((λ_ (𝟙_ V)).inv ≫ ((eHomEquiv V) g ⊗ₘ (eHomEquiv V) g') ≫ eComp V Y Y' Y'') ≫ eComp V X Y Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: 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)

Tactic:
Functor.LaxMonoidal.μ_natural_right_assoc

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 (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)
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
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    Functor.LaxMonoidal.ε F ≫
      F.map (ρ_ (𝟙_ V)).inv ≫ F.map ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) g) ≫ F.map (eComp V X✝ Y✝ Z✝)

Tactic:
eHomEquiv_comp,

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
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((λ_ (𝟙_ V)).inv ≫ ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) g) ≫ eComp V X✝ Y✝ Z✝) =
    Functor.LaxMonoidal.ε F ≫
      F.map (ρ_ (𝟙_ V)).inv ≫ F.map ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) g) ≫ F.map (eComp V X✝ Y✝ Z✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ σ i✝ = 𝟙 (mk n)

Tactic:
exact δ_comp_σ_self

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

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

Tactic:
exact δ_comp_σ_self

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

Goal state before:
pp: case of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1) = mk (m_1 + b)) (h : L.length = b), IsAdmissible m_1 L ∧ σ k = standardσ L ⋯

Tactic:
| @σ m k =>

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

Goal state before:
pp: case comp_of.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
m : ℕ
k : Fin (m + 1)
g : x✝ ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
h_rec :
  ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk (m + 1)) (h₂ : x✝ = mk (m_1 + b)) (h : L.length = b), IsAdmissible m_1 L ∧ g = standardσ L ⋯
⊢ ∃ L m_1 b,
    ∃ (h₁ : mk m_1 = mk m) (h₂ : x✝ = mk (m_1 + b)) (h : L.length = b), IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯

Tactic:
| @σ m k =>

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

Goal state before:
pp: X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (associativity'Iso X Y Z).hom.app xyz =
    𝟙
      (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
        xyz)

Tactic:
by
  change 𝟙 _ ≫ _ ≫ 𝟙 _ = _
  rw [Category.id_comp, Category.comp_id]
  rfl

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.castSucc)) k

Tactic:
toMk₁_of_le_castSucc,

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ 1 = (ConcreteCategory.hom (toMk₁ i.castSucc)) k

case neg.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
x : Fin (n + 1)
⊢ map' OrderHom.id x.castSucc = x.castSucc

Tactic:
rw [map'_eq_castSucc_iff]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
G : C
hG : P G
g : G ⟶ Y
⊢ (MonoOver.mk i).Factors g

Tactic:
exact h G hG g

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair

Tactic:
apply ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι := ⋯
this✝ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C := ⋯
G : C
hG : P G
this : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
⊢ HasCardinalLT (Arrow WalkingParallelPair) κ
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsDense
⊢ F.leftKanExtensionUnit F ≫ F.whiskerLeft (leftKanExtensionIso F).hom = F.rightUnitor.inv

Tactic:
simp [Functor.IsDense.leftKanExtensionIso]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerAnodyneExtensions ≤ modelCategoryQuillen.J.rlp.llp

Tactic:
innerAnodyneExtensions_eq_llp_rlp,

Goal state after:
⊢ innerHornInclusions.rlp.llp ≤ modelCategoryQuillen.J.rlp.llp