case nil
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a : α
l✝ : List α
p : β → Prop
f : (b : β) → p b → α
l : List β
h✝ : ∀ (x : β), x ∈ l → p x
h : ∀ (x : β), x ∈ [] → p x
⊢ Pairwise R (pmap f [] h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) []

case cons
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
⊢ Pairwise R (pmap f (a :: l) h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) (a :: l)
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a : α
l✝ : List α
p : β → Prop
f : (b : β) → p b → α
l : List β
h : ∀ (x : β), x ∈ l → p x
⊢ Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
induction' l with a l ihl
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
⊢ Pairwise R (pmap f (a :: l) h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) (a :: l)
case cons
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
⊢ Pairwise R (pmap f (a :: l) h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) (a :: l)
obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
⊢ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l →
    ((∀ (a' : α) (x : β) (h_1 : x ∈ l), f x (_ : p x) = a' → R (f a (_ : p a)) a') ↔
      ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂))
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
⊢ Pairwise R (pmap f (a :: l) h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) (a :: l)
simp only [ihl hl, pairwise_cons, bex_imp, pmap, and_congr_left_iff, mem_pmap]
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
x✝ : Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
⊢ (∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂)) →
    ∀ (a' : α) (x : β) (h_1 : x ∈ l), f x (_ : p x) = a' → R (f a (_ : p a)) a'
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
⊢ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l →
    ((∀ (a' : α) (x : β) (h_1 : x ∈ l), f x (_ : p x) = a' → R (f a (_ : p a)) a') ↔
      ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂))
refine' fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, _⟩
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
x✝ : Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
H : ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂)
b : β
hb : b ∈ l
⊢ R (f a (_ : p a)) (f b (_ : p b))
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
x✝ : Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
⊢ (∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂)) →
    ∀ (a' : α) (x : β) (h_1 : x ∈ l), f x (_ : p x) = a' → R (f a (_ : p a)) a'
rintro H _ b hb rfl
no goals
case cons.intro
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
x✝ : Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
H : ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂)
b : β
hb : b ∈ l
⊢ R (f a (_ : p a)) (f b (_ : p b))
exact H b hb _ _
no goals
case nil
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a : α
l✝ : List α
p : β → Prop
f : (b : β) → p b → α
l : List β
h✝ : ∀ (x : β), x ∈ l → p x
h : ∀ (x : β), x ∈ [] → p x
⊢ Pairwise R (pmap f [] h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) []
simp
no goals
α : Type u_2
β : Type u_1
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
⊢ p a ∧ ∀ (b : β), b ∈ l → p b
simpa using h