Theorem: Fin.list_length_le_of_nodup (Fifteen/Data/Fin/Basic.lean)

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
State after:
no goals

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 ‹_›
State after:
case zero
m n : Nat
l : List (Fin Nat.zero)
nodup : List.Nodup l
this : l = []
⊢ List.length l ≤ Nat.zero

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
State after:
case zero.refl
m n : Nat
nodup : List.Nodup []
⊢ List.length [] ≤ Nat.zero

State before:
case zero.refl
m n : Nat
nodup : List.Nodup []
⊢ List.length [] ≤ Nat.zero
Tactic:
exact Nat.le.refl
State after:
no goals

State before:
m n : Nat
l : List (Fin Nat.zero)
nodup : List.Nodup l
⊢ l = []
Tactic:
cases l
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✝ = []

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
State after:
case cons
m n : Nat
head✝ : Fin Nat.zero
tail✝ : List (Fin Nat.zero)
nodup : List.Nodup (head✝ :: tail✝)
⊢ head✝ :: tail✝ = []

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 ‹_›
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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]
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

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 ?_
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

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
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

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
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

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]
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

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) ?_
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'')

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'']
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'

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 _
State after:
no goals

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]
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

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
State after:
no goals

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
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

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 n)
hl' : l = List.map castSucc l'
⊢ List.length l ≤ Nat.succ n
Tactic:
cases hl'
State after:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length (List.map castSucc l') ≤ Nat.succ n

State before:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length (List.map castSucc l') ≤ Nat.succ n
Tactic:
rewrite [List.length_map]
State after:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length l' ≤ Nat.succ n

State before:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length l' ≤ Nat.succ n
Tactic:
refine trans (IH ?_) (n.le_succ)
State after:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.Nodup l'

State before:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.Nodup l'
Tactic:
exact List.nodup_of_nodup_map nodup
State after:
no goals