Theorem: φ_invFun_eq (Jordan/PermFibration.lean)

State before:
α : Type u_1
ι : Type u_2
p : α → ι
g : (i : ι) → Perm ↑{a | p a = i}
a : α
i : ι
h : p a = i
⊢ φ_invFun g a = ↑((g i) { val := a, property := h })
Tactic:
subst h
State after:
α : Type u_1
ι : Type u_2
p : α → ι
g : (i : ι) → Perm ↑{a | p a = i}
a : α
⊢ φ_invFun g a = ↑((g (p a)) { val := a, property := ⋯ })

State before:
α : Type u_1
ι : Type u_2
p : α → ι
g : (i : ι) → Perm ↑{a | p a = i}
a : α
⊢ φ_invFun g a = ↑((g (p a)) { val := a, property := ⋯ })
Tactic:
rfl
State after:
no goals