internlm/Lean-Github huggingface dataset:
Theorem: type_correct
Proof state before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type ctx t₁ with
    | some (Ty.arrow ty₁ ty₂) =>
      match type ctx t₂, fun __do_lift => if ty₁ = __do_lift then some ty₂ else none with
      | none, x => none
      | some a, b => b a
    | x => none) =
    some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
cases h₁ : type ctx t₁ <;> cases h₂ : type ctx t₂ <;> simp_all [h₁, h₂]
Proof state after:
case some.none
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝ : Ty
h :
  (match some val✝ with
    | some (Ty.arrow ty₁ ty₂) => none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝
h₂ : type ctx t₂ = none
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

case some.some
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h :
  (match some val✝¹ with
    | some (Ty.arrow ty₁ ty₂) => if ty₁ = val✝ then some ty₂ else none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Theorem: type_correct
Proof state before:
case some.none
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝ : Ty
h :
  (match some val✝ with
    | some (Ty.arrow ty₁ ty₂) => none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝
h₂ : type ctx t₂ = none
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

case some.some
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h :
  (match some val✝¹ with
    | some (Ty.arrow ty₁ ty₂) => if ty₁ = val✝ then some ty₂ else none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
all_goals split at h <;> try contradiction
Proof state after:
case some.some.h_1
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝ : Option Ty
ty₁✝ ty₂✝ : Ty
heq✝ : some val✝¹ = some (Ty.arrow ty₁✝ ty₂✝)
h : (if ty₁✝ = val✝ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Theorem: type_correct
Proof state before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
case _ ty₁ ty₂ _ ty₁₁ _ ha =>
  specialize hi₁ h₁
  split at h <;> simp_all
  exact .app hi₁ (hi₂ h₂)
Proof state after:
no goals
Theorem: type_correct
Proof state before:
case some.some
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h :
  (match some val✝¹ with
    | some (Ty.arrow ty₁ ty₂) => if ty₁ = val✝ then some ty₂ else none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
split at h <;> try contradiction
Proof state after:
case some.some.h_1
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝ : Option Ty
ty₁✝ ty₂✝ : Ty
heq✝ : some val✝¹ = some (Ty.arrow ty₁✝ ty₂✝)
h : (if ty₁✝ = val✝ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Theorem: type_correct
Proof state before:
case some.some.h_2
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝¹ : Option Ty
x✝ : ∀ (ty₁ ty₂ : Ty), some val✝¹ = some (Ty.arrow ty₁ ty₂) → False
h : none = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
contradiction
Proof state after:
no goals
Theorem: type_correct
Proof state before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
specialize hi₁ h₁
Proof state after:
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
hi₁ : ctx ⊢ t₁ ⋮ ty₁
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Theorem: type_correct
Proof state before:
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₁ : type ctx t₁ = some ty₁
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
ha : some ty₁ = some (Ty.arrow ty₁₁ ty₂✝)
h : (if ty₁₁ = ty₂ then some ty₂✝ else none) = some ty
hi₁ : ctx ⊢ t₁ ⋮ ty₁
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
split at h <;> simp_all
Proof state after:
case inl
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
hi₁ : ctx ⊢ t₁ ⋮ Ty.arrow ty₂ ty
h✝ : ty₁₁ = ty₂
h : ty₂✝ = ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Theorem: type_correct
Proof state before:
case inl
t₁ t₂ : Term
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty ty₁ ty₂ : Ty
h₂ : type ctx t₂ = some ty₂
x✝ : Option Ty
ty₁₁ ty₂✝ : Ty
hi₁ : ctx ⊢ t₁ ⋮ Ty.arrow ty₂ ty
h✝ : ty₁₁ = ty₂
h : ty₂✝ = ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
exact .app hi₁ (hi₂ h₂)
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty : Ty
h : ctx ⊢ t ⋮ ty
⊢ type ctx t = some ty
Tactic:
induction h <;> simp [type]
Proof state after:
case var
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ctx✝ x✝ = some ty✝

case abs
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)

case app
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
a_ih✝ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ctx✝ x✝ = some ty✝
Tactic:
case var         => assumption
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
Tactic:
case abs hi      => rw [hi]; rfl
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝
Tactic:
case app hi₁ hi₂ => simp [hi₁, hi₂]; exact if_pos rfl
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ctx✝ x✝ = some ty✝
Tactic:
assumption
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
Tactic:
rw [hi]
Proof state after:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← some ty₂✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← some ty₂✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝
Tactic:
simp [hi₁, hi₂]
Proof state after:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (do
      let __do_lift ← some ty₁✝
      if ty₁✝ = __do_lift then some ty₂✝ else none) =
    some ty₂✝
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (do
      let __do_lift ← some ty₁✝
      if ty₁✝ = __do_lift then some ty₂✝ else none) =
    some ty₂✝
Tactic:
exact if_pos rfl
Proof state after:
no goals
Theorem: Material.toFrom
Proof state before:
m : Material
⊢ m = fromIndex (index m)
Tactic:
cases m <;> simp [index, fromIndex]
Proof state after:
no goals
Theorem: Material.fromTo
Proof state before:
i : Fin 4
⊢ i = index (fromIndex i)
Tactic:
match i with 
| 0 => simp
| 1 => simp
| 2 => simp
| 3 => simp
Proof state after:
no goals
Theorem: Material.fromTo
Proof state before:
i : Fin 4
⊢ 0 = index (fromIndex 0)
Tactic:
simp
Proof state after:
no goals
Theorem: Material.fromTo
Proof state before:
i : Fin 4
⊢ 1 = index (fromIndex 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Material.fromTo
Proof state before:
i : Fin 4
⊢ 2 = index (fromIndex 2)
Tactic:
simp
Proof state after:
no goals
Theorem: Material.fromTo
Proof state before:
i : Fin 4
⊢ 3 = index (fromIndex 3)
Tactic:
simp
Proof state after:
no goals
Theorem: Array.modify_stable_size
Proof state before:
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr = size (modify arr n f)
Tactic:
simp [modify, modifyM, dite]
Proof state after:
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr =
    size
      (Id.run
        (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) (Nat.decLt n (size arr))))
Theorem: Array.modify_stable_size
Proof state before:
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr =
    size
      (Id.run
        (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) (Nat.decLt n (size arr))))
Tactic:
generalize Nat.decLt n (size arr) = q
Proof state after:
α : Type u_1
arr : Array α
f : α → α
n : Nat
q : Decidable (n < size arr)
⊢ size arr = size (Id.run (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) q))
Theorem: Array.modify_stable_size
Proof state before:
α : Type u_1
arr : Array α
f : α → α
n : Nat
q : Decidable (n < size arr)
⊢ size arr = size (Id.run (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) q))
Tactic:
cases q <;> simp [Id.run]
Proof state after:
no goals
Theorem: Array.ZipWithN.zipWithNSizeGo
Proof state before:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
⊢ size (go as bs f p arr i) = size as
Tactic:
unfold go
Proof state after:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
⊢ size
      (if q : i < size as then
        let a := as[i];
        let b := bs[i];
        go as bs f p (push arr (f a b)) (i + 1)
      else arr) =
    size as
Theorem: Array.ZipWithN.zipWithNSizeGo
Proof state before:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
⊢ size
      (if q : i < size as then
        let a := as[i];
        let b := bs[i];
        go as bs f p (push arr (f a b)) (i + 1)
      else arr) =
    size as
Tactic:
split
Proof state after:
case inl
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : i < size as
⊢ size
      (let a := as[i];
      let b := bs[i];
      go as bs f p (push arr (f a b)) (i + 1)) =
    size as

case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
Theorem: Array.ZipWithN.zipWithNSizeGo
Proof state before:
case inl
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : i < size as
⊢ size
      (let a := as[i];
      let b := bs[i];
      go as bs f p (push arr (f a b)) (i + 1)) =
    size as

case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
Tactic:
. apply zipWithNSizeGo
  . apply Nat.succ_le_of_lt
    assumption
  . rw [Array.size_push]
    simp
    assumption
Proof state after:
case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
Theorem: Array.ZipWithN.zipWithNSizeGo
Proof state before:
case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
Tactic:
. rw [<-ap] 
  apply Nat.le_antisymm
  . assumption
  . apply Nat.le_of_not_lt
    assumption
Proof state after:
no goals
Theorem: Array.ZipWithN.zipWithNSize
Proof state before:
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ size (zipWithN as bs f p) = size as
Tactic:
apply zipWithNSizeGo
Proof state after:
case ip
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 ≤ size as

case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]
Theorem: Array.ZipWithN.zipWithNSize
Proof state before:
case ip
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 ≤ size as

case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]
Tactic:
. apply Nat.zero_le
Proof state after:
case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]
Theorem: Array.ZipWithN.zipWithNSize
Proof state before:
case ap
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
⊢ 0 = size #[]
Tactic:
. simp [Array.size, List.length]
Proof state after:
no goals
Theorem: Packet.multNotSingle
Proof state before:
xs : List Packet
⊢ ¬IsSingle (Multiple xs)
Tactic:
intros ex
Proof state after:
xs : List Packet
ex : IsSingle (Multiple xs)
⊢ False
Theorem: Packet.multNotSingle
Proof state before:
xs : List Packet
ex : IsSingle (Multiple xs)
⊢ False
Tactic:
cases ex
Proof state after:
case intro
xs : List Packet
w✝ : Nat
h✝ : Multiple xs = Single w✝
⊢ False
Theorem: Packet.multNotSingle
Proof state before:
case intro
xs : List Packet
w✝ : Nat
h✝ : Multiple xs = Single w✝
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Packet.children_mult_levels
Proof state before:
x : Packet
ys : List Packet
⊢ levels (children x) + levels ys < level x + level (Multiple ys)
Tactic:
cases x <;> simp [children, levels, level]
Proof state after:
case Single
ys : List Packet
a✝ : Nat
⊢ 1 + levels ys < levels ys + 2

