Theorem: fstCmmap_apply (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝⁷ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
a : A
b : B
⊢ ((fstCmmap R A B) fun x => (a, b)) = a
Tactic:
simp only [fstCmmap, ContinuousMultilinearMap.ofSubsingleton_apply_apply,
  ContinuousLinearMap.coe_fst']
State after:
no goals