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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
i : ℕ
hi : i ≥ N
h : padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
⊢ ‖↑(f - const norm q) i‖ < ε

Tactic:
change norm (f i - q) < ε

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
i : ℕ
hi : i ≥ N
h : padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε'
⊢ ‖↑f i - q‖ < ε
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
⊢ f.app (op Δ) = g.app (op Δ)

Tactic:
apply s.hom_ext'

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : SimplicialObject C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
⊢ ∀ (A : IndexSet (op Δ)), (s.cofan (op Δ)).inj A ≫ f.app (op Δ) = (s.cofan (op Δ)).inj A ≫ g.app (op Δ)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
by_cases Isδ₀ i
    · exact K.d Δ.len Δ'.len
    · exact 0

Goal state after:
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 ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
by_cases h₁ : Δ = Δ'

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
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
Δ : SimplexCategoryᵒᵖ
⊢ 𝟙 (X.obj Δ) = ∑ A, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
apply s.hom_ext'

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ ∀ (A : IndexSet Δ), (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A, s.πSummand A ≫ (s.cofan Δ).inj A
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
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A = (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A

pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ b ∈ Finset.univ, b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 0

Tactic:
cofan_inj_πSummand_eq_id_assoc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A = (s.cofan Δ).inj A

case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ∀ b ∈ Finset.univ, b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 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
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
apply s.hom_ext'

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
⊢ ∀ (A : IndexSet (op ⦋n⦌)),
    (s.cofan (op ⦋n⦌)).inj A ≫ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = (s.cofan (op ⦋n⦌)).inj A ≫ 0
Module: Mathlib.CategoryTheory.SingleObj

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

Tactic:
← MonoidHom.comp_toFunctor,

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

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

Tactic:
← MonoidHom.comp_toFunctor,

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

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

pp: case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (TopCat.ofHom H.uliftMap)).map ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))

pp: case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯

pp: case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯

Tactic:
rw [eqToHom_trans, eqToHom_refl]

Goal state after:
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (TopCat.ofHom H.uliftMap)).map
      ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    𝟙
      ((π.map (TopCat.ofHom H.uliftMap)).obj
        ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).obj ({ as := { down := 0 } }, { as := x₁ })))

case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (TopCat.ofHom H.uliftMap)).map ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))

case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯

case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

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

pp: case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (TopCat.ofHom H.uliftMap)).map
    ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))

pp: case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯

pp: case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯

Tactic:
rw [eqToHom_trans, eqToHom_refl]

Goal state after:
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (TopCat.ofHom H.uliftMap)).map
      ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (uhpath01, 𝟙 (fromTop x₀))) ≫
    𝟙
      ((π.map (TopCat.ofHom H.uliftMap)).obj
        ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).obj ({ as := { down := 1 } }, { as := x₀ })))

case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (TopCat.ofHom H.uliftMap)).map
    ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))

case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯

case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y : C₁
φ : W.RightFraction X Y
⊢ ∃ ψ, φ.f ≫ ψ.s = φ.s ≫ ψ.f

Tactic:
by
    obtain ⟨T, s, _, f, rfl⟩ := φ.cases
    dsimp
    have := hW s (by assumption)
    exact ⟨{
      f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
      s := adj.unit.app Y
      hs := hW' Y}, by
      have := adj.unit.naturality s
      dsimp at this ⊢
      rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X✝ Y✝ Y : C
inst✝¹ : IsFibrant Y
h✝¹ : IsCofibrant Y
X : C
inst✝ : IsCofibrant X
h✝ : IsFibrant X
E : BifibrantObject.HoCat C ≌ H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
this :
  rightHomotopyClassToHom L =
    ⇑(BifibrantObject.HoCat.homEquivRight.trans
        (E.fullyFaithfulFunctor.homEquiv.trans
          ((e.app (BifibrantObject.mk X)).homCongr (e.app (BifibrantObject.mk Y)))))
⊢ Function.Bijective
    ⇑(BifibrantObject.HoCat.homEquivRight.trans
        (E.fullyFaithfulFunctor.homEquiv.trans
          ((e.app (BifibrantObject.mk X)).homCongr (e.app (BifibrantObject.mk Y)))))

Tactic:
exact Equiv.bijective _

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = f

Tactic:
obtain ⟨⟨f⟩, rfl⟩ := (bijective_leftHomotopyClassToHom L X Y).2 f

Goal state after:
case mk
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
w✝ : LeftHomotopyClass X Y
f : X ⟶ Y
⊢ ∃ a, L.map a = leftHomotopyClassToHom L (Quot.mk LeftHomotopyRel f)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ map (ContinuousMap.id X) = 𝟭 (FundamentalGroupoid X)

Tactic:
by
  simp only [map]; congr; ext x y ⟨p⟩; rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ map (g.comp f) = map f ⋙ map g

Tactic:
by
  simp only [map]; congr; ext x y ⟨p⟩; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ k = J.snd default

Tactic:
have := h.symm.le (Set.mem_univ k)
            push _ ∈ _ at this
            tauto

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Fibration f ↔ J.rlp f

Tactic:
rw [HomotopicalAlgebra.fibration_iff]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ fibrations SSet f ↔ J.rlp f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
d' : ℕ
⊢ c.simplex ∈ ((skeletonOfMono i) d').obj (op ⦋d⦌) ↔
    c.simplex ∈ Set.range ⇑(ConcreteCategory.hom (i.app (op ⦋d⦌))) ∨ d < d'

Tactic:
simp [skeletonOfMono, Y.mem_skeleton_obj_iff_of_nonDegenerate ⟨_, c.nonDegenerate⟩ d']

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

Goal state before:
pp: case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
⊢ ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈
    Set.range ⇑{ toFun := fun x ↦ ⟨↑x, ⋯⟩ } ∪ Set.range ⇑(ConcreteCategory.hom ((b i d).app (op n)))

Tactic:
let c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := by simpa }

Goal state after:
case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈
    Set.range ⇑{ toFun := fun x ↦ ⟨↑x, ⋯⟩ } ∪ Set.range ⇑(ConcreteCategory.hom ((b i d).app (op n)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
⊢ f.vertex j = g.vertex j

pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1)
⊢ f.arrow j = g.arrow j

Tactic:
· rcases Fin.eq_castSucc_or_eq_last j with ⟨k, hk⟩ | hl
    · rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]
    · simp only [hl, ← Fin.succ_last]
      rw [← f.arrow_tgt (Fin.last m), ← g.arrow_tgt (Fin.last m), h]

Goal state after:
case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1)
⊢ f.arrow j = g.arrow j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).vertex i =
    ((X.spine m hₘ Δ).interval j l h).vertex i

Tactic:
dsimp only [spine_vertex, Path.interval]

Goal state after:
case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯).op))
      ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ) =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by grind) =
          X.spine 2 (σ₀.app _ triangle) := by
        ext m
        dsimp [spine_arrow, Path.map_interval, Path.map_arrow]
        rw [← dsimp% σ₀.naturality_apply]
        apply congr_arg
        apply Subtype.ext
        ext a : 1
        fin_cases a <;> fin_cases m <;> rfl

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
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')).hom ≫
      X.fst ◁
          ((α_ Y.fst U U').inv ≫
            (Y.snd.β U).hom ▷ U' ≫ (α_ U Y.fst U').hom ≫ U ◁ (Y.snd.β U').hom ≫ (α_ U U' Y.fst).inv) ≫
        (α_ X.fst (U ⊗ U') Y.fst).inv ≫
          ((α_ X.fst U U').inv ≫
                (X.snd.β U).hom ▷ U' ≫ (α_ U X.fst U').hom ≫ U ◁ (X.snd.β U').hom ≫ (α_ U U' X.fst).inv) ▷
              Y.fst ≫
            (α_ (U ⊗ U') X.fst Y.fst).hom =
    𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.fst ⊗ U) ◁ (Y.snd.β U').hom ≫ (X.snd.β U).hom ▷ (U' ⊗ Y.fst)) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst)

Tactic:
monoidal

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).hom ▷ U' ⊗≫
        ((X.snd.β U).hom ▷ (Y.fst ⊗ U') ≫ (U ⊗ X.fst) ◁ (Y.snd.β U').hom) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst) =
    (α_ (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

Tactic:
monoidal

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
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) ⊗≫
      X.fst ◁ (Y.fst ◁ f ≫ (Y.snd.β U').hom) ⊗≫ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst)

Tactic:
monoidal

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
f : U ⟶ U'
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ ((Y.snd.β U).hom ≫ f ▷ Y.fst) ⊗≫ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst) =
    𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y.snd.β U).hom ⊗≫ (X.fst ◁ f ≫ (X.snd.β U').hom) ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst)

Tactic:
monoidal

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
f : U ⟶ U'
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y.snd.β U).hom ⊗≫ ((X.snd.β U).hom ≫ f ▷ X.fst) ▷ 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) ≫
      f ▷ (X.fst ⊗ Y.fst)

Tactic:
monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ₘ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map : (X Y : C) → (X ⟶[V] Y) ⟶ F_obj X ⟶[V] F_obj Y
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ₘ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
X Y : C
⊢ F_map X Y = G_map X Y

Tactic:
simpa using h_map X Y

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₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst ◁ f.f) ▷ 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) ⊗≫
      X.fst ◁ (f.f ▷ U ≫ (Y₂.snd.β U).hom) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Tactic:
monoidal

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₁ 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)

Tactic:
monoidal

Goal state after: