mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : V), { obj := G_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := G_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := G_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := G_obj, map := map✝, map_id := map_id✝ }.map f))
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹ } = { obj := G_obj, map := map✝, map_id := map_id✝ }

Tactic:
obtain rfl : F_obj = G_obj := (Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _

Goal state after:
V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝, map_id := map_id✝ }.map f))
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹ } = { obj := F_obj, map := map✝, map_id := map_id✝ }
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

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

Tactic:
induction Δ using SimplexCategory.rec with | _ n
  induction Δ' using SimplexCategory.rec with | _ n'
  dsimp
  -- We start with the case `i` is an identity
  by_cases h : n = n'
  · subst h
    simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
    dsimp
    simp only [id_comp, comp_id]
  by_cases hi : Isδ₀ i
  -- The case `i = δ 0`
  · have h' : n' = n + 1 := hi.left
    subst h'
    simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]
    rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]
    simp only [Preadditive.comp_sum]
    rw [Finset.sum_eq_single (0 : Fin (n + 2))]
    rotate_left
    · intro b _ hb
      rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]
    · simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]
    · simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]
      rfl
  -- The case `i ≠ δ 0`
  · rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]
    swap
    · by_contra h'
      exact h (congr_arg SimplexCategory.len h'.symm)
    rw [PInfty_comp_map_mono_eq_zero]
    · exact h
    · assumption

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 Y : SimplicialObject C
f : X ⟶ Y
⊢ (N₁ ⋙ Γ₂).map f ≫
      {
        f :=
          { app := fun Δ ↦ (Γ₀.splitting K[Y]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ Y.map A.e.op,
            naturality := ⋯ },
        comm := ⋯ } =
    {
        f :=
          { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op,
            naturality := ⋯ },
        comm := ⋯ } ≫
      (toKaroubi (SimplicialObject C)).map f

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ ((N₁ ⋙ Γ₂).map f ≫
        {
          f :=
            { app := fun Δ ↦ (Γ₀.splitting K[Y]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ Y.map A.e.op,
              naturality := ⋯ },
          comm := ⋯ }).f =
    ({
          f :=
            { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op,
              naturality := ⋯ },
          comm := ⋯ } ≫
        (toKaroubi (SimplicialObject C)).map f).f
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ cast hu hv p = p' ↔ p ≍ p'

Tactic:
rw [Path.cast_eq_cast]
  exact _root_.cast_eq_iff_heq

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
⊢ ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g

Tactic:
intro K L f g h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K L : BifibrantObject C
f g : K ⟶ L
h : homRel C f g
⊢ toHoCat.map f = toHoCat.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations (Over S)).IsStableUnderRetracts

Tactic:
by
  rw [cofibrations_over_def, MorphismProperty.over_eq_inverseImage]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations C).over.HasFactorization (trivialFibrations (Over S))

Tactic:
trivialFibrations_over_eq

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
S : C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (cofibrations C).over.HasFactorization (trivialFibrations C).over
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case mk.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₀ : Path x₀ x₁
γ₁ : Path x₁ x₂
γ₂ : Path x₂ x₃
⊢ ((mk γ₀).trans (mk γ₁)).trans (mk γ₂) = (mk γ₀).trans ((mk γ₁).trans (mk γ₂))

Tactic:
| mk γ₂ =>

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
⊢ Λ[n + 2, i].obj (op ⦋0⦌) = ⊤

Tactic:
ext j
  -- this was produced using `simp? [horn_eq_iSup]`
  simp only [horn_eq_iSup, Subfunctor.iSup_obj, Set.iUnion_coe_set,
    Set.mem_compl_iff, Set.mem_singleton_iff, Set.mem_iUnion, stdSimplex.mem_face_iff,
    Nat.reduceAdd, Finset.mem_compl, Finset.mem_singleton, exists_prop, Set.top_eq_univ,
    Set.mem_univ, iff_true]
  let S : Finset (Fin (n + 3)) := {i, j 0}
  have hS : ¬ (S = Finset.univ) := fun hS ↦ by
    have := Finset.card_le_card hS.symm.le
    simp only [Finset.card_univ, Fintype.card_fin, S] at this
    have := this.trans Finset.card_le_two
    lia
  rw [Finset.eq_univ_iff_forall, not_forall] at hS
  obtain ⟨k, hk⟩ := hS
  simp only [Finset.mem_insert, Finset.mem_singleton, not_or, S] at hk
  refine ⟨k, hk.1, fun a ↦ ?_⟩
  fin_cases a
  exact Ne.symm hk.2

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].toSSet.HasDimensionLT n

