case nil
ι : Type ?u.491056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
y : β
⊢ (y, x) ∈ map Prod.swap [] ↔ (x, y) ∈ []

case cons
ι : Type ?u.491056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ : α
y : β
x : α × β
xs : List (α × β)
xs_ih : (y, x✝) ∈ map Prod.swap xs ↔ (x✝, y) ∈ xs
⊢ (y, x✝) ∈ map Prod.swap (x :: xs) ↔ (x✝, y) ∈ x :: xs
ι : Type ?u.491056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
y : β
xs : List (α × β)
⊢ (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs
induction' xs with x xs xs_ih
no goals
case nil
ι : Type ?u.491056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
y : β
⊢ (y, x) ∈ map Prod.swap [] ↔ (x, y) ∈ []
simp only [not_mem_nil, map_nil]
case cons.mk
ι : Type ?u.491056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
y : β
xs : List (α × β)
xs_ih : (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs
a : α
b : β
⊢ (y, x) ∈ map Prod.swap ((a, b) :: xs) ↔ (x, y) ∈ (a, b) :: xs
case cons
ι : Type ?u.491056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ : α
y : β
x : α × β
xs : List (α × β)
xs_ih : (y, x✝) ∈ map Prod.swap xs ↔ (x✝, y) ∈ xs
⊢ (y, x✝) ∈ map Prod.swap (x :: xs) ↔ (x✝, y) ∈ x :: xs
cases' x with a b
no goals
case cons.mk
ι : Type ?u.491056
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
y : β
xs : List (α × β)
xs_ih : (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs
a : α
b : β
⊢ (y, x) ∈ map Prod.swap ((a, b) :: xs) ↔ (x, y) ∈ (a, b) :: xs
simp only [mem_cons, Prod.mk.inj_iff, map, Prod.swap_prod_mk, Prod.exists, xs_ih, and_comm]