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

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

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

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

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