α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → R a b → ∀ (h₁ : p a) (h₂ : p b), S (f a h₁) (f b h₂)
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ Pairwise S (List.pmap f l h)
refine' (pairwise_pmap h).2 (Pairwise.imp_of_mem _ hl)
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ S (f a✝³ h₁✝) (f b✝ h₂✝)
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → R a b → ∀ (h₁ : p a) (h₂ : p b), S (f a h₁) (f b h₂)
intros
case a
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ R a✝³ b✝
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ S (f a✝³ h₁✝) (f b✝ h₂✝)
apply hS
no goals
case a
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ R a✝³ b✝
assumption