-- Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
@[simp]
lemma N₂Γ₂ToKaroubiIso_hom_app (X : ChainComplex C ℕ) :
    (N₂Γ₂ToKaroubiIso.hom.app X).f = PInfty

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ PInfty.f n ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    PInfty.f n ≫ PInfty.f n

Tactic:
congr 1

Result:
case h.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
      PInfty.f n =
    PInfty.f n

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (N₂Γ₂ToKaroubiIso.hom.app X).f.f n = PInfty.f n

Tactic:
dsimp [N₂Γ₂ToKaroubiIso]

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (((PInfty.f n ≫
            (Γ₀.splitting X).desc (op ⦋n⦌) fun A =>
              𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
          PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))) ≫
        PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))) ≫
      PInfty.f n =
    PInfty.f n

Proof state:
case h.e_a.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Tactic:
apply id_comp

Result:
no goals

Proof state:
case h.e_a.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ ∀ (A : Splitting.IndexSet (op ⦋n⦌)),
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫
        ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
          PInfty.f n =
      ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Tactic:
intro A

Result:
case h.e_a.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
⊢ (N₂Γ₂ToKaroubiIso.hom.app X).f = PInfty

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (N₂Γ₂ToKaroubiIso.hom.app X).f.f n = PInfty.f n

Proof state:
case h.e_a.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Tactic:
rw [Splitting.ι_desc_assoc, assoc]

Result:
case h.e_a.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ PInfty.f n ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    PInfty.f n

Tactic:
conv_rhs =>
  rw [← PInfty_f_idem]

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ PInfty.f n ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    PInfty.f n ≫ PInfty.f n

Proof state:
case h.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
      PInfty.f n =
    PInfty.f n

Tactic:
apply (Γ₀.splitting X).hom_ext'

Result:
case h.e_a.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ ∀ (A : Splitting.IndexSet (op ⦋n⦌)),
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫
        ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
          PInfty.f n =
      ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ (((PInfty.f n ≫
            (Γ₀.splitting X).desc (op ⦋n⦌) fun A =>
              𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
          PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))) ≫
        PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌))) ≫
      PInfty.f n =
    PInfty.f n

Tactic:
simp only [comp_id, assoc, PInfty_f_idem]

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
⊢ PInfty.f n ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    PInfty.f n