mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : ReflQuiver W
inst✝² : ReflQuiver V
C : Type u_3
D : Type u_4
inst✝¹ : Category.{v_1, u_3} C
inst✝ : Category.{v_2, u_4} D
F : Cat.FreeRefl V ⥤ C
⊢ ∀ {v w : V} (f : v ⟶ w),
    (Cat.FreeRefl.lift ((fun F ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F)).map (Cat.FreeRefl.homMk f) =
      eqToHom ⋯ ≫ F.map (Cat.FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
cat_disch

Goal state after:
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:
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:
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:
cat_disch

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

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

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

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:
cat_disch

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((Functor.curry.obj (inverse X Y ⋙ functor X Y)).map (homMk e) ≫
          (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      (mk y) =
    ((mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj (mk y))) ⋯).hom ≫
          (Functor.curry.obj (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))).map (homMk e)).app
      (mk y)

Tactic:
cat_disch

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

Goal state before:
pp: m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ σ (Fin.ofNat (m + 2) a) ≫ σ (Fin.ofNat (m + 1) j) = σ (Fin.ofNat (m + 1 + 1) (j + 1)) ≫ σ (Fin.ofNat (m + 1) a)

Tactic:
convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
⊢ W = ⊤

Tactic:
ext ⟨a, ha⟩ ⟨b, hb⟩ f
  simp only [MorphismProperty.top_apply, iff_true]
  induction a using SimplexCategory.rec with | _ a
  induction b using SimplexCategory.rec with | _ b
  dsimp at ha hb
  generalize h : a + b = c
  induction c generalizing a b with
  | zero =>
    obtain rfl : a = 0 := by lia
    obtain rfl : b = 0 := by lia
    obtain rfl : f = 𝟙 _ := by
      ext i : 3
      apply Subsingleton.elim (α := Fin 1)
    apply MorphismProperty.id_mem
  | succ c hc =>
    by_cases h₁ : Function.Surjective f.hom.toOrderHom; swap
    · obtain _ | b := b
      · exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim
      · obtain ⟨i, g', hf'⟩ := eq_comp_δ_of_not_surjective _ h₁
        replace hf' : f = Hom.tr g' ≫ Hom.tr (SimplexCategory.δ i) :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (hc _ _ _ _ _ (by lia))
          (δ_mem _ (by lia) _)
    by_cases h₂ : Function.Injective f.hom.toOrderHom; swap
    · obtain _ | a := a
      · exact (h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim
      · obtain ⟨i, g', hf'⟩ := eq_σ_comp_of_not_injective _ h₂
        replace hf' : f = Hom.tr (SimplexCategory.σ i) ≫ Hom.tr g' :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (σ_mem _ (by lia) _) (hc _ _ _ _ _ (by lia))
    rw [← epi_iff_surjective] at h₁
    rw [← mono_iff_injective] at h₂
    obtain rfl : a = b := le_antisymm (len_le_of_mono f.hom) (len_le_of_epi f.hom)
    obtain rfl : f = 𝟙 _ := ObjectProperty.hom_ext _ (SimplexCategory.eq_id_of_epi _)
    apply W.id_mem

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

Goal state before:
pp: x✝² x✝¹ x✝ : Truncated 2
⊢ ((iso x✝² x✝¹).symm.hom ▷ hoFunctor₂.obj x✝ ≫
        (iso (x✝² ⊗ x✝¹) x✝).symm.hom ≫ hoFunctor₂.map (α_ x✝² x✝¹ x✝).hom).toFunctor =
    ((α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
        hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom).toFunctor

Tactic:
apply associativity

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

Goal state before:
pp: case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
⊢ ∃ a, toMk₁ a = f

pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
⊢ ∃ a, toMk₁ a = f

Tactic:
· refine ⟨(S.min' hS).castSucc, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
    dsimp [toMk₁_apply]
    split_ifs with h
    · have hi : i ∉ S := fun hi ↦ by have := S.min'_le _ hi; grind
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was: `grind` -/
      simp [S] at hi; grind
    · simp only [Fin.castSucc_lt_castSucc_iff, Finset.lt_min'_iff, not_forall,
        not_lt] at h
      obtain ⟨j, hj, hij⟩ := h
      have := f.toOrderHom.monotone hij
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was:
      `grind [show f j ≤ f i from f.toOrderHom.monotone hij]` -/
      simp_all [ConcreteCategory.hom, S]
      grind

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
⊢ ∃ a, toMk₁ a = f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin i
α : strArrowMk₂ f (SSet.StrictSegal.isPointwiseRightKanExtensionAt._proof_1 i hi) ⟶
  strArrowMk₂ (mkOfSucc k ≫ f) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3 :=
  homMk (Hom.tr (mkOfSucc k) ⋯ hi).op ⋯
⊢ (ConcreteCategory.hom (X.map (op f ≫ (mkOfSucc k).op)))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (X.map (mkOfSucc k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)

Tactic:
exact (isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans
        (ConcreteCategory.congr_hom (s.w α).symm x)

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:
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:
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:
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:
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:
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₁ : WithInitial.star ⟶ x✝²
f₂ : x✝¹ ⟶ x✝
⊢ inr WithInitial.star x✝¹ ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ x✝².inr x✝

Tactic:
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:
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:
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:
cat_disch

Goal state after:
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:
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:
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:
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:
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:
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:
cat_disch

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

Goal state before:
pp: x₁ y₁ z₁ x₂ y₂ z₂ : AugmentedSimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
g₁ : y₁ ⟶ z₁
g₂ : y₂ ⟶ z₂
⊢ (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
cat_disch

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ = h.index s

Tactic:
symm
  simp [← (h.isUniquelyCodimOneFace s).δ_eq_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
| Subcomplex.range φ

Tactic:
← Category.id_comp φ

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
| Subcomplex.range (𝟙 c.pt ≫ φ)
Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: case refine_1.left
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map
        WalkingParallelPairHom.left ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.zero))
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.one))).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.zero))
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.one))).hom ≫
      (parallelPair
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).fst
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).snd ⋙
            (evaluation C D).obj k).map
        WalkingParallelPairHom.left

Tactic:
cat_disch

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

Goal state before:
pp: case refine_1.right
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map
        WalkingParallelPairHom.right ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.zero))
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.one))).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.zero))
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.one))).hom ≫
      (parallelPair
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).fst
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).snd ⋙
            (evaluation C D).obj k).map
        WalkingParallelPairHom.right

Tactic:
cat_disch

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

Goal state before:
pp: case refine_1.id
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
X✝ : WalkingParallelPair
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map
        (WalkingParallelPairHom.id X✝) ≫
      (WalkingParallelPair.casesOn X✝
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.zero))
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.one))).hom =
    (WalkingParallelPair.casesOn X✝
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.zero))
          (Iso.refl
            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
              WalkingParallelPair.one))).hom ≫
      (parallelPair
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).fst
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).snd ⋙
            (evaluation C D).obj k).map
        (WalkingParallelPairHom.id X✝)

Tactic:
cat_disch

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

Goal state before:
pp: case zero
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).pt).hom =
    (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)).ι.app WalkingParallelPair.zero

Tactic:
cat_disch

Goal state after: