Theorem: Fin.snoc_three_apply (SetTheory/Formula.lean)

State before:
V : Type ?u.9943
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z : α
⊢ snoc (snoc (snoc l x) y) z { val := n, isLt := (_ : n < n + (2 + 1)) } = x
Tactic:
simp only [snoc]
State after:
V : Type ?u.9943
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z : α
⊢ (if h : n < n + 1 + 1 then
      if h_1 : n < n + 1 then
        if h_2 : n < n then
          l
            { val := n,
              isLt :=
                (_ :
                  { val := n,
                        isLt :=
                          (_ :
                            { val := n,
                                  isLt := (_ : { val := n, isLt := (_ : n < n + (2 + 1)) }.val < n + 1 + 1) }.val <
                              n + 1) }.val <
                    n) }
        else x
      else y
    else z) =
    x

State before:
V : Type ?u.9943
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z : α
⊢ (if h : n < n + 1 + 1 then
      if h_1 : n < n + 1 then
        if h_2 : n < n then
          l
            { val := n,
              isLt :=
                (_ :
                  { val := n,
                        isLt :=
                          (_ :
                            { val := n,
                                  isLt := (_ : { val := n, isLt := (_ : n < n + (2 + 1)) }.val < n + 1 + 1) }.val <
                              n + 1) }.val <
                    n) }
        else x
      else y
    else z) =
    x
Tactic:
have : n < n + 1 + 1 := Nat.lt_add _
State after:
V : Type ?u.9943
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z : α
this : n < n + 1 + 1
⊢ (if h : n < n + 1 + 1 then
      if h_1 : n < n + 1 then
        if h_2 : n < n then
          l
            { val := n,
              isLt :=
                (_ :
                  { val := n,
                        isLt :=
                          (_ :
                            { val := n,
                                  isLt := (_ : { val := n, isLt := (_ : n < n + (2 + 1)) }.val < n + 1 + 1) }.val <
                              n + 1) }.val <
                    n) }
        else x
      else y
    else z) =
    x

State before:
V : Type ?u.9943
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y z : α
this : n < n + 1 + 1
⊢ (if h : n < n + 1 + 1 then
      if h_1 : n < n + 1 then
        if h_2 : n < n then
          l
            { val := n,
              isLt :=
                (_ :
                  { val := n,
                        isLt :=
                          (_ :
                            { val := n,
                                  isLt := (_ : { val := n, isLt := (_ : n < n + (2 + 1)) }.val < n + 1 + 1) }.val <
                              n + 1) }.val <
                    n) }
        else x
      else y
    else z) =
    x
Tactic:
aesop
State after:
no goals