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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ (N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P =
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          N₁ ⋙
            (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
              (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
      P

Tactic:
refine HomologicalComplex.ext ?_ ?_

Goal state after:
case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).X =
    ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            N₁ ⋙
              (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
        P).X

case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).obj P).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫
          ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
                    N₁ ⋙
                      (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
                        (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj
                P).d
            i j
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)
⊢ IsIso (Γ₂N₂.natTrans.app P)

Tactic:
have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) := by
      have h := identity_N₂_objectwise P
      dsimp only [Functor.id_obj, Functor.comp_obj] at h
      rw [hom_comp_eq_id] at h
      rw [h]
      infer_instance

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
this : IsIso (N₂.map (Γ₂N₂.natTrans.app P))
⊢ IsIso (Γ₂N₂.natTrans.app P)
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

Tactic:
congr 2
    apply Subtype.ext
    simp only [coe_symm_eq]
    linarith

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

Goal state before:
pp: case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

Tactic:
congr 2
    apply Subtype.ext
    simp only [coe_symm_eq]
    linarith

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

Goal state before:
pp: x y : Path PUnit.unit PUnit.unit
⊢ x = y

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
⊢ (weakEquivalences (BifibrantObject C)).IsInvertedBy F ↔
    ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g

Tactic:
refine ⟨fun H K L f g h ↦ ?_, fun h X Y f hf ↦ ?_⟩
  · obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
    have := isCofibrant_of_cofibration P.ι
    have : IsIso (F.map (homMk P.ι)) := H _ (by
      rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
      exact inferInstanceAs (WeakEquivalence P.ι))
    simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp]
    congr 1
    simp [← cancel_epi (F.map (homMk P.ι)), ← Functor.map_comp]
  · rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty] at hf
    obtain ⟨g', h₁, h₂⟩ := RightHomotopyClass.whitehead f.hom
    refine ⟨F.map (homMk g'), ?_, ?_⟩
    all_goals
      rw [← F.map_comp, ← F.map_id]
      apply h
      assumption

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun i ↦ (U i).obj n) fun i j ↦ (V i j).obj n
⊢ IsColimit
    (((evaluation SimplexCategoryᵒᵖ (Type u)).obj n).mapCocone
      ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor))

Tactic:
exact (Multicofork.isColimitMapEquiv _ _).2
      (Types.isColimitOfMulticoequalizerDiagram h')

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

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ x₁ ∈ U i₁ ⊓ U i₂

Tactic:
exact ⟨h₁, h₂⟩

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

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ x₁ ∈ U i₁ ⊓ U i₂

Tactic:
exact ⟨h₁, h₂⟩

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].op.preimage (stdSimplex.opIso ⦋n⦌).inv = ∂Δ[n]

Tactic:
ext ⟨⟨d⟩⟩ j

Goal state after:
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ j ∈ (∂Δ[n].op.preimage (stdSimplex.opIso ⦋n⦌).inv).obj (op ⦋d⦌) ↔ j ∈ ∂Δ[n].obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i].op.preimage (stdSimplex.opIso ⦋n⦌).inv = Λ[n, i.rev]

Tactic:
ext ⟨⟨d⟩⟩ j

Goal state after:
n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
⊢ j ∈ (Λ[n, i].op.preimage (stdSimplex.opIso ⦋n⦌).inv).obj (op ⦋d⦌) ↔ j ∈ Λ[n, i.rev].obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
hS : {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
hk : ¬k = 0
⊢ False

Tactic:
· have := Finset.mem_univ (0 : Fin (n + 4))
      rw [← hS] at this
      -- this was produced using `simp? [Fin.ext_iff] at this`
      simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add,
        AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, mem_singleton,
        OfNat.ofNat_ne_zero, or_self, or_false] at this
      obtain rfl | rfl := this <;> tauto

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : S
⊢ (ConcreteCategory.hom (f ≫ inl f g)).toFun x = (ConcreteCategory.hom (g ≫ inr f g)).toFun x

Tactic:
exact Quot.sound (Rel.inl_inr x)

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
x₂ : ∐ X₁
i₁ : T
x₁ : X₁ i₁
hx : (hom (Limits.Sigma.map f)) ((hom ((Cofan.mk (∐ X₁) (Sigma.ι X₁)).inj i₁)) x₁) = (hom (Limits.Sigma.map f)) x₂
⊢ (hom ((Cofan.mk (∐ X₁) (Sigma.ι X₁)).inj i₁)) x₁ = x₂

Tactic:
obtain ⟨i₂, x₂, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₂

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  (hom (Limits.Sigma.map f)) ((hom ((Cofan.mk (∐ X₁) (Sigma.ι X₁)).inj i₁)) x₁) =
    (hom (Limits.Sigma.map f)) ((hom ((Cofan.mk (∐ X₁) (Sigma.ι X₁)).inj i₂)) x₂)
