mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Function.Bijective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩

Tactic:
constructor

Goal state after:
case left
n : ℕ
i : Fin (n + 2)
⊢ Function.Injective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩

case right
n : ℕ
i : Fin (n + 2)
⊢ Function.Surjective fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f✝ ≫
      (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y✝).X x)) ⋯).hom =
    (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X✝).X x)) ⋯).hom ≫
      ChainComplex.alternatingConst.map f✝

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
i✝ : ℕ
⊢ ((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f✝ ≫
          (HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y✝).X x))
              ⋯).hom).f
      i✝ =
    ((HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X✝).X x)) ⋯).hom ≫
          ChainComplex.alternatingConst.map f✝).f
      i✝
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
⊢ mapBifunctorMapMap F p e.hom e'.hom ≫ mapBifunctorMapMap F p e.inv e'.inv = 𝟙 (mapBifunctorMapObj F p X₁ Y₁)

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.hom e'.hom ≫ mapBifunctorMapMap F p e.inv e'.inv) x✝ =
    ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₁ Y₁) x✝
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
⊢ mapBifunctorMapMap F p e.inv e'.inv ≫ mapBifunctorMapMap F p e.hom e'.hom = 𝟙 (mapBifunctorMapObj F p X₂ Y₂)

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.inv e'.inv ≫ mapBifunctorMapMap F p e.hom e'.hom) x✝ =
    ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₂ Y₂) x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
⊢ face ∅ = ⊥

Tactic:
ext

Goal state after:
n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x✝ : Δ[n].obj x✝¹
⊢ x✝ ∈ (face ∅).obj x✝¹ ↔ x✝ ∈ ⊥.obj x✝¹
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
⊢ face univ = ⊤

Tactic:
ext

Goal state after:
n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x✝ : Δ[n].obj x✝¹
⊢ x✝ ∈ (face univ).obj x✝¹ ↔ x✝ ∈ ⊤.obj x✝¹
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ ¬1 = n✝ + 1 + 1

Tactic:
exact (Nat.one_lt_succ_succ _).ne

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

Goal state before:
pp: X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X✝ Y✝ : SimplexCategoryᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ Δ[m].map x✝ ≫ (objEquiv.trans h.homEquiv).toIso.hom = (objEquiv.trans h.homEquiv).toIso.hom ≫ X.map x✝

Tactic:
ext

Goal state after:
X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X✝ Y✝ : SimplexCategoryᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Δ[m].obj X✝
⊢ (ConcreteCategory.hom (Δ[m].map x✝¹ ≫ (objEquiv.trans h.homEquiv).toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom ((objEquiv.trans h.homEquiv).toIso.hom ≫ X.map x✝¹)).toFun x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso j).inv = (facePairComplIso i j h).inv ≫ stdSimplex.δ (i.castPred ⋯)

Tactic:
simp [← cancel_mono (faceSingletonComplIso j).hom,
    ← cancel_mono (Subcomplex.ι _), ← cancel_epi (facePairComplIso i j h).hom,
    facePairComplIso_hom_ι]

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

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

Tactic:
constructor

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

case right
n m : ℕ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩
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
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ l, ↑i = ↑j + 1 + l

Tactic:
Fin.castSucc_lt_iff_succ_le,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.succ ≤ i
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ l, ↑i = ↑j + 1 + l
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Bijective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
constructor

Goal state after:
case left
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Injective fun i ↦ ⟨↑x i, ⋯⟩

case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Surjective fun i ↦ ⟨↑x i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case left
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Mono (objEquiv ↑x)
⊢ Function.Injective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
rw [SimplexCategory.mono_iff_injective] at this

Goal state after:
case left
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
⊢ Function.Injective fun i ↦ ⟨↑x i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

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

Tactic:
rw [SimplexCategory.mono_iff_injective] at this

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: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ ↑x a ≤ ↑x b ↔ a ≤ b

Tactic:
constructor

Goal state after:
case mp
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ ↑x a ≤ ↑x b → a ≤ b

