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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ (fun f ↦ Edge.mk (ComposableArrows.mk₁ f) ⋯ ⋯) ((fun e ↦ eqToHom ⋯ ≫ ComposableArrows.hom e.edge ≫ eqToHom ⋯) e) = e

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ edgeMk (𝟙 x) = Edge.id (nerveEquiv.symm x)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ edgeMk (eqToHom ⋯ ≫ homEquiv e ≫ eqToHom ⋯) = e

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
f : x ⟶ y
⊢ homEquiv.symm (homEquiv (edgeMk f)) = homEquiv.symm f

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f₀₁ f₁₂) = (edgeMk f₀₁).edge

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f₀₁ f₁₂) = (edgeMk f₁₂).edge

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
⊢ (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f₀₁ f₁₂) = (edgeMk (f₀₁ ≫ f₁₂)).edge

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ ed.section_ ≫ X.hom = 𝟙 ((SimplicialObject.const C).obj X.right)

Tactic:
by cat_disch

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

Goal state before:
pp: case left
n m : ℕ
⊢ Function.Injective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩

Tactic:
rintro ⟨x₁, h₁⟩ ⟨x₂, h₂⟩ h₃

Goal state after:
case left
n m : ℕ
x₁ : Δ[n] _⦋m⦌
h₁ : x₁ ∈ Δ[n].nonDegenerate m
x₂ : Δ[n] _⦋m⦌
h₂ : x₂ ∈ Δ[n].nonDegenerate m
h₃ :
  (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨x₁, h₁⟩ =
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨x₂, h₂⟩
⊢ ⟨x₁, h₁⟩ = ⟨x₂, h₂⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
a : Fin ((unop (op ⦋m⦌)).len + 1)
⊢ ∀ ⦃a₂ : Fin ((unop (op ⦋m⦌)).len + 1)⦄,
    (Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)))) a =
        (Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))))
          a₂ →
      a = a₂

Tactic:
b

Goal state after:
case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
a b : Fin ((unop (op ⦋m⦌)).len + 1)
⊢ (Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)))) a =
      (Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)))) b →
    a = b
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a : Fin (d + 1)
⊢ ∀ {b : Fin (d + 1)}, (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b

Tactic:
b

Goal state after:
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ yonedaEquiv.symm (yonedaEquiv (toOfSimplex x)) = yonedaEquiv.symm ⟨x, ⋯⟩

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
⊢ ∀ (i j : I₁),
    c₁.Rel i j →
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i).X x)) ⋯).hom ≫
          ((flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁).obj K).d i j =
        ((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).d i j ≫
          (Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X j).X x)) ⋯).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
⊢ ∀ {X Y : HomologicalComplex₂ C c₁ c₂} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex₂ C c₁ c₂)).map f ≫
        (Hom.isoOfComponents
            (fun i₁ ↦ Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj Y).X i₁).X x)) ⋯)
            ⋯).hom =
      (Hom.isoOfComponents
            (fun i₁ ↦ Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj X).X i₁).X x)) ⋯)
            ⋯).hom ≫
        (flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₂ c₁
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i).X x)) ⋯).hom ≫
          ((𝟭 (HomologicalComplex₂ C c₂ c₁)).obj K).d i j =
        ((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).d i j ≫
          (Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X j).X x)) ⋯).hom

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
⊢ ∀ {X Y : HomologicalComplex₂ C c₂ c₁} (f : X ⟶ Y),
    (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).map f ≫
        (Hom.isoOfComponents
            (fun i₂ ↦
              Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj Y).X i₂).X x)) ⋯)
            ⋯).hom =
      (Hom.isoOfComponents
            (fun i₂ ↦
              Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj X).X i₂).X x)) ⋯)
            ⋯).hom ≫
        (𝟭 (HomologicalComplex₂ C c₂ c₁)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} C₃
inst✝³ : Category.{v_4, u_4} C₄
inst✝² : Category.{v_5, u_5} C₁₂
inst✝¹ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
ψ : X₃ ⟶ Y₃
⊢ { obj := fun X₃ ↦ mapTrifunctorMapObj F p X₁ X₂ X₃, map := fun {x x_1} φ ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ,
            map_id := ⋯, map_comp := ⋯ }.map
        ψ ≫
      mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 Y₃) =
    mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃) ≫
      { obj := fun X₃ ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
            map := fun {x x_1} φ ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ, map_id := ⋯, map_comp := ⋯ }.map
        ψ

Tactic:
by
        ext j i₁ i₂ i₃ h
        dsimp
        simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id,
          NatTrans.id_app, ι_mapTrifunctorMapMap, id_comp, NatTrans.naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) →
  Cocone
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i).1) ⋙ G.flip.obj (X₃ (↑i).2)) :=
  fun i ↦ (G.flip.obj (X₃ (↑i).2)).mapCocone (c₁₂ (↑i).1)
