Theorem: LoopProgram.ofLen_stmt_complete (FormalSystems/Computability/Loop.lean)

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

State before:
x y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := x } { index := y } n ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (x + y + n)) ∨
    stmt { index := x } { index := y } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x_1) (ofLen (x + y + n - ↑x_1))))
          (Finset.attach (Finset.range (x + y + n))) ∨
      stmt { index := x } { index := y } n ∈ baseProgram (x + y + n + 1)
Tactic:
cases' x with x'
State after:
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)

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'
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)

State before:
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)
Tactic:
cases' n with n'
State after:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.zero)) ∨
    stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
        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 + Nat.zero - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.zero))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈ baseProgram (Nat.zero + Nat.zero + Nat.zero + 1)

case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.succ n')) ∨
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ 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 + Nat.succ n' - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.succ n'))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
        baseProgram (Nat.zero + Nat.zero + Nat.succ 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)

State before:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.zero)) ∨
    stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
        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 + Nat.zero - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.zero))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈ baseProgram (Nat.zero + Nat.zero + Nat.zero + 1)

case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.succ n')) ∨
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ 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 + Nat.succ n' - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.succ n'))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
        baseProgram (Nat.zero + Nat.zero + Nat.succ 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)
Tactic:
. refine' .inr ∘ .inr $ lenOne_complete _ _
  cases' h_stmt with h h <;> rw [h] <;> rfl
State after:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.succ n')) ∨
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ 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 + Nat.succ n' - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.succ n'))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
        baseProgram (Nat.zero + Nat.zero + Nat.succ 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)

State before:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.succ n')) ∨
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ 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 + Nat.succ n' - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.succ n'))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
        baseProgram (Nat.zero + Nat.zero + Nat.succ 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)
Tactic:
. apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
  refine' ⟨stmt (.mk 0) (.mk 0) n', ⟨ofLen_stmt_complete _ h_stmt, _⟩⟩
  cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
State after:
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)

State before:
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)
Tactic:
. apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
  refine' ⟨stmt (.mk 0) (.mk y') n, ⟨_, _⟩⟩
  rw [Nat.add_succ, Nat.succ_add, Nat.succ_eq_add_one]
  apply ofLen_stmt_complete _ h_stmt
  cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
State after:
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)

State before:
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:
. apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
  refine' ⟨stmt (.mk x') (.mk y) n, ⟨_, _⟩⟩
  rw [Nat.succ_add, Nat.succ_add, Nat.succ_eq_add_one]
  apply ofLen_stmt_complete _ h_stmt
  cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
State after:
no goals

State before:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.zero)) ∨
    stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
        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 + Nat.zero - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.zero))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈ baseProgram (Nat.zero + Nat.zero + Nat.zero + 1)
Tactic:
refine' .inr ∘ .inr $ lenOne_complete _ _
State after:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ len (stmt { index := Nat.zero } { index := Nat.zero } Nat.zero) = 1

State before:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ len (stmt { index := Nat.zero } { index := Nat.zero } Nat.zero) = 1
Tactic:
cases' h_stmt with h h <;> rw [h] <;> rfl
State after:
no goals

State before:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.succ n')) ∨
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ 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 + Nat.succ n' - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.succ n'))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
        baseProgram (Nat.zero + Nat.zero + Nat.succ n' + 1)
Tactic:
apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
State after:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.zero + Nat.succ n'),
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne x

State before:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.zero + Nat.succ n'),
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne x
Tactic:
refine' ⟨stmt (.mk 0) (.mk 0) n', ⟨ofLen_stmt_complete _ h_stmt, _⟩⟩
State after:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne (stmt { index := 0 } { index := 0 } n')

State before:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne (stmt { index := 0 } { index := 0 } n')
Tactic:
cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
State after:
no goals

State before:
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)
Tactic:
apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
State after:
case zero.succ
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.succ y' + n), stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne x

State before:
case zero.succ
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.succ y' + n), stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne x
Tactic:
refine' ⟨stmt (.mk 0) (.mk y') n, ⟨_, _⟩⟩
State after:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + Nat.succ y' + n)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)

State before:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + Nat.succ y' + n)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Tactic:
rw [Nat.add_succ, Nat.succ_add, Nat.succ_eq_add_one]
State after:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + y' + n + 1)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)

State before:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + y' + n + 1)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Tactic:
apply ofLen_stmt_complete _ h_stmt
State after:
case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)

State before:
case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Tactic:
cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
State after:
no goals

State before:
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:
apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
State after:
case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ ∃ x ∈ ofLen (Nat.succ x' + y + n), stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne x

State before:
case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ ∃ x ∈ ofLen (Nat.succ x' + y + n), stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne x
Tactic:
refine' ⟨stmt (.mk x') (.mk y) n, ⟨_, _⟩⟩
State after:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (Nat.succ x' + y + n)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)

State before:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (Nat.succ x' + y + n)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Tactic:
rw [Nat.succ_add, Nat.succ_add, Nat.succ_eq_add_one]
State after:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (x' + y + n + 1)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)

State before:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (x' + y + n + 1)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Tactic:
apply ofLen_stmt_complete _ h_stmt
State after:
case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)

State before:
case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Tactic:
cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
State after:
no goals