awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
have mp : Bornology.IsVonNBounded 𝕜 s → ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
mp : Bornology.IsVonNBounded 𝕜 s → ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
have mpr : (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)) → Bornology.IsVonNBounded 𝕜 s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
have mp : ∀ ρ > 0,
  ∀ (hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)),
    ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
Tactic: rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, _, hρball⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
left : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)
⊢ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
have mp : ∀ (a : 𝕜) (ha : ρ < ‖a‖), ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
Tactic: rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
have mp : Bornology.IsBounded s → ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
mp : Bornology.IsBounded s → ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
⊢ Bornology.IsBounded s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
have mpr : (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)) → Bornology.IsBounded s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
have mp : (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)) →
  ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
Tactic: rw [isBounded_iff_subset_smul_ball 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)) → Bornology.IsBounded s
have mpr : (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)) → Bornology.IsVonNBounded 𝕜 s
Tactic: rw [← isVonNBounded_iff 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
h :
  ∃ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V ∧ IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
⊢ Continuous[inst_1, inst_4] f.toFun
have refine : ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
Tactic: refine continuous_of_continuousAt_zero f ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
h :
  ∃ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V ∧ IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
have rw : ∀ (A : Set F), Membership.mem (γ := Filter F) (𝓝 0) A → Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' A)
Tactic: rw [continuousAt_def, f.map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
h :
  ∃ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V ∧ IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
have rcases : ∀ (V : Set E) (hV : Membership.mem (γ := Filter E) (𝓝 0) V)
  (h : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)),
  Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
Tactic: rcases h with ⟨V, hV, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
have rcases : ∀ (r : ℝ) (hr : r > 0) (h : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f : (a : E) → F) '' V ⊆ c • U),
  Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
Tactic: rcases (h hU).exists_pos with ⟨r, hr, h⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f : (a : E) → F) '' V ⊆ c • U
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
have rcases : ∀ (x : 𝕜) (hx : r < ‖x‖), Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
Tactic: rcases NormedField.exists_lt_norm 𝕜 r with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f : (a : E) → F) '' V ⊆ c • U
x : 𝕜
hx : r < ‖x‖
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
have h₁ : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
Tactic: specialize h (σ x) (by simpa using hx.le)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
have x_ne : x ≠ 0
Tactic: have x_ne := norm_pos_iff.mp (hr.trans hx)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
x_ne : x ≠ 0
⊢ HSMul.hSMul (β := Set E) x⁻¹
      ((⇑f : (a : E) → F) ⁻¹' HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U) =
    (⇑f : (a : E) → F) ⁻¹' U
have rw : x⁻¹ • HSMul.hSMul (β := Set E) x ((⇑f : (a : E) → F) ⁻¹' U) = (⇑f : (a : E) → F) ⁻¹' U
Tactic: rw [x_ne.isUnit.preimage_smul_setₛₗ _, inv_smul_smul₀ x_ne _]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
x_ne : x ≠ 0
rw : x⁻¹ • HSMul.hSMul (β := Set E) x ((⇑f : (a : E) → F) ⁻¹' U) = (⇑f : (a : E) → F) ⁻¹' U
⊢ HSMul.hSMul (β := Set E) x⁻¹
      ((⇑f : (a : E) → F) ⁻¹' HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U) =
    (⇑f : (a : E) → F) ⁻¹' U
have rw₁ : Eq.{u_3 + 1} (α := Set E) ((⇑f : (a : E) → F) ⁻¹' U) ((⇑f : (a : E) → F) ⁻¹' U)
Tactic: rw [x_ne.isUnit.preimage_smul_setₛₗ _, inv_smul_smul₀ x_ne _]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
x_ne : x ≠ 0
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
have this : x⁻¹ • V ⊆ (⇑f : (a : E) → F) ⁻¹' U
Tactic: have : x⁻¹ • V ⊆ f ⁻¹' U :=
      calc
        x⁻¹ • V ⊆ x⁻¹ • f ⁻¹' f '' V := Set.smul_set_mono (Set.subset_preimage_image (⇑f) V)
        _ ⊆ x⁻¹ • f ⁻¹' (σ x • U) := Set.smul_set_mono (Set.preimage_mono h)
        _ = f ⁻¹' U := by rw [x_ne.isUnit.preimage_smul_setₛₗ _, inv_smul_smul₀ x_ne _]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
h_1 : IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' V)
r : ℝ
hr : r > 0
x : 𝕜
hx : r < ‖x‖
h : (⇑f : (a : E) → F) '' V ⊆ HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜') U
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ (⇑f : (a : E) → F) ⁻¹' U
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
have grw : Membership.mem (γ := Filter E) (𝓝 0) (x⁻¹ • V)
Tactic: grw [← this]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
have obtain : ∀ (c : 𝕜) (hc0 : 0 < ‖c‖) (hc1 : ‖c‖ < 1), ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
Tactic: obtain ⟨c, hc0, hc1⟩ := NormedField.exists_norm_lt_one 𝕜
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
have c_ne : c ≠ 0
Tactic: have c_ne := norm_pos_iff.mp hc0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
have rcases : ∀ (b : ℕ → Set E) (bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i))
  (bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ _root_.id (b i)),
  ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
Tactic: rcases (nhds_basis_balanced 𝕜 E).exists_antitone_subbasis with ⟨b, bE1, bE⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
⊢ HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
have refine_1 : ∀ (i : ℕ), True → ∃ (i' : ℕ), True ∧ c ^ i' • b i' ⊆ b i
Tactic: refine bE.1.to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
refine_1 : ∀ (i : ℕ), True → ∃ (i' : ℕ), True ∧ c ^ i' • b i' ⊆ b i
⊢ HasBasis.{u_3, 1} (α := E) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ c ^ n • b n
have refine_2 : ∀ (i' : ℕ), True → Membership.mem (γ := Filter E) (𝓝 0) (c ^ i' • b i')
Tactic: refine bE.1.to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
n : ℕ
h : True
⊢ ∃ (i' : ℕ), True ∧ c ^ i' • b i' ⊆ b n
have h : True ∧ c ^ n • b n ⊆ b n
Tactic: use n
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
n : ℕ
h : True
⊢ ‖c ^ n‖ ≤ 1
have grw : ‖c‖ ^ n ≤ 1
Tactic: grw [norm_pow, hc1, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
n : ℕ
h : True
grw : ‖c‖ ^ n ≤ 1
⊢ ‖c ^ n‖ ≤ 1
have grw₁ : HPow.hPow (α := ℝ) 1 n ≤ 1
Tactic: grw [norm_pow, hc1, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.ContinuousOfBounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : AddCommGroup F
inst_4 : TopologicalSpace F
inst_5 : NontriviallyNormedField 𝕜
inst_6 : Module 𝕜 E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : NormedField 𝕜'
inst_9 : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_10 : RingHomIsometric σ
inst_11 : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded.{u_2, u_4} 𝕜' (E := F) ((⇑f : (a : E) → F) '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), Membership.mem (γ := Filter E) (𝓝 0) (b i) ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis.{u_3, 0} (α := E) (𝓝 0) fun (i : ℕ) ↦ b i
n : ℕ
h : True
grw : ‖c‖ ^ n ≤ 1
grw₁ : HPow.hPow (α := ℝ) 1 n ≤ 1
⊢ ‖c ^ n‖ ≤ 1
have grw₂ : LE.le (α := ℝ) 1 1
Tactic: grw [norm_pow, hc1, one_pow]