-- 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:
𝕜 : 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 : Continuous ⇑φ.toEquiv
⊢ Continuous (⇑φ ∘ ⇑(ker l).mkQ)

Tactic:
exact this.comp continuous_quot_mk

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
⊢ induced (⇑φ.toEquiv.symm) inferInstance = UniformSpace.toTopologicalSpace

Tactic:
refine unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
  (continuousSMul_induced φ.symm.toMulActionHom) ?_

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

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

Tactic:
have hlφ : (l : E → 𝕜) = φ ∘ (LinearMap.ker l).mkQ := by ext; rfl

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

Tactic:
by_cases H : finrank 𝕜 (LinearMap.range l) = 0

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 : finrank 𝕜 ↥(range l) = 0
⊢ Continuous ⇑l

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

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

Tactic:
rw [hlφ]

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
this : Continuous ⇑φ.toEquiv
⊢ Continuous (⇑φ ∘ ⇑(ker l).mkQ)

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 : finrank 𝕜 ↥(range l) = 0
⊢ Continuous ⇑l

Tactic:
rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at 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 ⇑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
⊢ Continuous ⇑l

Tactic:
have hi : Function.Injective ((LinearMap.ker l).liftQ l (le_refl _)) := by
  rw [← LinearMap.ker_eq_bot]
  exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)

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 ⋯)
⊢ 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 ⋯)
⊢ Function.Surjective ⇑((ker l).liftQ l ⋯)

Tactic:
rw [← LinearMap.range_eq_top, Submodule.range_liftQ]

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

Tactic:
exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)

Result:
no goals