case cons.false
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = false
⊢ p x = true

case cons.true
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true
case cons
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
⊢ p x = true
cases hp : p hd
no goals
case cons.false
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = false
⊢ p x = true
simp [hp] at hx
case cons.true
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true
case cons.true
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
hp : p hd = true
⊢ p x = true
rw [hp, mem_cons] at hx
case cons.true.inl
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p x = true
⊢ p x = true

case cons.true.inr
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true
case cons.true
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true
rcases hx with (rfl | hx)
no goals
case cons.true.inl
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p x = true
⊢ p x = true
exact hp
no goals
case cons.true.inr
ι : Type ?u.414998
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true
exact IH hx