[GOAL]
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
R : Type u_4
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H R
inst✝ : SmoothRing I R
⊢ Smooth I I fun a => -a
[PROOFSTEP]
simpa only [neg_one_mul] using @smooth_mul_left 𝕜 _ H _ E _ _ I R _ _ _ _ (-1)
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
⊢ Smooth (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) 𝓘(𝕜, 𝕜) fun p => p.fst * p.snd
[PROOFSTEP]
rw [smooth_iff]
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
⊢ (Continuous fun p => p.fst * p.snd) ∧
    ∀ (x : 𝕜 × 𝕜) (y : 𝕜),
      ContDiffOn 𝕜 ⊤
        (↑(extChartAt 𝓘(𝕜, 𝕜) y) ∘
          (fun p => p.fst * p.snd) ∘ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)))
        ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
          ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)) ⁻¹'
            ((fun p => p.fst * p.snd) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source))
[PROOFSTEP]
refine' ⟨continuous_mul, fun x y => _⟩
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 ⊤
    (↑(extChartAt 𝓘(𝕜, 𝕜) y) ∘
      (fun p => p.fst * p.snd) ∘ ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)))
    ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
      ↑(LocalEquiv.symm (extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x)) ⁻¹'
        ((fun p => p.fst * p.snd) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source))
[PROOFSTEP]
simp only [Prod.mk.eta, mfld_simps]
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 ⊤ (fun p => p.fst * p.snd) Set.univ
[PROOFSTEP]
rw [contDiffOn_univ]
[GOAL]
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
src✝ : LieAddGroup 𝓘(𝕜, 𝕜) 𝕜 := normedSpaceLieAddGroup
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiff 𝕜 ⊤ fun p => p.fst * p.snd
[PROOFSTEP]
exact contDiff_mul
