-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h : ∀ x ∈ l, p x) :
    Pairwise R (l.pmap f h) ↔
      Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
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

Tactic:
induction l with
| nil => simp
| cons a l ihl =>
  obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
  simp only [ihl hl, pairwise_cons, exists₂_imp, pmap, and_congr_left_iff, mem_pmap]
  refine fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, ?_⟩
  rintro H _ b hb rfl
  exact H b hb _ _

Result:
no goals

Proof state:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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)

Tactic:
simp only [ihl hl, pairwise_cons, exists₂_imp, pmap, and_congr_left_iff, mem_pmap]

Result:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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 ⋯ = a' → R (f a ⋯) a') ↔
      ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂))

Proof state:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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 ⋯ = a' → R (f a ⋯) a'

Tactic:
rintro H _ b hb rfl

Result:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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 ⋯) (f b ⋯)

Proof state:
case cons
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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)

Tactic:
obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h

Result:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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)

Proof state:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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 ⋯) (f b ⋯)

Tactic:
exact H b hb _ _

Result:
no goals

Proof state:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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 ⋯ = a' → R (f a ⋯) a') ↔
      ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂))

Tactic:
refine fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, ?_⟩

Result:
case cons.intro
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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 ⋯ = a' → R (f a ⋯) a'

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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

Tactic:
simpa using h

Result:
no goals

Proof state:
case nil
β : Type u_1
α : Type u_2
R : α → α → Prop
p : β → Prop
f : (b : β) → p b → α
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₂)) []

Tactic:
simp

Result:
no goals