Theorem: arrowAction.mem_stabilizer_iff (Jordan/PermFibration.lean)

State before:
α : Type u_1
ι : Type u_2
p : α → ι
g : Perm α
⊢ g ∈ stabilizer (Perm α) p ↔ p ∘ ⇑g = p
Tactic:
rw [eq_comm, ← g.comp_symm_eq]
State after:
α : Type u_1
ι : Type u_2
p : α → ι
g : Perm α
⊢ g ∈ stabilizer (Perm α) p ↔ p ∘ ⇑g.symm = p

State before:
α : Type u_1
ι : Type u_2
p : α → ι
g : Perm α
⊢ g ∈ stabilizer (Perm α) p ↔ p ∘ ⇑g.symm = p
Tactic:
rfl
State after:
no goals