Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : EInt
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ n) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) n))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) n f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) n f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) n f)
      n (𝟙 n) =
    𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) n)

Tactic:
induction n using WithBotTop.rec

Goal state after:
case bot
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ ⊥) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) ⊥ f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) ⊥ f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) ⊥ f)
      ⊥ (𝟙 ⊥) =
    𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)

case coe
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a✝ : ℤ
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ WithBotTop.coe a✝) →
        (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a✝)))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) (WithBotTop.coe a✝) f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) (WithBotTop.coe a✝) f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) (WithBotTop.coe a✝) f)
      (WithBotTop.coe a✝) (𝟙 (WithBotTop.coe a✝)) =
    𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a✝))

case top
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ ⊤) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊥)) (fun b f ↦ 0) (fun f ↦ 0) ⊤ f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec 0 t.truncLT (𝟭 C) (WithBotTop.coe a) ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncLTOfLE a b ⋯) (fun f ↦ t.truncLTι a) ⊤ f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤ ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)) ⊤ f)
      ⊤ (𝟙 ⊤) =
    𝟙 (WithBotTop.rec 0 t.truncLT (𝟭 C) ⊤)