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 (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 z))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) z f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) z f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) z f)
      ⊤ (f ≫ g) =
    WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ ⊥) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊥ f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊥ f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊥ f)
        ⊤ f ≫
      WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ z) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 z))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) z f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) z f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) 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 (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊥ f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊥ f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊥ f)
      ⊤ (f ≫ g) =
    WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ ⊥) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊥ f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊥ f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊥ f)
        ⊤ f ≫
      WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ ⊥) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊥ f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊥ f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊥ 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 (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a✝)))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) (WithBotTop.coe a✝) f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) (WithBotTop.coe a✝) f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) (WithBotTop.coe a✝) f)
      ⊤ (f ≫ g) =
    WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ ⊥) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊥ f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊥ f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊥ f)
        ⊤ f ≫
      WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ WithBotTop.coe a✝) →
          (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a✝)))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) (WithBotTop.coe a✝) f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) (WithBotTop.coe a✝) f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) (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 (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤))
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊤ f)
      (fun a f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (WithBotTop.coe a ⟶ y) →
            (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
          (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊤ f)
      (fun f ↦
        WithBotTop.rec (motive := fun {y} ↦
          (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0) (fun b f ↦ 0)
          (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊤ f)
      ⊤ (f ≫ g) =
    WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ ⊥) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊥ f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊥ f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊥ f)
        ⊤ f ≫
      WithBotTop.rec (motive := fun {x} ↦
        (x ⟶ ⊤) → (WithBotTop.rec (𝟭 C) t.truncGE 0 x ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤))
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊥ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊥)) (fun b f ↦ t.truncGEπ b) (fun f ↦ 0) ⊤ f)
        (fun a f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (WithBotTop.coe a ⟶ y) →
              (WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y))
            (fun f ↦ 0) (fun b f ↦ t.natTransTruncGEOfLE a b ⋯) (fun f ↦ 0) ⊤ f)
        (fun f ↦
          WithBotTop.rec (motive := fun {y} ↦
            (⊤ ⟶ y) → (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤ ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y)) (fun f ↦ 0)
            (fun b f ↦ 0) (fun f ↦ 𝟙 (WithBotTop.rec (𝟭 C) t.truncGE 0 ⊤)) ⊤ f)
        ⊥ g