awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x_1 : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
φ_cont : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
x : E
hx : ∀ (i : ι), Eq.{u_5 + 1} (α := 𝕜) ((f i : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
simp_rw : 𝓝 x = 𝓝 0
simp_rw₁ : Eq.{u_6 + 1} (α := Filter E) (⨅ (i : ι), 𝓝 x) (⨅ (i : ι), 𝓝 0)
simp_rw₂ :
  Eq.{u_6 + 1} (α := Filter E)
    (⨅ (i : ι),
      Filter.comap.{u_6, u_5} (β := 𝕜) ((⇑(f i) : (a : E) → 𝕜) : (a : E) → 𝕜) (𝓝 ((f i : (a : E) → 𝕜) x) : Filter 𝕜))
    (⨅ (i : ι),
      Filter.comap.{u_6, u_5} (β := 𝕜) ((⇑(f i) : (a : E) → 𝕜) : (a : E) → 𝕜) (𝓝 ((f i : (a : E) → 𝕜) 0) : Filter 𝕜))
⊢ Inseparable x 0
have simp_rw₃ : Eq.{u_6 + 1} (α := Filter E) (⨅ (i : ι), Filter.comap.{u_6, u_5} (β := 𝕜) (⇑(f i) : (a : E) → 𝕜) (𝓝 0))
  (⨅ (i : ι),
    Filter.comap.{u_6, u_5} (β := 𝕜) ((⇑(f i) : (a : E) → 𝕜) : (a : E) → 𝕜) (𝓝 ((f i : (a : E) → 𝕜) 0) : Filter 𝕜))
Tactic: simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
Goal:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst : Finite ι
inst_1 : Field 𝕜
t𝕜 : TopologicalSpace 𝕜
inst_2 : IsTopologicalRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : T0Space 𝕜
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
x_1 : TopologicalSpace E := ⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜
φ_cont : Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) t𝕜, t𝕜] (⇑φ : (a : E) → 𝕜)
x : E
hx : ∀ (i : ι), Eq.{u_5 + 1} (α := 𝕜) ((f i : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ Eq.{u_5 + 1} (α := 𝕜) ((φ : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
have this : Inseparable x 0
Tactic: have : Inseparable x 0 := by
      -- Maybe missing lemmas about `Inseparable`?
      simp_rw [Inseparable, nhds_iInf, nhds_induced, hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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𝕜
this : Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)
have simp_rw : Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ (i : ι), 𝕜 ∙ f i) φ ↔
  ∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ
Tactic: simp_rw [this, ← mem_span_iff_continuous_of_finite, Submodule.span_range_eq_iSup,
      iSup_subtype]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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𝕜
this : Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ (i : ι), 𝕜 ∙ f i) φ ↔
    ∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ
have rw : (∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ) ↔
  ∃ (s : Finset ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (⨆ i ∈ s, 𝕜 ∙ f i) φ
Tactic: rw [Submodule.mem_iSup_iff_exists_finset]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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𝕜
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (Submodule.span 𝕜 (Set.range f)) φ ↔
    Continuous[⨅ (i : ι), induced (⇑(f i) : (a : E) → 𝕜) inferInstance, inferInstance] (⇑φ : (a : E) → 𝕜)
have φ₁ : Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
Tactic: suffices
      Continuous[t₁, t𝕜] φ ↔ ∃ s : Finset ι, Continuous[t₂ s, t𝕜] φ by
    simp_rw [this, ← mem_span_iff_continuous_of_finite, Submodule.span_range_eq_iSup,
      iSup_subtype]
    rw [Submodule.mem_iSup_iff_exists_finset]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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𝕜
⊢ Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
have t₁_group : IsTopologicalAddGroup E
Tactic: have t₁_group : @IsTopologicalAddGroup E t₁ _ :=
    topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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
⊢ Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
have t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
Tactic: have t₂_group (s : Finset ι) : @IsTopologicalAddGroup E (t₂ s) _ :=
    topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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
⊢ Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
have t₁_smul : ContinuousSMul 𝕜 E
Tactic: have t₁_smul : @ContinuousSMul 𝕜 E _ _ t₁ :=
    continuousSMul_iInf fun _ ↦ continuousSMul_induced _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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
⊢ Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
have t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
Tactic: have t₂_smul (s : Finset ι) : @ContinuousSMul 𝕜 E _ _ (t₂ s) :=
    continuousSMul_iInf fun _ ↦ continuousSMul_induced _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
⊢ Continuous[t₁, t𝕜] (⇑φ : (a : E) → 𝕜) ↔ ∃ (s : Finset ι), Continuous[t₂ s, t𝕜] (⇑φ : (a : E) → 𝕜)
have simp_rw : Continuous[t₁, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ) ↔
  ∃ (s : Finset ι), Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
Tactic: simp_rw [WithSeminorms.continuous_iff_continuous_comp (norm_withSeminorms 𝕜 𝕜), forall_const]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
| Continuous[t₁, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
have rw : Membership.mem (γ := Filter E) (⨅ (i : ι), 𝓝 0)
  (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)
Tactic: rw [Seminorm.continuous_iff one_pos, nhds_iInf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
⊢ Continuous[t₁, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ) ↔
    ∃ (s : Finset ι), Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
have conv : 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 [Seminorm.continuous_iff one_pos, nhds_iInf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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 ι
| Continuous[t₂ s, _] (⇑(Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) : (a : E) → ℝ)
have rw : Membership.mem (γ := Filter E) (⨅ (i : ι), ⨅ (h : i ∈ s), 𝓝 0)
  (Seminorm.ball (𝕜 := 𝕜) (Seminorm.comp (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 𝕜) φ) 0 1)
Tactic: rw [letI := t₂ s; Seminorm.continuous_iff one_pos, nhds_iInf, iInf_subtype]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
⊢ 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) → ℝ)
have 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)
Tactic: conv in Continuous _ =>
    rw [letI := t₂ s; Seminorm.continuous_iff one_pos, nhds_iInf, iInf_subtype]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
⊢ 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)
have 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)
Tactic: rw [Filter.mem_iInf_finite]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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𝕜
⊢ 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)
have this : IsTopologicalAddGroup E
Tactic: have : IsTopologicalAddGroup E := topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
have 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))
Tactic: simp_rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, nhds_iInf, nhds_induced, map_zero,
      ← comap_norm_nhds_zero (E := 𝕜), Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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
⊢ 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)
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
⊢ 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)
have 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)
Tactic: rw [LinearMap.mem_span_iff_continuous]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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)
⊢ 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)
have 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) → 𝕜)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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) → 𝕜)
⊢ ∃ (s : Finset ι) (c : ℝ≥0), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)
have H₁ : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (goal)
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), φ.toSeminorm ≤ HSMul.hSMul (β := Seminorm 𝕜 E) c (s.sup fun (i : ι) ↦ (f i).toSeminorm)
have 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)
Tactic: rcases Seminorm.bound_of_continuous this _ H with ⟨s, C, -, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WeakDual (hypothesis)
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)
⊢ ∃ (a : F), (WeakBilin.eval B : (a : F) → StrongDual 𝕜 (WeakBilin B)) a = f
have 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 →ₗ[𝕜] 𝕜)
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
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 * ‖x‖ ≤ max M 1 * ‖x‖
have hbc : M ≤ max M 1
Tactic: gcongr