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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0

Tactic:
rcases n with _ | n <;> dsimp [objD]

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow =
    0

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ =
    0
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ ↑(if (if k.castSucc < i then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < i then k.castSucc else k.succ).castSucc
      else (if k.castSucc < i then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < i.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)

Tactic:
rcases i with ⟨i, _⟩

Goal state after:
n : ℕ
j : Fin (n + 2)
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝ : i < n + 2
H : ⟨i, isLt✝⟩ ≤ j
⊢ ↑(if (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).castSucc
      else (if k.castSucc < ⟨i, isLt✝⟩ then k.castSucc else k.succ).succ) =
    ↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < ⟨i, isLt✝⟩.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ i.succ ≫ σ i)) j) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) j)

Tactic:
rcases i with ⟨i, _⟩

Goal state after:
n : ℕ
j : Fin (⦋n⦌.len + 1)
i : ℕ
isLt✝ : i < n + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, isLt✝⟩.succ ≫ σ ⟨i, isLt✝⟩)) j) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) j)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ j
k : Fin (⦋m⦌.len + 1)
⊢ (Hom.toOrderHom (factor_δ f j ≫ δ j)) k = (Hom.toOrderHom f) k

Tactic:
cases j using Fin.cases

Goal state after:
case zero
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ 0
⊢ (Hom.toOrderHom (factor_δ f 0 ≫ δ 0)) k = (Hom.toOrderHom f) k

case succ
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
i✝ : Fin (n + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ i✝.succ
⊢ (Hom.toOrderHom (factor_δ f i✝.succ ≫ δ i✝.succ)) k = (Hom.toOrderHom f) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case succ
i : ℕ
hi' : ∀ {n m : ℕ} (h : n + i = m), σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h
n m : ℕ
h : n + (i + 1) = m
⊢ σ₀Iter (i + 1 + 1) ⋯ = σ 0 ≫ σ₀Iter (i + 1) h

Tactic:
rw [σ₀Iter_succ, hi' (by lia), σ₀Iter_succ, Category.assoc]

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ j ≫ σ₀Iter i hi)) k) = ↑((ConcreteCategory.hom (σ₀Iter (i + 1) ⋯)) k)

Tactic:
dsimp% ConcreteCategory.comp_apply (σ j) (σ₀Iter i),

Goal state after:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) ((ConcreteCategory.hom (σ j)) k)) =
    ↑((ConcreteCategory.hom (σ₀Iter (i + 1) ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case succ
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n m : ℕ
hi : n + (i + 1) = m
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌

Tactic:
obtain rfl : m = (n + i) + 1 := by lia

Goal state after:
case succ
i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n : ℕ
hi : n + (i + 1) = n + i + 1
⊢ δ₀Iter (i + 1) hi ≫ σ₀Iter (i + 1) hi = 𝟙 ⦋n⦌
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
hi : n + i = m
⊢ δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌

Tactic:
by
  induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    simp
  | succ i hi' =>
    obtain rfl : m = (n + i) + 1 := by lia
    rw [δ₀Iter_succ_assoc .., σ₀Iter_succ',
      dsimp% reassoc_of% δ_comp_σ_self (n := n + i) (i := 0), hi']

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
x y : SimplexCategory
g : x ⟶ y
j : Fin (x.len + 1)
⊢ f.hom ≫ WidePushout.ι (fun x ↦ f.hom) ((SimplexCategory.Hom.toOrderHom g) j) = WidePushout.head fun x ↦ f.hom

Tactic:
rw [← WidePushout.arrow_ι]

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

Goal state before:
pp: X : SSet
s t : X.S
⊢ s.simplex ∈ t.subcomplex.obj (Opposite.op ⦋s.dim⦌) ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex

Tactic:
Subfunctor.ofSection_obj,

Goal state after:
X : SSet
s t : X.S
⊢ s.simplex ∈ {u | ∃ f, (ConcreteCategory.hom (X.map f)) t.simplex = u} ↔
    ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.simplex ∈ y.subcomplex.obj (Opposite.op ⦋x.dim⦌)

Tactic:
exact ⟨_, hf⟩

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

Goal state before:
pp: X Y : Truncated 2
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f g : Edge x y
⊢ f = g

Tactic:
by ext; subsingleton

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ s ∈ (nerve X).nonDegenerate n ↔ Function.Injective s.obj

Tactic:
mem_nerve_nonDegenerate_iff_strictMono

Goal state after:
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ StrictMono s.obj ↔ Function.Injective s.obj
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case succ
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ Δ[m].HasDimensionLT d

Tactic:
exact hasDimensionLT_of_le _ (m + 1) _

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
j : Fin ((unop (op ⦋n + 1⦌)).len + 1)
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove j) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) j

Tactic:
cases j using Fin.cases

Goal state after:
case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove 0) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) 0

case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove i✝.succ) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) i✝.succ
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
j : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove j) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) j

Tactic:
cases j using Fin.cases

Goal state after:
case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove 0) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) 0

case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
i✝ : Fin (unop (op ⦋n + 1 + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove i✝.succ) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) i✝.succ
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
j : Fin 1
⊢ (ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j

pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.base fun x ↦ f.hom

Tactic:
· fin_cases j
      simp

Goal state after:
case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.base fun x ↦ f.hom
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:
Linear.units_smul_comp,

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.ι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' ⋯
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
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₁ c₂ c (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    (c₂.ε₂ c₁ c (i₂, i₁) • (K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.flip.ιTotal c i₂ (c₁.next i₁) j' h₃) ≫
      K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
Linear.units_smul_comp,

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
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₁ c₂ c (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    c₂.ε₂ c₁ c (i₂, i₁) •
      ((K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.flip.ιTotal c i₂ (c₁.next i₁) j' h₃) ≫
        K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
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:
Linear.units_smul_comp,

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.ι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' ⋯
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
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₂ c₂ c (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    (c₂.ε₁ c₁ c (i₂, i₁) • (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ K.flip.ιTotal c (c₂.next i₂) i₁ j' h₃) ≫
      K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
Linear.units_smul_comp,

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
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₂ c₂ c (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    c₂.ε₁ c₁ c (i₂, i₁) •
      ((K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ K.flip.ιTotal c (c₂.next i₂) i₁ j' h₃) ≫
        K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: 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 L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ map e.inv c₁₂ ≫ map e.hom c₁₂ = 𝟙 (L.total c₁₂)

Tactic:
by rw [← map_comp, e.inv_hom_id, map_id]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
HomologicalComplex₂.d₂_eq _ _ _ hi₂ _ hj',

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          (c₁.ε₂ c₂ c (i₁, i₂) •
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj') =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          (c₁.ε₂ c₂ c (i₁, i₂) •
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj') =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
HomologicalComplex₂.d₂_eq _ _ _ hi₂ _
        (by rw [← c.next_eq' (ComplexShape.rel_π₂ c₁ c i₁' hi₂), hj]),

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          (c₁.ε₂ c₂ c (i₁, i₂) •
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj') =
    -(c₁.ε₂ c₂ c (i₁', i₂) •
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁').d i₂ i₂' ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁' i₂' (c.next j) ⋯) ≫
        hom₁ h₁ f₂ F c (c.next j) j