case cons
α : Type u_1
β : Type ?u.2465
R S T : α → α → Prop
a✝ : α
l✝ : List α
x✝¹ : Pairwise R l✝ ∧ Pairwise S l✝
hS✝ : Pairwise S l✝
a : α
l : List α
R1 : ∀ (a' : α), a' ∈ l → R a a'
R2 : Pairwise R l
IH : Pairwise R l ∧ Pairwise S l → Pairwise S l → Pairwise (fun a b => R a b ∧ S a b) l
x✝ : ((∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l) ∧ (∀ (a' : α), a' ∈ l → S a a') ∧ Pairwise S l
hS : (∀ (a' : α), a' ∈ l → S a a') ∧ Pairwise S l
⊢ (∀ (a' : α), a' ∈ l → R a a' ∧ S a a') ∧ Pairwise (fun a b => R a b ∧ S a b) l
α : Type u_1
β : Type ?u.2465
R S T : α → α → Prop
a : α
l : List α
x✝ : Pairwise R l ∧ Pairwise S l
hR : Pairwise R l
hS : Pairwise S l
⊢ Pairwise (fun a b => R a b ∧ S a b) l
induction' hR with a l R1 R2 IH <;> simp only [Pairwise.nil, pairwise_cons] at *
no goals
case cons
α : Type u_1
β : Type ?u.2465
R S T : α → α → Prop
a✝ : α
l✝ : List α
x✝¹ : Pairwise R l✝ ∧ Pairwise S l✝
hS✝ : Pairwise S l✝
a : α
l : List α
R1 : ∀ (a' : α), a' ∈ l → R a a'
R2 : Pairwise R l
IH : Pairwise R l ∧ Pairwise S l → Pairwise S l → Pairwise (fun a b => R a b ∧ S a b) l
x✝ : ((∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l) ∧ (∀ (a' : α), a' ∈ l → S a a') ∧ Pairwise S l
hS : (∀ (a' : α), a' ∈ l → S a a') ∧ Pairwise S l
⊢ (∀ (a' : α), a' ∈ l → R a a' ∧ S a a') ∧ Pairwise (fun a b => R a b ∧ S a b) l
exact ⟨fun b bl => ⟨R1 b bl, hS.1 b bl⟩, IH ⟨R2, hS.2⟩ hS.2⟩