-- 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
⊢ ⇑e '' closure s = closure (⇑e '' s)

Tactic:
have he' (f : E →L[𝕜] 𝕜) : (e_dual.symm f : F →ₗ[𝕜] 𝕜) = e.symm.dualMap f := by
  simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢
  have (g : E →L[𝕜] 𝕜) : ⇑g = e_dual.symm g ∘ e := by
    have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
    simpa
  ext x
  conv_rhs => rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]
  simp

Result:
𝕜 : 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)

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)
⊢ ⇑(e_dual.symm f) = ⇑(e.symm.dualMap ↑f)

Tactic:
have (g : E →L[𝕜] 𝕜) : ⇑g = e_dual.symm g ∘ e := by
  have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
  simpa

Result:
𝕜 : 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)

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
f : E →L[𝕜] 𝕜
⊢ ↑(e_dual.symm f) = e.symm.dualMap ↑f

Tactic:
simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢

Result:
𝕜 : 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)
⊢ ⇑(e_dual.symm f) = ⇑(e.symm.dualMap ↑f)

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_dual.symm f) ∘ ⇑e) (e.symm x)

Tactic:
simp

Result:
no goals