mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) ≫
      adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))) =
    𝟙 (bifibrantResolution.obj (toHoCat.obj (mk X)))

Tactic:
comp_hom_eq_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) =
    inv (adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))))
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)) =
    𝟙 (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X))

Tactic:
comp_hom_eq_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) =
    inv (BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)))
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
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ 𝟙 (I.right (J.fst default)) ≫ s.inl = s.inl

Tactic:
Category.id_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ s.inl = s.inl
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
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ 𝟙 (I.right (J.snd default)) ≫ s.inr = s.inr

Tactic:
Category.id_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ s.inr = s.inr
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

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

Tactic:
obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x

Goal state after:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm f ∈ Λ[n, i].obj (op ⦋m⦌) ↔ stdSimplex.objEquiv.symm f ∈ Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm (SimplexCategory.δ i))) ∪ {i} ≠ Set.univ
⊢ Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm (SimplexCategory.δ i))) ∪ {i} = Set.univ

Tactic:
rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
      Fin.range_succAbove, Set.compl_union_self]

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

Goal state before:
pp: m n : ℕ
h : m < n
x : Δ[n] _⦋m⦌
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌) ↔ x ∈ Set.univ

Tactic:
obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x

Goal state after:
m n : ℕ
h : m < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[n].obj (op ⦋m⦌) ↔ stdSimplex.objEquiv.symm f ∈ Set.univ
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
hf : (monomorphisms (Type u)).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ monomorphisms (Type u) φ

Tactic:
simp only [functorCategory, monomorphisms.iff, mono_iff_injective] at hf ⊢

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
⊢ Function.Injective ⇑(hom φ)
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

Goal state before:
pp: S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (0 + 1)
h0 : 0 < i
hn : i < Fin.last 0
σ₀ : Λ[0, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[0, i].ι ≫ σ

Tactic:
| =>

Goal state after:
S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (0 + 1)
h0 : 0 < i
hn : i < Fin.last 0
σ₀ : Λ[0, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[0, i].ι ≫ σ
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

Goal state before:
pp: S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (1 + 1)
h0 : 0 < i
hn : i < Fin.last 1
σ₀ : Λ[1, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[1, i].ι ≫ σ

Tactic:
| =>

Goal state after:
S : SSet
inst✝ : S.Quasicategory
n : ℕ
i : Fin (1 + 1)
h0 : 0 < i
hn : i < Fin.last 1
σ₀ : Λ[1, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[1, i].ι ≫ σ
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

Goal state before:
pp: S : SSet
inst✝ : S.Quasicategory
n✝ n : ℕ
i : Fin (n + 2 + 1)
h0 : 0 < i
hn : i < Fin.last (n + 2)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[n + 2, i].ι ≫ σ

Tactic:
| =>

Goal state after:
S : SSet
inst✝ : S.Quasicategory
n✝ n : ℕ
i : Fin (n + 2 + 1)
h0 : 0 < i
hn : i < Fin.last (n + 2)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
⊢ ∃ σ, σ₀ = Λ[n + 2, i].ι ≫ σ
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ (isColimit i).desc hf.multicofork = f j hj

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso j).inv]

Goal state after:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
    (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «2»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
· dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 0 2 (by simp)).hom,
          ← Category.assoc]
        convert! h₀₂ <;> decide

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp ((eId Cat a).toFunctor.map (𝟙 { down := { as := () } })) η ≍ η

Tactic:
exact congr_arg_heq (·.toFunctor.map η) (e_id_comp (V := Cat) a b)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) ≍ η

