internlm/Lean-Github huggingface dataset:
Theorem: Schema.lookupType_nths_eq_lookupType
Proof state before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ lookupType (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hnths } =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName hnths }
Tactic:
simp only [Schema.nths, Schema.map, Schema.lookupType, htoprove]
Proof state after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName HasName.hd }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof state before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst, snd := hasNameOfNthsHasName HasName.hd }
Tactic:
unfold Schema.hasNameOfNthsHasName
Proof state after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd :=
          match (nth sch n (_ : Nat.succ n ≤ length sch)).fst, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                  (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                      (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := Nat.succ n, isLt := pf }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof state before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType ((snm, sτ) :: sch)
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd :=
          match (nth sch n (_ : Nat.succ n ≤ length sch)).fst, hasNameEqHeadOrTail HasName.hd, HasName.hd with
          |
          .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                  (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst),
            Sum.inl
              (EqT.refl
                .((nth ((snm, sτ) :: sch) { val := Nat.succ n, isLt := pf }.val
                      (_ : { val := Nat.succ n, isLt := pf }.val < length ((snm, sτ) :: sch))).fst)),
            h => hasNthName { val := Nat.succ n, isLt := pf }
          | hdr, Sum.inr hhnm, h => hasNameOfNthsHasName hhnm }
Tactic:
simp only [Schema.hasNameEqHeadOrTail, Schema.hasNthName, Schema.lookupType]
Proof state after:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType sch
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd := hasNthName { val := n, isLt := (_ : n < length sch) } }
Theorem: Schema.lookupType_nths_eq_lookupType
Proof state before:
case refl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
snm : η
sτ : Type u_1
sch : List Header
n : Nat
pf : Nat.succ n < length ((snm, sτ) :: sch)
ns : List (Fin (length ((snm, sτ) :: sch)))
hnths :
  HasName (nth sch n (_ : Nat.succ n ≤ length sch)).fst
    (nths ((snm, sτ) :: sch) ({ val := Nat.succ n, isLt := pf } :: ns))
h : hasNameEqHeadOrTail hnths = Sum.inl (EqT.refl (nth sch n (_ : Nat.succ n ≤ length sch)).fst)
htoprove : hnths = HasName.hd
⊢ (nth sch n (_ : Nat.succ n ≤ length sch)).snd =
    lookupType sch
      { fst := (nth sch n (_ : Nat.succ n ≤ length sch)).fst,
        snd := hasNthName { val := n, isLt := (_ : n < length sch) } }
Tactic:
apply Schema.lookup_nth
Proof state after:
no goals
Theorem: Nat.add_lt_add_of_lt
Proof state before:
⊢ ∀ (a m n : Nat), m < n → m + a < n + a
Tactic:
intros a m n h
Proof state after:
a m n : Nat
h : m < n
⊢ m + a < n + a
Theorem: Nat.add_lt_add_of_lt
Proof state before:
a m n : Nat
h : m < n
⊢ m + a < n + a
Tactic:
induction a with
| zero => exact h
| succ n' ih =>
 rw [←Nat.add_one, ←Nat.add_assoc, ←Nat.add_assoc, Nat.add_one, Nat.add_one]
 apply Nat.succ_lt_succ
 exact ih
Proof state after:
no goals
Theorem: Nat.add_lt_add_of_lt
Proof state before:
case zero
m n : Nat
h : m < n
⊢ m + zero < n + zero
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.add_lt_add_of_lt
Proof state before:
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ m + succ n' < n + succ n'
Tactic:
rw [←Nat.add_one, ←Nat.add_assoc, ←Nat.add_assoc, Nat.add_one, Nat.add_one]
Proof state after:
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ succ (m + n') < succ (n + n')
Theorem: Nat.add_lt_add_of_lt
Proof state before:
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ succ (m + n') < succ (n + n')
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case succ.a
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ m + n' < n + n'
Theorem: Nat.add_lt_add_of_lt
Proof state before:
case succ.a
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ m + n' < n + n'
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.length_filterTR_le
Proof state before:
α : Type u_1
g : α → Bool
xs : List α
⊢ ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
Tactic:
induction xs with
| nil =>
  intro rs
  simp only [filter, filterTR.loop]
  rw [List.length_reverse]
  simp only [length, Nat.zero_add]
  apply Nat.le.refl
| cons x xs ih =>
  intro rs
  simp only [filter, filterTR.loop]
  cases (g x) with
  | true => simp only
            apply Nat.le_trans (ih (x::rs))
            simp only [length]
            rw [Nat.add_comm (length rs), Nat.add_assoc]
            apply Nat.le.refl
  | false => simp only [length]
             apply Nat.le_trans (ih rs)
             rw [Nat.add_comm (length xs) 1,
                 Nat.add_assoc 1,
                 Nat.add_comm 1,
                 Nat.add_one]
             apply Nat.le.step
             apply Nat.le.refl
