-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem ContinuousLinearMap.continuous_det : Continuous fun f : E →L[𝕜] E => f.det

Proof state:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous fun f => LinearMap.det ↑f

Tactic:
simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]

Result:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous fun f => ((LinearMap.toMatrix b b) ↑f).det

Proof state:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous fun f => (LinearMap.toMatrix b b) ↑f

Tactic:
exact
  ((LinearMap.toMatrix b b).toLinearMap.comp
      (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional

Result:
no goals

Proof state:
case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E)
⊢ Continuous fun f =>
    (if H : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E) then LinearMap.detAux (Trunc.mk ⋯.some) else 1) ↑f

Tactic:
simpa only [h, MonoidHom.one_apply, dif_neg, not_false_iff] using continuous_const

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
⊢ Continuous fun f => LinearMap.det ↑f

Tactic:
by_cases h : ∃ s : Finset E, Nonempty (Basis (↥s) 𝕜 E)

Result:
case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E)
⊢ Continuous fun f => LinearMap.det ↑f

case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E)
⊢ Continuous fun f => LinearMap.det ↑f

Proof state:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
⊢ Continuous fun f => LinearMap.det ↑f

Tactic:
haveI : FiniteDimensional 𝕜 E := FiniteDimensional.of_fintype_basis b

Result:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous fun f => LinearMap.det ↑f

Proof state:
case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E)
⊢ Continuous fun f => LinearMap.det ↑f

Tactic:
rw [LinearMap.det_def]

Result:
case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E)
⊢ Continuous fun f =>
    (if H : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E) then LinearMap.detAux (Trunc.mk ⋯.some) else 1) ↑f

Proof state:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous fun f => ((LinearMap.toMatrix b b) ↑f).det

Tactic:
refine Continuous.matrix_det ?_

Result:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous fun f => (LinearMap.toMatrix b b) ↑f

Proof state:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous fun f => LinearMap.det ↑f

Tactic:
classical
simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]
refine Continuous.matrix_det ?_
exact
  ((LinearMap.toMatrix b b).toLinearMap.comp
      (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
⊢ Continuous fun f => f.det

Tactic:
change Continuous fun f : E →L[𝕜] E => LinearMap.det (f : E →ₗ[𝕜] E)

Result:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
⊢ Continuous fun f => LinearMap.det ↑f

Proof state:
case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 E)
⊢ Continuous fun f => LinearMap.det ↑f

Tactic:
rcases h with ⟨s, ⟨b⟩⟩

Result:
case pos.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis { x // x ∈ s } 𝕜 E
⊢ Continuous fun f => LinearMap.det ↑f