case h
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
⊢ i ∈ ↑σ '' s ↔ i ∈ s
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
⊢ ↑σ '' s = s
ext i
case h.inl
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
⊢ i ∈ ↑σ '' s ↔ i ∈ s

case h.inr
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
⊢ i ∈ ↑σ '' s ↔ i ∈ s
case h
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
⊢ i ∈ ↑σ '' s ↔ i ∈ s
obtain hi | hi := eq_or_ne (σ i) i
case h.inl
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
⊢ i ∈ ↑σ '' s → i ∈ s
case h.inl
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
⊢ i ∈ ↑σ '' s ↔ i ∈ s
refine' ⟨_, fun h => ⟨i, h, hi⟩⟩
case h.inl.intro.intro
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
j : α
hj : j ∈ s
h : ↑σ j = i
⊢ i ∈ s
case h.inl
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
⊢ i ∈ ↑σ '' s → i ∈ s
rintro ⟨j, hj, h⟩
no goals
case h.inl.intro.intro
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
j : α
hj : j ∈ s
h : ↑σ j = i
⊢ i ∈ s
rwa [σ.injective (hi.trans h.symm)]
case h.inr
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
h : ↑σ (↑σ.symm i) = ↑σ.symm i
⊢ ↑σ i = i
case h.inr
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
⊢ i ∈ ↑σ '' s ↔ i ∈ s
refine' iff_of_true ⟨σ.symm i, hs fun h => hi _, σ.apply_symm_apply _⟩ (hs hi)
no goals
case h.inr
α : Type u_1
β : Type ?u.57571
γ : Type ?u.57574
ι : Sort ?u.57577
ι' : Sort ?u.57580
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
h : ↑σ (↑σ.symm i) = ↑σ.symm i
⊢ ↑σ i = i
convert congr_arg σ h <;> exact (σ.apply_symm_apply _).symm