mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
⊢ ∀ (X : ↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X✝)),
    ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫ (ofNerve₂ ↑Y✝).hom).obj X =
      ((ofNerve₂ ↑X✝).hom ≫ ReflQuiv.forget.map F).obj X

Tactic:
by cat_disch

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

Goal state before:
pp: V W x✝ : Truncated 2
⊢ ∀ ⦃x y : x✝.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    (mapHomotopyCategory (𝟙 x✝)).toCatHom.toFunctor.map (HomotopyCategory.homMk e) =
      eqToHom ⋯ ≫ (𝟙 (Cat.of x✝.HomotopyCategory)).toFunctor.map (HomotopyCategory.homMk e) ≫ eqToHom ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: V W X✝ Y✝ Z✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ∀ ⦃x y : X✝.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    (mapHomotopyCategory (x✝¹ ≫ x✝)).toCatHom.toFunctor.map (HomotopyCategory.homMk e) =
      eqToHom ⋯ ≫
        ((mapHomotopyCategory x✝¹).toCatHom ≫ (mapHomotopyCategory x✝).toCatHom).toFunctor.map
            (HomotopyCategory.homMk e) ≫
          eqToHom ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ ∀ (x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })),
    mkNatTrans (fun y ↦ homMk ((Edge.id x).tensor (Edge.id y))) ⋯ =
      𝟙 (lift (fun y ↦ mk (x, y)) (fun {y₀ y₁} e ↦ homMk ((Edge.id x).tensor e)) ⋯ ⋯)

Tactic:
by cat_disch

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

Goal state before:
pp: case neg.«_@».Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne.3003013004._hygCtx._hyg.53.«1»
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj : (ConcreteCategory.hom f) i = (fun i ↦ i) ⟨1, ⋯⟩
⊢ 0 = (ConcreteCategory.hom f) i

Tactic:
· exact (hS ⟨i, by simpa [S]⟩).elim

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (𝟙_ SSet).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom
                (({ app := fun x ↦ ↾fun x_1 ↦ (Functor.const (Fin ((Opposite.unop x).len + 1))).obj (𝟙 i),
                        naturality := ⋯ } ≫
                      nerveMap (functorMap f i i)).app
                  n✝)).toFun
            x✝).obj
        X =
      ((ConcreteCategory.hom
                (↾fun x ↦ (Functor.const (Fin ((Opposite.unop n✝).len + 1))).obj (𝟙 { as := f i.as }))).toFun
            x✝).obj
        X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : ((i ⟶[SSet] j) ⊗ j ⟶[SSet] k).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom
                (({ app := fun x ↦ ↾fun x_1 ↦ Functor.prod' x_1.1 x_1.2 ⋙ i.compFunctor j k, naturality := ⋯ } ≫
                      nerveMap (functorMap f i k)).app
                  n✝)).toFun
            x✝).obj
        X =
      ((ConcreteCategory.hom
                (((nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
                      {
                        app := fun x ↦
                          ↾fun x_1 ↦
                            Functor.prod' x_1.1 x_1.2 ⋙ { as := f i.as }.compFunctor { as := f j.as } { as := f k.as },
                        naturality := ⋯ }).app
                  n✝)).toFun
            x✝).obj
        X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (i ⟶[SSet] j).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom (((functor OrderHom.id).map i j ≫ eqToHom ⋯).app n✝)).toFun x✝).obj X =
      ((ConcreteCategory.hom (((EnrichedFunctor.id SSet (SimplicialThickening J)).map i j).app n✝)).toFun x✝).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (i ⟶[SSet] j).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    ((ConcreteCategory.hom (((functor (g.comp f)).map i j ≫ eqToHom ⋯).app n✝)).toFun x✝).obj X =
      ((ConcreteCategory.hom (((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n✝)).toFun x✝).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁ y₁ x₂ y₂ : AugmentedSimplexCategory
f₁✝ : x₁ ⟶ y₁
f₂✝ : x₂ ⟶ y₂
x✝² x✝¹ x✝ : AugmentedSimplexCategory
f₁ : x✝² ⟶ x✝¹
f₂ : WithInitial.star ⟶ x✝
⊢ x✝².inl WithInitial.star ≫ (f₁ ⊗ₘ f₂) = f₁ ≫ x✝¹.inl x✝

Tactic:
by cat_disch

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

Goal state before:
pp: case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ (∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) →
    { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }

Tactic:
· rintro ⟨i, h₁, h₂⟩
    refine ⟨rfl, SimplexCategory.δ i, ⟨inferInstance, h₁⟩, fun f ⟨h₃, h₄⟩ ↦ ?_⟩
    obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono f
    obtain rfl : j = i := h₂ _ h₄
    rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁ y₁ x₂ y₂ : AugmentedSimplexCategory
f₁✝ : x₁ ⟶ y₁
f₂✝ : x₂ ⟶ y₂
x✝² x✝¹ x✝ : AugmentedSimplexCategory
f₁ : WithInitial.star ⟶ x✝²
f₂ : x✝¹ ⟶ x✝
⊢ inr WithInitial.star x✝¹ ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ x✝².inr x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ (WithInitial.star ⊗ x✝¹).inr x✝ ≫ (α_ WithInitial.star x✝¹ x✝).hom = x✝¹.inr x✝ ≫ inr WithInitial.star (x✝¹ ⊗ x✝)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ (x✝¹ ⊗ WithInitial.star).inr x✝ ≫ (α_ x✝¹ WithInitial.star x✝).hom =
    inr WithInitial.star x✝ ≫ x✝¹.inr (WithInitial.star ⊗ x✝)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ (x✝¹ ⊗ x✝).inr WithInitial.star ≫ (α_ x✝¹ x✝ WithInitial.star).hom =
    x✝.inr WithInitial.star ≫ x✝¹.inr (x✝ ⊗ WithInitial.star)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inl' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i

Tactic:
have e₁ := inl'_eval x y i

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inl' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ inl WithInitial.star x✝¹ ≫ (WithInitial.star ⊗ x✝¹).inl x✝ ≫ (α_ WithInitial.star x✝¹ x✝).hom =
    inl WithInitial.star (x✝¹ ⊗ x✝)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inl WithInitial.star ≫ (x✝¹ ⊗ WithInitial.star).inl x✝ ≫ (α_ x✝¹ WithInitial.star x✝).hom =
    x✝¹.inl (WithInitial.star ⊗ x✝)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inl x✝ ≫ (x✝¹ ⊗ x✝).inl WithInitial.star ≫ (α_ x✝¹ x✝ WithInitial.star).hom = x✝¹.inl (x✝ ⊗ WithInitial.star)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ inr WithInitial.star x✝¹ ≫ (WithInitial.star ⊗ x✝¹).inl x✝ ≫ (α_ WithInitial.star x✝¹ x✝).hom =
    x✝¹.inl x✝ ≫ inr WithInitial.star (x✝¹ ⊗ x✝)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inr WithInitial.star ≫ (x✝¹ ⊗ WithInitial.star).inl x✝ ≫ (α_ x✝¹ WithInitial.star x✝).hom =
    inl WithInitial.star x✝ ≫ x✝¹.inr (WithInitial.star ⊗ x✝)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y z x✝¹ x✝ : AugmentedSimplexCategory
⊢ x✝¹.inr x✝ ≫ (x✝¹ ⊗ x✝).inl WithInitial.star ≫ (α_ x✝¹ x✝ WithInitial.star).hom =
    x✝.inl WithInitial.star ≫ x✝¹.inr (x✝ ⊗ WithInitial.star)

Tactic:
by cat_disch

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

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
a : Fin (n + 1)
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, (objEquiv z) a = (objEquiv z) a₂ → a = a₂

Tactic:
b

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
a b : Fin (n + 1)
⊢ (objEquiv z) a = (objEquiv z) b → a = b
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ∃ s_1,
    (↑s).toS = { dim := (↑s_1).dim + 1, simplex := ((↑(P.p s_1)).cast ⋯).simplex } ∨
      (↑s).toS =
        { dim := (↑s_1).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s_1)).cast ⋯).simplex }

