mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : k = J.fst default ∨ k = J.snd default
⊢ k = J.snd default

Tactic:
tauto

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
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
⊢ c.π k ≫ m = c.π k ≫ hc.desc (isPushout.multicofork h h' s)

Tactic:
have := h.symm.le (Set.mem_univ k)

Goal state after:
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
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
this : k ∈ {J.fst default, J.snd default}
⊢ c.π k ≫ m = c.π k ≫ hc.desc (isPushout.multicofork h h' s)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x✝ : Δ[n].obj x✝¹
⊢ (∃ x, ∀ (x_1 : Fin ((unop x✝¹).len + 1)), ¬(stdSimplex.asOrderHom x✝) x_1 = x) ↔
    ∃ i, ∀ (x : Fin ((unop x✝¹).len + 1)), ¬(SimplexCategory.Hom.toOrderHom (stdSimplex.objEquiv x✝)) x = i

Tactic:
tauto

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

Goal state before:
pp: 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

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case false
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ false ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    false ∈ Set.univ

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case true
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ true ∈ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} ↔
    true ∈ Set.univ

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ (MultispanShape.ofLinearOrder Bool).fst default ≠ (MultispanShape.ofLinearOrder Bool).snd default

Tactic:
tauto

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

Goal state before:
pp: case neg.inl
n k : ℕ
h : k < n + 2
hk : ¬k = 0
hi : 0 < n + 4
h₀ : 0 < ⟨0, hi⟩
hₙ : ⟨0, hi⟩ < Fin.last (n + 3)
hS : {⟨0, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
⊢ False

Tactic:
tauto

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

Goal state before:
pp: case neg.inr
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
hk : ¬0 = 0
⊢ False

Tactic:
tauto

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

Goal state before:
pp: case zero
X : SSet
i : Fin (0 + 2)
f : (j : Fin (0 + 2)) → j ≠ i → (Δ[0] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

Tactic:
· rintro ⟨⟨a, b⟩, hab⟩
      grind

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f 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 : i.succ.castSucc < j
⊢ (X.spine m ⋯ ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.castSucc

Tactic:
rw [spine_arrow, ← Functor.map_comp_apply, ← op_comp, ← tr_comp,
    mkOfSucc_δ_lt hij, spineToSimplex_arrow]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ ((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom =
    (α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y) ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
      (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
        ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)

Tactic:
ext ⟨⟨f, g⟩, h⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : (coyoneda.obj (op (𝟙_ C))).obj Z
f : (coyoneda.obj (op (𝟙_ C))).obj X
g : (coyoneda.obj (op (𝟙_ C))).obj Y
⊢ (ConcreteCategory.hom
          (((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
            (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom)).toFun
      ((f, g), h) =
    (ConcreteCategory.hom
          ((α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y)
                ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
            (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
              ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2))).toFun
      ((f, g), h)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
⊢ (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y ↔ S.obj n x ∧ T.obj n y

Tactic:
tauto

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : Y.obj n
y : X.obj n
⊢ ((ConcreteCategory.hom ((β_ Y X).hom.app n)) (x, y)).2 ∈ T.obj n ∨
      ((ConcreteCategory.hom ((β_ Y X).hom.app n)) (x, y)).1 ∈ S.obj n ↔
    y ∈ S.obj n ∨ x ∈ T.obj n

Tactic:
tauto

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

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hf : HomotopicL f f'
hg✝ : HomotopicL g g'
hg : (id y).CompStruct g g'
⊢ HomotopicL h h'

Tactic:
rcases hf with ⟨hf⟩

Goal state after:
A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hg✝ : HomotopicL g g'
hg : (id y).CompStruct g g'
hf : f.CompStruct (id y) f'
⊢ HomotopicL h h'
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W X : Truncated 2
inst✝ : Subsingleton (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
x y : X.HomotopyCategory
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective
    obtain ⟨y, rfl⟩ := y.mk_surjective
    obtain rfl := Subsingleton.elim x y
    rfl

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

Goal state before:
pp: x y : OneTruncation₂ ((truncation 2).obj Δ[0])
⊢ x ⟶ y

Tactic:
obtain rfl : x = default := Unique.uniq _ _
    obtain rfl : y = default := Unique.uniq _ _
    exact 𝟙rq instUniqueOneTruncation₂DeltaZero.default

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

Goal state before:
pp: case comp_of
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : degeneracies.multiplicativeClosure f✝
h : degeneracies g✝
hf_ih✝ : IsSplitEpi f✝
⊢ IsSplitEpi (f✝ ≫ g✝)

Tactic:
cases h

Goal state after:
case comp_of.σ
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 1)
f✝ : x✝ ⟶ mk (n✝ + 1)
hf✝ : degeneracies.multiplicativeClosure f✝
hf_ih✝ : IsSplitEpi f✝
⊢ IsSplitEpi (f✝ ≫ σ i✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure f✝
h : faces g✝
hf_ih✝ : IsSplitMono f✝
⊢ IsSplitMono (f✝ ≫ g✝)

Tactic:
cases h

Goal state after:
case comp_of.δ
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
f✝ : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure f✝
hf_ih✝ : IsSplitMono f✝
⊢ IsSplitMono (f✝ ≫ δ i✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case zero.of
i : Fin (0 + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (0 + 1)
h : faces f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h

Goal state after:
case zero.of.δ
i : Fin (0 + 1)
i✝ : Fin (0 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.of
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 : SimplexCategoryGenRel
f : x ⟶ mk (n + 1 + 1)
h : faces f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h

Goal state after:
case succ.of.δ
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)
i✝ : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m : ℕ
hL : IsAdmissible (m + 1) []
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j [])

Tactic:
exact IsAdmissible.singleton hj

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

Goal state before:
pp: X Y : Truncated 2
inst✝¹ : Unique (Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 }))
inst✝ : Subsingleton (Y.obj (Opposite.op { obj := ⦋1⦌, property := isoTerminal._proof_1 }))
⊢ CategoryTheory.Prod.fst X.HomotopyCategory ↑Cat.chosenTerminal =
    (𝟭 X.HomotopyCategory).prod (isoTerminal Y).inv.toFunctor ⋙ inverse X Y ⋙ mapHomotopyCategory (fst X Y)

Tactic:
by
  rw [inverse_comp_mapHomotopyCategory_fst]
  rfl

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ s
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ s
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
⊢ i = j

Tactic:
wlog hij : i < j generalizing i j

Goal state after:
case inr
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
this : ∀ ⦃i j : Fin (n + 2)⦄, toMk₁ i = toMk₁ j → i < j → i = j
hij : ¬i < j
⊢ i = j

n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ i = j
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) → ∀ (i : Fin (n + 1)), (f i).castSucc < x

Tactic:
intro h i

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
⊢ (f i).castSucc < x
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
⊢ l ∈ f.I ∪ g.I → i.as ≤ l

Tactic:
by
      rintro (h | h)
      exacts [(f.left_le l h), (Path.le f).trans (g.left_le l h)]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (II.σ i).unop = (δ i.succ.castSucc).op.unop

Tactic:
ext x : 3; apply II.map'_predAbove

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
⊢ ∃ x_1, Mono x_1 ∧ (ConcreteCategory.hom (X.map x_1.op)) y.simplex = x.simplex

Tactic:
obtain ⟨f, _, hf⟩ := le_iff_exists_mono.1 h

Goal state after:
X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
w✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ ∃ x_1, Mono x_1 ∧ (ConcreteCategory.hom (X.map x_1.op)) y.simplex = x.simplex
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
⊢ c.pt.Finite

Tactic:
rw [← finite_subcomplex_top_iff, ← iSup_range_eq_top_of_isColimit hc, finite_iSup_iff]

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
⊢ ∀ (i : J), (Subcomplex.range (c.ι.app i)).toSSet.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{?u.4, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ (⊥_ SSet).Finite

Tactic:
apply finite_of_isColimit (initialIsInitial (C := SSet.{u}))
  rintro ⟨⟨⟩⟩

Goal state after:
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₁ : ¬stdSimplex.face {c.index}ᶜ ≤ stdSimplex.face {⋯.index ⋯}ᶜ
h₂ : (ConcreteCategory.hom (X.map (SimplexCategory.δ (⋯.index ⋯)).op)) ((↑(P.p c.s)).cast ⋯).simplex = (↑c.s).simplex
this : Mono (SimplexCategory.δ (⋯.index ⋯))
⊢ False

Tactic:
tauto

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = 1 • H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 2))

Tactic:
one_smul

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 2))
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 ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
⊢ Order.succ j < i

Tactic:
← Order.IsSuccLimit.succ_lt_iff hi

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : Order.succ j < i
c : f.Cell j
⊢ Order.succ j < i
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasEqualizers C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
⊢ ∀ {Z : C} (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i

Tactic:
tauto

Goal state after:
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✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim + 1⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim + 1⦌)
hy :
  (ConcreteCategory.hom ((x'.horn.ι ≫ x'.ιSigmaStdSimplex).app (op ⦋c.dim + 1⦌))) ⟨y, hy'⟩ =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))))
⊢ False

Tactic:
NatTrans.comp_app_apply,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim + 1⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim + 1⦌)
hy :
  (ConcreteCategory.hom (x'.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      ((ConcreteCategory.hom (x'.horn.ι.app (op ⦋c.dim + 1⦌))) ⟨y, hy'⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim + 1⦌)))
      (stdSimplex.objEquiv.symm (𝟙 (unop (op ⦋c.dim + 1⦌))))
⊢ False
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✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim⦌)
hy :
  (ConcreteCategory.hom ((x'.horn.ι ≫ x'.ιSigmaStdSimplex).app (op ⦋c.dim⦌))) ⟨y, hy'⟩ =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
⊢ False

Tactic:
NatTrans.comp_app_apply,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c x' : f.Cell j
y : Δ[x'.dim + 1] _⦋c.dim⦌
hy' : y ∈ x'.horn.obj (op ⦋c.dim⦌)
hy :
  (ConcreteCategory.hom (x'.ιSigmaStdSimplex.app (op ⦋c.dim⦌)))
      ((ConcreteCategory.hom (x'.horn.ι.app (op ⦋c.dim⦌))) ⟨y, hy'⟩) =
    (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
⊢ False
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst✝ : Mono i
hi : ¬IsIso i
this : ∀ (G : C), P G → ∀ (g : G ⟶ Y), ∃ f, f ≫ i = g
⊢ False

Tactic:
exact hi (hP.isIso_of_mono i this)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
⊢ Mono
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))

Tactic:
let Φ := CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙
        (P.colimitsCardinalClosure κ).ι

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
⊢ Mono
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))