Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case top.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
z : EInt
g : ⊥ ⟶ z
g' : ⊥ ≤ z
f : ⊤ ⟶ ⊥
f' : ⊤ ≤ ⊥
⊢ WithBotTop.rec (motive := fun {x} ↦
      (x ⟶ z) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) z))
      (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) z 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) z 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) ⊤)) z f)
      ⊤ (f ≫ g) =
    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)
        ⊤ f ≫
      WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ z) → (WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) z))
        (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) z 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) z 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) ⊤)) z f)
        ⊥ g

Tactic:
induction z using WithBotTop.rec

Goal state after:
case top.bot.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
f : ⊤ ⟶ ⊥
f' : ⊤ ≤ ⊥
g : ⊥ ⟶ ⊥
g' : ⊥ ≤ ⊥
⊢ 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)
      ⊤ (f ≫ g) =
    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)
        ⊤ f ≫
      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)
        ⊥ g

case top.bot.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
f : ⊤ ⟶ ⊥
f' : ⊤ ≤ ⊥
a✝ : ℤ
g : ⊥ ⟶ WithBotTop.coe a✝
g' : ⊥ ≤ WithBotTop.coe 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)
      ⊤ (f ≫ g) =
    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)
        ⊤ f ≫
      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)
        ⊥ g

case top.bot.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
f : ⊤ ⟶ ⊥
f' : ⊤ ≤ ⊥
g : ⊥ ⟶ ⊤
g' : ⊥ ≤ ⊤
⊢ 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)
      ⊤ (f ≫ g) =
    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)
        ⊤ f ≫
      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)
        ⊥ g