internlm/Lean-Github huggingface dataset:
Theorem: List.length_fins
Proof state before:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
Tactic:
intro i hi acc
Proof state after:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n i hi acc) = length acc + i
Theorem: List.length_fins
Proof state before:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n i hi acc) = length acc + i
Tactic:
induction i generalizing acc <;>
  (unfold fins.finsAux; simp_all [Nat.succ_add, Nat.add_succ])
Proof state after:
no goals
Theorem: List.length_fins
Proof state before:
n : Nat
this : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
have := this n (Nat.le_refl _) []
Proof state after:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = length [] + n
⊢ length (fins.finsAux n n ⋯ []) = n
Theorem: List.length_fins
Proof state before:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = length [] + n
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
simp at this
Proof state after:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = n
⊢ length (fins.finsAux n n ⋯ []) = n
Theorem: List.length_fins
Proof state before:
n : Nat
this✝ : ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)), length (fins.finsAux n i hi acc) = length acc + i
this : length (fins.finsAux n n ⋯ []) = n
⊢ length (fins.finsAux n n ⋯ []) = n
Tactic:
exact this
Proof state after:
no goals
Theorem: List.length_fins
Proof state before:
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n (Nat.succ n✝) hi acc) = length acc + Nat.succ n✝
Tactic:
unfold fins.finsAux
Proof state after:
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n n✝ ⋯ ({ val := n✝, isLt := hi } :: acc)) = length acc + Nat.succ n✝
Theorem: List.length_fins
Proof state before:
case succ
n n✝ : Nat
n_ih✝ : ∀ (hi : n✝ ≤ n) (acc : List (Fin n)), length (fins.finsAux n n✝ hi acc) = length acc + n✝
hi : Nat.succ n✝ ≤ n
acc : List (Fin n)
⊢ length (fins.finsAux n n✝ ⋯ ({ val := n✝, isLt := hi } :: acc)) = length acc + Nat.succ n✝
Tactic:
simp_all [Nat.succ_add, Nat.add_succ]
Proof state after:
no goals
Theorem: List.fins_succ
Proof state before:
n : Nat
⊢ fins (Nat.succ n) = map Fin.castSucc (fins n) ++ [Fin.last n]
Tactic:
unfold fins
Proof state after:
n : Nat
⊢ fins.finsAux (Nat.succ n) (Nat.succ n) ⋯ [] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
n : Nat
⊢ fins.finsAux (Nat.succ n) (Nat.succ n) ⋯ [] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
conv => lhs; unfold fins.finsAux
Proof state after:
n : Nat
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
n : Nat
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
suffices ∀ i (hi : i ≤ n) acc,
    fins.finsAux n.succ i (trans hi (Nat.le_succ _)) (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
  by have := this n (Nat.le_refl _) []; simpa using this
Proof state after:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
n : Nat
⊢ ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
Tactic:
intro i hi acc
Proof state after:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
n i : Nat
hi : i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
Tactic:
induction i generalizing acc with
| zero => unfold fins.finsAux; simp
| succ i ih =>
  unfold fins.finsAux
  replace ih := ih (Nat.le_of_lt hi) (⟨i,hi⟩ :: acc)
  simpa using ih
Proof state after:
no goals
Theorem: List.fins_succ
Proof state before:
n : Nat
this :
  ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
have := this n (Nat.le_refl _) []
Proof state after:
n : Nat
this✝ :
  ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
this :
  fins.finsAux (Nat.succ n) n ⋯ (map Fin.castSucc [] ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
n : Nat
this✝ :
  ∀ (i : Nat) (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
this :
  fins.finsAux (Nat.succ n) n ⋯ (map Fin.castSucc [] ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) n ⋯ [{ val := n, isLt := ⋯ }] = map Fin.castSucc (fins.finsAux n n ⋯ []) ++ [Fin.last n]
Tactic:
simpa using this
Proof state after:
no goals
Theorem: List.fins_succ
Proof state before:
case zero
n : Nat
hi : Nat.zero ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) Nat.zero ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n Nat.zero hi acc) ++ [Fin.last n]
Tactic:
unfold fins.finsAux
Proof state after:
case zero
n : Nat
hi : Nat.zero ≤ n
acc : List (Fin n)
⊢ map Fin.castSucc acc ++ [Fin.last n] = map Fin.castSucc acc ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
case zero
n : Nat
hi : Nat.zero ≤ n
acc : List (Fin n)
⊢ map Fin.castSucc acc ++ [Fin.last n] = map Fin.castSucc acc ++ [Fin.last n]
Tactic:
simp
Proof state after:
no goals
Theorem: List.fins_succ
Proof state before:
case succ
n i : Nat
ih :
  ∀ (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) (Nat.succ i) ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n (Nat.succ i) hi acc) ++ [Fin.last n]
