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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e = 𝟙 (unop Δ) ≫ A.e

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e = A.e
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ 𝟙 (K.X (unop A.fst).len) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : A.e ≫ 𝟙 (unop A.fst) = (𝟙 Δ).unop ≫ A.e
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun A ↦ Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X = 𝟙 ((normalizedMooreComplex A).obj X) ≫ inclusionOfMooreComplexMap X

Tactic:
id_comp

Goal state after:
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X = inclusionOfMooreComplexMap X
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    𝟙 (K.X (unop A.fst).len) ≫ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e)

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun n ↦ K.X n) Δ))) A =
    Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e)
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✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B = 0

Tactic:
dsimp [πSummand]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ((s.cofan Δ).inj A ≫ s.desc Δ fun B_1 ↦ if h : B_1 = B then eqToHom ⋯ else 0) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: case e'_2.e'_7
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A = ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A

Tactic:
id_comp

Goal state after:
case e'_2.e'_7
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A = ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') ⟨op Δ'', ⟨e, ⋯⟩⟩ =
    Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') ⟨op Δ'', ⟨e, ⋯⟩⟩ =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫
      𝟙 (Γ₂.obj (N₂.obj { X := X, p := 𝟙 X, idem := ⋯ })) ≫
        (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₁.natTrans.app X =
    Γ₂N₂ToKaroubiIso.inv.app X ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }
Module: Mathlib.AlgebraicTopology.ModelCategory.Transport

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this✝ : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ ModelCategory C

Tactic:
exact {
    cm1a := ⟨fun _ _ _ ↦ Adjunction.hasLimitsOfShape_of_equivalence e.functor⟩
    cm1b := ⟨fun _ _ _ ↦ Adjunction.hasColimitsOfShape_of_equivalence e.functor⟩
    cm2 := by rw [h₃]; infer_instance
    cm3a := by rw [h₃]; infer_instance
    cm3b := by rw [h₂]; infer_instance
    cm3c := by rw [h₁]; infer_instance
    cm4a _ _ _ _ _ := by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance
    cm4b _ _ _ _ _ := by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance
    cm5a := by rw [h₁', h₂]; infer_instance
    cm5b := by rw [h₁, h₂']; infer_instance }

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
⊢ ModelCategory C

Tactic:
have h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor := by
    simp [trivialCofibrations, h₁, h₃]
  have h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor := by
    simp [trivialFibrations, h₂, h₃]
  have {X Y : C} (f : X ⟶ Y) [hf : Cofibration f] : Cofibration (e.functor.map f) := by
    simpa [cofibration_iff, h₁] using hf
  have {X Y : C} (f : X ⟶ Y) [hf : Fibration f] : Fibration (e.functor.map f) := by
    simpa [fibration_iff, h₂] using hf
  have {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f] : WeakEquivalence (e.functor.map f) := by
    simpa [weakEquivalence_iff, h₃] using hf
  exact {
    cm1a := ⟨fun _ _ _ ↦ Adjunction.hasLimitsOfShape_of_equivalence e.functor⟩
    cm1b := ⟨fun _ _ _ ↦ Adjunction.hasColimitsOfShape_of_equivalence e.functor⟩
    cm2 := by rw [h₃]; infer_instance
    cm3a := by rw [h₃]; infer_instance
    cm3b := by rw [h₂]; infer_instance
    cm3c := by rw [h₁]; infer_instance
    cm4a _ _ _ _ _ := by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance
    cm4b _ _ _ _ _ := by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance
    cm5a := by rw [h₁', h₂]; infer_instance
    cm5b := by rw [h₁, h₂']; infer_instance }

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ ∃ j, j ≠ i ∧ j ∉ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)

Tactic:
by_contra!
    have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop
    have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)
    simp only [SimplexCategory.len_mk, Finset.top_eq_univ, Finset.card_univ, Fintype.card_fin,
      Finset.card_singleton, add_le_add_iff_right] at this
    have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
    lia

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

Goal state before:
pp: case mp
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case mp
n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k
⊢ ∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case mpr
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ j_1, ∀ (x : Fin (d + 1)), ¬j x = j_1) → ∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case mpr
n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬j x = k
⊢ ∃ j_1, ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = j_1
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X Y : SSet
p : X ⟶ Y
inst✝ : InnerFibration p
hY : InnerFibration (terminal.from Y)
⊢ innerFibrations (p ≫ terminal.from Y)

Tactic:
refine innerFibrations.comp_mem _ _ InnerFibration.mem hY.mem

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

Goal state before:
pp: case succ
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ { s // X.spine (n + 1) s = p }

Tactic:
refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
    · rw [p.arrow_tgt 0]
      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0
    · ext i
      obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
      · dsimp
        rw [map_mkOfSucc_zero_concat]
      · simpa [spine_arrow, ← SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp),
          op_comp, Functor.map_comp_apply, ← SimplicialObject.δ_def, δ₀_concat,
          ← p.arrow_interval 1 n i i.succ (by grind) (by grind)] using
            Path.congr_arrow (hn (p.interval 1 n)).prop i

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 Y Y₁ Z : C
α : Y ≅ Y₁
⊢ ((eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z = eComp V X Y Z

Tactic:
simp [← eHomWhiskerLeft_comp]

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✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (f ≫ g))) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f)) ≫
      ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g))

