no goals
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
bs : List α
x✝ : [] ⊆ bs
⊢ card [] ≤ card bs
simp
no goals
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
⊢ card (a :: as) ≤ card bs
cases Decidable.em (a ∈ as) with
| inl h' =>
  have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
  simp [h', card_subset_le hsub']
| inr h' =>
  have : a ∈ bs := hsub (Mem.head ..)
  rw [card_cons_of_not_mem h', card_remove_of_mem this]
  apply Nat.add_le_add_right
  apply card_subset_le
  intro x xmem
  rw [mem_remove_iff]
  exact ⟨hsub (mem_cons_of_mem _ xmem), fun h ↦ h' (h ▸ xmem)⟩
case inl
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
hsub' : as ⊆ bs
⊢ card (a :: as) ≤ card bs
case inl
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
⊢ card (a :: as) ≤ card bs
have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
no goals
case inl
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
hsub' : as ⊆ bs
⊢ card (a :: as) ≤ card bs
simp [h', card_subset_le hsub']
case inr
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card (a :: as) ≤ card bs
case inr
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
⊢ card (a :: as) ≤ card bs
have : a ∈ bs := hsub (Mem.head ..)
case inr
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card as + 1 ≤ card (remove a bs) + 1
case inr
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card (a :: as) ≤ card bs
rw [card_cons_of_not_mem h', card_remove_of_mem this]
case inr.h
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card as ≤ card (remove a bs)
case inr
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card as + 1 ≤ card (remove a bs) + 1
apply Nat.add_le_add_right
case inr.h.a
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ as ⊆ remove a bs
case inr.h
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card as ≤ card (remove a bs)
apply card_subset_le
case inr.h.a
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
x : α
xmem : x ∈ as
⊢ x ∈ remove a bs
case inr.h.a
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ as ⊆ remove a bs
intro x xmem
case inr.h.a
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
x : α
xmem : x ∈ as
⊢ x ∈ bs ∧ x ≠ a
case inr.h.a
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
x : α
xmem : x ∈ as
⊢ x ∈ remove a bs
rw [mem_remove_iff]
no goals
case inr.h.a
α : Type u_1
β : Sort ?u.43987
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
x : α
xmem : x ∈ as
⊢ x ∈ bs ∧ x ≠ a
exact ⟨hsub (mem_cons_of_mem _ xmem), fun h ↦ h' (h ▸ xmem)⟩