Tactic:
rw [boundary_eq_iSup, hasDimensionLT_iSup_iff]

Goal state after:
n : ℕ
⊢ ∀ (i : Fin (n + 1)), (stdSimplex.face {i}ᶜ).toSSet.HasDimensionLT n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

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

Tactic:
by
  ext ⟨⟨d⟩⟩ j
  simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_boundary_iff_notMem_range, Set.mem_range,
    stdSimplex.opObjEquiv_opObjEquiv_symm_apply, not_exists]
  constructor
  all_goals
  · rintro ⟨k, hk⟩
    exact ⟨k.rev, fun l _ ↦ hk l.rev (by aesop)⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (ι i)

Tactic:
← mono_comp_iff_of_isIso (stdSimplex.faceSingletonComplIso i).inv,

Goal state after:
n : ℕ
i : Fin (n + 2)
⊢ Mono ((stdSimplex.faceSingletonComplIso i).inv ≫ ι i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋a⦌ i ≫ φ.hom) ⋯ hₘ).op)) Δ =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ

Tactic:
SimplexCategory.const_comp

Goal state after:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const { obj := ⦋m⦌, property := hₘ }.obj ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op))
      Δ =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((ρ_ (𝟙_ C)).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom) ≫ (f ⊗ₘ g ⊗ₘ h)

Tactic:
triangle_assoc_comp_right_inv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| 𝟙_ C ◁ (λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g ⊗ₘ h)
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 (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]

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'
⊢ eqToHom ⋯ ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
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'
⊢ eqToHom ⋯ ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]

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'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
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'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]

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'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 (homEquiv f')) (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
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'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 (homEquiv f')) (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]

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'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (CatEnriched.hComp (Hom.base θ) (Hom.base κ)) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Monoidal.Center

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