case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)
Theorem: Packet.children_mult_levels
Proof state before:
case Single
ys : List Packet
a✝ : Nat
⊢ 1 + levels ys < levels ys + 2

case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)
Tactic:
. case Single x => 
  rw [Nat.add_comm]
  apply Nat.lt_succ_self
Proof state after:
case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)
Theorem: Packet.children_mult_levels
Proof state before:
case Multiple
ys a✝ : List Packet
⊢ levels a✝ + levels ys < levels a✝ + 2 + (levels ys + 2)
Tactic:
. case Multiple xs => 
  conv => 
    rhs
    rw [Nat.add_assoc]
    conv => 
      rhs
      rw [← Nat.add_assoc]
      conv => 
        lhs
        rw [Nat.add_comm]  
      rw [Nat.add_assoc]
      simp [Nat.add]
    rw [←Nat.add_assoc]
  apply @Nat.add_lt_add_left 0
  apply Nat.zero_lt_succ
Proof state after:
no goals
Theorem: Packet.children_mult_levels
Proof state before:
ys : List Packet
x : Nat
⊢ 1 + levels ys < levels ys + 2
Tactic:
rw [Nat.add_comm]
Proof state after:
ys : List Packet
x : Nat
⊢ levels ys + 1 < levels ys + 2
Theorem: Packet.children_mult_levels
Proof state before:
ys : List Packet
x : Nat
⊢ levels ys + 1 < levels ys + 2
Tactic:
apply Nat.lt_succ_self
Proof state after:
no goals
Theorem: Packet.children_mult_levels
Proof state before:
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + 2 + (levels ys + 2)
Tactic:
conv => 
  rhs
  rw [Nat.add_assoc]
  conv => 
    rhs
    rw [← Nat.add_assoc]
    conv => 
      lhs
      rw [Nat.add_comm]  
    rw [Nat.add_assoc]
    simp [Nat.add]
  rw [←Nat.add_assoc]
