awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x : E |
      ∀ (i : StrongDual 𝕜 E) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1} =
    s
have refine : ∀ (x : E)
  (hx :
    Membership.mem (γ := Set E)
      {x : E |
        ∀ (i : StrongDual 𝕜 E) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
          (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
      x),
  x ∈ s
Tactic: refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l c hc => hc x hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E |
      ∀ (i : StrongDual 𝕜 E) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
    x
⊢ x ∈ s
have by_contra : ∀ (h : x ∉ s), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E |
      ∀ (i : StrongDual 𝕜 E) (i_1 : ℝ) (i_2 : ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) y : 𝕜) ≤ i_1),
        (re : (a : 𝕜) → ℝ) ((i : (a : E) → 𝕜) x : 𝕜) ≤ i_1}
    x
h : x ∉ s
⊢ False
have obtain : ∀ (l : StrongDual 𝕜 E) (c : ℝ) (hls : ∀ a ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) a : 𝕜) < c)
  (hl : c < (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) x : 𝕜)), False
Tactic: obtain ⟨l, c, hls, hl⟩ := geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs₁ hs₂ h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
⊢ ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ), ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨0, 0, fun _ _ ↦ by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
this : Nonempty ι
⊢ ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ), ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s
have this₁ : ⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i} = s
Tactic: have : ⋂ i : ι, { x | re (l i x) ≤ c i } = s := by
    simpa only [ι, iInter_sigma, iInter_subtype, l, c] using iInter_halfSpaces_eq' hs₁ hs₂
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : RCLike 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c }
l : ι → StrongDual 𝕜 E :=
  fun (lc : ι) ↦
    lc.fst (β := fun (l : StrongDual 𝕜 E) ↦ { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })
c : ι → ℝ :=
  fun (lc : ι) ↦
    (↑(lc.snd (β := fun (l : StrongDual 𝕜 E) ↦
          { c : ℝ // ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l : (a : E) → 𝕜) y : 𝕜) ≤ c })) :
      ℝ)
hc : ∀ (i : ι), ∀ y ∈ s, (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) y : 𝕜) ≤ c i := ⋯
this_1 : Nonempty ι
this : ⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i} = s
⊢ ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ), ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s
have obtain : ∀ (k : ℕ → ι)
  (hk :
    Eq.{u_2 + 1} (α := Set E) (⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l (k n) : (a : E) → 𝕜) x : 𝕜) ≤ c (k n)})
      (⋂ (i : ι), {x : E | (re : (a : 𝕜) → ℝ) ((l i : (a : E) → 𝕜) x : 𝕜) ≤ c i})),
  ∃ (l : ℕ → StrongDual 𝕜 E) (c : ℕ → ℝ), ⋂ (n : ℕ), {x : E | (re : (a : 𝕜) → ℝ) ((l n : (a : E) → 𝕜) x : 𝕜) ≤ c n} = s
Tactic: obtain ⟨k, hk⟩ := eq_closed_inter_nat (fun i : ι ↦ { x | re (l i x) ≤ c i })
    (fun i ↦ isClosed_le (continuous_re.comp (l i).continuous) continuous_const)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.StrongTopology (goal)
Goal:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalAddGroup F
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : Module 𝕜₁ E
inst_10 : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst_11 : Module R F
inst_12 : ContinuousConstSMul R F
inst_13 : LocallyConvexSpace R F
inst_14 : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
⊢ LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖)
have apply : ∀ (i : Prod.{u_4, u_5} (Set E) (Set F)),
  i.1 ∈ 𝔖 ∧ Membership.mem (γ := Filter F) (𝓝 0) i.2 ∧ Convex R i.2 →
    Convex R (E := UniformConvergenceCLM σ F 𝔖)
      {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ i.1, Membership.mem (α := F) (id i.2) ((f : (a : E) → F) x : F)}
Tactic: apply LocallyConvexSpace.ofBasisZero _ _ _ _
    (UniformConvergenceCLM.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂
      (LocallyConvexSpace.convex_basis_zero R F)) _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h :
  ∀ (x : E) (y : F⋆),
    Eq.{u_2 + 1} (α := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F) : 𝕜₂)
      ((y : (a : F) → 𝕜₂) ((B : (a : E) → F) x : F) : 𝕜₂)
