[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
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h : G
⊢ 𝑳 I (g * h) = ContMDiffMap.comp (𝑳 I g) (𝑳 I h)
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : 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
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h x✝ : G
⊢ ↑(𝑳 I (g * h)) x✝ = ↑(ContMDiffMap.comp (𝑳 I g) (𝑳 I h)) x✝
[PROOFSTEP]
simp only [ContMDiffMap.comp_apply, L_apply, mul_assoc]
[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
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h : G
⊢ 𝑹 I (g * h) = ContMDiffMap.comp (𝑹 I h) (𝑹 I g)
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : 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
G✝ : Type u_4
inst✝¹² : Mul G✝
inst✝¹¹ : TopologicalSpace G✝
inst✝¹⁰ : ChartedSpace H G✝
inst✝⁹ : SmoothMul I G✝
E' : Type u_5
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H' M
g✝ h✝ : G✝
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : SmoothMul I G
g h x✝ : G
⊢ ↑(𝑹 I (g * h)) x✝ = ↑(ContMDiffMap.comp (𝑹 I h) (𝑹 I g)) x✝
[PROOFSTEP]
simp only [ContMDiffMap.comp_apply, R_apply, mul_assoc]
[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
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
⊢ Smooth I I fun a => a ^ 0
[PROOFSTEP]
simp only [pow_zero]
[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
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
⊢ Smooth I I fun a => 1
[PROOFSTEP]
exact smooth_const
[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
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
k : ℕ
⊢ Smooth I I fun a => a ^ (k + 1)
[PROOFSTEP]
simpa [pow_succ] using smooth_id.mul (smooth_pow _)
[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
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
f g : SmoothMonoidMorphism I I' G G'
h : (fun a => a.toFun) f = (fun a => a.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
𝕜 : 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
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
g : SmoothMonoidMorphism I I' G G'
toMonoidHom✝ : G →* G'
smooth_toFun✝ : Smooth I I' toMonoidHom✝.toFun
h : (fun a => a.toFun) { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ } = (fun a => a.toFun) g
⊢ { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
𝕜 : 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
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
toMonoidHom✝¹ : G →* G'
smooth_toFun✝¹ : Smooth I I' toMonoidHom✝¹.toFun
toMonoidHom✝ : G →* G'
smooth_toFun✝ : Smooth I I' toMonoidHom✝.toFun
h :
  (fun a => a.toFun) { toMonoidHom := toMonoidHom✝¹, smooth_toFun := smooth_toFun✝¹ } =
    (fun a => a.toFun) { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, smooth_toFun := smooth_toFun✝¹ } =
    { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMonoidHom
𝕜 : 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
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : SmoothMul I G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : SmoothMul I' G'
toMonoidHom✝¹ : G →* G'
smooth_toFun✝¹ : Smooth I I' toMonoidHom✝¹.toFun
toMonoidHom✝ : G →* G'
smooth_toFun✝ : Smooth I I' toMonoidHom✝.toFun
h :
  (fun a => a.toFun) { toMonoidHom := toMonoidHom✝¹, smooth_toFun := smooth_toFun✝¹ } =
    (fun a => a.toFun) { toMonoidHom := toMonoidHom✝, smooth_toFun := smooth_toFun✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), i ∈ t → ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i in t, f i x) s x
[PROOFSTEP]
simp only [← Finset.prod_apply]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), i ∈ t → ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt I' I n (fun x => Finset.prod t (fun c => f c) x) s x
[PROOFSTEP]
exact contMDiffWithinAt_finset_prod' h
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), ContMDiff I' I n (f i)
hfin : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (i : ι), f i x
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x✝ : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), ContMDiff I' I n (f i)
hfin : LocallyFinite fun i => mulSupport (f i)
x : M
⊢ ContMDiffAt I' I n (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
rcases finprod_eventually_eq_prod hfin x with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s✝ : Set M
x✝ : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
h : ∀ (i : ι), ContMDiff I' I n (f i)
hfin : LocallyFinite fun i => mulSupport (f i)
x : M
s : Finset ι
hs : ∀ᶠ (y : M) in nhds x, ∏ᶠ (i : ι), f i y = ∏ i in s, f i y
⊢ ContMDiffAt I' I n (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
exact (contMDiff_finset_prod (fun i _ => h i) x).congr_of_eventuallyEq hs
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (i : ι) (_ : p i), f i x
[PROOFSTEP]
simp only [← finprod_subtype_eq_finprod_cond]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
n : ℕ∞
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (j : { i // p i }), f (↑j) x
[PROOFSTEP]
exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Smooth (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) 𝓘(𝕜, E) fun p => p.fst + p.snd
[PROOFSTEP]
rw [← modelWithCornersSelf_prod]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Smooth 𝓘(𝕜, E × E) 𝓘(𝕜, E) fun p => p.fst + p.snd
[PROOFSTEP]
exact contDiff_add.contMDiff
[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
G : Type u_4
inst✝⁸ : DivInvMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : SmoothMul I G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : M → G
s : Set M
x : M
n : ℕ∞
c : G
hf : ContMDiffWithinAt I' I n f s x
⊢ ContMDiffWithinAt I' I n (fun x => f x / c) s x
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul contMDiffWithinAt_const
