awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
s : Finset ι
rw :
  Membership.mem (γ := Filter E) (⨅ (i : ι), ⨅ (h : i ∈ s), 𝓝 0)
    (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)
| Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)

Tactic:
rw [letI := t₂ s; Seminorm.continuous_iff one_pos, nhds_iInf, iInf_subtype]

Premises used: nhds_iInf, iInf_subtype, Seminorm.continuous_iff, one_pos
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
conv :
  Membership.mem (γ := Filter E) (⨅ (i : ι), 𝓝 0)
      (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1) ↔
    ∃ (s : Finset ι),
      Membership.mem (γ := Filter E) (⨅ (i : ι), ⨅ (h : i ∈ s), 𝓝 0)
        (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)
⊢ Membership.mem (γ := Filter E) (⨅ (i : ι), 𝓝 0)
      (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1) ↔
    ∃ (s : Finset ι), Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)

Tactic:
conv in Continuous _ =>
    rw [letI := t₂ s; Seminorm.continuous_iff one_pos, nhds_iInf, iInf_subtype]

Premises used: nhds_iInf, Continuous, iInf_subtype
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
t₂ : (s : Finset ι) → TopologicalSpace E := fun (s : Finset ι) ↦ ⨅ (i : ↥s), induced (⇑(f (↑i : ι)) : (a : E) → 𝕜) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
rw rw₁ :
  (∃ (t : Finset ι),
      Membership.mem (γ := Filter E) (⨅ i ∈ t, 𝓝 0)
        (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)) ↔
    ∃ (s : Finset ι),
      Membership.mem (γ := Filter E) (⨅ (i : ι), ⨅ (h : i ∈ s), 𝓝 0)
        (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)
⊢ Membership.mem (γ := Filter E) (⨅ (i : ι), 𝓝 0)
      (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1) ↔
    ∃ (s : Finset ι),
      Membership.mem (γ := Filter E) (⨅ (i : ι), ⨅ (h : i ∈ s), 𝓝 0)
        (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)

Tactic:
rw [Filter.mem_iInf_finite]

Premises used: Filter.mem_iInf_finite
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
⊢ IsTopologicalAddGroup E

Tactic:
have : IsTopologicalAddGroup E := topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this : IsTopologicalAddGroup E
simp_rw :
  Eq.{u_6 + 1} (α := Filter E)
    (⨅ (i : ι), Filter.comap (Function.comp.{u_6 + 1, u_5 + 1, 1} (β := 𝕜) norm (⇑(f i) : (a : E) → 𝕜)) (𝓝 0))
    (⨅ (i : ι), Filter.comap (β := ℝ) (⇑(f i).toSeminorm : (a : E) → ℝ) (𝓝 0))
⊢ WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm

Tactic:
simp_rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_iInf, nhds_induced, map_zero,
      ← comap_norm_nhds_zero (E := 𝕜), Filter.comap_comap]

Premises used: nhds_iInf, comap_norm_nhds_zero, map_zero, Filter.comap_comap, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_induced
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this : IsTopologicalAddGroup E
⊢ Eq.{u_6 + 1} (α := Filter E)
    (⨅ (i : ι), Filter.comap (Function.comp.{u_6 + 1, u_5 + 1, 1} (β := 𝕜) norm (⇑(f i) : (a : E) → 𝕜)) (𝓝 0))
    (⨅ (i : ι), Filter.comap (β := ℝ) (⇑(f i).toSeminorm : (a : E) → ℝ) (𝓝 0))

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this : IsTopologicalAddGroup E
⊢ WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm

Tactic:
have : WithSeminorms (fun i ↦ (f i).toSeminorm) := by
    simp_rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_iInf, nhds_induced, map_zero,
      ← comap_norm_nhds_zero (E := 𝕜), Filter.comap_comap]
    rfl
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
rw :
  Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜) ↔
    ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)

Tactic:
rw [LinearMap.mem_span_iff_continuous]

Premises used: LinearMap.mem_span_iff_continuous
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
mp :
  Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜) →
    ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)
mpr :
  (∃ (s : Finset ι) (c : ℝ≥0),
      φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)) →
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)
⊢ Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜) ↔
    ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
H : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)
⊢ Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, _]
    (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)