Tactic:
f.comm

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y₁.snd.β U).hom ≫ U ◁ f.f) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ (ConcreteCategory.hom (K.map ((Opposite.unop Δ').const ⦋0⦌ 0).op)) x =
    (ConcreteCategory.hom (K.map f)) ((ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) x)

Tactic:
← Functor.map_comp_apply

Goal state after:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ (ConcreteCategory.hom (K.map ((Opposite.unop Δ').const ⦋0⦌ 0).op)) x =
    (ConcreteCategory.hom (K.map (((Opposite.unop Δ).const ⦋0⦌ 0).op ≫ f))) x
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ (f.f ▷ U ≫ (X₂.snd.β U).hom) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    ((α_ 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 ◁ f.f ▷ Y.fst

Tactic:
f.comm

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ ((X₁.snd.β U).hom ≫ U ◁ f.f) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    ((α_ 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 ◁ f.f ▷ Y.fst
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ f.f ▷ Y.fst ▷ 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 =
    ((α_ 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 ◁ f.f ▷ Y.fst

Tactic:
calc
    _ = 𝟙 _ ⊗≫
      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (HalfBraiding.β Y.snd U).hom) ⊗≫
        (HalfBraiding.β X₂.snd U).hom ▷ Y.fst ⊗≫ 𝟙 _ := by monoidal
    _ = 𝟙 _ ⊗≫
      X₁.fst ◁ (HalfBraiding.β Y.snd U).hom ⊗≫
        (f.f ▷ U ≫ (HalfBraiding.β X₂.snd U).hom) ▷ Y.fst ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; monoidal
    _ = _ := by rw [f.comm]; monoidal

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

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ (freeReflMap (𝟙 X)).toCatHom = 𝟙 (of (FreeRefl ↑X))

Tactic:
ext1

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ (freeReflMap (𝟙 X)).toCatHom.toFunctor = (𝟙 (of (FreeRefl ↑X))).toFunctor
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ (freeReflMap (f ≫ g)).toCatHom = (freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom

Tactic:
ext1

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ (freeReflMap (f ≫ g)).toCatHom.toFunctor = ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ (ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom =
    (FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f

Tactic:
ext1

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor =
    ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: X'✝ X✝ : ReflQuiv
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ forget.obj Y✝
⊢ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X'✝) Y✝).trans adj.homEquiv).symm (x✝¹ ≫ x✝) =
    Cat.freeRefl.map x✝¹ ≫ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X✝) Y✝).trans adj.homEquiv).symm x✝

Tactic:
ext1

Goal state after:
X'✝ X✝ : ReflQuiv
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ forget.obj Y✝
⊢ (((Cat.Hom.equivFunctor (Cat.freeRefl.obj X'✝) Y✝).trans adj.homEquiv).symm (x✝¹ ≫ x✝)).toFunctor =
    (Cat.freeRefl.map x✝¹ ≫ ((Cat.Hom.equivFunctor (Cat.freeRefl.obj X✝) Y✝).trans adj.homEquiv).symm x✝).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : V.HomotopyCategory ⥤ D
φ : (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀ ⦃x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x✝¹ x✝ : V.HomotopyCategory
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ φ x✝.1.as = φ x✝¹.1.as ≫ G.map f

Tactic:
have : MorphismProperty.naturalityProperty (fun (x : V.HomotopyCategory) ↦ φ _) = ⊤ :=
      morphismProperty_eq_top (fun e ↦ hφ e)

Goal state after:
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : V.HomotopyCategory ⥤ D
φ : (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀ ⦃x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x✝¹ x✝ : V.HomotopyCategory
f : x✝¹ ⟶ x✝
this : (MorphismProperty.naturalityProperty fun x ↦ φ x.1.as) = ⊤
⊢ F.map f ≫ φ x✝.1.as = φ x✝¹.1.as ≫ G.map f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W x✝ : Truncated 2
⊢ (mapHomotopyCategory (𝟙 x✝)).toCatHom = 𝟙 (Cat.of x✝.HomotopyCategory)

Tactic:
ext1

Goal state after:
V W x✝ : Truncated 2
⊢ (mapHomotopyCategory (𝟙 x✝)).toCatHom.toFunctor = (𝟙 (Cat.of x✝.HomotopyCategory)).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W X✝ Y✝ Z✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mapHomotopyCategory (x✝¹ ≫ x✝)).toCatHom = (mapHomotopyCategory x✝¹).toCatHom ≫ (mapHomotopyCategory x✝).toCatHom

Tactic:
ext1

Goal state after:
V W X✝ Y✝ Z✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mapHomotopyCategory (x✝¹ ≫ x✝)).toCatHom.toFunctor =
    ((mapHomotopyCategory x✝¹).toCatHom ≫ (mapHomotopyCategory x✝).toCatHom).toFunctor
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

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

Tactic:
exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_le h]⟩

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

Goal state before:
pp: case neg
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
have : a < m + 2 := by grind

Goal state after:
case neg
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
⊢ ∃ a, toMk₁ a = f

Tactic:
refine ⟨Fin.last _, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
    dsimp [toMk₁_apply]
    rw [if_pos (by simp)]
    obtain ⟨j, hj⟩ : ∃ (j : Fin 2), f i = j := ⟨_, rfl⟩
    fin_cases j
    · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was: `grind` -/
      simp_all
    · exact (hS ⟨i, by simpa [S]⟩).elim

Goal state after: