[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
as : List α
x : α
⊢ x ∈ List.insert a as ↔ x ∈ a :: as
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
as bs : List α
x : α
⊢ x ∈ as ∪ bs ↔ x ∈ as ++ bs
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
⊢ b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
[PROOFSTEP]
induction as with
| nil => simp [remove]
| cons a' as ih =>
  simp [remove]
  cases Decidable.em (a = a') with
  | inl h =>
    simp only [if_pos h, ih]
    exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
  | inr h =>
    simp [if_neg h, ih]
    constructor
    {focus
        intro h'
        cases h' with
        | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
        | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
    }
    intro ⟨h1, h2⟩
    cases h1 with
    | inl h1' => exact Or.inl h1'
    | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
⊢ b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
[PROOFSTEP]
induction as with
| nil => simp [remove]
| cons a' as ih =>
  simp [remove]
  cases Decidable.em (a = a') with
  | inl h =>
    simp only [if_pos h, ih]
    exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
  | inr h =>
    simp [if_neg h, ih]
    constructor
    {focus
        intro h'
        cases h' with
        | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
        | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
    }
    intro ⟨h1, h2⟩
    cases h1 with
    | inl h1' => exact Or.inl h1'
    | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case nil
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
⊢ b ∈ remove a [] ↔ b ∈ [] ∧ b ≠ a
[PROOFSTEP]

| nil => simp [remove]
[GOAL]
case nil
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
⊢ b ∈ remove a [] ↔ b ∈ [] ∧ b ≠ a
[PROOFSTEP]
simp [remove]
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
⊢ b ∈ remove a (a' :: as) ↔ b ∈ a' :: as ∧ b ≠ a
[PROOFSTEP]

| cons a' as ih =>
  simp [remove]
  cases Decidable.em (a = a') with
  | inl h =>
    simp only [if_pos h, ih]
    exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
  | inr h =>
    simp [if_neg h, ih]
    constructor
    {focus
        intro h'
        cases h' with
        | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
        | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
    }
    intro ⟨h1, h2⟩
    cases h1 with
    | inl h1' => exact Or.inl h1'
    | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
⊢ b ∈ remove a (a' :: as) ↔ b ∈ a' :: as ∧ b ≠ a
[PROOFSTEP]
simp [remove]
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases Decidable.em (a = a') with
| inl h =>
  simp only [if_pos h, ih]
  exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
| inr h =>
  simp [if_neg h, ih]
  constructor
  {focus
      intro h'
      cases h' with
      | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
      | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
  }
  intro ⟨h1, h2⟩
  cases h1 with
  | inl h1' => exact Or.inl h1'
  | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
x✝ : a = a' ∨ ¬a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases Decidable.em (a = a') with
| inl h =>
  simp only [if_pos h, ih]
  exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
| inr h =>
  simp [if_neg h, ih]
  constructor
  {focus
      intro h'
      cases h' with
      | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
      | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
  }
  intro ⟨h1, h2⟩
  cases h1 with
  | inl h1' => exact Or.inl h1'
  | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inl h =>
  simp only [if_pos h, ih]
  exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
[GOAL]
case cons.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
simp only [if_pos h, ih]
[GOAL]
case cons.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : a = a'
⊢ b ∈ as ∧ b ≠ a ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
[GOAL]
case cons.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inr h =>
  simp [if_neg h, ih]
  constructor
  {focus
      intro h'
      cases h' with
      | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
      | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
  }
  intro ⟨h1, h2⟩
  cases h1 with
  | inl h1' => exact Or.inl h1'
  | inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b ∈ if a = a' then remove a as else a' :: remove a as) ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
simp [if_neg h, ih]
[GOAL]
case cons.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a ↔ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
constructor
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a → (b = a' ∨ b ∈ as) ∧ ¬b = a
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a → b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
{focus
    intro h'
    cases h' with
    | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
    | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
}
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a → (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
focus
  intro h'
  cases h' with
  | inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
  | inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a → (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
intro h'
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h' : b = a' ∨ b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases h' with
| inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
| inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h' : b = a' ∨ b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
cases h' with
| inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
| inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
[GOAL]
case cons.inr.mp.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
[GOAL]
case cons.inr.mp.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]

| inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mp.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h₁ : b ∈ as ∧ ¬b = a
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a
[PROOFSTEP]
exact ⟨Or.inr h₁.1, h₁.2⟩
[GOAL]
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
⊢ (b = a' ∨ b ∈ as) ∧ ¬b = a → b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
intro ⟨h1, h2⟩
[GOAL]
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h1 : b = a' ∨ b ∈ as
h2 : ¬b = a
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
cases h1 with
| inl h1' => exact Or.inl h1'
| inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h1 : b = a' ∨ b ∈ as
h2 : ¬b = a
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
cases h1 with
| inl h1' => exact Or.inl h1'
| inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr.mpr.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]

| inl h1' => exact Or.inl h1'
[GOAL]
case cons.inr.mpr.inl
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b = a'
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
exact Or.inl h1'
[GOAL]
case cons.inr.mpr.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b ∈ as
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]

| inr h1' => exact Or.inr ⟨h1', h2⟩
[GOAL]
case cons.inr.mpr.inr
α : Type u_1
β : Sort ?u.8926
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b a' : α
as : List α
ih : b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
h : ¬a = a'
h2 : ¬b = a
h1' : b ∈ as
⊢ b = a' ∨ b ∈ as ∧ ¬b = a
[PROOFSTEP]
exact Or.inr ⟨h1', h2⟩
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
x✝ : ¬a ∈ []
⊢ remove a [] = []
[PROOFSTEP]
simp [remove]
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
⊢ remove a (a' :: as) = a' :: as
[PROOFSTEP]
have h1 : a ≠ a' := fun h' ↦ h (by rw [h']; apply mem_cons_self)
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h' : a = a'
⊢ a ∈ a' :: as
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h' : a = a'
⊢ a' ∈ a' :: as
[PROOFSTEP]
apply mem_cons_self
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h1 : a ≠ a'
⊢ remove a (a' :: as) = a' :: as
[PROOFSTEP]
have h2 : a ∉ as := fun h' ↦ h (mem_cons_of_mem _ h')
[GOAL]
α : Type u_1
β : Sort ?u.19025
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : ¬a ∈ a' :: as
h1 : a ≠ a'
h2 : ¬a ∈ as
⊢ remove a (a' :: as) = a' :: as
[PROOFSTEP]
simp [remove, h1, remove_eq_of_not_mem h2]
[GOAL]
α : Type u_1
β : Sort ?u.19685
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
h : b ∈ remove a as
⊢ b ∈ as
[PROOFSTEP]
rw [mem_remove_iff] at h 
[GOAL]
α : Type u_1
β : Sort ?u.19685
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
h : b ∈ as ∧ b ≠ a
⊢ b ∈ as
[PROOFSTEP]
exact
  h.1
    /- card -/
[GOAL]
α : Type u_1
β : Sort ?u.20767
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card (a :: as) = card as
[PROOFSTEP]
simp [card, h]
[GOAL]
α : Type u_1
β : Sort ?u.21944
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card (a :: as) = card as + 1
[PROOFSTEP]
simp [card, h]
[GOAL]
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h => simp [h, Nat.le_refl]
| inr h => simp [h, Nat.le_succ]
[GOAL]
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (a ∈ as) with
| inl h => simp [h, Nat.le_refl]
| inr h => simp [h, Nat.le_succ]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]

| inl h => simp [h, Nat.le_refl]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
simp [h, Nat.le_refl]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]

| inr h => simp [h, Nat.le_succ]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.22769
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card as ≤ card (a :: as)
[PROOFSTEP]
simp [h, Nat.le_succ]
[GOAL]
α : Type u_1
β : Sort ?u.25043
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card (List.insert a as) = card as
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Sort ?u.25854
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card (List.insert a as) = card as + 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
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₃]
[GOAL]
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
x✝ : a = a' ∨ ¬a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
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₃]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]

| 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'']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
simp [remove, if_pos h']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
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'']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : a = a'
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card (a' :: as) = card (remove a as) + 1
[PROOFSTEP]
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'']
[GOAL]
case inl.inl
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]

| inl h'' =>
  have h₃ : a' ∈ as := h' ▸ h''
  simp [card_remove_of_mem h'', h₃]
[GOAL]
case inl.inl
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
have h₃ : a' ∈ as := h' ▸ h''
[GOAL]
case inl.inl
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
simp [card_remove_of_mem h'', h₃]
[GOAL]
case inl.inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]

| inr h'' =>
  have h₃ : a' ∉ as := h' ▸ h''
  simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
[GOAL]
case inl.inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
have h₃ : a' ∉ as := h' ▸ h''
[GOAL]
case inl.inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
simp [card_cons_of_not_mem h₃, remove_eq_of_not_mem h'']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]

| 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₃]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
⊢ card (a' :: as) = card (remove a (a' :: as)) + 1
[PROOFSTEP]
have h₃ : a ∈ as := (mem_cons.1 h).resolve_left h'
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
simp [remove, h']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
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₃]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.27827
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a a' : α
as : List α
h : a ∈ a' :: as
h' : ¬a = a'
h₃ : a ∈ as
x✝ : a' ∈ as ∨ ¬a' ∈ as
⊢ card (a' :: as) = card (a' :: remove a as) + 1
[PROOFSTEP]
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₃]
[GOAL]
case inr.inl
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]

