case nil
α : Type uu
β : Type vv
l₁✝¹ l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝ l₂✝¹ l₁ l₂✝ : List α
p✝ : l₁ ~ l₂✝
l₂ : List α
p : [] ~ l₂
⊢ Pairwise R l₂

case cons
α : Type uu
β : Type vv
l₁✝² l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝¹ l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
l₂ : List α
p : a :: l₁ ~ l₂
⊢ Pairwise R l₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
R : α → α → Prop
S : Symmetric R
l₁✝ l₂✝ l₁ l₂ : List α
p : l₁ ~ l₂
d : Pairwise R l₁
⊢ Pairwise R l₂
induction' d with a l₁ h _ IH generalizing l₂
case nil
α : Type uu
β : Type vv
l₁✝¹ l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝ l₂✝¹ l₁ l₂✝ : List α
p✝ : l₁ ~ l₂✝
l₂ : List α
p : [] ~ l₂
⊢ Pairwise R []
case nil
α : Type uu
β : Type vv
l₁✝¹ l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝ l₂✝¹ l₁ l₂✝ : List α
p✝ : l₁ ~ l₂✝
l₂ : List α
p : [] ~ l₂
⊢ Pairwise R l₂
rw [← p.nil_eq]
no goals
case nil
α : Type uu
β : Type vv
l₁✝¹ l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝ l₂✝¹ l₁ l₂✝ : List α
p✝ : l₁ ~ l₂✝
l₂ : List α
p : [] ~ l₂
⊢ Pairwise R []
constructor
case cons
α : Type uu
β : Type vv
l₁✝² l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝¹ l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
l₂ : List α
p : a :: l₁ ~ l₂
this : a ∈ l₂
⊢ Pairwise R l₂
case cons
α : Type uu
β : Type vv
l₁✝² l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝¹ l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
l₂ : List α
p : a :: l₁ ~ l₂
⊢ Pairwise R l₂
have : a ∈ l₂ := p.subset (mem_cons_self _ _)
case cons.intro.intro
α : Type uu
β : Type vv
l₁✝² l₂✝¹ : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝ l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a :: l₁ ~ s₂ ++ a :: t₂
this : a ∈ s₂ ++ a :: t₂
⊢ Pairwise R (s₂ ++ a :: t₂)
case cons
α : Type uu
β : Type vv
l₁✝² l₂✝² : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝¹ l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
l₂ : List α
p : a :: l₁ ~ l₂
this : a ∈ l₂
⊢ Pairwise R l₂
rcases mem_split this with ⟨s₂, t₂, rfl⟩
case cons.intro.intro
α : Type uu
β : Type vv
l₁✝² l₂✝¹ : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝ l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a :: l₁ ~ s₂ ++ a :: t₂
this : a ∈ s₂ ++ a :: t₂
p' : l₁ ~ s₂ ++ t₂
⊢ Pairwise R (s₂ ++ a :: t₂)
case cons.intro.intro
α : Type uu
β : Type vv
l₁✝² l₂✝¹ : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝ l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a :: l₁ ~ s₂ ++ a :: t₂
this : a ∈ s₂ ++ a :: t₂
⊢ Pairwise R (s₂ ++ a :: t₂)
have p' := (p.trans perm_middle).cons_inv
case cons.intro.intro
α : Type uu
β : Type vv
l₁✝² l₂✝¹ : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝ l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a :: l₁ ~ s₂ ++ a :: t₂
this : a ∈ s₂ ++ a :: t₂
p' : l₁ ~ s₂ ++ t₂
b : α
m : b ∈ s₂ ++ t₂
⊢ R a b
case cons.intro.intro
α : Type uu
β : Type vv
l₁✝² l₂✝¹ : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝ l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a :: l₁ ~ s₂ ++ a :: t₂
this : a ∈ s₂ ++ a :: t₂
p' : l₁ ~ s₂ ++ t₂
⊢ Pairwise R (s₂ ++ a :: t₂)
refine' (pairwise_middle S).2 (pairwise_cons.2 ⟨fun b m => _, IH _ p'⟩)
no goals
case cons.intro.intro
α : Type uu
β : Type vv
l₁✝² l₂✝¹ : List α
R : α → α → Prop
S : Symmetric R
l₁✝¹ l₂✝ l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
a : α
l₁ : List α
h : ∀ (a' : α), a' ∈ l₁ → R a a'
a✝ : Pairwise R l₁
IH : ∀ (l₂ : List α), l₁ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a :: l₁ ~ s₂ ++ a :: t₂
this : a ∈ s₂ ++ a :: t₂
p' : l₁ ~ s₂ ++ t₂
b : α
m : b ∈ s₂ ++ t₂
⊢ R a b
exact h _ (p'.symm.subset m)