no goals
G : Type u_1
inst✝³ : Group G
H K : Subgroup G
S T✝ : Set G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
T : ↑(leftTransversals ↑H)
q : G ⧸ H
⊢ ↑(↑(toEquiv (_ : ↑(f • T) ∈ leftTransversals ↑H)) q) = f • ↑(↑(toEquiv (_ : ↑T ∈ leftTransversals ↑H)) (f⁻¹ • q))
rw [smul_toEquiv, smul_inv_smul]