Theorem: Misc.List.Pairwise.imp_of_mem (LeanSAT/Util/Misc.lean)

State before:
case nil
α : Type u_1
R S : α → α → Prop
l : List α
H : ∀ {a b : α}, a ∈ [] → b ∈ [] → R a b → S a b
⊢ Pairwise S []
Tactic:
constructor
State after:
no goals

State before:
case cons
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S (a :: l)
Tactic:
constructor
State after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'

case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l

State before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'
Tactic:
intro a' a'_in_l
State after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
⊢ S a a'

State before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
⊢ S a a'
Tactic:
have a_in_al : a ∈ a :: l := by simp
State after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
⊢ S a a'

State before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
⊢ S a a'
Tactic:
have a'_in_al : a' ∈ a :: l := by simp [a'_in_l]
State after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
a'_in_al : a' ∈ a :: l
⊢ S a a'

State before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
a'_in_al : a' ∈ a :: l
⊢ S a a'
Tactic:
exact H a_in_al a'_in_al (r a' a'_in_l)
State after:
no goals

State before:
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
⊢ a ∈ a :: l
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
⊢ a' ∈ a :: l
Tactic:
simp [a'_in_l]
State after:
no goals

State before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l
Tactic:
exact ih fun {a b} m m' => H (List.mem_cons_of_mem _ m) (List.mem_cons_of_mem _ m')
State after:
no goals