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

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

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

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

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

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