no goals
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
cases Decidable.em (a = a') with
| inl h' =>
  simp [remove, if_pos h']
  cases Decidable.em (a ∈ as) with
  | inl h'' =>
    have h₃ : a' ∈ as := h' ▸ h''
    simp [card_remove_of_mem h'', h₃]
  | inr h'' =>
    have h₃ : a' ∉ as := h' ▸ h''
    simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
| inr h' =>
    have h₃ : a ∈ as := (mem_cons.1 h).resolve_left h'
    simp [remove, h']
    cases Decidable.em (a' ∈ as) with
    | inl h'' =>
      have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
      simp [h'', this, card_remove_of_mem h₃]
    | inr h'' =>
      have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
      simp [h'', this, card_remove_of_mem h₃]
case inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a as) + 1
case inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
simp [remove, if_pos h']
no goals
case inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a as) + 1
cases Decidable.em (a ∈ as) with
| inl h'' =>
  have h₃ : a' ∈ as := h' ▸ h''
  simp [card_remove_of_mem h'', h₃]
| inr h'' =>
  have h₃ : a' ∉ as := h' ▸ h''
  simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
case inl.inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : a ∈ as
h₃ : a' ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
case inl.inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
have h₃ : a' ∈ as := h' ▸ h''
no goals
case inl.inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : a ∈ as
h₃ : a' ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
simp [card_remove_of_mem h'', h₃]
case inl.inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : ¬a ∈ as
h₃ : ¬a' ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
case inl.inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : ¬a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
have h₃ : a' ∉ as := h' ▸ h''
no goals
case inl.inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
h'' : ¬a ∈ as
h₃ : ¬a' ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
case inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
case inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
have h₃ : a ∈ as := (mem_cons.1 h).resolve_left h'
case inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
case inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
simp [remove, h']
no goals
case inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
cases Decidable.em (a' ∈ as) with
| inl h'' =>
  have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
  simp [h'', this, card_remove_of_mem h₃]
| inr h'' =>
  have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
  simp [h'', this, card_remove_of_mem h₃]
case inr.inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
this : a' ∈ remove a as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
case inr.inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
no goals
case inr.inl
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
this : a' ∈ remove a as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
simp [h'', this, card_remove_of_mem h₃]
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ a' ∈ as ∧ a' ≠ a
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ a' ∈ remove a as
rw [mem_remove_iff]
no goals
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : a' ∈ as
⊢ a' ∈ as ∧ a' ≠ a
exact ⟨h'', Ne.symm h'⟩
case inr.inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : ¬a' ∈ as
this : ¬a' ∈ remove a as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
case inr.inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : ¬a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
no goals
case inr.inr
α : Type u_1
β : Sort ?u.28067
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
h'' : ¬a' ∈ as
this : ¬a' ∈ remove a as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
simp [h'', this, card_remove_of_mem h₃]