Tactic:
rw [WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const] at H

Premises used: norm_withSeminorms, forall_const, WithSeminorms.continuous_iff_continuous_comp
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
H :
  Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, _]
    (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
mp :
  ∀ (s : Finset ι) (C : ℝ≥0)
    (hC :
      Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ ≤
        HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (i : ι) ↦ (f i).toSeminorm)),
    ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)
⊢ ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)

Tactic:
rcases Seminorm.bound_of_continuous this _ H with ⟨s, C, -, hC⟩

Premises used: Seminorm.bound_of_continuous
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
H :
  Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, _]
    (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
s : Finset ι
C : ℝ≥0
hC :
  Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ ≤
    HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (i : ι) ↦ (f i).toSeminorm)
⊢ ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)

Tactic:
⟨s, C, hC⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
H :
  Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, _]
    (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
s : Finset ι
C : ℝ≥0
hC :
  Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ ≤
    HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (i : ι) ↦ (f i).toSeminorm)
⊢ ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)

Tactic:
exact ⟨s, C, hC⟩
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
H : ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)
⊢ Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)

Tactic:
WithSeminorms.continuous_normedSpace_rng _ this _ H

Premises used: WithSeminorms.continuous_normedSpace_rng
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
this_1 : IsTopologicalAddGroup E
this : WithSeminorms.{u_5, u_6, u_4} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (f i).toSeminorm
H : ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)
⊢ Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)

Tactic:
exact WithSeminorms.continuous_normedSpace_rng _ this _ H

Premises used: WithSeminorms.continuous_normedSpace_rng
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
f : StrongDual.{u_5, u_6} 𝕜 (WeakBilin B)
⊢ Membership.mem (γ := Submodule 𝕜 (LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id 𝕜) (WeakBilin B) 𝕜))
    (Submodule.span 𝕜 (↑(ContinuousLinearMap.coeLM 𝕜 ∘ₗ WeakBilin.eval B).range : Set (WeakBilin B →ₗ[𝕜] 𝕜)))
    (↑f : WeakBilin B →ₗ[𝕜] 𝕜)

Tactic:
simpa [coe_range, mem_span_iff_continuous, continuous_iff_le_induced, ← induced_to_pi] using
      f.continuous.le_induced

Premises used: LinearMap.coe_range, continuous_iff_le_induced, ContinuousLinearMap.continuous, Continuous.le_induced, induced_to_pi, LinearMap.mem_span_iff_continuous
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
f : StrongDual.{u_5, u_6} 𝕜 (WeakBilin B)
⊢ Membership.mem (γ := Submodule 𝕜 (LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id 𝕜) (WeakBilin B) 𝕜))
    (Submodule.span 𝕜 (↑(ContinuousLinearMap.coeLM 𝕜 ∘ₗ WeakBilin.eval B).range : Set (WeakBilin B →ₗ[𝕜] 𝕜)))
    (↑f : WeakBilin B →ₗ[𝕜] 𝕜)

Tactic:
have : f.toLinearMap ∈
      Submodule.span 𝕜 (ContinuousLinearMap.coeLM 𝕜 ∘ₗ WeakBilin.eval B).range := by
    simpa [coe_range, mem_span_iff_continuous, continuous_iff_le_induced, ← induced_to_pi] using
      f.continuous.le_induced
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
f : StrongDual.{u_5, u_6} 𝕜 (WeakBilin B)
this :
  Membership.mem (γ := Submodule 𝕜 (LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id 𝕜) (WeakBilin B) 𝕜))
    (Submodule.span 𝕜 (↑(ContinuousLinearMap.coeLM 𝕜 ∘ₗ WeakBilin.eval B).range : Set (WeakBilin B →ₗ[𝕜] 𝕜)))
    (↑f : WeakBilin B →ₗ[𝕜] 𝕜)
⊢ ∃ (a : F), (WeakBilin.eval B : (a : F) → StrongDual 𝕜 (WeakBilin B)) a = f

Tactic:
simpa
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ WithSeminorms B.toSeminormFamily

Tactic:
let e : F ≃ (Σ _ : F, Fin 1) := .symm <| .sigmaUnique _ _
  withSeminorms_induced (withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜 𝕜))
    (LinearMap.ltoFun 𝕜 F 𝕜 𝕜 ∘ₗ B : (WeakBilin B) →ₗ[𝕜] (F → 𝕜)) |>.congr_equiv e

