-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem isOpenMap_of_finiteDimensional (f : F →ₗ[𝕜] E) (hf : Function.Surjective f) :
    IsOpenMap f

Proof state:
case intro.refine_1
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
⊢ ContinuousAt (fun y => g (y - f x) + x) (f x)

Tactic:
exact
  ((g.continuous_of_finiteDimensional.comp <| continuous_id.sub continuous_const).add
      continuous_const).continuousAt

Result:
no goals

Proof state:
case intro.refine_2
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
⊢ (fun y => g (y - f x) + x) (f x) = x

Tactic:
simp only

Result:
case intro.refine_2
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
⊢ g (f x - f x) + x = x

Proof state:
case intro.refine_2
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
⊢ g (f x - f x) + x = x

Tactic:
rw [sub_self, map_zero, zero_add]

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
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
⊢ IsOpenMap ⇑f

Tactic:
obtain ⟨g, hg⟩ := f.exists_rightInverse_of_surjective (LinearMap.range_eq_top.2 hf)

Result:
case intro
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
⊢ IsOpenMap ⇑f

Proof state:
case intro
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
⊢ IsOpenMap ⇑f

Tactic:
refine IsOpenMap.of_sections fun x => ⟨fun y => g (y - f x) + x, ?_, ?_, fun y => ?_⟩

Result:
case intro.refine_1
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
⊢ ContinuousAt (fun y => g (y - f x) + x) (f x)

case intro.refine_2
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
⊢ (fun y => g (y - f x) + x) (f x) = x

case intro.refine_3
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
y : E
⊢ f ((fun y => g (y - f x) + x) y) = y

Proof state:
case intro.refine_3
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ⇑f
g : E →ₗ[𝕜] F
hg : f ∘ₗ g = id
x : F
y : E
⊢ f ((fun y => g (y - f x) + x) y) = y

Tactic:
simp only [map_sub, map_add, ← comp_apply f g, hg, id_apply, sub_add_cancel]

Result:
no goals