Tactic:
refine ⟨s, Or.inr ?_⟩

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ (↑s).toS =
    { dim := (↑s).dim,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).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 ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
⊢ f.t j ≫ homOfLE ⋯ = f.m j ≫ f.b j

Tactic:
ext c : 1
  simp [← cancel_mono (Subcomplex.ι _)]

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

Goal state before:
pp: case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) = y

Tactic:
simpa only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
        x.ι_b_app_apply, x.ι_t_app_apply] using! h.symm

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

Goal state before:
pp: case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : ↑(P.p c.s) = ↑c'.s
⊢ Cell.type₁ f c = Cell.type₂ f c'

Tactic:
exact (P.ne _ _ h).elim

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
⊢ ∃ J_1 x, ∃ (_ : IsCardinalFiltered J_1 κ), (⊤.map F).colimitsOfShape J_1 X

Tactic:
have ip := F.denseAt X

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
ip : F.DenseAt X
⊢ ∃ J_1 x, ∃ (_ : IsCardinalFiltered J_1 κ), (⊤.map F).colimitsOfShape J_1 X
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
hl.succ_le_simplex_fst_iff,

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
⊢ ¬l.succ ≤ i ↔ i < l.succ
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)
β : Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π
⊢ Nonempty (Arrow.LiftStruct β)

