Theorem: ContinuousMultilinearMap.domDomCongrLinearEquiv'_symm_apply_piCongrLeft'_symm (ForML/ContinuousMultilinearMap.lean)

State before:
R : Type u_1
inst✝¹⁰ : Semiring R
S : Type u_2
inst✝⁹ : Semiring S
ι : Type u_3
inst✝⁸ : Fintype ι
ι' : Type u_4
inst✝⁷ : Fintype ι'
D : ι → Type u_5
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝⁵ : (i : ι) → Module R (D i)
F : Type u_6
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module R F
inst✝² : Module S F
inst✝¹ : ContinuousConstSMul S F
inst✝ : SMulCommClass R S F
σ : ι ≃ ι'
f : ContinuousMultilinearMap R (fun i => D (σ.symm i)) F
x : (i' : ι') → D (σ.symm i')
⊢ ((LinearEquiv.symm (domDomCongrLinearEquiv' R S D F σ)) f) ((Equiv.piCongrLeft' D σ).symm x) = f x
Tactic:
rw [domDomCongrLinearEquiv'_symm_apply, Equiv.apply_symm_apply]
State after:
no goals