Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := Nat.zero } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + y + n)) ∨
    stmt { index := Nat.zero } { index := y } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (Nat.zero + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + y + n))) ∨
      stmt { index := Nat.zero } { index := y } n ∈ baseProgram (Nat.zero + y + n + 1)

case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.succ x' + y + n)) ∨
    stmt { index := Nat.succ x' } { index := y } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x =>
            Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (Nat.succ x' + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.succ x' + y + n))) ∨
      stmt { index := Nat.succ x' } { index := y } n ∈ baseProgram (Nat.succ x' + y + n + 1)
Tactic:
cases' y with y'
Proof state after:
case zero.zero
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := Nat.zero } { index := Nat.zero } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + n)) ∨
    stmt { index := Nat.zero } { index := Nat.zero } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x =>
            Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (Nat.zero + Nat.zero + n - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + n))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } n ∈ baseProgram (Nat.zero + Nat.zero + n + 1)

case zero.succ
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.succ y' + n)) ∨
    stmt { index := Nat.zero } { index := Nat.succ y' } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x =>
            Finset.image (fun x => concat x.1 x.2)
              (Finset.product (ofLen ↑x) (ofLen (Nat.zero + Nat.succ y' + n - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.succ y' + n))) ∨
      stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ baseProgram (Nat.zero + Nat.succ y' + n + 1)

case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.succ x' + y + n)) ∨
    stmt { index := Nat.succ x' } { index := y } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x =>
            Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (Nat.succ x' + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.succ x' + y + n))) ∨
      stmt { index := Nat.succ x' } { index := y } n ∈ baseProgram (Nat.succ x' + y + n + 1)