no goals
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝¹ : List α
x✝ : Disjoint [] x✝¹
⊢ card ([] ++ x✝¹) = card [] + card x✝¹
simp
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
have disj' : Disjoint as bs := fun _ h1 h2 ↦ disj (mem_cons_of_mem a h1) h2
no goals
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
cases Decidable.em (a ∈ as) with
| inl h =>
  simp [h, card_append_disjoint disj']
| inr h =>
  have h1 : a ∉ bs := fun h' ↦ disj (mem_cons_self a as) h'
  simp [h, h1, card_append_disjoint disj']
  rw [Nat.add_right_comm]
no goals
case inl
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
simp [h, card_append_disjoint disj']
case inr
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
h1 : ¬a ∈ bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
case inr
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
have h1 : a ∉ bs := fun h' ↦ disj (mem_cons_self a as) h'
case inr
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
h1 : ¬a ∈ bs
⊢ card as + card bs + 1 = card as + 1 + card bs
case inr
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
h1 : ¬a ∈ bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
simp [h, h1, card_append_disjoint disj']
no goals
case inr
α : Type u_1
β : Sort ?u.49007
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
h : ¬a ∈ as
h1 : ¬a ∈ bs
⊢ card as + card bs + 1 = card as + 1 + card bs
rw [Nat.add_right_comm]