-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem LinearMap.continuous_of_isClosed_ker (l : E →ₗ[𝕜] 𝕜)
    (hl : IsClosed (LinearMap.ker l : Set E)) :
    Continuous l

Proof state:
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 ↥(range l) = 0
this✝ : finrank 𝕜 ↥(range l) = 1
hi : Function.Injective ⇑((ker l).liftQ l ⋯)
hs : Function.Surjective ⇑((ker l).liftQ l ⋯)
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective ((ker l).liftQ l ⋯) ⋯
hlφ : ⇑l = ⇑φ ∘ ⇑(ker l).mkQ
this : induced (⇑φ.toEquiv.symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ Continuous ⇑φ.toEquiv

Tactic:
exact continuous_coinduced_rng

Result:
no goals

Proof state:
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 ↥(range l) = 0
this : finrank 𝕜 ↥(range l) = 1
hi : Function.Injective ⇑((ker l).liftQ l ⋯)
hs : Function.Surjective ⇑((ker l).liftQ l ⋯)
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective ((ker l).liftQ l ⋯) ⋯
hlφ : ⇑l = ⇑φ ∘ ⇑(ker l).mkQ
⊢ Continuous ⇑l

Tactic:
suffices Continuous φ.toEquiv by
  rw [hlφ]
  exact this.comp continuous_quot_mk

Result:
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 ↥(range l) = 0
this : finrank 𝕜 ↥(range l) = 1
hi : Function.Injective ⇑((ker l).liftQ l ⋯)
hs : Function.Surjective ⇑((ker l).liftQ l ⋯)
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective ((ker l).liftQ l ⋯) ⋯
hlφ : ⇑l = ⇑φ ∘ ⇑(ker l).mkQ
⊢ Continuous ⇑φ.toEquiv

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 ↥(range l) = 0
this : finrank 𝕜 ↥(range l) = 1
hi : Function.Injective ⇑((ker l).liftQ l ⋯)
hs : Function.Surjective ⇑((ker l).liftQ l ⋯)
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective ((ker l).liftQ l ⋯) ⋯
hlφ : ⇑l = ⇑φ ∘ ⇑(ker l).mkQ
⊢ Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
exact fun x y hxy =>
  @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
    (φ.toEquiv.symm.injective.ne hxy)

Result:
no goals

Proof state:
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 ↥(range l) = 0
this : finrank 𝕜 ↥(range l) = 1
hi : Function.Injective ⇑((ker l).liftQ l ⋯)
⊢ Continuous ⇑l

Tactic:
have hs : Function.Surjective ((LinearMap.ker l).liftQ l (le_refl _)) := by
  rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
  exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)

Result:
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 ↥(range l) = 0
this : finrank 𝕜 ↥(range l) = 1
hi : Function.Injective ⇑((ker l).liftQ l ⋯)
hs : Function.Surjective ⇑((ker l).liftQ l ⋯)
⊢ Continuous ⇑l

Proof state:
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 ↥(range l) = 0
this : finrank 𝕜 ↥(range l) = 1
hi : Function.Injective ⇑((ker l).liftQ l ⋯)
hs : Function.Surjective ⇑((ker l).liftQ l ⋯)
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective ((ker l).liftQ l ⋯) ⋯
x✝ : E
⊢ l x✝ = (⇑φ ∘ ⇑(ker l).mkQ) x✝

Tactic:
rfl

Result:
no goals