-- 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
⊢ Continuous ⇑l

Tactic:
have : finrank 𝕜 (LinearMap.range l) = 1 :=
  le_antisymm (finrank_self 𝕜 ▸ l.range.finrank_le) (zero_lt_iff.mpr H)

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
⊢ 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
⊢ Continuous ⇑φ.toEquiv

Tactic:
have : induced φ.toEquiv.symm inferInstance = hnorm.toUniformSpace.toTopologicalSpace := by
  refine unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
    (continuousSMul_induced φ.symm.toMulActionHom) ?_
  rw [t2Space_iff]
  exact fun x y hxy =>
    @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
      (φ.toEquiv.symm.injective.ne hxy)

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
this : induced (⇑φ.toEquiv.symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ 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
⊢ Function.Injective ⇑((ker l).liftQ l ⋯)

Tactic:
rw [← LinearMap.ker_eq_bot]

Result:
𝕜 : 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
⊢ ker ((ker l).liftQ l ⋯) = ⊥

Proof state:
case pos
𝕜 : 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 : l = 0
⊢ Continuous ⇑0

Tactic:
exact continuous_zero

Result:
no goals

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
⊢ T2Space 𝕜

Tactic:
rw [t2Space_iff]

Result:
𝕜 : 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

Proof state:
case pos
𝕜 : 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 : l = 0
⊢ Continuous ⇑l

Tactic:
rw [H]

Result:
case pos
𝕜 : 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 : l = 0
⊢ Continuous ⇑0

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 ⋯)
⊢ Continuous ⇑l

Tactic:
let φ : (E ⧸ LinearMap.ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective ((LinearMap.ker l).liftQ l (le_refl _)) ⟨hi, hs⟩

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 ⋯) ⋯
⊢ Continuous ⇑l

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 ⋯)
⊢ range l = ⊤

Tactic:
exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)

Result:
no goals

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 ⋯) ⋯
⊢ ⇑l = ⇑φ ∘ ⇑(ker l).mkQ

Tactic:
ext

Result:
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✝