Tactic:
unfold fins.finsAux
Proof state after:
case succ
n i : Nat
ih :
  ∀ (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
case succ
n i : Nat
ih :
  ∀ (hi : i ≤ n) (acc : List (Fin n)),
    fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc acc ++ [Fin.last n]) =
      map Fin.castSucc (fins.finsAux n i hi acc) ++ [Fin.last n]
hi : Nat.succ i ≤ n
acc : List (Fin n)
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
Tactic:
replace ih := ih (Nat.le_of_lt hi) (⟨i,hi⟩ :: acc)
Proof state after:
case succ
n i : Nat
hi : Nat.succ i ≤ n
acc : List (Fin n)
ih :
  fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc ({ val := i, isLt := hi } :: acc) ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
Theorem: List.fins_succ
Proof state before:
case succ
n i : Nat
hi : Nat.succ i ≤ n
acc : List (Fin n)
ih :
  fins.finsAux (Nat.succ n) i ⋯ (map Fin.castSucc ({ val := i, isLt := hi } :: acc) ++ [Fin.last n]) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
⊢ fins.finsAux (Nat.succ n) i ⋯ ({ val := i, isLt := ⋯ } :: (map Fin.castSucc acc ++ [Fin.last n])) =
    map Fin.castSucc (fins.finsAux n i ⋯ ({ val := i, isLt := hi } :: acc)) ++ [Fin.last n]
