-- Module: Mathlib.Analysis.SpecialFunctions.PolarCoord
Goal:
p : ℝ × ℝ
h :
  Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
      Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
          Eq (α := AddCommMonoid (ℝ × ℝ)) Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid →
            HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
              Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid →
                HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
                  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
                      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-p.1 * sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
                    p.1 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((cos ∘ Prod.snd) p) (ContinuousLinearMap.fst ℝ ℝ ℝ)
h₁ :
  Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
      Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
          Eq (α := AddCommMonoid (ℝ × ℝ)) Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid →
            HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
              Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid →
                HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
                  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (sin p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
                      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 * cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
                    p.1 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((sin ∘ Prod.snd) p) (ContinuousLinearMap.fst ℝ ℝ ℝ)
⊢ HasFDerivAt (↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (cos p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
          HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (-p.1 * sin p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ)).prod
      (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (sin p.2) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
        HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 * cos p.2) (ContinuousLinearMap.snd ℝ ℝ ℝ)))
    p

Tactic:
convert!
    HasFDerivAt.prodMk (𝕜 := ℝ)
      (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
      (hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using
    2

Premises used: Real.hasDerivAt_sin, Real.hasDerivAt_cos, HasFDerivAt.mul, HasFDerivAt.prodMk, HasDerivAt.comp_hasFDerivAt, Prod.snd