Proof state after:
no goals
Theorem: List.length_filterTR_le
Proof state before:
case nil
α : Type u_1
g : α → Bool
⊢ ∀ (rs : List α), length (filterTR.loop g [] rs) ≤ length [] + length rs
Tactic:
intro rs
Proof state after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (filterTR.loop g [] rs) ≤ length [] + length rs
Theorem: List.length_filterTR_le
Proof state before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (filterTR.loop g [] rs) ≤ length [] + length rs
Tactic:
simp only [filter, filterTR.loop]
Proof state after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (reverse rs) ≤ length [] + length rs
Theorem: List.length_filterTR_le
Proof state before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length (reverse rs) ≤ length [] + length rs
Tactic:
rw [List.length_reverse]
Proof state after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length [] + length rs
Theorem: List.length_filterTR_le
Proof state before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length [] + length rs
Tactic:
simp only [length, Nat.zero_add]
Proof state after:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length rs
Theorem: List.length_filterTR_le
Proof state before:
case nil
α : Type u_1
g : α → Bool
rs : List α
⊢ length rs ≤ length rs
Tactic:
apply Nat.le.refl
Proof state after:
no goals
Theorem: List.length_filterTR_le
Proof state before:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
⊢ ∀ (rs : List α), length (filterTR.loop g (x :: xs) rs) ≤ length (x :: xs) + length rs
Tactic:
intro rs
Proof state after:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length (filterTR.loop g (x :: xs) rs) ≤ length (x :: xs) + length rs
Theorem: List.length_filterTR_le
Proof state before:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length (filterTR.loop g (x :: xs) rs) ≤ length (x :: xs) + length rs
Tactic:
simp only [filter, filterTR.loop]
Proof state after:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length
      (match g x with
      | true => filterTR.loop g xs (x :: rs)
      | false => filterTR.loop g xs rs) ≤
    length (x :: xs) + length rs
Theorem: List.length_filterTR_le
Proof state before:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length
      (match g x with
      | true => filterTR.loop g xs (x :: rs)
      | false => filterTR.loop g xs rs) ≤
    length (x :: xs) + length rs
Tactic:
cases (g x) with
| true => simp only
          apply Nat.le_trans (ih (x::rs))
          simp only [length]
          rw [Nat.add_comm (length rs), Nat.add_assoc]
          apply Nat.le.refl
| false => simp only [length]
           apply Nat.le_trans (ih rs)
           rw [Nat.add_comm (length xs) 1,
               Nat.add_assoc 1,
               Nat.add_comm 1,
               Nat.add_one]
           apply Nat.le.step
           apply Nat.le.refl
Proof state after:
no goals
Theorem: List.length_filterTR_le
Proof state before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length
      (match true with
      | true => filterTR.loop g xs (x :: rs)
      | false => filterTR.loop g xs rs) ≤
    length (x :: xs) + length rs
Tactic:
simp only
Proof state after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length (filterTR.loop g xs (x :: rs)) ≤ length (x :: xs) + length rs
Theorem: List.length_filterTR_le
Proof state before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length (filterTR.loop g xs (x :: rs)) ≤ length (x :: xs) + length rs
Tactic:
apply Nat.le_trans (ih (x::rs))
Proof state after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length (x :: rs) ≤ length (x :: xs) + length rs
Theorem: List.length_filterTR_le
Proof state before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length (x :: rs) ≤ length (x :: xs) + length rs
Tactic:
simp only [length]
Proof state after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (length rs + 1) ≤ length xs + 1 + length rs
Theorem: List.length_filterTR_le
Proof state before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (length rs + 1) ≤ length xs + 1 + length rs
Tactic:
rw [Nat.add_comm (length rs), Nat.add_assoc]
Proof state after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (1 + length rs) ≤ length xs + (1 + length rs)
Theorem: List.length_filterTR_le
Proof state before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + (1 + length rs) ≤ length xs + (1 + length rs)
Tactic:
apply Nat.le.refl
Proof state after:
no goals
Theorem: List.length_filterTR_le
Proof state before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length
      (match false with
      | true => filterTR.loop g xs (x :: rs)
      | false => filterTR.loop g xs rs) ≤
    length (x :: xs) + length rs
Tactic:
simp only [length]
Proof state after:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length (filterTR.loop g xs rs) ≤ length xs + 1 + length rs
Theorem: List.length_filterTR_le
Proof state before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length (filterTR.loop g xs rs) ≤ length xs + 1 + length rs
Tactic:
apply Nat.le_trans (ih rs)
Proof state after:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length rs ≤ length xs + 1 + length rs
Theorem: List.length_filterTR_le
Proof state before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length rs ≤ length xs + 1 + length rs
Tactic:
rw [Nat.add_comm (length xs) 1,
    Nat.add_assoc 1,
    Nat.add_comm 1,
    Nat.add_one]