Tactic:
ForgetEnrichment.homTo_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
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✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      (Functor.LaxMonoidal.ε F ≫
        F.map
          (((λ_ (𝟙_ V)).inv ≫ (ForgetEnrichment.homTo V f ⊗ₘ ForgetEnrichment.homTo V g)) ≫
            eComp V (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝))) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f)) ≫
      ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g))
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.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.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 ◁ (X.snd.β Y.fst).hom

Tactic:
← IsIso.inv_comp_eq,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ inv (α_ X.fst Y.fst U).hom ≫
      (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
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.snd.β U).hom ≫ (X.snd.β (U ⊗ Y.fst)).hom ≫ (α_ 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

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ 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 ≫ (α_ U Y.fst X.fst).inv) ≫
        (α_ 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.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : generators.multiplicativeClosure' ≤ P
⊢ P f

Tactic:
← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure',

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : generators.multiplicativeClosure ≤ P
⊢ P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi (toSimplexCategory.map e)

Tactic:
by
  constructor
  constructor
  apply SplitEpi.map
  exact isSplitEpi_P_σ he |>.exists_splitEpi.some

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

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ (i.succ.pred ⋯)

Tactic:
Fin.pred_succ

Goal state after:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

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

Tactic:
#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 [Fin.predAbove_of_castSucc_lt, toMk₁_of_le_castSucc]` -/

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : i < k
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ i.castSucc < x.succ.castSucc

Tactic:
simpa [Fin.le_castSucc_iff]

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

Goal state before:
pp: case pos.left
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ x.succ.pred ⋯

Tactic:
Fin.pred_succ

Goal state after:
case pos.left
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
⊢ (j.pred ⋯).succ < x.succ

Tactic:
Fin.succ_pred

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
⊢ j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : i.castSucc < j
⊢ (j.pred ⋯).succ < x.succ

Tactic:
Fin.succ_pred

Goal state after:
case pos
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : i.castSucc < j
⊢ j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n

Tactic:
· rw [nonDegenerate_iff_injective_objEquiv]
    intro h a b hab
    simp only [DFunLike.ext_iff, orderHomOfSimplex_coe, OrderHom.id_coe, id_eq] at h
    rw [← h a, ← h b, Fin.ext_iff]
    change ((objEquiv z a).1 : ℕ) + (objEquiv z a).2 = (objEquiv z b).1 + (objEquiv z b).2
    simp only [hab]

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : SimplexCategory
f g : m ⟶ ⦋n⦌
h : (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map g.op)) x
this : Mono (yonedaEquiv.symm x)
⊢ stdSimplex.map f = stdSimplex.map g

Tactic:
rw [← cancel_mono (yonedaEquiv.symm x)]

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : SimplexCategory
f g : m ⟶ ⦋n⦌
h : (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map g.op)) x
this : Mono (yonedaEquiv.symm x)
⊢ stdSimplex.map f ≫ yonedaEquiv.symm x = stdSimplex.map g ≫ yonedaEquiv.symm x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : OrderBot ι
⊢ f.filtration ⊥ = A

Tactic:
simp [filtration_def]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
hxy : c.s = c'.s
⊢ False

Tactic:
rw [hxy] at hi
    exact (lt_irrefl _ hi).elim

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : ¬(x.cast hd).simplex.1 i < k.succ
this : i ≤ l.castSucc
| k.castSucc

Tactic:
rw [← hl.simplex_fst_castSucc]

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : ¬(x.cast hd).simplex.1 i < k.succ
this : i ≤ l.castSucc
| (x.cast hd).simplex.1 l.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ φ x hd i.castSucc < φ x hd i.succ

Tactic:
rw [φ_of_gt _ _ _ (by grind), φ_of_gt _ _ _ (by grind)]
    exact hx' (by grind)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
hl' : IsIndex y hd' l'.succ
h : hl.δ = hl'.δ
h₁ : ⋯.type₁ ⋯ = hl'.type₁
⊢ x = y

Tactic:
have h₂ := hl.isType₂_δ.type₁_eq_of_δ_eq hl.type₁ rfl rfl

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d' : ℕ
hd' : y.dim = d' + 1
l' : Fin (d' + 1)
hl' : IsIndex y hd' l'.succ
h : hl.δ = hl'.δ
h₁ : ⋯.type₁ ⋯ = hl'.type₁
h₂ : ⋯.type₁ ⋯ = hl.type₁
⊢ x = y