Theorem: List.forallr_Mem (Algdata/Logic/BishopFin.lean)

State before:
α : Type u
p : α → Prop
⊢ ∀ {l : List α}, List.forallr p l → ∀ (a : α), a ∈ l → p a
Tactic:
intro l hlp a hMem
State after:
α : Type u
p : α → Prop
l : List α
hlp : List.forallr p l
a : α
hMem : a ∈ l
⊢ p a

State before:
α : Type u
p : α → Prop
l : List α
hlp : List.forallr p l
a : α
hMem : a ∈ l
⊢ p a
Tactic:
induction l
State after:
case nil
α : Type u
p : α → Prop
a : α
hlp : List.forallr p []
hMem : a ∈ []
⊢ p a

case cons
α : Type u
p : α → Prop
a head✝ : α
tail✝ : List α
tail_ih✝ : List.forallr p tail✝ → a ∈ tail✝ → p a
hlp : List.forallr p (head✝ :: tail✝)
hMem : a ∈ head✝ :: tail✝
⊢ p a

State before:
α : Type u
p : α → Prop
a : α
hlp : List.forallr p []
hMem : a ∈ []
⊢ p a
Tactic:
case nil => cases hMem
State after:
no goals

State before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : a ∈ hhead :: htail
⊢ p a
Tactic:
case cons hhead htail h_ind =>
  cases hMem
  case head => cases hlp; assumption
  case tail hMem => apply h_ind ?_ hMem; cases hlp; assumption
State after:
no goals

State before:
α : Type u
p : α → Prop
a : α
hlp : List.forallr p []
hMem : a ∈ []
⊢ p a
Tactic:
cases hMem
State after:
no goals

State before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : a ∈ hhead :: htail
⊢ p a
Tactic:
cases hMem
State after:
case head
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (a :: htail)
⊢ p a

case tail
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
a✝ : Mem a htail
⊢ p a

State before:
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (a :: htail)
⊢ p a
Tactic:
case head => cases hlp; assumption
State after:
no goals

State before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ p a
Tactic:
case tail hMem => apply h_ind ?_ hMem; cases hlp; assumption
State after:
no goals

State before:
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (a :: htail)
⊢ p a
Tactic:
cases hlp
State after:
case cons
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
a✝¹ : p a
a✝ : List.forallr p htail
⊢ p a

State before:
case cons
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
a✝¹ : p a
a✝ : List.forallr p htail
⊢ p a
Tactic:
assumption
State after:
no goals

State before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ p a
Tactic:
apply h_ind ?_ hMem
State after:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ List.forallr p htail

State before:
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : Mem a htail
⊢ List.forallr p htail
Tactic:
cases hlp
State after:
case cons
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hMem : Mem a htail
a✝¹ : p hhead
a✝ : List.forallr p htail
⊢ List.forallr p htail

State before:
case cons
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hMem : Mem a htail
a✝¹ : p hhead
a✝ : List.forallr p htail
⊢ List.forallr p htail
Tactic:
assumption
State after:
no goals