| 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₃]
[GOAL]
case inr.inl
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
have : a' ∈ remove a as := by rw [mem_remove_iff]; exact ⟨h'', Ne.symm h'⟩
[GOAL]
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
rw [mem_remove_iff]
[GOAL]
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
exact ⟨h'', Ne.symm h'⟩
[GOAL]
case inr.inl
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr.inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]

| inr h'' =>
  have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
  simp [h'', this, card_remove_of_mem h₃]
[GOAL]
case inr.inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
have : a' ∉ remove a as := fun h ↦ h'' (mem_of_mem_remove h)
[GOAL]
case inr.inr
α : Type u_1
β : Sort ?u.27827
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
[PROOFSTEP]
simp [h'', this, card_remove_of_mem h₃]
[GOAL]
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
bs : List α
x✝ : [] ⊆ bs
⊢ card [] ≤ card bs
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
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)⟩
[GOAL]
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
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)⟩
[GOAL]
case inl
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]

| inl h' =>
  have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
  simp [h', card_subset_le hsub']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
have hsub' : as ⊆ bs := fun _ xmem ↦ hsub (mem_cons_of_mem a xmem)
[GOAL]
case inl
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : a ∈ as
hsub' : as ⊆ bs
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
simp [h', card_subset_le hsub']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]

