Theorem: ContinuousMultilinearMap.domDomCongrLinearEquiv'_apply_piCongrLeft' (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 D F
x : (i : ι) → D i
⊢ ((domDomCongrLinearEquiv' R S D F σ) f) ((Equiv.piCongrLeft' D σ) x) = f x
Tactic:
rw [domDomCongrLinearEquiv'_apply, Equiv.symm_apply_apply]
State after:
no goals