-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem ContinuousLinearMap.isOpen_injective [FiniteDimensional 𝕜 E] :
    IsOpen { L : E →L[𝕜] F | Injective L }

Proof state:
case intro.intro
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}

Tactic:
filter_upwards [this] with φ hφ

Result:
case h
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
⊢ Injective ⇑φ

Proof state:
case h
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
⊢ ∃ K > 0, AntilipschitzWith K ⇑↑φ

Tactic:
exact ⟨(K⁻¹ - ‖φ - φ₀‖₊)⁻¹, inv_pos_of_pos (tsub_pos_of_lt hφ),
  H.add_sub_lipschitzWith (φ - φ₀).lipschitz hφ⟩

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
⊢ IsOpen {L | Injective ⇑L}

Tactic:
rw [isOpen_iff_eventually]

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
⊢ ∀ x ∈ {L | Injective ⇑L}, ∀ᶠ (y : E →L[𝕜] F) in 𝓝 x, y ∈ {L | Injective ⇑L}

Proof state:
case intro.intro
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}

Tactic:
have : ∀ᶠ φ in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹ := eventually_nnnorm_sub_lt _ <| inv_pos_of_pos K_pos

Result:
case intro.intro
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}

Tactic:
rcases φ₀.injective_iff_antilipschitz.mp hφ₀ with ⟨K, K_pos, H⟩

Result:
case intro.intro
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
⊢ ∀ x ∈ {L | Injective ⇑L}, ∀ᶠ (y : E →L[𝕜] F) in 𝓝 x, y ∈ {L | Injective ⇑L}

Tactic:
rintro φ₀ hφ₀

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀, y ∈ {L | Injective ⇑L}

Proof state:
case h
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
⊢ Injective ⇑φ

Tactic:
apply φ.injective_iff_antilipschitz.mpr

Result:
case h
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ : φ₀ ∈ {L | Injective ⇑L}
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith K ⇑↑φ₀
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
⊢ ∃ K > 0, AntilipschitzWith K ⇑↑φ