| 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)⟩
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
have : a ∈ bs := hsub (Mem.head ..)
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card (a :: as) ≤ card bs
[PROOFSTEP]
rw [card_cons_of_not_mem h', card_remove_of_mem this]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.43663
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
[PROOFSTEP]
apply Nat.add_le_add_right
[GOAL]
case inr.h
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ card as ≤ card (remove a bs)
[PROOFSTEP]
apply card_subset_le
[GOAL]
case inr.h.a
α : Type u_1
β : Sort ?u.43663
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
hsub : a :: as ⊆ bs
h' : ¬a ∈ as
this : a ∈ bs
⊢ as ⊆ remove a bs
[PROOFSTEP]
intro x xmem
[GOAL]
case inr.h.a
α : Type u_1
β : Sort ?u.43663
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
[PROOFSTEP]
rw [mem_remove_iff]
[GOAL]
case inr.h.a
α : Type u_1
β : Sort ?u.43663
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
[PROOFSTEP]
exact ⟨hsub (mem_cons_of_mem _ xmem), fun h ↦ h' (h ▸ xmem)⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ card (map f as) ≤ card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    rw [map, card_cons_of_mem h]
    apply Nat.le_trans ih (card_le_card_cons ..)
  | inr h =>
    have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
    exact Nat.add_le_add_right ih _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ card (map f as) ≤ card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    rw [map, card_cons_of_mem h]
    apply Nat.le_trans ih (card_le_card_cons ..)
  | inr h =>
    have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
    exact Nat.add_le_add_right ih _
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ card (map f []) ≤ card []
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ card (map f []) ≤ card []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]

| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    rw [map, card_cons_of_mem h]
    apply Nat.le_trans ih (card_le_card_cons ..)
  | inr h =>
    have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
    exact Nat.add_le_add_right ih _
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  rw [map, card_cons_of_mem h]
  apply Nat.le_trans ih (card_le_card_cons ..)
| inr h =>
  have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
  exact Nat.add_le_add_right ih _
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
x✝ : f a ∈ map f as ∨ ¬f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  rw [map, card_cons_of_mem h]
  apply Nat.le_trans ih (card_le_card_cons ..)
| inr h =>
  have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
  exact Nat.add_le_add_right ih _
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]

| inl h =>
  rw [map, card_cons_of_mem h]
  apply Nat.le_trans ih (card_le_card_cons ..)
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_mem h]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f as) ≤ card (a :: as)
[PROOFSTEP]
apply Nat.le_trans ih (card_le_card_cons ..)
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]