Proof state after:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length rs ≤ Nat.succ (length xs + length rs)
Theorem: List.length_filterTR_le
Proof state before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ length xs + length rs ≤ Nat.succ (length xs + length rs)
Tactic:
apply Nat.le.step
Proof state after:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ Nat.le (length xs + length rs) (length xs + length rs)
Theorem: List.length_filterTR_le
Proof state before:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : ∀ (rs : List α), length (filterTR.loop g xs rs) ≤ length xs + length rs
rs : List α
⊢ Nat.le (length xs + length rs) (length xs + length rs)
Tactic:
apply Nat.le.refl
Proof state after:
no goals
Theorem: List.filter_length
Proof state before:
α : Type u_1
g : α → Bool
xs : List α
⊢ length (filter g xs) ≤ length xs
Tactic:
induction xs with
| nil => simp [length]
| cons x xs ih =>
   simp only [filter]
   cases (g x) with
   | true =>
     simp only
     apply Nat.succ_le_succ
     exact ih
   | false =>
     simp only
     apply Nat.le.step
     exact ih
Proof state after:
no goals
Theorem: List.filter_length
Proof state before:
case nil
α : Type u_1
g : α → Bool
⊢ length (filter g []) ≤ length []
Tactic:
simp [length]
Proof state after:
no goals
Theorem: List.filter_length
Proof state before:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g (x :: xs)) ≤ length (x :: xs)
Tactic:
simp only [filter]
Proof state after:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match g x with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
Theorem: List.filter_length
Proof state before:
case cons
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match g x with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
Tactic:
cases (g x) with
| true =>
  simp only
  apply Nat.succ_le_succ
  exact ih
| false =>
  simp only
  apply Nat.le.step
  exact ih
Proof state after:
no goals
Theorem: List.filter_length
Proof state before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match true with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
Tactic:
simp only
Proof state after:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (x :: filter g xs) ≤ length (x :: xs)
Theorem: List.filter_length
Proof state before:
case cons.true
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (x :: filter g xs) ≤ length (x :: xs)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case cons.true.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length xs
Theorem: List.filter_length
Proof state before:
case cons.true.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.filter_length
Proof state before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length
      (match false with
      | true => x :: filter g xs
      | false => filter g xs) ≤
    length (x :: xs)
Tactic:
simp only
Proof state after:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length (x :: xs)
Theorem: List.filter_length
Proof state before:
case cons.false
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ length (filter g xs) ≤ length (x :: xs)
Tactic:
apply Nat.le.step
Proof state after:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ Nat.le (length (filter g xs)) (length xs)
Theorem: List.filter_length
Proof state before:
case cons.false.a
α : Type u_1
g : α → Bool
x : α
xs : List α
ih : length (filter g xs) ≤ length xs
⊢ Nat.le (length (filter g xs)) (length xs)
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.split_length_fst'
Proof state before:
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split (x₁ :: x₂ :: xs)).fst ≤ length (x₁ :: x₂ :: xs)
Tactic:
simp only [split, length]
Proof state after:
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst + 1 ≤ length xs + 1 + 1
Theorem: List.split_length_fst'
Proof state before:
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst + 1 ≤ length xs + 1 + 1
Tactic:
apply Nat.le.step
Proof state after:
case a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ Nat.le (length (split xs).fst + 1) (length xs + 1)
Theorem: List.split_length_fst'
Proof state before:
case a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ Nat.le (length (split xs).fst + 1) (length xs + 1)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a.a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst ≤ length xs
Theorem: List.split_length_fst'
Proof state before:
case a.a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst ≤ length xs
Tactic:
apply ih
Proof state after:
no goals
Theorem: List.split_length_fst
Proof state before:
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (x₁ :: x₂ :: x :: x' :: xs) ≤ 1 ∨
    length (split (x₁ :: x₂ :: x :: x' :: xs)).fst < length (x₁ :: x₂ :: x :: x' :: xs)
Tactic:
simp only [split, length]
Proof state after:
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length xs + 1 + 1 + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1
Theorem: List.split_length_fst
Proof state before:
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length xs + 1 + 1 + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1
Tactic:
apply Or.intro_right
Proof state after:
case h
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1
Theorem: List.split_length_fst
Proof state before:
case h
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 < length xs + 3
Theorem: List.split_length_fst
Proof state before:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 < length xs + 3
Tactic:
simp [length, Nat.add] at ih
Proof state after:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 3
Theorem: List.split_length_fst
Proof state before:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 3
Tactic:
apply Nat.lt.step
Proof state after:
case h.a.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 2