Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case e'_12.e'_15
p : ℝ × ℝ
e_4✝¹ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝¹ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝¹ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_4✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = Prod.normedAddCommGroup.toAddCommMonoid
e_6✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_9✝ : Field.toSemifield.toDivisionSemiring.toAddCommMonoid = normedAddCommGroup.toAddCommMonoid
e_10✝ : Semiring.toModule ≍ RCLike.toInnerProductSpaceReal.toModule
⊢ cos p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.1 * sin p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.1 • -sin p.2 • ContinuousLinearMap.snd ℝ ℝ ℝ + (cos ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ

pp: case e'_12.e'_16
p : ℝ × ℝ
e_4✝¹ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝¹ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝¹ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_4✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = Prod.normedAddCommGroup.toAddCommMonoid
e_6✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_13✝ : Field.toSemifield.toDivisionSemiring.toAddCommMonoid = normedAddCommGroup.toAddCommMonoid
e_14✝ : Semiring.toModule ≍ RCLike.toInnerProductSpaceReal.toModule
⊢ sin p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 * cos p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.1 • cos p.2 • ContinuousLinearMap.snd ℝ ℝ ℝ + (sin ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ

Tactic:
<;>

Goal state after:
case e'_12.e'_15
p : ℝ × ℝ
e_4✝¹ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝¹ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝¹ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_4✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = Prod.normedAddCommGroup.toAddCommMonoid
e_6✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_9✝ : Field.toSemifield.toDivisionSemiring.toAddCommMonoid = normedAddCommGroup.toAddCommMonoid
e_10✝ : Semiring.toModule ≍ RCLike.toInnerProductSpaceReal.toModule
⊢ cos p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.1 * sin p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.1 • -sin p.2 • ContinuousLinearMap.snd ℝ ℝ ℝ + (cos ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ

case e'_12.e'_16
p : ℝ × ℝ
e_4✝¹ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝¹ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝¹ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_4✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_5✝ : Prod.instAddCommMonoid = Prod.normedAddCommGroup.toAddCommMonoid
e_6✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_13✝ : Field.toSemifield.toDivisionSemiring.toAddCommMonoid = normedAddCommGroup.toAddCommMonoid
e_14✝ : Semiring.toModule ≍ RCLike.toInnerProductSpaceReal.toModule
⊢ sin p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 * cos p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    p.1 • cos p.2 • ContinuousLinearMap.snd ℝ ℝ ℝ + (sin ∘ Prod.snd) p • ContinuousLinearMap.fst ℝ ℝ ℝ