-- Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
theorem contDiffOn_clm_apply {f : D → E →L[𝕜] F} {s : Set D} [FiniteDimensional 𝕜 E] :
    ContDiffOn 𝕜 n f s ↔ ∀ y, ContDiffOn 𝕜 n (fun x => f x y) s

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F := (e₁.arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContDiffOn 𝕜 n ((⇑e₂.symm ∘ ⇑e₂) ∘ f) s

Tactic:
exact e₂.symm.contDiff.comp_contDiffOn (contDiffOn_pi.mpr fun i => h _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
⊢ ContDiffOn 𝕜 n f s

Tactic:
let d := finrank 𝕜 E

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
⊢ ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
⊢ ContDiffOn 𝕜 n f s ↔ ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s

Tactic:
refine ⟨fun h y => h.clm_apply contDiffOn_const, fun h => ?_⟩

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
⊢ ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
⊢ ContDiffOn 𝕜 n f s

Tactic:
have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
⊢ ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
⊢ ContDiffOn 𝕜 n f s

Tactic:
let e₁ := ContinuousLinearEquiv.ofFinrankEq hd

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
⊢ ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
⊢ ContDiffOn 𝕜 n f s

Tactic:
let e₂ := (e₁.arrowCongr (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing (Fin d))

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F := (e₁.arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F := (e₁.arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContDiffOn 𝕜 n f s

Tactic:
rw [← id_comp f, ← e₂.symm_comp_self]

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
s : Set D
inst✝ : FiniteDimensional 𝕜 E
h : ∀ (y : E), ContDiffOn 𝕜 n (fun x => (f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F := (e₁.arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContDiffOn 𝕜 n ((⇑e₂.symm ∘ ⇑e₂) ∘ f) s