Tactic:
simpa using ih
Proof state after:
no goals
Theorem: List.get_fins
Proof state before:
n : Nat
i : Fin (length (fins n))
⊢ ↑i < n
Tactic:
cases i
Proof state after:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ ↑{ val := val✝, isLt := isLt✝ } < n
Theorem: List.get_fins
Proof state before:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ ↑{ val := val✝, isLt := isLt✝ } < n
Tactic:
simp
Proof state after:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ val✝ < n
Theorem: List.get_fins
Proof state before:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ val✝ < n
Tactic:
simp_all
Proof state after:
no goals
Theorem: List.get_fins
Proof state before:
n : Nat
i : Fin (length (fins n))
⊢ get (fins n) i = { val := ↑i, isLt := ⋯ }
Tactic:
rcases i with ⟨j,hj⟩
Proof state after:
case mk
n j : Nat
hj : j < length (fins n)
⊢ get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case mk
n j : Nat
hj : j < length (fins n)
⊢ get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }
Tactic:
revert hj
Proof state after:
case mk
n j : Nat
⊢ ∀ (hj : j < length (fins n)), get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case mk
n j : Nat
⊢ ∀ (hj : j < length (fins n)), get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }
Tactic:
simp
Proof state after:
case mk
n j : Nat
⊢ ∀ (hj : j < n), get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case mk
n j : Nat
⊢ ∀ (hj : j < n), get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }
Tactic:
intro hj
Proof state after:
case mk
n j : Nat
hj : j < n
⊢ get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case mk
n j : Nat
hj : j < n
⊢ get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }
Tactic:
apply Option.some_inj.mp
Proof state after:
case mk
n j : Nat
hj : j < n
⊢ some (get (fins n) { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case mk
n j : Nat
hj : j < n
⊢ some (get (fins n) { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }
Tactic:
rw [← get?_eq_get]
Proof state after:
case mk
n j : Nat
hj : j < n
⊢ get? (fins n) j = some { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case mk
n j : Nat
hj : j < n
⊢ get? (fins n) j = some { val := j, isLt := ⋯ }
Tactic:
induction n
Proof state after:
case mk.zero
j : Nat
hj : j < Nat.zero
⊢ get? (fins Nat.zero) j = some { val := j, isLt := ⋯ }

case mk.succ
j n✝ : Nat
n_ih✝ : ∀ (hj : j < n✝), get? (fins n✝) j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n✝
⊢ get? (fins (Nat.succ n✝)) j = some { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case mk.zero
j : Nat
hj : j < Nat.zero
⊢ get? (fins Nat.zero) j = some { val := j, isLt := ⋯ }
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.get_fins
Proof state before:
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (fins (Nat.succ n')) j = some { val := j, isLt := ⋯ }
Tactic:
conv => lhs; rw [fins_succ]
Proof state after:
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
by_cases h : j = n'
Proof state after:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }

case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
rw [get?_append_right]
Proof state after:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? [Fin.last n'] (j - length (map Fin.castSucc (fins n'))) = some { val := j, isLt := ⋯ }

case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ length (map Fin.castSucc (fins n')) ≤ j
Theorem: List.get_fins
Proof state before:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? [Fin.last n'] (j - length (map Fin.castSucc (fins n'))) = some { val := j, isLt := ⋯ }
Tactic:
simp [h, Fin.last]
Proof state after:
no goals
Theorem: List.get_fins
Proof state before:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ length (map Fin.castSucc (fins n')) ≤ j
Tactic:
simp [h]
Proof state after:
no goals
Theorem: List.get_fins
Proof state before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
have : j < n' := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) h
Proof state after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this : j < n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this : j < n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
have := ih this
Proof state after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Theorem: List.get_fins
Proof state before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
rw [get?_append, get?_map, this]
Proof state after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ Option.map Fin.castSucc (some { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }

case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < length (map Fin.castSucc (fins n'))
Theorem: List.get_fins
Proof state before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ Option.map Fin.castSucc (some { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }
Tactic:
simp
Proof state after:
no goals
Theorem: List.get_fins
Proof state before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < length (map Fin.castSucc (fins n'))
Tactic:
simp
Proof state after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < n'
Theorem: List.get_fins
Proof state before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < n'
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_fins
Proof state before:
n : Nat
x : Fin n
⊢ x ∈ fins n
Tactic:
rw [mem_iff_get]
Proof state after:
n : Nat
x : Fin n
⊢ ∃ n_1, get (fins n) n_1 = x
Theorem: List.mem_fins
Proof state before:
n : Nat
x : Fin n
⊢ ∃ n_1, get (fins n) n_1 = x
Tactic:
refine ⟨⟨x,?_⟩,?_⟩
Proof state after:
case refine_1
n : Nat
x : Fin n
⊢ ↑x < length (fins n)

case refine_2
n : Nat
x : Fin n
⊢ get (fins n) { val := ↑x, isLt := ?refine_1 } = x
Theorem: List.mem_fins
Proof state before:
case refine_1
n : Nat
x : Fin n
⊢ ↑x < length (fins n)
Tactic:
simp
Proof state after:
no goals
Theorem: List.mem_fins
Proof state before:
case refine_2
n : Nat
x : Fin n
⊢ get (fins n) { val := ↑x, isLt := ⋯ } = x
Tactic:
simp
Proof state after:
no goals
Theorem: List.sizeOf_filter
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
L : List α
⊢ sizeOf (filter f L) ≤ sizeOf L
Tactic:
induction L <;> simp [filter]
Proof state after:
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) ≤
    1 + sizeOf head✝ + sizeOf tail✝
Theorem: List.sizeOf_filter
Proof state before:
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) ≤
    1 + sizeOf head✝ + sizeOf tail✝
Tactic:
split
Proof state after:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (head✝ :: filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝

case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Theorem: List.sizeOf_filter
Proof state before:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (head✝ :: filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝

case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
. simp
  apply Nat.add_le_add_left
  assumption
Proof state after:
case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Theorem: List.sizeOf_filter
Proof state before:
case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
. apply Nat.le_trans ?_ (Nat.le_add_left _ _)
  assumption
Proof state after:
no goals
Theorem: List.sizeOf_filter
Proof state before:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (head✝ :: filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
simp
Proof state after:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ 1 + sizeOf head✝ + sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Theorem: List.sizeOf_filter
Proof state before:
case cons.h_1
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ 1 + sizeOf head✝ + sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
apply Nat.add_le_add_left
Proof state after:
case cons.h_1.h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝
Theorem: List.sizeOf_filter
Proof state before:
case cons.h_1.h
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = true
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝
Tactic:
assumption
Proof state after:
no goals
Theorem: List.sizeOf_filter
Proof state before:
case cons.h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ 1 + sizeOf head✝ + sizeOf tail✝
Tactic:
apply Nat.le_trans ?_ (Nat.le_add_left _ _)
Proof state after:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝
Theorem: List.sizeOf_filter
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : sizeOf (filter f tail✝) ≤ sizeOf tail✝
x✝ : Bool
heq✝ : f head✝ = false
⊢ sizeOf (filter f tail✝) ≤ sizeOf tail✝
Tactic:
assumption
Proof state after:
no goals
Theorem: List.sizeOf_filter_lt_of_ne
Proof state before:
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
L : List α
h : filter f L ≠ L
⊢ sizeOf (filter f L) < sizeOf L
Tactic:
induction L <;> simp [filter] at *
Proof state after:
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ¬filter f tail✝ = tail✝ → sizeOf (filter f tail✝) < sizeOf tail✝
h :
  ¬(match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) =
      head✝ :: tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) <
    1 + sizeOf head✝ + sizeOf tail✝