| inr h =>
  have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
  exact Nat.add_le_add_right ih _
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f (a :: as)) ≤ card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f as) + 1 ≤ card as + 1
[PROOFSTEP]
exact Nat.add_le_add_right ih _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ inj_on f as → card (map f as) = card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    intro inj_on'
    cases (exists_of_mem_map h) with
    | intro x hx =>
      have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
      have h1 : a ∈ as := this ▸ hx.1
      have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
      rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
  | inr h =>
    intro inj_on'
    have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ inj_on f as → card (map f as) = card as
[PROOFSTEP]
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    intro inj_on'
    cases (exists_of_mem_map h) with
    | intro x hx =>
      have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
      have h1 : a ∈ as := this ▸ hx.1
      have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
      rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
  | inr h =>
    intro inj_on'
    have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ inj_on f [] → card (map f []) = card []
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ inj_on f [] → card (map f []) = card []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    intro inj_on'
    cases (exists_of_mem_map h) with
    | intro x hx =>
      have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
      have h1 : a ∈ as := this ▸ hx.1
      have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
      rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
  | inr h =>
    intro inj_on'
    have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  intro inj_on'
  cases (exists_of_mem_map h) with
  | intro x hx =>
    have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
    have h1 : a ∈ as := this ▸ hx.1
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
| inr h =>
  intro inj_on'
  have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
x✝ : f a ∈ map f as ∨ ¬f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  intro inj_on'
  cases (exists_of_mem_map h) with
  | intro x hx =>
    have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
    have h1 : a ∈ as := this ▸ hx.1
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
| inr h =>
  intro inj_on'
  have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| inl h =>
  intro inj_on'
  cases (exists_of_mem_map h) with
  | intro x hx =>
    have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
    have h1 : a ∈ as := this ▸ hx.1
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
intro inj_on'
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases (exists_of_mem_map h) with
| intro x hx =>
  have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
  have h1 : a ∈ as := this ▸ hx.1
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x✝ : ∃ a_1, a_1 ∈ as ∧ f a_1 = f a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
cases (exists_of_mem_map h) with
| intro x hx =>
  have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
  have h1 : a ∈ as := this ▸ hx.1
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| intro x hx =>
  have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
  have h1 : a ∈ as := this ▸ hx.1
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h1 : a ∈ as := this ▸ hx.1
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
[GOAL]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
h2 : inj_on f as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]

| inr h =>
  intro inj_on'
  have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
intro inj_on'
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬a ∈ as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬a ∈ as
h2 : inj_on f as
⊢ card (map f (a :: as)) = card (a :: as)
[PROOFSTEP]
rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
[GOAL]
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝¹ : List α
x✝ : Disjoint [] x✝¹
⊢ card ([] ++ x✝¹) = card [] + card x✝¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
have disj' : Disjoint as bs := fun _ h1 h2 ↦ disj (mem_cons_of_mem a h1) h2
[GOAL]
α : Type u_1
β : Sort ?u.48627
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
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Sort ?u.48627
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as bs : List α
disj : Disjoint (a :: as) bs
disj' : Disjoint as bs
x✝ : a ∈ as ∨ ¬a ∈ as
⊢ card (a :: as ++ bs) = card (a :: as) + card bs
[PROOFSTEP]
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]
[GOAL]
case inl
α : Type u_1
β : Sort ?u.48627
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
[PROOFSTEP]

| inl h => simp [h, card_append_disjoint disj']
[GOAL]
case inl
α : Type u_1
β : Sort ?u.48627
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
[PROOFSTEP]
simp [h, card_append_disjoint disj']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
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
[PROOFSTEP]

| 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]
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
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
[PROOFSTEP]
have h1 : a ∉ bs := fun h' ↦ disj (mem_cons_self a as) h'
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
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
[PROOFSTEP]
simp [h, h1, card_append_disjoint disj']
[GOAL]
case inr
α : Type u_1
β : Sort ?u.48627
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
[PROOFSTEP]
rw [Nat.add_right_comm]
[GOAL]
α : Type u_1
β : Sort ?u.54019
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
as bs : List α
h : Disjoint as bs
⊢ card (as ∪ bs) = card as + card bs
[PROOFSTEP]
rw [card_eq_of_equiv (union_equiv_append as bs), card_append_disjoint h]
