internlm/Lean-Github huggingface dataset:
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (a : Fin (n + 1)), a ∈ l → ↑a < n
Tactic:
intro i hi
Proof state after:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
⊢ ↑i < n
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_1
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
⊢ ↑i < n
Tactic:
cases Nat.eq_or_lt_of_le i.2 with
| inl heq => cases i; cases heq; exact absurd hi h
| inr hlt => exact Nat.lt_of_succ_lt_succ hlt
Proof state after:
no goals
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_1.inl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
heq : Nat.succ ↑i = n + 1
⊢ ↑i < n
Tactic:
cases i
Proof state after:
case refine_1.inl.mk
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
val✝ : Nat
isLt✝ : val✝ < n + 1
hi : { val := val✝, isLt := isLt✝ } ∈ l
heq : Nat.succ ↑{ val := val✝, isLt := isLt✝ } = n + 1
⊢ ↑{ val := val✝, isLt := isLt✝ } < n
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_1.inl.mk
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
val✝ : Nat
isLt✝ : val✝ < n + 1
hi : { val := val✝, isLt := isLt✝ } ∈ l
heq : Nat.succ ↑{ val := val✝, isLt := isLt✝ } = n + 1
⊢ ↑{ val := val✝, isLt := isLt✝ } < n
Tactic:
cases heq
Proof state after:
case refine_1.inl.mk.refl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
isLt✝ : n < n + 1
hi : { val := n, isLt := isLt✝ } ∈ l
⊢ ↑{ val := n, isLt := isLt✝ } < n
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_1.inl.mk.refl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
isLt✝ : n < n + 1
hi : { val := n, isLt := isLt✝ } ∈ l
⊢ ↑{ val := n, isLt := isLt✝ } < n
Tactic:
exact absurd hi h
Proof state after:
no goals
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_1.inr
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Fin (n + 1)
hi : i ∈ l
hlt : Nat.succ ↑i < n + 1
⊢ ↑i < n
Tactic:
exact Nat.lt_of_succ_lt_succ hlt
Proof state after:
no goals
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ l = List.map castSucc (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))
Tactic:
apply List.ext_get
Proof state after:
case refine_2.hl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ List.length l =
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))

case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2.hl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ List.length l =
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))

case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Tactic:
. rw [List.length_map, List.length_pmap]
Proof state after:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Tactic:
. intro i hi _
  rewrite [List.get_map, List.get_pmap]
  rfl
Proof state after:
no goals
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2.hl
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ List.length l =
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
Tactic:
rw [List.length_map, List.length_pmap]
Proof state after:
no goals
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
⊢ ∀ (n_1 : Nat) (h₁ : n_1 < List.length l)
    (h₂ :
      n_1 <
        List.length
          (List.map castSucc
            (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))),
    List.get l { val := n_1, isLt := h₁ } =
      List.get
        (List.map castSucc
          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
        { val := n_1, isLt := h₂ }
Tactic:
intro i hi _
Proof state after:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    List.get
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
      { val := i, isLt := h₂✝ }
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    List.get
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
      { val := i, isLt := h₂✝ }
Tactic:
rewrite [List.get_map, List.get_pmap]
Proof state after:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    castSucc
      {
        val :=
          ↑(List.get l
              (cast
                (_ :
                  List.length
                      (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                    List.length l)
                { val := ↑{ val := i, isLt := h₂✝ },
                  isLt :=
                    (_ :
                      ↑{ val := i, isLt := h₂✝ } <
                        List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })),
        isLt :=
          (_ :
            ↑(List.get l
                  (cast
                    (_ :
                      List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                        List.length l)
                    { val := ↑{ val := i, isLt := h₂✝ },
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := h₂✝ } <
                            List.length
                              (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                                (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })) <
              n) }
Theorem: Fin.restrict_of_not_mem_last
Proof state before:
case refine_2.h
m n : Nat
l : List (Fin (n + 1))
h : ¬last n ∈ l
i : Nat
hi : i < List.length l
h₂✝ :
  i <
    List.length
      (List.map castSucc
        (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)))
⊢ List.get l { val := i, isLt := hi } =
    castSucc
      {
        val :=
          ↑(List.get l
              (cast
                (_ :
                  List.length
                      (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                    List.length l)
                { val := ↑{ val := i, isLt := h₂✝ },
                  isLt :=
                    (_ :
                      ↑{ val := i, isLt := h₂✝ } <
                        List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })),
        isLt :=
          (_ :
            ↑(List.get l
                  (cast
                    (_ :
                      List.length
                          (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                            (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n)) =
                        List.length l)
                    { val := ↑{ val := i, isLt := h₂✝ },
                      isLt :=
                        (_ :
                          ↑{ val := i, isLt := h₂✝ } <
                            List.length
                              (List.pmap (fun i hi => { val := ↑i, isLt := hi }) l
                                (_ : ∀ (i : Fin (n + 1)), i ∈ l → ↑i < n))) })) <
              n) }
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n : Nat
l : List (Fin n)
nodup : List.Nodup l
⊢ List.length l ≤ n
Tactic:
induction n with
| zero =>
  have : l = [] := by cases l; rfl; exact Fin.elim0 ‹_›
  cases this; exact Nat.le.refl
| succ n IH =>
  if hn : Fin.last n ∈ l then
    let l' := l.erase <| Fin.last n
    have : l'.length = l.length.pred := List.length_erase_of_mem hn
    have : l.length = l'.length + 1 := Eq.symm <| by
      rewrite [this]
      exact Nat.succ_pred_eq_of_pos <| List.length_pos_of_mem hn
    rewrite [this]; refine Nat.succ_le_succ ?_
    have : last n ∉ l' := List.not_mem_erase_of_nodup _ nodup
    let ⟨l'',hl''⟩ := restrict_of_not_mem_last this
    rewrite [hl'', List.length_map]
    refine IH <| List.nodup_of_nodup_map (f:=castSucc) ?_
    rewrite [← hl'']
    exact nodup.erase _
  else
    let ⟨l',hl'⟩ := restrict_of_not_mem_last hn
    cases hl'; rewrite [List.length_map]
    refine trans (IH ?_) (n.le_succ)
    exact List.nodup_of_nodup_map nodup
Proof state after:
no goals
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case zero
m n : Nat
l : List (Fin Nat.zero)
nodup : List.Nodup l
⊢ List.length l ≤ Nat.zero
Tactic:
have : l = [] := by cases l; rfl; exact Fin.elim0 ‹_›
Proof state after:
case zero
m n : Nat
l : List (Fin Nat.zero)
nodup : List.Nodup l
this : l = []
⊢ List.length l ≤ Nat.zero
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case zero
m n : Nat
l : List (Fin Nat.zero)
nodup : List.Nodup l
this : l = []
⊢ List.length l ≤ Nat.zero
Tactic:
cases this
Proof state after:
case zero.refl
m n : Nat
nodup : List.Nodup []
⊢ List.length [] ≤ Nat.zero
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case zero.refl
m n : Nat
nodup : List.Nodup []
⊢ List.length [] ≤ Nat.zero
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n : Nat
l : List (Fin Nat.zero)
nodup : List.Nodup l
⊢ l = []
Tactic:
cases l
Proof state after:
case nil
m n : Nat
nodup : List.Nodup []
⊢ [] = []

case cons
m n : Nat
head✝ : Fin Nat.zero
tail✝ : List (Fin Nat.zero)
nodup : List.Nodup (head✝ :: tail✝)
⊢ head✝ :: tail✝ = []
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case nil
m n : Nat
nodup : List.Nodup []
⊢ [] = []

case cons
m n : Nat
head✝ : Fin Nat.zero
tail✝ : List (Fin Nat.zero)
nodup : List.Nodup (head✝ :: tail✝)
⊢ head✝ :: tail✝ = []
Tactic:
rfl
Proof state after:
case cons
m n : Nat
head✝ : Fin Nat.zero
tail✝ : List (Fin Nat.zero)
nodup : List.Nodup (head✝ :: tail✝)
⊢ head✝ :: tail✝ = []
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case cons
m n : Nat
head✝ : Fin Nat.zero
tail✝ : List (Fin Nat.zero)
nodup : List.Nodup (head✝ :: tail✝)
⊢ head✝ :: tail✝ = []
Tactic:
exact Fin.elim0 ‹_›
Proof state after:
no goals
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case succ
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
⊢ List.length l ≤ Nat.succ n
Tactic:
if hn : Fin.last n ∈ l then
  let l' := l.erase <| Fin.last n
  have : l'.length = l.length.pred := List.length_erase_of_mem hn
  have : l.length = l'.length + 1 := Eq.symm <| by
    rewrite [this]
    exact Nat.succ_pred_eq_of_pos <| List.length_pos_of_mem hn
  rewrite [this]; refine Nat.succ_le_succ ?_
  have : last n ∉ l' := List.not_mem_erase_of_nodup _ nodup
  let ⟨l'',hl''⟩ := restrict_of_not_mem_last this
  rewrite [hl'', List.length_map]
  refine IH <| List.nodup_of_nodup_map (f:=castSucc) ?_
  rewrite [← hl'']
  exact nodup.erase _
else
  let ⟨l',hl'⟩ := restrict_of_not_mem_last hn
  cases hl'; rewrite [List.length_map]
  refine trans (IH ?_) (n.le_succ)
  exact List.nodup_of_nodup_map nodup
Proof state after:
no goals
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
⊢ List.length l ≤ Nat.succ n
Tactic:
let l' := l.erase <| Fin.last n
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
⊢ List.length l ≤ Nat.succ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
⊢ List.length l ≤ Nat.succ n
Tactic:
have : l'.length = l.length.pred := List.length_erase_of_mem hn
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this : List.length l' = Nat.pred (List.length l)
⊢ List.length l ≤ Nat.succ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this : List.length l' = Nat.pred (List.length l)
⊢ List.length l ≤ Nat.succ n
Tactic:
have : l.length = l'.length + 1 := Eq.symm <| by
  rewrite [this]
  exact Nat.succ_pred_eq_of_pos <| List.length_pos_of_mem hn
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝ : List.length l' = Nat.pred (List.length l)
this : List.length l = List.length l' + 1
⊢ List.length l ≤ Nat.succ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝ : List.length l' = Nat.pred (List.length l)
this : List.length l = List.length l' + 1
⊢ List.length l ≤ Nat.succ n
Tactic:
rewrite [this]
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝ : List.length l' = Nat.pred (List.length l)
this : List.length l = List.length l' + 1
⊢ List.length l' + 1 ≤ Nat.succ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝ : List.length l' = Nat.pred (List.length l)
this : List.length l = List.length l' + 1
⊢ List.length l' + 1 ≤ Nat.succ n
Tactic:
refine Nat.succ_le_succ ?_
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝ : List.length l' = Nat.pred (List.length l)
this : List.length l = List.length l' + 1
⊢ List.length l' ≤ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝ : List.length l' = Nat.pred (List.length l)
this : List.length l = List.length l' + 1
⊢ List.length l' ≤ n
Tactic:
have : last n ∉ l' := List.not_mem_erase_of_nodup _ nodup
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
⊢ List.length l' ≤ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
⊢ List.length l' ≤ n
Tactic:
let ⟨l'',hl''⟩ := restrict_of_not_mem_last this
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.length l' ≤ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.length l' ≤ n
Tactic:
rewrite [hl'', List.length_map]
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.length l'' ≤ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.length l'' ≤ n
Tactic:
refine IH <| List.nodup_of_nodup_map (f:=castSucc) ?_
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.Nodup (List.map castSucc l'')
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.Nodup (List.map castSucc l'')
Tactic:
rewrite [← hl'']
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.Nodup l'
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this✝¹ : List.length l' = Nat.pred (List.length l)
this✝ : List.length l = List.length l' + 1
this : ¬last n ∈ l'
l'' : List (Fin n)
hl'' : l' = List.map castSucc l''
⊢ List.Nodup l'
Tactic:
exact nodup.erase _
Proof state after:
no goals
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this : List.length l' = Nat.pred (List.length l)
⊢ List.length l' + 1 = List.length l
Tactic:
rewrite [this]
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this : List.length l' = Nat.pred (List.length l)
⊢ Nat.pred (List.length l) + 1 = List.length l
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : last n ∈ l
l' : List (Fin (Nat.succ n)) := List.erase l (last n)
this : List.length l' = Nat.pred (List.length l)
⊢ Nat.pred (List.length l) + 1 = List.length l
Tactic:
exact Nat.succ_pred_eq_of_pos <| List.length_pos_of_mem hn
Proof state after:
no goals
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : ¬last n ∈ l
⊢ List.length l ≤ Nat.succ n
Tactic:
let ⟨l',hl'⟩ := restrict_of_not_mem_last hn
Proof state after:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : ¬last n ∈ l
l' : List (Fin n)
hl' : l = List.map castSucc l'
⊢ List.length l ≤ Nat.succ n