-- Mathlib/Analysis/LocallyConvex/WeakSpace.lean
theorem LinearEquiv.image_closure_of_convex' {s : Set E} (hs : Convex ℝ s) (e : E ≃ₗ[𝕜] F)
    (e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜))
    (he : ∀ f : F →L[𝕜] 𝕜, (e_dual f : E →ₗ[𝕜] 𝕜) = e.dualMap f) :
    e '' (closure s) = closure (e '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
he : ∀ (f : F →L[𝕜] 𝕜), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : E →L[𝕜] 𝕜), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ⇑e '' closure s = closure (⇑e '' s)

Tactic:
refine e.image_closure_of_convex hs ?_ ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
he : ∀ (f : F →L[𝕜] 𝕜), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : E →L[𝕜] 𝕜), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : F →L[𝕜] 𝕜), Continuous ⇑(e.dualMap ↑f)

case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
he : ∀ (f : F →L[𝕜] 𝕜), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : E →L[𝕜] 𝕜), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : E →L[𝕜] 𝕜), Continuous ⇑(e.symm.dualMap ↑f)

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
he : ∀ (f : F →L[𝕜] 𝕜), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : E →L[𝕜] 𝕜), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : F →L[𝕜] 𝕜), Continuous ⇑(e.dualMap ↑f)

Tactic:
simpa [← he] using fun f ↦ map_continuous (e_dual f)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
f : E →L[𝕜] 𝕜
he : ∀ (f : F →L[𝕜] 𝕜), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : E →L[𝕜] 𝕜), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
⊢ ⇑(e_dual.symm f) = ⇑(e.symm.dualMap ↑f)

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
f : E →L[𝕜] 𝕜
he : ∀ (f : F →L[𝕜] 𝕜), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : E →L[𝕜] 𝕜), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
⊢ (e_dual.symm f) x = (e.symm.dualMap ↑f) x

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
f : E →L[𝕜] 𝕜
he : ∀ (f : F →L[𝕜] 𝕜), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : E →L[𝕜] 𝕜), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
⊢ (e_dual.symm f) x = (e.symm.dualMap ↑f) x

Tactic:
conv_rhs => rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
f : E →L[𝕜] 𝕜
he : ∀ (f : F →L[𝕜] 𝕜), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : E →L[𝕜] 𝕜), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
⊢ (e_dual.symm f) x = (⇑(e_dual.symm f) ∘ ⇑e) (e.symm x)

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
he : ∀ (f : F →L[𝕜] 𝕜), ↑(e_dual f) = e.dualMap ↑f
he' : ∀ (f : E →L[𝕜] 𝕜), ↑(e_dual.symm f) = e.symm.dualMap ↑f
⊢ ∀ (f : E →L[𝕜] 𝕜), Continuous ⇑(e.symm.dualMap ↑f)

Tactic:
simpa [← he'] using fun f ↦ map_continuous (e_dual.symm f)

Result:
no goals