case mpr
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ a ≤ b → ↑x a ≤ ↑x b
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ { toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨x, ⋯⟩ = ⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩

Tactic:
ext

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ↑({ toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨x, ⋯⟩) = ↑⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬1 = i + 2

Tactic:
exact (Nat.one_lt_succ_succ _).ne

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ IsIso (toOfSimplex x) ↔ Mono (yonedaEquiv.symm x)

Tactic:
constructor

Goal state after:
case mp
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ IsIso (toOfSimplex x) → Mono (yonedaEquiv.symm x)

case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Mono (yonedaEquiv.symm x) → IsIso (toOfSimplex x)
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 L : HomologicalComplex₂ C c₁ c₂
f : K.toGradedObject ⟶ L.toGradedObject
comm₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), c₁.Rel i₁ i₁' → f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ f (i₁', i₂)
comm₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), c₂.Rel i₂ i₂' → f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ f (i₁, i₂')
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
i₂ : I₂
⊢ ({ f := fun i₂ ↦ f (i₁, i₂), comm' := ⋯ } ≫ L.d i₁ i₁').f i₂ =
    (K.d i₁ i₁' ≫ { f := fun i₂ ↦ f (i₁', i₂), comm' := ⋯ }).f i₂

Tactic:
exact comm₁ i₁ i₁' i₂ h₁

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 L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i✝ j✝ : I₂
a✝ : c₂.Rel i✝ j✝
⊢ { f := fun j ↦ (f.f j).f i✝, comm' := ⋯ } ≫ L.flip.d i✝ j✝ =
    K.flip.d i✝ j✝ ≫ { f := fun j ↦ (f.f j).f j✝, comm' := ⋯ }

Tactic:
ext

Goal state after:
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 L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i✝¹ j✝ : I₂
a✝ : c₂.Rel i✝¹ j✝
i✝ : I₁
⊢ ({ f := fun j ↦ (f.f j).f i✝¹, comm' := ⋯ } ≫ L.flip.d i✝¹ j✝).f i✝ =
    (K.flip.d i✝¹ j✝ ≫ { f := fun j ↦ (f.f j).f j✝, comm' := ⋯ }).f i✝
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      (i + 1) =
    (((dNext (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD (i + 1)) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f (i + 1)

Tactic:
| succ i =>

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (F.map 0).app (K₂.X i₂) = 0

Tactic:
Functor.map_zero,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ NatTrans.app 0 (K₂.X i₂) = 0
Module: Mathlib.Algebra.Homology.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ (F.map 0).app (K₂.X i₂) = 0

Tactic:
Functor.map_zero,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ NatTrans.app 0 (K₂.X i₂) = 0
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s' ≫
      AlternatingFaceMapComplex.ε.app X =
    𝟙 ((ChainComplex.single₀ C).obj (point.obj X))

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ (((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s' ≫
          AlternatingFaceMapComplex.ε.app X).f
      0 =
    (𝟙 ((ChainComplex.single₀ C).obj (point.obj X))).f 0
Module: Mathlib.Algebra.Homology.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
⊢ HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (𝟙 K₂).f) ⋯ ⋯ =
    𝟙
      (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
        (fun i₁ i₁' i₂ ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (fun i₁ i₂ i₂' ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯
        ⋯ ⋯ ⋯)

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i✝¹ : I₁
i✝ : I₂
⊢ ((HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (𝟙 K₂).f) ⋯ ⋯).f i✝¹).f i✝ =
    ((𝟙
              (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
                (fun i₁ i₁' i₂ ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
                (fun i₁ i₂ i₂' ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)).f
          i✝¹).f
      i✝
Module: Mathlib.Algebra.Homology.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
X✝ Y✝ Z✝ : HomologicalComplex C₂ c₂
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).f) ⋯ ⋯ =
    HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map f.f) ⋯ ⋯ ≫
      HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map g.f) ⋯ ⋯

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
X✝ Y✝ Z✝ : HomologicalComplex C₂ c₂
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝¹ : I₁
i✝ : I₂
⊢ ((HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).f) ⋯ ⋯).f i✝¹).f i✝ =
    ((HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map f.f) ⋯ ⋯ ≫
              HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map g.f) ⋯ ⋯).f
          i✝¹).f
      i✝
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

Tactic:
rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, ← c₁₂.next_eq' h₁, h]

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

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

case mpr
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.HasTotal c → K.flip.HasTotal c
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j : J
⊢ ((K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) ≫
      K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) =
    𝟙 ((K.flip.total c).X j)

Tactic:
ext

Goal state after:
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
i₁✝ : I₂
i₂✝ : I₁
hi✝ : c₂.π c₁ c (i₁✝, i₂✝) = j
⊢ (K.flip.ιTotal c i₁✝ i₂✝ j hi✝ ≫
      (K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) ≫
        K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) =
    K.flip.ιTotal c i₁✝ i₂✝ j hi✝ ≫ 𝟙 ((K.flip.total c).X j)
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j : J
⊢ ((K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) ≫
      K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) =
    𝟙 ((K.total c).X j)

Tactic:
ext

Goal state after:
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
i₁✝ : I₁
i₂✝ : I₂
hi✝ : c₁.π c₂ c (i₁✝, i₂✝) = j
⊢ (K.ιTotal c i₁✝ i₂✝ j hi✝ ≫
      (K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) ≫
        K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) =
    K.ιTotal c i₁✝ i₂✝ j hi✝ ≫ 𝟙 ((K.total c).X j)
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case neg
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'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
K.D₁_shape _ _ _ h₀,

Goal state after:
case neg
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'
⊢ (K.totalFlipIsoX c j).hom ≫ 0 = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom