Theorem: List.Nodup.length_le_of_subset (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l l₁ : List α
nodup : Nodup l
h : l ⊆ l₁
⊢ length l ≤ length l₁
Tactic:
induction l generalizing l₁ with
| nil => exact l₁.length.zero_le
| cons a l IH =>
  have .cons nodup_head (nodup_tail : l.Nodup) := nodup
  let ⟨ha,hl⟩ := cons_subset.mp h
  clear nodup h
  have ⟨l₁', l₁'', hl₁⟩ := mem_iff_append.mp ha
  cases hl₁; clear ha
  have : l ⊆ l₁' ++ l₁'' := fun b hb => 
    match mem_append.mp (hl hb) with
    | .inl hb => mem_append.mpr <| Or.inl hb
    | .inr hb => mem_append.mpr <| Or.inr <|
      match hb with
      | .head _ => absurd rfl <| nodup_head b ‹b ∈ l›
      | .tail _ h => h
  specialize IH nodup_tail this
  simp only [length_append, length_cons] at IH ⊢
  exact Nat.succ_le_succ IH
State after:
no goals

State before:
case nil
α : Type u
β : Type v
l₁ : List α
nodup : Nodup []
h : [] ⊆ l₁
⊢ length [] ≤ length l₁
Tactic:
exact l₁.length.zero_le
State after:
no goals

State before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Tactic:
have .cons nodup_head (nodup_tail : l.Nodup) := nodup
State after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ length (a :: l) ≤ length l₁

State before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ length (a :: l) ≤ length l₁
Tactic:
let ⟨ha,hl⟩ := cons_subset.mp h
State after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁

State before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup : Nodup (a :: l)
h : a :: l ⊆ l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Tactic:
clear nodup h
State after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁

State before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
⊢ length (a :: l) ≤ length l₁
Tactic:
have ⟨l₁', l₁'', hl₁⟩ := mem_iff_append.mp ha
State after:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
l₁' l₁'' : List α
hl₁ : l₁ = l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length l₁

State before:
case cons
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
l₁ : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
ha : a ∈ l₁
hl : l ⊆ l₁
l₁' l₁'' : List α
hl₁ : l₁ = l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length l₁
Tactic:
cases hl₁
State after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
ha : a ∈ l₁' ++ a :: l₁''
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')

State before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
ha : a ∈ l₁' ++ a :: l₁''
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
clear ha
State after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')

State before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
have : l ⊆ l₁' ++ l₁'' := fun b hb => 
  match mem_append.mp (hl hb) with
  | .inl hb => mem_append.mpr <| Or.inl hb
  | .inr hb => mem_append.mpr <| Or.inr <|
    match hb with
    | .head _ => absurd rfl <| nodup_head b ‹b ∈ l›
    | .tail _ h => h
State after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')

State before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
IH : ∀ {l₁ : List α}, Nodup l → l ⊆ l₁ → length l ≤ length l₁
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
specialize IH nodup_tail this
State after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length (l₁' ++ l₁'')
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')

State before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length (l₁' ++ l₁'')
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
Tactic:
simp only [length_append, length_cons] at IH ⊢
State after:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length l₁' + length l₁''
⊢ Nat.succ (length l) ≤ length l₁' + Nat.succ (length l₁'')

State before:
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length l₁' + length l₁''
⊢ Nat.succ (length l) ≤ length l₁' + Nat.succ (length l₁'')
Tactic:
exact Nat.succ_le_succ IH
State after:
no goals