Tactic:
simp [hComp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
⊢ ∀ {a b : CatEnrichedOrdinary C} {f g : a ⟶ b} (η : f ⟶ g), hComp η (𝟙 (𝟙 b)) = (eqToIso ⋯).hom ≫ η ≫ (eqToIso ⋯).inv

Tactic:
simp [hComp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
⊢ x.app = y.app

Tactic:
ext; apply h

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_obj : C → D
G_map : (X Y : C) → (X ⟶[V] Y) ⟶ G_obj X ⟶[V] G_obj Y
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (G_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 (G_obj X) (G_obj Y) (G_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_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 := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
| =>

Goal state after:
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_obj : C → D
G_map : (X Y : C) → (X ⟶[V] Y) ⟶ G_obj X ⟶[V] G_obj Y
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (G_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 (G_obj X) (G_obj Y) (G_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_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 := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
f : ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
⊢ ∀
    ⦃a₂ :
      ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶
        ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))⦄,
    ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W a₂ → f = a₂

Tactic:
g

Goal state after:
case inj
V : Type v
inst✝⁷ : Category.{w, v} V
inst✝⁶ : MonoidalCategory V
C✝ : Type u₁
inst✝⁵ : EnrichedCategory V C✝
W : Type v'
inst✝⁴ : Category.{w', v'} W
inst✝³ : MonoidalCategory W
C : Type u₁
inst✝² : EnrichedCategory W C
D : Type u₂
inst✝¹ : EnrichedCategory W D
E : Type u₃
inst✝ : EnrichedCategory W E
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z✝))
⊢ ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W g → f = g
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
α β : F ⟶ G
h : ∀ (X : C), α.out.app X = β.out.app X
⊢ α = β

Tactic:
rcases α with ⟨α⟩

Goal state after:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
inst✝¹ : EnrichedCategory V C
D : Type u₂
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
β : F ⟶ G
α : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α }.out.app X = β.out.app X
⊢ { out := α } = β
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : GradedNatTrans ((Center.ofBraided V).obj (unop X✝)) F G
X Y : C
p :
  (β_ (unop X✝) (X ⟶[V] Y)).hom ≫ (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ (f.unop ≫ σ.app X ⊗ₘ 𝟙 (X ⟶[V] Y) ≫ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)

Tactic:
Category.id_comp

Goal state after:
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : GradedNatTrans ((Center.ofBraided V).obj (unop X✝)) F G
X Y : C
p :
  (β_ (unop X✝) (X ⟶[V] Y)).hom ≫ (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ⊤.prod T ⊓ S.prod ⊤ = S.prod T

Tactic:
ext n ⟨x, y⟩

Goal state after:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
⊢ (x, y) ∈ (⊤.prod T ⊓ S.prod ⊤).obj n ↔ (x, y) ∈ (S.prod T).obj n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (β_ Y X).hom = T.unionProd S

Tactic:
ext n ⟨x, y⟩

Goal state after:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : Y.obj n
y : X.obj n
⊢ (x, y) ∈ ((S.unionProd T).preimage (β_ Y X).hom).obj n ↔ (x, y) ∈ (T.unionProd S).obj n
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : ∀ (x y : V), Subsingleton (x ⟶ y)
x✝ y : FreeRefl V
x : V
⊢ Unique (x ⟶ x)

Tactic:
exact (unique_iff_subsingleton_and_nonempty _ |>.mpr ⟨inferInstance, ⟨𝟙rq _⟩⟩).some

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

Goal state before:
pp: case cast
n : ℕ
i : Fin (n + 1)
⊢ mk (n + 1) ⟶ mk n

Tactic:
| cast i =>

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

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

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

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

Goal state before:
pp: X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)

Tactic:
by
    obtain ⟨z, e, m, he, hm, fac⟩ := exists_P_σ_P_δ_factorization f
    exact ⟨⟨z, e, m, fac.symm, he, hm⟩⟩

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

Goal state before:
pp: case right
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
⊢ σ k = standardσ [↑k] ⋯

Tactic:
simp [standardσ]

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ simplicialEvalσ L L[k] = simplicialEvalσ L (L[k] + 1)

Tactic:
by
  induction L generalizing m k <;> grind [→ IsAdmissible.singleton]

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

Goal state before:
pp: case left
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty

pp: case right
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ ∀ ⦃b : Finset β⦄, b ⊆ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b

Tactic:
· exact Finset.image_nonempty.mpr (K.isRelLowerSet_faces hs').1

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ x.subcomplex ≤ y.subcomplex

Tactic:
← y.subcomplex_cast hxy.dim_eq,

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ x.subcomplex ≤ (y.cast ⋯).subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

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

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

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) }
⊢ ∃ s, x = h.type₁ s ∨ x = h.type₂ s

Tactic:
exact ⟨s, Or.inr (by rwa [N.ext_iff, SSet.N.ext_iff])⟩

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ ⊤.image φ = ⨆ j, (Subcomplex.range (c.ι.app j)).image φ

Tactic:
← iSup_range_eq_top_of_isColimit hc,

Goal state after:
J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X : SSet
φ : c.pt ⟶ X
⊢ (⨆ j, Subcomplex.range (c.ι.app j)).image φ = ⨆ j, (Subcomplex.range (c.ι.app j)).image φ
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), (F.obj j).HasDimensionLT n
⊢ ⊤.toSSet.HasDimensionLT n

Tactic:
← iSup_range_eq_top_of_isColimit hc,

Goal state after:
J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), (F.obj j).HasDimensionLT n
⊢ (⨆ j, Subcomplex.range (c.ι.app j)).toSSet.HasDimensionLT n
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
inst✝¹ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
inst✝ : Finite J
h : ∀ (j : J), (F.obj j).Finite
⊢ ⊤.toSSet.Finite

Tactic:
← iSup_range_eq_top_of_isColimit hc,

Goal state after:
J : Type u_1
inst✝² : Category.{u_2, u_1} J
inst✝¹ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
inst✝ : Finite J
h : ∀ (j : J), (F.obj j).Finite
⊢ (⨆ j, Subcomplex.range (c.ι.app j)).toSSet.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: case refine_1
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ⨆ j, Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f) ≤ ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)

Tactic:
simp only [iSup_le_iff, Discrete.forall]

Goal state after:
case refine_1
ι : Type v
inst✝¹ : HasColimitsOfShape (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst✝ : HasCoproduct X
f : ∐ X ⟶ Y
⊢ ∀ (a' : ι),
    Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := a' } ≫ f) ≤ ⨆ i, Subcomplex.range (Sigma.ι X i ≫ f)