Proof state after:
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + levels ys + (2 + 2)
Theorem: Packet.children_mult_levels
Proof state before:
ys xs : List Packet
⊢ levels xs + levels ys < levels xs + levels ys + (2 + 2)
Tactic:
apply @Nat.add_lt_add_left 0
Proof state after:
case h
ys xs : List Packet
⊢ 0 < 2 + 2
Theorem: Packet.children_mult_levels
Proof state before:
case h
ys xs : List Packet
⊢ 0 < 2 + 2
Tactic:
apply Nat.zero_lt_succ
Proof state after:
no goals
Theorem: Packet.children_levels
Proof state before:
x y : Packet
p : ¬(IsSingle x ∧ IsSingle y)
⊢ levels (children x) + levels (children y) < level x + level y
Tactic:
cases x
Proof state after:
case Single
y : Packet
a✝ : Nat
p : ¬(IsSingle (Single a✝) ∧ IsSingle y)
⊢ levels (children (Single a✝)) + levels (children y) < level (Single a✝) + level y

case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y
Theorem: Packet.children_levels
Proof state before:
case Single
y : Packet
a✝ : Nat
p : ¬(IsSingle (Single a✝) ∧ IsSingle y)
⊢ levels (children (Single a✝)) + levels (children y) < level (Single a✝) + level y

