-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pairwise R l)
    (h₃ : l.Pairwise (flip R)) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
h₁ : ∀ (x : α✝), x ∈ a :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
⊢ ∀ ⦃x : α✝⦄, x ∈ a :: l → ∀ ⦃y : α✝⦄, y ∈ a :: l → R x y

Tactic:
simp only [mem_cons]

Result:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
h₁ : ∀ (x : α✝), x ∈ a :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
⊢ ∀ ⦃x : α✝⦄, x = a ∨ x ∈ l → ∀ ⦃y : α✝⦄, y = a ∨ y ∈ l → R x y

Proof state:
case cons.inl.inl
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
y : α✝
h₁ : ∀ (x : α✝), x ∈ y :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R y a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R y a') ∧ Pairwise (flip R) l
⊢ R y y

Tactic:
exact h₁ _ (l.mem_cons_self _)

Result:
no goals

Proof state:
case nil
α✝ : Type u_1
R : α✝ → α✝ → Prop
h₁ : ∀ (x : α✝), x ∈ [] → R x x
h₂ : Pairwise R []
h₃ : Pairwise (flip R) []
⊢ ∀ ⦃x : α✝⦄, x ∈ [] → ∀ ⦃y : α✝⦄, y ∈ [] → R x y

Tactic:
exact forall_mem_nil _

Result:
no goals

Proof state:
case cons.inr.inl
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
x : α✝
hx : x ∈ l
y : α✝
h₁ : ∀ (x : α✝), x ∈ y :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R y a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R y a') ∧ Pairwise (flip R) l
⊢ R x y

Tactic:
exact h₃.1 _ hx

Result:
no goals

Proof state:
case cons.inr.inr
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
h₁ : ∀ (x : α✝), x ∈ a :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
x : α✝
hx : x ∈ l
y : α✝
hy : y ∈ l
⊢ R x y

Tactic:
exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy

Result:
no goals

Proof state:
case cons.inl.inr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
x : α✝
h₁ : ∀ (x_1 : α✝), x_1 ∈ x :: l → R x_1 x_1
h₂ : (∀ (a' : α✝), a' ∈ l → R x a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R x a') ∧ Pairwise (flip R) l
y : α✝
hy : y ∈ l
⊢ R x y

Tactic:
exact h₂.1 _ hy

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
h₁ : ∀ (x : α✝), x ∈ a :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
⊢ ∀ ⦃x : α✝⦄, x = a ∨ x ∈ l → ∀ ⦃y : α✝⦄, y = a ∨ y ∈ l → R x y

Tactic:
rintro x (rfl | hx) y (rfl | hy)

Result:
case cons.inl.inl
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
y : α✝
h₁ : ∀ (x : α✝), x ∈ y :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R y a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R y a') ∧ Pairwise (flip R) l
⊢ R y y

case cons.inl.inr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
x : α✝
h₁ : ∀ (x_1 : α✝), x_1 ∈ x :: l → R x_1 x_1
h₂ : (∀ (a' : α✝), a' ∈ l → R x a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R x a') ∧ Pairwise (flip R) l
y : α✝
hy : y ∈ l
⊢ R x y

case cons.inr.inl
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
x : α✝
hx : x ∈ l
y : α✝
h₁ : ∀ (x : α✝), x ∈ y :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R y a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R y a') ∧ Pairwise (flip R) l
⊢ R x y

case cons.inr.inr
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
h₁ : ∀ (x : α✝), x ∈ a :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
x : α✝
hx : x ∈ l
y : α✝
hy : y ∈ l
⊢ R x y

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
h₁ : ∀ (x : α✝), x ∈ a :: l → R x x
h₂ : Pairwise R (a :: l)
h₃ : Pairwise (flip R) (a :: l)
⊢ ∀ ⦃x : α✝⦄, x ∈ a :: l → ∀ ⦃y : α✝⦄, y ∈ a :: l → R x y

Tactic:
rw [pairwise_cons] at h₂ h₃

Result:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
ih : (∀ (x : α✝), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α✝⦄, x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
h₁ : ∀ (x : α✝), x ∈ a :: l → R x x
h₂ : (∀ (a' : α✝), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α✝), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
⊢ ∀ ⦃x : α✝⦄, x ∈ a :: l → ∀ ⦃y : α✝⦄, y ∈ a :: l → R x y