case intro.intro
ι : Type ?u.2112
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l
ι : Type ?u.2112
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
hf : Involutive f
x : α
l : List α
⊢ (∃ y, y ∈ l ∧ f y = x) → f x ∈ l
rintro ⟨y, h, rfl⟩
no goals
case intro.intro
ι : Type ?u.2112
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l
rwa [hf y]