Tactic:
obtain ⟨α, rfl⟩ := (adj₂.arrowHomEquiv sq₁₂ sq₁₃).surjective β

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
h : ∀ (φ : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃), Nonempty (Arrow.LiftStruct φ)
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
⊢ Nonempty (Arrow.LiftStruct ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

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

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

Tactic:
· obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hi)
    rw [φ_of_lt _ _ _ (by grind), Fin.castPred_castSucc]
    rw [Fin.castSucc_lt_iff_succ_le] at hi
    obtain hi | hi :=  hi.lt_or_eq
    · rw [φ_of_lt _ _ _ (by grind)]
      exact hx' (Fin.lt_def.2 (by dsimp; grind))
    · rw [← Fin.castSucc_succ, hi, φ_castSucc]
      refine lt_of_le_of_ne ⟨?_, ?_⟩ ?_
      · dsimp
        rw [simplex_fst_le_castSucc_iff]
        grind
      · exact stdSimplex.monotone_apply _
          (by dsimp; rw [← hi]; exact Fin.castSucc_le_succ i)
      · intro h
        rw [Prod.ext_iff] at h
        dsimp at h
        obtain ⟨h₁, h₂⟩ := h
        apply hx _ hd i.succ
        rw [isIndex_succ]
        refine ⟨h₁, ?_, by aesop⟩
        have := φ_succAbove x hd (min x hd)
        rw [Fin.succAbove_castSucc_self] at this
        rw [← φ_succ_fst x hd, this, hi]
        dsimp

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

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

Goal state before:
pp: α : Type u
⊢ Function.LeftInverse Codiscrete.mk Codiscrete.as

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.CodiscreteCategory

Goal state before:
pp: α : Type u
⊢ Function.RightInverse Codiscrete.mk Codiscrete.as

Tactic:
by cat_disch

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

Goal state before:
pp: case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : i < l.castSucc
⊢ i = l.castSucc ∨ i = l.succ

pp: case inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) l.castSucc)) (x.cast hd).simplex
⊢ l.castSucc = l.castSucc ∨ l.castSucc = l.succ

pp: case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : l.castSucc < i
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
· obtain ⟨l, rfl⟩ := Fin.eq_succ_of_ne_zero (i := l) (by grind)
    refine (hu _ rfl l.succ ?_).elim
    simp [isIndex_succ, S.cast_simplex_rfl, hu', stdSimplex.δ_apply,
      Fin.succAbove_of_lt_succ i l.castSucc hi,
      Fin.succAbove_of_lt_succ i l.succ (by grind), dsimp% hl.simplex_fst_succ,
      dsimp% hl.simplex_snd_succ, dsimp% hl.simplex_fst_castSucc]

Goal state after:
case inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) l.castSucc)) (x.cast hd).simplex
⊢ l.castSucc = l.castSucc ∨ l.castSucc = l.succ

case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : l.castSucc < i
⊢ i = l.castSucc ∨ i = l.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case pos
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
hi : i = s.index.castSucc
⊢ φ s.δ ⋯ i = (objEquiv (s.x.cast ⋯).simplex) i

Tactic:
subst hi

Goal state after:
case pos
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ φ s.δ ⋯ s.index.castSucc = (objEquiv (s.x.cast ⋯).simplex) s.index.castSucc
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : MonoidalCategory C
X₁✝ X₂✝ X₃ : Arrow C
W : C
inst✝ : BraidedCategory C
X₁ X₂ : Arrow C
⊢ (pushoutSymmetry (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≪≫
          HasColimit.isoOfNatIso (spanExt (β_ X₁.left X₂.left) (β_ X₁.left X₂.right) (β_ X₁.right X₂.left) ⋯ ⋯)).hom ≫
      (X₂ □ X₁).hom =
    (X₁ □ X₂).hom ≫ (β_ X₁.right X₂.right).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
f₁ : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
⊢ sq₁₂.mapArrowLeft sq₁₂ (𝟙 f₁) = 𝟙 (Arrow.mk sq₁₂.ι)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
f₁'' : Arrow C₁
sq₁₂'' : F.PushoutObjObj f₁''.hom f₂.hom
sq : f₁ ⟶ f₁'
sq' : f₁' ⟶ f₁''
⊢ sq₁₂.mapArrowLeft sq₁₂' sq ≫ sq₁₂'.mapArrowLeft sq₁₂'' sq' = sq₁₂.mapArrowLeft sq₁₂'' (sq ≫ sq')

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (HomologicalComplex.sc' (X.chainComplex R) 1 0 0).g = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R T : C
f : T ⟶ (X.chainComplex R).X 0
⊢ f ≫ (HomologicalComplex.sc' (X.chainComplex R) 1 0 0).g = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
f₁ : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
⊢ sq₁₂.mapArrowRight sq₁₂ (𝟙 f₂) = 𝟙 (Arrow.mk sq₁₂.ι)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
f₂'' : Arrow C₂
sq₁₂'' : F.PushoutObjObj f₁.hom f₂''.hom
sq : f₂ ⟶ f₂'
sq' : f₂' ⟶ f₂''
⊢ sq₁₂.mapArrowRight sq₁₂' sq ≫ sq₁₂'.mapArrowRight sq₁₂'' sq' = sq₁₂.mapArrowRight sq₁₂'' (sq ≫ sq')

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
f₁ : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
⊢ sq₁₃.mapArrowLeft sq₁₃ (𝟙 f₁) = 𝟙 (Arrow.mk sq₁₃.π)

Tactic:
by cat_disch

Goal state after: