internlm/Lean-Github huggingface dataset:
Theorem: SetTheory.interpret_eqOPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.eqSingleton (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc y)) (termSucc (termSucc z))))
            (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
              (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })))))
      v l ↔
    interpretTerm V v l x = pair {interpretTerm V v l y} (pair (interpretTerm V v l y) (interpretTerm V v l z))
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_isOPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isOPair x) v l ↔ IsOPair (interpretTerm V v l x)
Tactic:
unfold BoundedFormula.isOPair IsOPair opair
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.eqOPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
            (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) }))))
      v l ↔
    ∃ y z, interpretTerm V v l x = pair {y} (pair y z)
Theorem: SetTheory.interpret_isOPair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.eqOPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
            (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) }))))
      v l ↔
    ∃ y z, interpretTerm V v l x = pair {y} (pair y z)
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_memProd'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memProd x y z) v l ↔
    ∃ a, a ∈ interpretTerm V v l y ∧ ∃ b, b ∈ interpretTerm V v l z ∧ interpretTerm V v l x = opair a b
Tactic:
unfold BoundedFormula.memProd
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.mem (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc z))))
            (BoundedFormula.eqOPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
              (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })))))
      v l ↔
    ∃ a, a ∈ interpretTerm V v l y ∧ ∃ b, b ∈ interpretTerm V v l z ∧ interpretTerm V v l x = opair a b
Theorem: SetTheory.interpret_memProd'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.mem (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc z))))
            (BoundedFormula.eqOPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
              (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })))))
      v l ↔
    ∃ a, a ∈ interpretTerm V v l y ∧ ∃ b, b ∈ interpretTerm V v l z ∧ interpretTerm V v l x = opair a b
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_prod_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈ prod x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b
Tactic:
unfold prod
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈
      sep (BoundedFormula.memProd (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then x else y)
        (power (power (x ∪ y))) ↔
    ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b
Theorem: SetTheory.mem_prod_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈
      sep (BoundedFormula.memProd (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then x else y)
        (power (power (x ∪ y))) ↔
    ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b
Tactic:
simp only [mem_sep_iff, mem_power_iff, interpret_memProd', interpret_inl, ite_true,
  ite_false, interpret_inr, and_iff_right_iff_imp, forall_exists_index, and_imp]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∀ (x_1 : V), x_1 ∈ x → ∀ (x_2 : V), x_2 ∈ y → z = opair x_1 x_2 → z ⊆ power (x ∪ y)
Theorem: SetTheory.mem_prod_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∀ (x_1 : V), x_1 ∈ x → ∀ (x_2 : V), x_2 ∈ y → z = opair x_1 x_2 → z ⊆ power (x ∪ y)
Tactic:
rintro a ha b hb rfl
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ opair a b ⊆ power (x ∪ y)
Theorem: SetTheory.mem_prod_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ opair a b ⊆ power (x ∪ y)
Tactic:
intro z hz
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z ∈ opair a b
⊢ z ∈ power (x ∪ y)
Theorem: SetTheory.mem_prod_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z ∈ opair a b
⊢ z ∈ power (x ∪ y)
Tactic:
rw [opair, mem_pair_iff] at hz
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
z : V
hz : z = {a} ∨ z = pair a b
⊢ z ∈ power (x ∪ y)
Theorem: SetTheory.mem_prod_iff
Proof state before:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ∈ power (x ∪ y)
Tactic:
rw [mem_power_iff]
Proof state after:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ⊆ x ∪ y
Theorem: SetTheory.mem_prod_iff
Proof state before:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ pair a b ⊆ x ∪ y
Tactic:
intro t ht
Proof state after:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
t : V
ht : t ∈ pair a b
⊢ t ∈ x ∪ y
Theorem: SetTheory.mem_prod_iff
Proof state before:
case inr
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
t : V
ht : t ∈ pair a b
⊢ t ∈ x ∪ y
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.opair_mem_prod_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z a b : V
⊢ opair a b ∈ prod x y ↔ a ∈ x ∧ b ∈ y
Tactic:
rw [mem_prod_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z a b : V
⊢ (∃ a_1, a_1 ∈ x ∧ ∃ b_1, b_1 ∈ y ∧ opair a b = opair a_1 b_1) ↔ a ∈ x ∧ b ∈ y
Theorem: SetTheory.opair_mem_prod_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z a b : V
⊢ (∃ a_1, a_1 ∈ x ∧ ∃ b_1, b_1 ∈ y ∧ opair a b = opair a_1 b_1) ↔ a ∈ x ∧ b ∈ y
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_isOPairIn
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memProd x y z) v l ↔
    interpretTerm V v l x ∈ prod (interpretTerm V v l y) (interpretTerm V v l z)
Tactic:
rw [mem_prod_iff, interpret_memProd']
Proof state after:
no goals
Theorem: not_not
Proof state before:
V : Type ?u.5243
inst✝ : SetTheory V
p : Prop
⊢ ¬¬p ↔ p
Tactic:
by_cases p <;> aesop
Proof state after:
no goals
Theorem: not_forall
Proof state before:
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
Tactic:
constructor
Proof state after:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) → ∃ x, ¬p x

case mpr
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (∃ x, ¬p x) → ¬∀ (x : α), p x
Theorem: not_forall
Proof state before:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) → ∃ x, ¬p x
Tactic:
by_contra
Proof state after:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
x✝ : ¬((¬∀ (x : α), p x) → ∃ x, ¬p x)
⊢ False
Theorem: not_forall
Proof state before:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
x✝ : ¬((¬∀ (x : α), p x) → ∃ x, ¬p x)
⊢ False
Tactic:
aesop
Proof state after:
no goals
Theorem: not_forall
Proof state before:
case mpr
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (∃ x, ¬p x) → ¬∀ (x : α), p x
Tactic:
aesop
Proof state after:
no goals
Theorem: or_iff
Proof state before:
V : Type ?u.6497
inst✝ : SetTheory V
p q : Prop
⊢ p ∨ q ↔ ¬p → q
Tactic:
by_cases p <;> aesop
Proof state after:
no goals
Theorem: and_iff
Proof state before:
V : Type ?u.6701
inst✝ : SetTheory V
p q : Prop
⊢ p ∧ q ↔ ¬(p → ¬q)
Tactic:
by_cases p <;> aesop
Proof state after:
no goals
Theorem: Fin.snoc_castSucc
Proof state before:
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ snoc l x (castSucc k) = l k
Tactic:
rw [Fin.snoc, dif_pos]
Proof state after:
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ l { val := (castSucc k).val, isLt := ?hc } = l k

case hc
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ (castSucc k).val < n
Theorem: Fin.snoc_castSucc
Proof state before:
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ l { val := (castSucc k).val, isLt := ?hc } = l k

case hc
V : Type ?u.7418
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
k : Fin n
⊢ (castSucc k).val < n
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.lt_add
Proof state before:
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
⊢ n < n + (m + 1)
Tactic:
induction m with
| zero =>
    rw [Nat.lt_succ]
    exact Nat.le_refl n
| succ m ih =>
    rw [← Nat.add_assoc, Nat.lt_succ]
    exact Nat.le_of_lt ih
Proof state after:
no goals
Theorem: Nat.lt_add
Proof state before:
case zero
V : Type ?u.7600
inst✝ : SetTheory V
n : Nat
⊢ n < n + (zero + 1)
Tactic:
rw [Nat.lt_succ]
Proof state after:
case zero
V : Type ?u.7600
inst✝ : SetTheory V
n : Nat
⊢ n ≤ n
Theorem: Nat.lt_add
Proof state before:
case zero
V : Type ?u.7600
inst✝ : SetTheory V
n : Nat
⊢ n ≤ n
Tactic:
exact Nat.le_refl n
Proof state after:
no goals
Theorem: Nat.lt_add
Proof state before:
case succ
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
ih : n < n + (m + 1)
⊢ n < n + (succ m + 1)
Tactic:
rw [← Nat.add_assoc, Nat.lt_succ]
Proof state after:
case succ
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
ih : n < n + (m + 1)
⊢ n ≤ n + succ m
Theorem: Nat.lt_add
Proof state before:
case succ
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
ih : n < n + (m + 1)
⊢ n ≤ n + succ m
Tactic:
exact Nat.le_of_lt ih
Proof state after:
no goals
Theorem: Fin.snoc_last_apply
Proof state before:
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ snoc l x (last n) = x
Tactic:
simp only [snoc]
Proof state after:
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : (last n).val < n then l { val := (last n).val, isLt := h } else x) = x
Theorem: Fin.snoc_last_apply
Proof state before:
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : (last n).val < n then l { val := (last n).val, isLt := h } else x) = x
Tactic:
aesop
Proof state after:
no goals
Theorem: Fin.snoc_apply
Proof state before:
V : Type ?u.8297
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ snoc l x { val := n, isLt := (_ : n < Nat.succ n) } = x
Tactic:
simp only [snoc]
Proof state after:
V : Type ?u.8297
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : n < n then l { val := n, isLt := (_ : { val := n, isLt := (_ : n < Nat.succ n) }.val < n) } else x) = x
Theorem: Fin.snoc_apply
Proof state before:
V : Type ?u.8297
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : n < n then l { val := n, isLt := (_ : { val := n, isLt := (_ : n < Nat.succ n) }.val < n) } else x) = x
Tactic:
aesop
Proof state after:
no goals
Theorem: Fin.snoc_two_apply
Proof state before:
V : Type ?u.8870
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y : α
⊢ snoc (snoc l x) y { val := n, isLt := (_ : n < n + (1 + 1)) } = x
Tactic:
simp only [snoc]
Proof state after:
V : Type ?u.8870
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y : α
⊢ (if h : n < n + 1 then
      if h_1 : n < n then
        l
          { val := n,
            isLt := (_ : { val := n, isLt := (_ : { val := n, isLt := (_ : n < n + (1 + 1)) }.val < n + 1) }.val < n) }
      else x
    else y) =
    x
Theorem: Fin.snoc_two_apply
Proof state before:
V : Type ?u.8870
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x y : α
⊢ (if h : n < n + 1 then
      if h_1 : n < n then
        l
          { val := n,
            isLt := (_ : { val := n, isLt := (_ : { val := n, isLt := (_ : n < n + (1 + 1)) }.val < n + 1) }.val < n) }
      else x
    else y) =
    x
Tactic:
aesop
Proof state after:
no goals
Theorem: Fin.snoc_three_apply
Proof 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]
Proof 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
Theorem: Fin.snoc_three_apply
Proof 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 _
Proof 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
Theorem: Fin.snoc_three_apply
Proof 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
Proof state after:
no goals
Theorem: Fin.snoc_four_apply
Proof 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]
Proof 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
Theorem: Fin.snoc_four_apply
Proof 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 _
Proof 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
Theorem: Fin.snoc_four_apply
Proof 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 _
Proof 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
Theorem: Fin.snoc_four_apply
Proof 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
Proof state after:
no goals