⊢ (hom ((Cofan.mk (∐ X₁) (Sigma.ι X₁)).inj i₁)) x₁ = (hom ((Cofan.mk (∐ X₁) (Sigma.ι X₁)).inj i₂)) x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: case succ
n : ℕ
inst✝ : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ J Λ[n + 1, i].ι

Tactic:
simp only [J, iSup_iff]

Goal state after:
case succ
n : ℕ
inst✝ : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ ∃ i_1, ofHoms (fun i ↦ Λ[i_1 + 1, i].ι) Λ[n + 1, i].ι
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)

Tactic:
· rw [inl_rel'_inr_iff] at hyz
        obtain ⟨s, hs, rfl⟩ := hyz
        obtain rfl := (mono_iff_injective f).1 inferInstance hs
        rw [← h]
        apply Rel'.inl_inr

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

Goal state before:
pp: case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) → ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
rintro ⟨⟩

Goal state after:
case mp.inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ ∃ s,
    (ConcreteCategory.hom f) s = (ConcreteCategory.hom f) s✝ ∧ (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ ⊤ ⊆ ((skeletonOfMono i) n).obj (op ⦋d⦌)

Tactic:
← Y.skeleton_obj_eq_top h

Goal state after:
X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ (Y.skeleton n).obj (op ⦋d⦌) ⊆ ((skeletonOfMono i) n).obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (X.spine m ⋯ ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.succ

Tactic:
by
  rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
⊢ (α_ X.fst Y.fst (U ⊗ U') ≪≫
        X.fst ◁ᵢ Y.snd.β (U ⊗ U') ≪≫
          (α_ X.fst (U ⊗ U') Y.fst).symm ≪≫ X.snd.β (U ⊗ U') ▷ᵢ Y.fst ≪≫ α_ (U ⊗ U') X.fst Y.fst).hom =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      (α_ X.fst Y.fst U ≪≫
              X.fst ◁ᵢ Y.snd.β U ≪≫ (α_ X.fst U Y.fst).symm ≪≫ X.snd.β U ▷ᵢ Y.fst ≪≫ α_ U X.fst Y.fst).hom ▷
          U' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              (α_ X.fst Y.fst U' ≪≫
                  X.fst ◁ᵢ Y.snd.β U' ≪≫ (α_ X.fst U' Y.fst).symm ≪≫ X.snd.β U' ▷ᵢ Y.fst ≪≫ α_ U' X.fst Y.fst).hom ≫
            (α_ U U' (X.fst ⊗ Y.fst)).inv

Tactic:
dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
⊢ (α_ X.fst Y.fst (U ⊗ U')).hom ≫
      X.fst ◁ (Y.snd.β (U ⊗ U')).hom ≫
        (α_ X.fst (U ⊗ U') Y.fst).inv ≫ (X.snd.β (U ⊗ U')).hom ▷ Y.fst ≫ (α_ (U ⊗ U') X.fst Y.fst).hom =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ X.fst Y.fst U).hom ≫
            X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ▷
          U' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              ((α_ X.fst Y.fst U').hom ≫
                X.fst ◁ (Y.snd.β U').hom ≫
                  (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom) ≫
            (α_ U U' (X.fst ⊗ Y.fst)).inv
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ (X.fst ⊗ Y.fst) ◁ f ≫
      (α_ X.fst Y.fst U' ≪≫
          X.fst ◁ᵢ Y.snd.β U' ≪≫ (α_ X.fst U' Y.fst).symm ≪≫ X.snd.β U' ▷ᵢ Y.fst ≪≫ α_ U' X.fst Y.fst).hom =
    (α_ X.fst Y.fst U ≪≫ X.fst ◁ᵢ Y.snd.β U ≪≫ (α_ X.fst U Y.fst).symm ≪≫ X.snd.β U ▷ᵢ Y.fst ≪≫ α_ U X.fst Y.fst).hom ≫
      f ▷ (X.fst ⊗ Y.fst)

Tactic:
dsimp only [Iso.trans_hom, whiskerLeftIso_hom, Iso.symm_hom, whiskerRightIso_hom]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ (X.fst ⊗ Y.fst) ◁ f ≫
      (α_ X.fst Y.fst U').hom ≫
        X.fst ◁ (Y.snd.β U').hom ≫ (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom =
    ((α_ X.fst Y.fst U).hom ≫
        X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ≫
      f ▷ (X.fst ⊗ Y.fst)
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)) =
    (λ_ (𝟙_ W)).inv ≫
      Functor.LaxMonoidal.ε F ▷ 𝟙_ W ≫
        F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
          (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
            Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)

Tactic:
whiskerRight_id_assoc,

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 ((eHomEquiv V) (f ≫ g)) =
    (λ_ (𝟙_ W)).inv ≫
      (ρ_ (𝟙_ W)).hom ≫
        Functor.LaxMonoidal.ε F ≫
          (ρ_ (F.obj (𝟙_ V))).inv ≫
            F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
              (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
                Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)
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✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ (ConcreteCategory.hom (eId (Type v) X ≫ ↾fun f ↦ F.map f)).toFun PUnit.unit =
    (ConcreteCategory.hom (eId (Type v) (F.obj X))).toFun PUnit.unit

Tactic:
exact F.map_id X

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ (α_ X.fst Y.fst U).inv ≫
      (X.snd.β Y.fst).hom ▷ U ≫
        (α_ Y.fst X.fst U).hom ≫
          Y.fst ◁ (X.snd.β U).hom ≫ (α_ Y.fst U X.fst).inv ≫ (Y.snd.β U).hom ▷ X.fst ≫ (α_ U Y.fst X.fst).hom =
    X.fst ◁ (Y.snd.β U).hom ≫
      (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom ≫ U ◁ (X.snd.β Y.fst).hom

Tactic:
← HalfBraiding.monoidal_assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ (X.snd.β (Y.fst ⊗ U)).hom ≫ (Y.snd.β U).hom ▷ X.fst ≫ (α_ U Y.fst X.fst).hom =
    X.fst ◁ (Y.snd.β U).hom ≫
      (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom ≫ U ◁ (X.snd.β Y.fst).hom
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
h : HomotopicL f g
⊢ HomotopicR f g

Tactic:
rcases h with ⟨h⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
h : f.CompStruct (Edge.id y) g
⊢ HomotopicR f g
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
h : HomotopicR f g
⊢ HomotopicL f g

Tactic:
rcases h with ⟨h⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
h : (Edge.id x).CompStruct f g
⊢ HomotopicL f g
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.comp_of.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k
        · exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩
        · obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf
          exact ⟨z, e, m ≫ δ j', he, P_δ.comp_mem _ _ hm (P_δ.δ j'),
            by simp [h'', reassoc_of% fac]⟩

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

Goal state before:
pp: X✝ Y✝ x✝¹ : Truncated 2
x✝ : X✝ ⟶ Y✝
⊢ hoFunctor₂.obj x✝¹ ◁ hoFunctor₂.map x✝ ≫ (iso x✝¹ Y✝).symm.hom = (iso x✝¹ X✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ◁ x✝)

Tactic:
by ext; apply id_prod_mapHomotopyCategory_comp_inverse

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : ∃ x_1 ∈ K.faces, Finset.image f x_1 = x
⊢ x.Nonempty ∧ ∀ ⦃b : Finset β⦄, b ⊆ x → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b

Tactic:
obtain ⟨s', hs', rfl⟩ := h

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty ∧
    ∀ ⦃b : Finset β⦄, b ⊆ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

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

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

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

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

Tactic:
exact f.monotone (I.left_le k hk)

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

Goal state before:
pp: case inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
obtain ⟨y, hy⟩ | hx := Fin.eq_castSucc_or_eq_last (map' g x.castSucc)
    · rw [hy]
      rw [map'_eq_castSucc_iff] at hy
      obtain ⟨z, hz⟩ | hz := Fin.eq_castSucc_or_eq_last (map' f y.castSucc)
      · rw [hz, Eq.comm]
        rw [map'_eq_castSucc_iff] at hz ⊢
        constructor
        · refine hy.1.trans ?_
          simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]
          exact g.monotone (by simpa using hz.1)
        · intro i hi
          exact hy.2 (f i) (by simpa using hz.2 i hi)
      · rw [hz, Eq.comm]
        rw [map'_eq_last_iff] at hz ⊢
        intro i
        exact hy.2 (f i) (by simpa using hz i)
    · rw [Eq.comm, hx, map'_last]
      rw [map'_eq_last_iff] at hx ⊢
      intro i
      apply hx

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

Goal state before:
pp: case inl
n : ℕ
i x : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

pp: case inr
n : ℕ
i : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } (Fin.last (n + 1)) = i.succ.castSucc.succAbove (Fin.last (n + 1))

Tactic:
· by_cases! hi : i < x
    · rw [Fin.succAbove_of_le_castSucc _ _ (by simpa), Fin.succ_castSucc, map'_eq_castSucc_iff]
      simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
      constructor
      · rw [Fin.predAbove_of_castSucc_lt _ _
          (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]
      · intro j hj
        by_cases! h : i.castSucc < j
        · rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff,
            Fin.succ_pred]
        · rw [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]
          exact lt_of_le_of_lt h hi
    · rw [Fin.succAbove_of_castSucc_lt _ _ (by simpa), map'_eq_castSucc_iff]
      simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
      constructor
      · simp only [i.predAbove_of_le_castSucc x.castSucc (by simpa),
          Fin.castPred_castSucc, le_refl]
      · intro j hj
        by_cases! h : i.castSucc < j
        · rw [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
          exact hj.trans x.castSucc_lt_succ
        · rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } (Fin.last (n + 1)) = i.succ.castSucc.succAbove (Fin.last (n + 1))