⊢ A = B
have simp_rw : ∀ (x : E) (x_1 : F →L[𝕜₂] 𝕜₂),
  Eq.{u_2 + 1} (α := 𝕜₂)
    ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((A : (a : E) → F) x) :
            (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
          (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
        x_1 :
      𝕜₂)
    ((((LinearMap.flip (ContinuousLinearMap.coeLM 𝕜₂) : (a : F) → (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) ((B : (a : E) → F) x) :
            (F →L[𝕜₂] 𝕜₂) →ₗ[𝕜₂] 𝕜₂) :
          (a : F →L[𝕜₂] 𝕜₂) → 𝕜₂)
        x_1 :
      𝕜₂)
Tactic: simp_rw [ContinuousLinearMapWOT.ext_iff, ← (separatingDual_iff_injective.mp H).eq_iff,
    LinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x y : E →SWOT[σ] F
⊢ (fun (x_1 : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x_1 with
      | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x + y : (a : E) → F) x_2 : F)) =
    HAdd.hAdd (α := E × F⋆ → 𝕜₂)
      (fun (x_1 : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x_1 with
        | (x_2, y) => (y : (a : F) → 𝕜₂) ((x : (a : E) → F) x_2 : F))
      fun (x : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x with
      | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F)
have h : ∀ (x_1 : E × F⋆),
  (match (motive := E × F⋆ → 𝕜₂) x_1 with
    | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x + y : (a : E) → F) x_2 : F)) =
    HAdd.hAdd (α := E × F⋆ → 𝕜₂) (β := E × F⋆ → 𝕜₂)
      (fun (x_2 : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x_2 with
        | (x_3, y) => (y : (a : F) → 𝕜₂) ((x : (a : E) → F) x_3 : F))
      (fun (x : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x with
        | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
x : 𝕜₂
y : E →SWOT[σ] F
⊢ (fun (x_1 : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x_1 with
      | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x • y : (a : E) → F) x_2 : F)) =
    HSMul.hSMul (α := 𝕜₂) (β := E × F⋆ → 𝕜₂) ((RingHom.id 𝕜₂ : (a : 𝕜₂) → 𝕜₂) x : 𝕜₂) fun (x : E × F⋆) ↦
      match (motive := E × F⋆ → 𝕜₂) x with
      | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F)
have h : ∀ (x_1 : E × F⋆),
  (match (motive := E × F⋆ → 𝕜₂) x_1 with
    | (x_2, y_1) => (y_1 : (a : F) → 𝕜₂) ((x • y : (a : E) → F) x_2 : F)) =
    HSMul.hSMul (α := 𝕜₂) (β := E × F⋆ → 𝕜₂) ((RingHom.id 𝕜₂ : (a : 𝕜₂) → 𝕜₂) x : 𝕜₂)
      (fun (x : E × F⋆) ↦
        match (motive := E × F⋆ → 𝕜₂) x with
        | (x, y_1) => (y_1 : (a : F) → 𝕜₂) ((y : (a : E) → F) x : F))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : SeparatingDual 𝕜₂ F
⊢ IsEmbedding (X := E →SWOT[σ] F) (Y := E × F⋆ → 𝕜₂) (⇑(inducingFn σ E F) : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂)
have refine : ∀ (A B : E →SWOT[σ] F)
  (hAB :
    Eq (α := E × F⋆ → 𝕜₂) ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) A : E × F⋆ → 𝕜₂)
      ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) B : E × F⋆ → 𝕜₂)),
  A = B
Tactic: refine Function.Injective.isEmbedding_induced fun A B hAB => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
inst_10 : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
hAB :
  Eq (α := E × F⋆ → 𝕜₂) ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) A : E × F⋆ → 𝕜₂)
    ((inducingFn σ E F : (a : E →SWOT[σ] F) → E × F⋆ → 𝕜₂) B : E × F⋆ → 𝕜₂)
⊢ A = B
have rw : ∀ (x : E) (y : F⋆),
  Eq.{u_2 + 1} (α := 𝕜₂) ((y : (a : F) → 𝕜₂) ((A : (a : E) → F) x : F) : 𝕜₂)
    ((y : (a : F) → 𝕜₂) ((B : (a : E) → F) x : F) : 𝕜₂)
