Theorem: Fin.tuple_sequence₂ (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Fin 2 → Type u
x : (i : Fin 2) → m (α i)
⊢ tupleSequence x = do
    let r₀ ← x 0
    let r₁ ← x 1
    pure (cons r₀ (cons r₁ default))
Tactic:
simp [Fin.tupleSequence, functor_norm]
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Fin 2 → Type u
x : (i : Fin 2) → m (α i)
⊢ (do
      let r ← x 0
      let x ← tail x 0
      pure (cons r (cons x default))) =
    do
    let r₀ ← x 0
    let r₁ ← x 1
    pure (cons r₀ (cons r₁ default))

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Fin 2 → Type u
x : (i : Fin 2) → m (α i)
⊢ (do
      let r ← x 0
      let x ← tail x 0
      pure (cons r (cons x default))) =
    do
    let r₀ ← x 0
    let r₁ ← x 1
    pure (cons r₀ (cons r₁ default))
Tactic:
rfl
State after:
no goals