no goals
α : Type u_1
β : Sort ?u.8992
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
⊢ b ∈ remove a as ↔ b ∈ as ∧ b ≠ a
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⟩
no goals
case nil
α : Type u_1
β : Sort ?u.8992
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
⊢ b ∈ remove a [] ↔ b ∈ [] ∧ b ≠ a
simp [remove]
case cons
α : Type u_1
β : Sort ?u.8992
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
case cons
α : Type u_1
β : Sort ?u.8992
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
simp [remove]
no goals
case cons
α : Type u_1
β : Sort ?u.8992
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
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⟩
case cons.inl
α : Type u_1
β : Sort ?u.8992
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
case cons.inl
α : Type u_1
β : Sort ?u.8992
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
simp only [if_pos h, ih]
no goals
case cons.inl
α : Type u_1
β : Sort ?u.8992
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
exact ⟨fun ⟨h1, h2⟩ ↦ ⟨Or.inr h1, h2⟩, fun ⟨h1, h2⟩ ↦ ⟨Or.resolve_left h1 (h ▸ h2), h2⟩⟩
case cons.inr
α : Type u_1
β : Sort ?u.8992
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
α : Type u_1
β : Sort ?u.8992
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
simp [if_neg h, ih]
case cons.inr.mp
α : Type u_1
β : Sort ?u.8992
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.8992
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
α : Type u_1
β : Sort ?u.8992
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
constructor
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8992
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.mp
α : Type u_1
β : Sort ?u.8992
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.8992
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
{ 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⟩ }
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8992
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
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8992
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
intro ⟨h1, h2⟩
no goals
case cons.inr.mpr
α : Type u_1
β : Sort ?u.8992
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
cases h1 with
| inl h1' => exact Or.inl h1'
| inr h1' => exact Or.inr ⟨h1', h2⟩
case cons.inr.mp
α : Type u_1
β : Sort ?u.8992
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
case cons.inr.mp
α : Type u_1
β : Sort ?u.8992
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
intro h'
no goals
case cons.inr.mp
α : Type u_1
β : Sort ?u.8992
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
cases h' with
| inl h₁ => exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
| inr h₁ => exact ⟨Or.inr h₁.1, h₁.2⟩
no goals
case cons.inr.mp.inl
α : Type u_1
β : Sort ?u.8992
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
exact ⟨Or.inl h₁, h₁.symm ▸ (Ne.symm h)⟩
no goals
case cons.inr.mp.inr
α : Type u_1
β : Sort ?u.8992
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
exact ⟨Or.inr h₁.1, h₁.2⟩
no goals
case cons.inr.mpr.inl
α : Type u_1
β : Sort ?u.8992
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
exact Or.inl h1'
no goals
case cons.inr.mpr.inr
α : Type u_1
β : Sort ?u.8992
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
exact Or.inr ⟨h1', h2⟩