case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : finrank 𝕜 { x // x ∈ range l } = 0
⊢ Continuous ↑l

case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
⊢ Continuous ↑l
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
⊢ Continuous ↑l
by_cases H : finrank 𝕜 (LinearMap.range l) = 0
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : l = 0
⊢ Continuous ↑l
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : finrank 𝕜 { x // x ∈ range l } = 0
⊢ Continuous ↑l
rw [finrank_eq_zero, LinearMap.range_eq_bot] at H
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : l = 0
⊢ Continuous ↑0
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : l = 0
⊢ Continuous ↑l
rw [H]
no goals
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : l = 0
⊢ Continuous ↑0
exact continuous_zero
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ Continuous ↑l
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
⊢ Continuous ↑l
have : finrank 𝕜 (LinearMap.range l) = 1 :=
  le_antisymm (finrank_self 𝕜 ▸ l.range.finrank_le) (zero_lt_iff.mpr H)
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Continuous ↑l
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ Continuous ↑l
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 _)
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Continuous ↑l
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Continuous ↑l
have hs : Function.Surjective ((LinearMap.ker l).liftQ l (le_refl _)) := by
  rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
  exact eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
⊢ Continuous ↑l
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Continuous ↑l
let φ : (E ⧸ LinearMap.ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective ((LinearMap.ker l).liftQ l (le_refl _)) ⟨hi, hs⟩
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ Continuous ↑l
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
⊢ Continuous ↑l
have hlφ : (l : E → 𝕜) = φ ∘ (LinearMap.ker l).mkQ := by ext; rfl
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ Continuous ↑l
suffices Continuous φ.toEquiv by
  rw [hlφ]
  exact this.comp continuous_quot_mk
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
have : induced φ.toEquiv.symm inferInstance = hnorm.toUniformSpace.toTopologicalSpace := by
  refine'
    unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
      (continuousSMul_induced φ.symm.toLinearMap) _
  refine (@t2Space_iff 𝕜 (induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance)).mpr ?_
  exact fun x y hxy =>
    @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
      (φ.toEquiv.symm.injective.ne hxy)
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
rw [this.symm, Equiv.induced_symm]
no goals
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
exact continuous_coinduced_rng
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ ker (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) = ⊥
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
rw [← LinearMap.ker_eq_bot]
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ ker (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) = ⊥
exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ range l = ⊤
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ range l = ⊤
exact eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
x✝ : E
⊢ ↑l x✝ = (↑φ ∘ ↑(Submodule.mkQ (ker l))) x✝
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
⊢ ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
ext
no goals
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
x✝ : E
⊢ ↑l x✝ = (↑φ ∘ ↑(Submodule.mkQ (ker l))) x✝
rfl
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : Continuous ↑(LinearEquiv.toEquiv φ)
⊢ Continuous (↑φ ∘ ↑(Submodule.mkQ (ker l)))
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : Continuous ↑(LinearEquiv.toEquiv φ)
⊢ Continuous ↑l
rw [hlφ]
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : Continuous ↑(LinearEquiv.toEquiv φ)
⊢ Continuous (↑φ ∘ ↑(Submodule.mkQ (ker l)))
exact this.comp continuous_quot_mk
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ T2Space 𝕜
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
refine'
  unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
    (continuousSMul_induced φ.symm.toLinearMap) _
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ ∀ (x y : 𝕜), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ T2Space 𝕜
refine (@t2Space_iff 𝕜 (induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance)).mpr ?_
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜 E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : TopologicalAddGroup E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalAddGroup F
inst✝⁵ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁴ : AddCommGroup F'
inst✝³ : Module 𝕜 F'
inst✝² : TopologicalSpace F'
inst✝¹ : TopologicalAddGroup F'
inst✝ : ContinuousSMul 𝕜 F'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ ∀ (x y : 𝕜), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
exact fun x y hxy =>
  @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
    (φ.toEquiv.symm.injective.ne hxy)