Tactic: rw [ContinuousLinearMapWOT.ext_dual_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst_10 : DistribSMul S F
inst_11 : SMulCommClass 𝕜₂ S F
inst_12 : ContinuousConstSMul S F
inst_13 : SMul S 𝕜₂
inst_14 : IsScalarTower S 𝕜₂ 𝕜₂
inst_15 : IsScalarTower S 𝕜₂ F
c : S
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (x : F →WOT[𝕜₂] F) ↦ c • x
have apply : ∀ (x : F) (x_1 : F⋆),
  Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
    (x_1 : (a : F) → 𝕜₂) ((c • a : (a : F) → F) x : F)
Tactic: apply continuous_of_dual_apply_continuous fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : Module 𝕜₁ E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : Module 𝕜₂ F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst_10 : DistribSMul S F
inst_11 : SMulCommClass 𝕜₂ S F
inst_12 : ContinuousConstSMul S F
inst_13 : SMul S 𝕜₂
inst_14 : IsScalarTower S 𝕜₂ 𝕜₂
inst_15 : IsScalarTower S 𝕜₂ F
c : S
x : F
x_1 : F⋆
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
    (x_1 : (a : F) → 𝕜₂) ((c • a : (a : F) → F) x : F)
have simp : Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : F →WOT[𝕜₂] F) ↦
  HSMul.hSMul (β := 𝕜₂) c ((x_1 : (a : F) → 𝕜₂) ((a : (a : F) → F) x : F) : 𝕜₂)
Tactic: simp only [smul_apply, ContinuousLinearMap.map_smul_of_tower]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (f : E →SWOT[σ₁₂] F) ↦ g.comp f
have refine : ∀ (x : E) (z : StrongDual 𝕜₃ G),
  Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)
Tactic: refine continuous_of_dual_apply_continuous fun x z ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (hypothesis)
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)
have σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
Tactic: have σ_bij : Function.Bijective σ₂₃ := ⟨σ₂₃.injective, RingHomSurjective.is_surjective⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
| Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)
have h : ∀ (a : E →SWOT[σ₁₂] F), ((z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G) : 𝕜₃)
Tactic: enter [1, a]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
a : E →SWOT[σ₁₂] F
| ((z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G) : 𝕜₃)
have h : ((σ_li : (a : 𝕜₂) → 𝕜₃)
    ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) :
      𝕜₂) :
  𝕜₃)
Tactic: rw [← σ_li.apply_symm_apply (z _), comp_apply, ← toCLM_apply]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
| Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)
have h : ∀ (a : E →SWOT[σ₁₂] F),
  ((σ_li : (a : 𝕜₂) → 𝕜₃)
      ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) :
        𝕜₂) :
    𝕜₃)
Tactic: enter [1, a]; rw [← σ_li.apply_symm_apply (z _), comp_apply, ← toCLM_apply]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakOperatorTopology (goal)
Goal:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : AddCommGroup E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup F
inst_8 : TopologicalSpace F
inst_9 : Module 𝕜₂ F
inst_10 : AddCommGroup G
inst_11 : TopologicalSpace G
inst_12 : Module 𝕜₃ G
inst_13 : IsTopologicalAddGroup F
inst_14 : ContinuousConstSMul 𝕜₂ F
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
inst_17 : RingHomSurjective σ₂₃
inst_18 : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective.{u_6 + 1, u_7 + 1} (α := 𝕜₂) (β := 𝕜₃) (⇑σ₂₃ : (a : 𝕜₂) → 𝕜₃)
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) := ⋯
invPair_symm : RingHomInvPair (↑σ_equiv.symm : 𝕜₃ →+* 𝕜₂) σ₂₃ := ⋯
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv : 𝕜₂ ≃ₛₗ[σ₂₃] 𝕜₃ := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
    (z : (a : G) → 𝕜₃) ((g.comp a : (a : E) → G) x : G)
have conv : Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : E →SWOT[σ₁₂] F) ↦
  (σ_li : (a : 𝕜₂) → 𝕜₃)
    ((σ_li.symm : (a : 𝕜₃) → 𝕜₂) ((z : (a : G) → 𝕜₃) ((g.toCLM : (a : F) → G) ((a : (a : E) → F) x : F) : G) : 𝕜₃) : 𝕜₂)
Tactic: conv => enter [1, a]; rw [← σ_li.apply_symm_apply (z _), comp_apply, ← toCLM_apply]