hc₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) → IsColimit (c₁₂' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → ρ₁₂.I₁₂ × I₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (ρ₁₂.p (i₁, i₂), i₃)
i₁₂ : ρ₁₂.I₁₂
i₃ : I₃
x✝ : ↑(p' ⁻¹' {(i₁₂, i₃)})
i₁ : I₁
i₂ : I₂
i₃' : I₃
hi : (i₁, i₂, i₃') ∈ p' ⁻¹' {(i₁₂, i₃)}
⊢ (i₁, i₂) ∈ ρ₁₂.p ⁻¹' {i₁₂}

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Associator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ((associator.hom.app (X₁ (i₁, i₂, i₃).1)).app (X₂ (i₁, i₂, i₃).2.1)).app (X₃ (i₁, i₂, i₃).2.2) ≫
      (((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).ιMapObj r (i₁, i₂, i₃) j h ≫
        (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
erw [ι_mapBifunctorComp₂₃MapObjIso_hom]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) →
  Cocone
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i).1) ⋙ G.flip.obj (X₃ (↑i).2)) :=
  fun i ↦ (G.flip.obj (X₃ (↑i).2)).mapCocone (c₁₂ (↑i).1)
hc₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) → IsColimit (c₁₂' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → ρ₁₂.I₁₂ × I₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (ρ₁₂.p (i₁, i₂), i₃)
i₁₂ : ρ₁₂.I₁₂
i₃ : I₃
x✝ : ↑(ρ₁₂.p ⁻¹' {i₁₂})
i₁ : I₁
i₂ : I₂
hi : (i₁, i₂) ∈ ρ₁₂.p ⁻¹' {i₁₂}
⊢ (i₁, i₂, i₃) ∈ p' ⁻¹' {(i₁₂, i₃)}

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) →
  Cocone
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i).1) ⋙ G.flip.obj (X₃ (↑i).2)) :=
  fun i ↦ (G.flip.obj (X₃ (↑i).2)).mapCocone (c₁₂ (↑i).1)
hc₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) → IsColimit (c₁₂' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → ρ₁₂.I₁₂ × I₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (ρ₁₂.p (i₁, i₂), i₃)
i₁₂ : ρ₁₂.I₁₂
i₃ : I₃
x✝ : ↑(p' ⁻¹' {(i₁₂, i₃)})
i₁ : I₁
i₂ : I₂
i₃' : I₃
hi : (i₁, i₂, i₃') ∈ p' ⁻¹' {(i₁₂, i₃)}
⊢ i₃ = i₃'

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : TotalComplexShape c₂ c₁ c
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c
⊢ K.flip.HasTotal c ↔ K.HasTotal c

Tactic:
constructor
  · intro
    change K.flip.flip.HasTotal c
    have := TotalComplexShapeSymmetry.symmetry c₁ c₂ c
    infer_instance
  · intro
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
⊢ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯ ≫ K.D₁ c j j' =
    K.flip.ιTotal c i₂ i₁ j h₁ ≫
      K.flip.D₂ c j j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
ι_D₁,

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
⊢ c₁.σ c₂ c i₁ i₂ • K.d₁ c i₁ i₂ j' =
    K.flip.ιTotal c i₂ i₁ j h₁ ≫
      K.flip.D₂ c j j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₂₃ : ρ₂₃.I₂₃
h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃
⊢ ρ₂₃.q (i₁, i₂₃) = j

Tactic:
rw [← h, ← h₂₃, ← ρ₂₃.hpq]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun i₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) →
  Cocone (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i).2) ⋙ F.obj (X₁ (↑i).1)) :=
  fun i ↦ (F.obj (X₁ (↑i).1)).mapCocone (c₂₃ (↑i).2)
hc₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → IsColimit (c₂₃' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → I₁ × ρ₂₃.I₂₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (i₁, ρ₂₃.p (i₂, i₃))
i₁ : I₁
i₂₃ : ρ₂₃.I₂₃
x✝ : ↑(p' ⁻¹' {(i₁, i₂₃)})
i₁' : I₁
i₂ : I₂
i₃ : I₃
hi : (i₁', i₂, i₃) ∈ p' ⁻¹' {(i₁, i₂₃)}
⊢ (i₂, i₃) ∈ ρ₂₃.p ⁻¹' {i₂₃}

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun i₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) →
  Cocone (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i).2) ⋙ F.obj (X₁ (↑i).1)) :=
  fun i ↦ (F.obj (X₁ (↑i).1)).mapCocone (c₂₃ (↑i).2)
hc₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → IsColimit (c₂₃' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → I₁ × ρ₂₃.I₂₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (i₁, ρ₂₃.p (i₂, i₃))
i₁ : I₁
i₂₃ : ρ₂₃.I₂₃
x✝ : ↑(ρ₂₃.p ⁻¹' {i₂₃})
i₂ : I₂
i₃ : I₃
hi : (i₂, i₃) ∈ ρ₂₃.p ⁻¹' {i₂₃}
⊢ (i₁, i₂, i₃) ∈ p' ⁻¹' {(i₁, i₂₃)}

Tactic:
by cat_disch

Goal state after: