mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ { app := fun P ↦ { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun P ↦ { f := { f := fun n ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (functor ⋙ inverse)

Tactic:
ext
    dsimp
    simp only [HomologicalComplex.p_idem]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
h : ⦋n + 1⦌ = ⦋n⦌
⊢ False

Tactic:
exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)

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

Goal state before:
pp: case e'_2
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₁ = p 1

Tactic:
simp only [Path.target]

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

Goal state before:
pp: case e'_3
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ x₃ = q 1

Tactic:
simp only [Path.target]

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

Goal state before:
pp: t : ↑I
⊢ transReflReparamAux t ∈ I

Tactic:
unfold transReflReparamAux

Goal state after:
t : ↑I
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (p.reparam (fun t ↦ ⟨transReflReparamAux t, ⋯⟩) trans_refl_reparam._proof_1 ⋯ ⋯) x✝

Tactic:
unfold transReflReparamAux

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ =
    (p.reparam (fun t ↦ ⟨if ↑t ≤ 1 / 2 then 2 * ↑t else 1, ⋯⟩) trans_refl_reparam._proof_1 ⋯ ⋯) x✝
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lcofπ F)
G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
    CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lcofπ F)
G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

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
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
⊢ ∀ {X Y : WalkingMultispan J} (f : X ⟶ Y),
    (d.map F).multispan.map f ≫
        (match Y with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
      (match X with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
        (d.multispan ⋙ F).map f

Tactic:
by rintro _ _ (_ | _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
s : Limits.Fork f g
⊢ lift f g s.ι ⋯ ≫ (fork f g).ι = s.ι

Tactic:
by dsimp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : ¬S = Finset.univ
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1

Tactic:
rw [Finset.eq_univ_iff_forall, not_forall] at hS

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, j 0}
hS : ∃ x, x ∉ S
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 1), ¬j i = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
⊢ Λ[n, i].obj (op ⦋m⦌) = Set.univ

Tactic:
ext x
  obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x
  obtain ⟨j, hij, hj⟩ : ∃ (j : Fin (n + 1)), j ≠ i ∧ j ∉ Set.range f.toOrderHom := by
    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
  have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.{u}.symm f) i = j :=
    ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩
  simpa [horn_eq_iSup] using this

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : {j}ᶜᶜ.card = 1
⊢ j ≠ i

Tactic:
rintro rfl

Goal state after:
n : ℕ
A : Δ[n + 1].Subcomplex
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : {j}ᶜᶜ.card = 1
h : ¬stdSimplex.face {j}ᶜ ≤ A
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : a ∈ A.obj (op ⦋n⦌)
⊢ a ∉ {objEquiv.symm (𝟙 (unop (op ⦋n⦌)))}

Tactic:
rintro rfl

Goal state after:
case inr
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha : objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ A.obj (op ⦋n⦌)
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

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

Tactic:
rintro rfl

Goal state after:
case refine_1
n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case pos
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : m < n
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)

pp: case neg
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : n ≤ m
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)

Tactic:
· simp [boundary_obj_eq_univ m n h₃]

Goal state after:
case neg
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : A.toSSet.HasDimensionLT n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : x ∈ Δ[n].nonDegenerate m
h₂ : x ∈ A.obj (op ⦋m⦌)
h₃ : n ≤ m
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case mp
n : ℕ
A : Δ[n].Subcomplex
⊢ A = ∂Δ[n] → ∂Δ[n] ≤ A ∧ A ≠ ⊤

Tactic:
rintro rfl

Goal state after:
case mp
n : ℕ
⊢ ∂Δ[n] ≤ ∂Δ[n] ∧ ∂Δ[n] ≠ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : ¬{i, a, b} = univ
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)

Tactic:
rw [Finset.eq_univ_iff_forall, not_forall] at hS

Goal state after:
n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : ∃ x, x ∉ {i, a, b}
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ¬{i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1

Tactic:
rw [Finset.eq_univ_iff_forall, not_forall] at hS

Goal state after:
case refine_3
n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : ∃ x, x ∉ {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ ∃ i_1, ¬i_1 = i ∧ ∀ (i : Fin 3), ¬(stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯) i = i_1
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)

Tactic:
rintro rfl

Goal state after:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr x₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2} ≤ Λ[2, 0]

Tactic:
rw [sup_le_iff]

Goal state after:
case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 0] ∧ stdSimplex.face {0, 2} ≤ Λ[2, 0]
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
rw [sup_le_iff]

Goal state after:
case a
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1] ∧ stdSimplex.face {1, 2} ≤ Λ[2, 1]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
⊢ X.skeleton 0 = ⊥

Tactic:
by
  simp [skeleton]

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

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 2]

Tactic:
rw [sup_le_iff]

Goal state after:
case a
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 2] ∧ stdSimplex.face {1, 2} ≤ Λ[2, 2]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.inl
X : SSet
n d : ℕ
hd✝¹ : d < n + 1
hd✝ : d ≤ n
x : ↑(X.nonDegenerate ↑⟨d, hd✝¹⟩)
hd : d < n
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
exact (X.ofSimplex_le_skeleton _ hd).trans le_sup_left

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

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

Tactic:
rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]

Goal state after:
case h
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
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:
rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_gt hij, spineToSimplex_arrow]

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

Goal state before:
pp: 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 ⋯
⊢ ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)

Tactic:
ext m

Goal state after:
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 ⋯
m : Fin (1 + 1)
⊢ (((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯).arrow m =
    (X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)).arrow m
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case succ.refine_2.inl
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯) = p.arrow 0

