Theorem: List.all_pred (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (all xs fun x => decide (p x)) = true ↔ ∀ (x : α), x ∈ xs → p x
Tactic:
simp only [all]
State after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true ↔ ∀ (x : α), x ∈ xs → p x

State before:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true ↔ ∀ (x : α), x ∈ xs → p x
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true → ∀ (x : α), x ∈ xs → p x

case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true

State before:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true → ∀ (x : α), x ∈ xs → p x

case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. intros hforward x hx
  induction hx with
  | head as =>
    simp [foldr] at hforward
    apply And.left hforward
  | tail a h ih =>
    apply ih
    simp [foldr] at hforward
    apply And.right hforward
State after:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true

State before:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. intros hbackward
  induction xs with
  | nil => simp [foldr]
  | cons x xs ih =>
    simp [foldr]
    apply And.intro
    . apply hbackward x (List.Mem.head _)
    . apply ih
      intro x' hx'
      apply hbackward _ $ List.Mem.tail _ hx'
State after:
no goals

State before:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true → ∀ (x : α), x ∈ xs → p x
Tactic:
intros hforward x hx
State after:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hforward : foldr (fun a r => decide (p a) && r) true xs = true
x : α
hx : x ∈ xs
⊢ p x

State before:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hforward : foldr (fun a r => decide (p a) && r) true xs = true
x : α
hx : x ∈ xs
⊢ p x
Tactic:
induction hx with
| head as =>
  simp [foldr] at hforward
  apply And.left hforward
| tail a h ih =>
  apply ih
  simp [foldr] at hforward
  apply And.right hforward
State after:
no goals

State before:
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : foldr (fun a r => decide (p a) && r) true (x :: as) = true
⊢ p x
Tactic:
simp [foldr] at hforward
State after:
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : p x ∧ foldr (fun a r => decide (p a) && r) true as = true
⊢ p x

State before:
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : p x ∧ foldr (fun a r => decide (p a) && r) true as = true
⊢ p x
Tactic:
apply And.left hforward
State after:
no goals

State before:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ p x
Tactic:
apply ih
State after:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true

State before:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true
Tactic:
simp [foldr] at hforward
State after:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : p a ∧ foldr (fun a r => decide (p a) && r) true as✝ = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true

State before:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : p a ∧ foldr (fun a r => decide (p a) && r) true as✝ = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true
Tactic:
apply And.right hforward
State after:
no goals

State before:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
intros hbackward
State after:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hbackward : ∀ (x : α), x ∈ xs → p x
⊢ foldr (fun a r => decide (p a) && r) true xs = true

State before:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hbackward : ∀ (x : α), x ∈ xs → p x
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
induction xs with
| nil => simp [foldr]
| cons x xs ih =>
  simp [foldr]
  apply And.intro
  . apply hbackward x (List.Mem.head _)
  . apply ih
    intro x' hx'
    apply hbackward _ $ List.Mem.tail _ hx'
State after:
no goals

State before:
case mpr.nil
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
hbackward : ∀ (x : α), x ∈ [] → p x
⊢ foldr (fun a r => decide (p a) && r) true [] = true
Tactic:
simp [foldr]
State after:
no goals

State before:
case mpr.cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true (x :: xs) = true
Tactic:
simp [foldr]
State after:
case mpr.cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x ∧ foldr (fun a r => decide (p a) && r) true xs = true

State before:
case mpr.cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x ∧ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
apply And.intro
State after:
case mpr.cons.left
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x

case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true

State before:
case mpr.cons.left
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x

case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. apply hbackward x (List.Mem.head _)
State after:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true

State before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. apply ih
  intro x' hx'
  apply hbackward _ $ List.Mem.tail _ hx'
State after:
no goals

State before:
case mpr.cons.left
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x
Tactic:
apply hbackward x (List.Mem.head _)
State after:
no goals

State before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
apply ih
State after:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ ∀ (x : α), x ∈ xs → p x

State before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ ∀ (x : α), x ∈ xs → p x
Tactic:
intro x' hx'
State after:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
x' : α
hx' : x' ∈ xs
⊢ p x'

State before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
x' : α
hx' : x' ∈ xs
⊢ p x'
Tactic:
apply hbackward _ $ List.Mem.tail _ hx'
State after:
no goals