case H
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun x y => x ≠ y → R x y

case H₁
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

case H₂
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
apply Pairwise.forall_of_forall
case H₁
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

case H₂
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
case H
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun x y => x ≠ y → R x y

case H₁
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

case H₂
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
. exact fun a b h hne => hR (h hne.symm)
case H₂
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
case H₁
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

case H₂
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
. exact fun _ _ hx => (hx rfl).elim
no goals
case H₂
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
. exact hl.imp (@fun a b h _ => by exact h)
no goals
case H
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun x y => x ≠ y → R x y
exact fun a b h hne => hR (h hne.symm)
no goals
case H₁
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x
exact fun _ _ hx => (hx rfl).elim
no goals
case H₂
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
exact hl.imp (@fun a b h _ => by exact h)
no goals
α : Type u_1
β : Type ?u.6230
R S T : α → α → Prop
a✝ : α
l : List α
hR : Symmetric R
hl : Pairwise R l
a b : α
h : R a b
x✝ : a ≠ b
⊢ R a b
exact h