[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ (List.bind l fun x => [x]) = l
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
⊢ (List.bind [] fun x => [x]) = []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
head✝ : α
tail✝ : List α
tail_ih✝ : (List.bind tail✝ fun x => [x]) = tail✝
⊢ (List.bind (head✝ :: tail✝) fun x => [x]) = head✝ :: tail✝
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = List.bind l fun x => [f x]
[PROOFSTEP]
simp only [← map_singleton]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = List.bind l fun x => map f [x]
[PROOFSTEP]
rw [← bind_singleton' l, bind_map, bind_singleton']
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
l : List α
f : α → List β
g : β → List γ
⊢ List.bind (List.bind l f) g = List.bind l fun x => List.bind (f x) g
[PROOFSTEP]
induction l
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → List β
g : β → List γ
⊢ List.bind (List.bind [] f) g = List.bind [] fun x => List.bind (f x) g
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → List β
g : β → List γ
head✝ : α
tail✝ : List α
tail_ih✝ : List.bind (List.bind tail✝ f) g = List.bind tail✝ fun x => List.bind (f x) g
⊢ List.bind (List.bind (head✝ :: tail✝) f) g = List.bind (head✝ :: tail✝) fun x => List.bind (f x) g
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
⊢ ¬∃ x, x ∈ [] ∧ p x
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ∃ x, x ∈ xs ∧ p x
⊢ ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
cases' h₂ with y h
[GOAL]
case intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
y : α
h : y ∈ xs ∧ p y
⊢ ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
cases' h with hm hp
[GOAL]
case intro.intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
y : α
hm : y ∈ xs
hp : p y
⊢ ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
exact ⟨y, mem_cons_of_mem _ hm, hp⟩
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
⊢ ¬∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
intro h
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
h : ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
⊢ False
[PROOFSTEP]
cases' h with y h
[GOAL]
case intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
h : y ∈ x :: xs ∧ p y
⊢ False
[PROOFSTEP]
cases' h with hm hp
[GOAL]
case intro.intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p y
⊢ False
[PROOFSTEP]
cases' mem_cons.1 hm with h h
[GOAL]
case intro.intro.inl
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p y
h : y = x
⊢ False
[PROOFSTEP]
rw [h] at hp 
[GOAL]
case intro.intro.inl
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p x
h : y = x
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case intro.intro.inr
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p y
h : y ∈ xs
⊢ False
[PROOFSTEP]
exact absurd ⟨y, h, hp⟩ h₂
