case nil
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a : α
l : List α
h₁✝ : ∀ (x : α), x ∈ l → R x x
h₂✝ : Pairwise R l
h₃✝ : Pairwise (flip R) l
h₁ : ∀ (x : α), x ∈ [] → R x x
h₂ : Pairwise R []
h₃ : Pairwise (flip R) []
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → R x y

case cons
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a : α
l : List α
h₁ : ∀ (x : α), x ∈ l → R x x
h₂ : Pairwise R l
h₃ : Pairwise (flip R) l
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
induction' l with a l ih
case cons
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
case cons
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
rw [pairwise_cons] at h₂ h₃
case cons
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
case cons
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
simp only [mem_cons]
case cons.inl.inl
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
β : Type ?u.5128
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
β : Type ?u.5128
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
case cons
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
rintro x (rfl | hx) y (rfl | hy)
no goals
case nil
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a : α
l : List α
h₁✝ : ∀ (x : α), x ∈ l → R x x
h₂✝ : Pairwise R l
h₃✝ : Pairwise (flip R) l
h₁ : ∀ (x : α), x ∈ [] → R x x
h₂ : Pairwise R []
h₃ : Pairwise (flip R) []
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → R x y
exact forall_mem_nil _
no goals
case cons.inl.inl
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
exact h₁ _ (l.mem_cons_self _)
no goals
case cons.inl.inr
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
exact h₂.1 _ hy
no goals
case cons.inr.inl
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
exact h₃.1 _ hx
no goals
case cons.inr.inr
α : Type u_1
β : Type ?u.5128
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
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
exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy