-- Mathlib/Analysis/Normed/Operator/Banach.lean
lemma bijective_iff_dense_range_and_antilipschitz (f : E →SL[σ] F) :
    Bijective f ↔ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c f

Proof state:
case eq_top
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ (LinearMap.range f).topologicalClosure = ⊤

case anti
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ ∃ c, AntilipschitzWith c ⇑f

case surj
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (LinearMap.range f).topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ Surjective ⇑f

Tactic:
case eq_top => simpa [SetLike.ext'_iff] using h.2.denseRange.closure_eq

Result:
case anti
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ ∃ c, AntilipschitzWith c ⇑f

case surj
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (LinearMap.range f).topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ Surjective ⇑f

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
⊢ Bijective ⇑f ↔ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f

Tactic:
refine ⟨fun h ↦ ⟨?eq_top, ?anti⟩, fun ⟨hd, c, hf⟩ ↦ ⟨hf.injective, ?surj⟩⟩

Result:
case eq_top
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ (LinearMap.range f).topologicalClosure = ⊤

case anti
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ ∃ c, AntilipschitzWith c ⇑f

case surj
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (LinearMap.range f).topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ Surjective ⇑f

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ (LinearMap.range f).topologicalClosure = ⊤

Tactic:
simpa [SetLike.ext'_iff] using h.2.denseRange.closure_eq

Result:
no goals

Proof state:
case anti
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective ⇑f
⊢ ∃ c, AntilipschitzWith c ⇑f

case surj
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (LinearMap.range f).topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ Surjective ⇑f

Tactic:
case anti =>
  refine ⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩ <;>
  simp only [LinearMap.range_eq_top, LinearMapClass.ker_eq_bot, h.1, h.2]

Result:
case surj
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (LinearMap.range f).topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ Surjective ⇑f