case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y
Tactic:
. case Single x =>
  cases y
  . case Single y =>
    apply False.elim
    apply p
    constructor
    . exists x
    . exists y
  . case Multiple ys => 
    apply children_mult_levels
Proof state after:
case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y
Theorem: Packet.children_levels
Proof state before:
case Multiple
y : Packet
a✝ : List Packet
p : ¬(IsSingle (Multiple a✝) ∧ IsSingle y)
⊢ levels (children (Multiple a✝)) + levels (children y) < level (Multiple a✝) + level y
Tactic:
. case Multiple xs =>
    conv => 
      lhs
      rw [Nat.add_comm] 
    conv => 
      rhs
      rw [Nat.add_comm] 
    apply children_mult_levels
Proof state after:
no goals
Theorem: Packet.children_levels
Proof state before:
y : Packet
x : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle y)
⊢ levels (children (Single x)) + levels (children y) < level (Single x) + level y
Tactic:
cases y
Proof state after:
case Single
x a✝ : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single a✝))
⊢ levels (children (Single x)) + levels (children (Single a✝)) < level (Single x) + level (Single a✝)

case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)
Theorem: Packet.children_levels
Proof state before:
case Single
x a✝ : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single a✝))
⊢ levels (children (Single x)) + levels (children (Single a✝)) < level (Single x) + level (Single a✝)

case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)
Tactic:
. case Single y =>
  apply False.elim
  apply p
  constructor
  . exists x
  . exists y
Proof state after:
case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)
Theorem: Packet.children_levels
Proof state before:
case Multiple
x : Nat
a✝ : List Packet
p : ¬(IsSingle (Single x) ∧ IsSingle (Multiple a✝))
⊢ levels (children (Single x)) + levels (children (Multiple a✝)) < level (Single x) + level (Multiple a✝)
Tactic:
. case Multiple ys => 
  apply children_mult_levels
Proof state after:
no goals
Theorem: Packet.children_levels
Proof state before:
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ levels (children (Single x)) + levels (children (Single y)) < level (Single x) + level (Single y)
Tactic:
apply False.elim
Proof state after:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ False
Theorem: Packet.children_levels
Proof state before:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ False
Tactic:
apply p
Proof state after:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x) ∧ IsSingle (Single y)
Theorem: Packet.children_levels
Proof state before:
case h
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x) ∧ IsSingle (Single y)
Tactic:
constructor
Proof state after:
case h.left
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x)

case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)