Premises used: LinearMap.ltoFun, LinearMap.toSeminormFamily, SeminormFamily.comp, LinearMap.toSeminorm, LinearMap.comp, WithSeminorms.congr_equiv, withSeminorms_pi, norm_withSeminorms, Seminorm.comp, Equiv.symm, OfNat.ofNat, Fin, Equiv.sigmaUnique, LinearMap.withSeminorms_induced
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ Filter.HasBasis (𝓝 0) (fun (x : Set E) ↦ x ∈ B.toSeminormFamily.basisSets) _root_.id

Tactic:
LinearMap.weakBilin_withSeminorms B |>.hasBasis

Premises used: Set.Mem, instAddCommMonoidWeakBilin._aux_1, instAddCommMonoidWeakBilin._aux_4, instModuleWeakBilin._aux_1, LinearMap.weakBilin_withSeminorms, WeakBilin, WithSeminorms.hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.WeakDual
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : NormedSpace ℝ 𝕜
inst_6 : Module ℝ E
inst_7 : IsScalarTower ℝ 𝕜 E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ LocallyConvexSpace.{0, u_2} ℝ (WeakBilin B)

Tactic:
B.weakBilin_withSeminorms.toLocallyConvexSpace

Premises used: WithSeminorms.toLocallyConvexSpace, instAddCommMonoidWeakBilin._aux_1, instAddCommMonoidWeakBilin._aux_4, LinearMap.weakBilin_withSeminorms
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
hbc : M ≤ max M 1
⊢ M * ‖x‖ ≤ max M 1 * ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M ≤ max M 1

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
f : V₁ →+ V₂
K : ℝ≥0
h : LipschitzWith.{u_2, u_3} (α := V₁) (β := V₂) K (⇑f : (a : V₁) → V₂)
x : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ (↑K : ℝ) * ‖x‖

Tactic:
simpa only [map_zero, dist_zero_right] using h.dist_le_mul x 0

Premises used: LipschitzWith.dist_le_mul, map_zero, OfNat.ofNat, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
h : f.toFun = g.toFun
mk :
  ∀ (toFun : V₁ → V₂) (map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂)
    (bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖)
    (h : { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ }.toFun = g.toFun),
    { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f g_1 g : NormedAddGroupHom V₁ V₂
toFun : V₁ → V₂
map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂
bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖
h : { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ }.toFun = g.toFun
mk :
  ∀ (toFun_1 : V₁ → V₂) (map_add'_1 : ∀ (v₁ v₂ : V₁), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂)
    (bound'_1 : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun_1 v‖ ≤ C * ‖v‖)
    (h :
      { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ }.toFun =
        { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 : NormedAddGroupHom V₁ V₂ }.toFun),
    { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } =
      { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 }
⊢ { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
toFun : V₁ → V₂
map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂
bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖
toFun_1 : V₁ → V₂
map_add'_1 : ∀ (v₁ v₂ : V₁), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂
bound'_1 : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun_1 v‖ ≤ C * ‖v‖
h :
  { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ }.toFun =
    { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 : NormedAddGroupHom V₁ V₂ }.toFun
⊢ { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } =
    { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
H : Eq (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
mk :
  ∀ (toFun : V₁ → V₂) (map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂)
    (bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖)
    (H :
      Eq (α := (a : V₁) → V₂)
        (⇑{ toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
        (⇑g : (a : V₁) → V₂)),
    { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
g : NormedAddGroupHom V₁ V₂
toFun : V₁ → V₂
map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂
bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖
H :
  Eq (α := (a : V₁) → V₂)
    (⇑{ toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
    (⇑g : (a : V₁) → V₂)
mk :
  ∀ (toFun_1 : V₁ → V₂) (map_add'_1 : ∀ (v₁ v₂ : V₁), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂)
    (bound'_1 : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun_1 v‖ ≤ C * ‖v‖)
    (H :
      Eq (α := (a : V₁) → V₂)
        (⇑{ toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
        (⇑{ toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)),
    { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } =
      { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 }
⊢ { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } = g

Tactic:
cases g