Tactic:
rw [map_mkOfSucc_zero_concat]

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
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✝
⊢ (e (X✝ ⟶[V] Z✝)) ((eHomEquiv V) (f ≫ g)) =
    (λ_ (𝟙_ W)).inv ≫ ((e (X✝ ⟶[V] Y✝)) ((eHomEquiv V) f) ⊗ₘ (e (Y✝ ⟶[V] Z✝)) ((eHomEquiv V) g)) ≫ eComp W X✝ Y✝ Z✝

Tactic:
rw [h, h, h, ← tensorHom_comp_tensorHom_assoc, eComp_eq, tensorHom_def_assoc,
      whiskerRight_id_assoc, unitors_inv_equal, Iso.inv_hom_id_assoc,
      Functor.LaxMonoidal.μ_natural_assoc, Functor.LaxMonoidal.right_unitality_inv_assoc,
      eHomEquiv_comp, ← F.map_comp, ← F.map_comp, unitors_inv_equal]

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : (X ⊗ Y).obj n
⊢ x ∈ (S.unionProd T).obj n ↔ x.2 ∈ T.obj n ∨ x.1 ∈ S.obj n

Tactic:
dsimp [unionProd, Set.prod]
  cat_disch

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

Tactic:
by
      rw [← whisker_exchange]; 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 : 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

Tactic:
← HalfBraiding.naturality_assoc,

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.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
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: C : Type u
inst✝ : Category.{max u v, u} C
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (adj.counit.app (Cat.of C)).toFunctor.map ((Cat.FreeRefl.quotientFunctor C).map f.toPath) =
    𝟙 ((adj.counit.app (Cat.of C)).toFunctor.obj ((Cat.FreeRefl.quotientFunctor C).obj x✝¹)) ≫
      composePath f.toPath ≫ 𝟙 x✝

Tactic:
simp only [adj_counit_app, composePath_toPath, comp_id, id_comp]

Goal state after:
C : Type u
inst✝ : Category.{max u v, u} C
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (Cat.FreeRefl.lift (𝟭rq C)).toCatHom.toFunctor.map ((Cat.FreeRefl.quotientFunctor C).map f.toPath) = f
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
V : Cᵒᵖ ⥤ Type w
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
γ : X ⟶ Z
φ : (fun X ↦ X) (V.obj (op Z))
⊢ α ≫ β = γ →
    (ConcreteCategory.hom (V.map α.op)) ((ConcreteCategory.hom (V.map β.op)) φ) = (ConcreteCategory.hom (V.map γ.op)) φ

Tactic:
rintro rfl

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
V : Cᵒᵖ ⥤ Type w
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
φ : (fun X ↦ X) (V.obj (op Z))
⊢ (ConcreteCategory.hom (V.map α.op)) ((ConcreteCategory.hom (V.map β.op)) φ) =
    (ConcreteCategory.hom (V.map (α ≫ β).op)) φ
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.deg X ≤ r.deg Y

Tactic:
← r.degHom_id X,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.degHom (𝟙 X) ≤ r.deg Y
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

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

Tactic:
by
  suffices generators.multiplicativeClosure ≤ P by
    rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this
    rw [this]
    apply MorphismProperty.top_apply
  intro _ _ f hf
  induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (comp_δ (𝟙 _) i id)
    · simpa using! (comp_σ (𝟙 _) i id)
  | id n => exact id
  | comp_of f g hf hg hrec =>
    rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (comp_δ f i hrec)
    · simpa using! (comp_σ f i hrec)

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

Goal state before:
pp: x y : SimplexCategoryGenRel
h : x.len = y.len
⊢ x = y

Tactic:
by
  cases x
  cases y
  simp only [mk_len] at h
  congr

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

Goal state before:
pp: case succ.comp_of.inr.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
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
z : SimplexCategoryGenRel
e : x ⟶ z
m : z ⟶ mk n
he : P_σ e
hm : P_δ m
fac : f ≫ σ j = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
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.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ i = hxy.index hd → (ConcreteCategory.hom (SimplicialObject.δ X i)) (y.cast ⋯).simplex = (x.cast hd).simplex

Tactic:
rintro rfl

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index hd))) (y.cast ⋯).simplex = (x.cast hd).simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ x ≤ y

Tactic:
by
  have := hxy.δ_index rfl
  simp only [cast_simplex_rfl] at this
  rw [S.le_def, ← y.subcomplex_cast hxy.dim_eq, Subfunctor.ofSection_le_iff,
    ← this]
  exact ⟨(SimplexCategory.δ _).op, rfl⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
hx : x ∈ P.I
y : A.N
hy : y ∈ P.II
⊢ ↑⟨x, hx⟩ ≠ ↑⟨y, hy⟩

Tactic:
rintro rfl

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
hx : x ∈ P.I
hy : ↑⟨x, hx⟩ ∈ P.II
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
g : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Mono g
⊢ monoOfLE h = g → (ConcreteCategory.hom (X.map g.op)) y.simplex = x.simplex

Tactic:
rintro rfl

Goal state after:
X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
inst✝ : Mono (monoOfLE h)
⊢ (ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex = x.simplex
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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
h : ∃ x ∈ c.horn.obj (op ⦋(↑c.s).dim⦌), (ConcreteCategory.hom (c.map.app (op ⦋(↑c.s).dim⦌))) x = (↑c.s).simplex
⊢ False

Tactic:
obtain ⟨x, h₁, h₂⟩ := h

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
x : Δ[c.dim + 1] _⦋(↑c.s).dim⦌
h₁ : x ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (c.map.app (op ⦋(↑c.s).dim⦌))) x = (↑c.s).simplex
⊢ False
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ ∀ (j : WalkingCospan),
    (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
        (c x✝).π.app j =
      𝟙 (c x✝).pt ≫ (c x✝).π.app j

Tactic:
rintro (_ | _ | _); all_goals simp

Goal state after: