awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Metric.closedBall 0 r)

Tactic:
isVonNBounded_of_isBounded _ Metric.isBounded_closedBall

Premises used: Metric.isBounded_closedBall, NormedSpace.isVonNBounded_of_isBounded
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
⟨fun h ↦ ?_, isVonNBounded_of_isBounded _⟩

Premises used: NormedSpace.isVonNBounded_of_isBounded, Iff.intro
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
refine : ∀ (h : Bornology.IsVonNBounded 𝕜 s), Bornology.IsBounded s
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
refine ⟨fun h ↦ ?_, isVonNBounded_of_isBounded _⟩
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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
rcases :
  ∀ (ρ : ℝ) (hρ : ρ > 0) (hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)),
    Bornology.IsBounded s
⊢ Bornology.IsBounded s

Tactic:
rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, hρ, hρball⟩

Premises used: Metric.ball_mem_nhds, zero_lt_one, Absorbs.exists_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)
rcases : ∀ (a : 𝕜) (ha : ρ < ‖a‖), Bornology.IsBounded s
⊢ Bornology.IsBounded s

Tactic:
rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩

Premises used: NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)
a : 𝕜
ha : ρ < ‖a‖
⊢ s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)

Tactic:
specialize hρball a ha.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
⊢ s ⊆ Metric.ball 0 (‖a‖ * 1)

Tactic:
rw [← ball_normSeminorm 𝕜 E, Seminorm.smul_ball_zero (norm_pos_iff.1 <| hρ.trans ha),
    ball_normSeminorm] at hρball

Premises used: norm_pos_iff, ball_normSeminorm, Iff.mp, LT.lt.trans, Seminorm.smul_ball_zero
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ Metric.ball 0 (‖a‖ * 1)
⊢ Bornology.IsBounded s

Tactic:
Metric.isBounded_ball.subset hρball

Premises used: Metric.isBounded_ball, Bornology.IsBounded.subset
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ Metric.ball 0 (‖a‖ * 1)
⊢ Bornology.IsBounded s

Tactic:
exact Metric.isBounded_ball.subset hρball

Premises used: Metric.isBounded_ball, Bornology.IsBounded.subset
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
rw : Bornology.IsBounded s ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
rw₁ rw₂ : (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r

Tactic:
rw [NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le]

Premises used: NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
α : Type u_6
f : α → E
s : Set α
simp_rw : (∃ (r : ℝ), ∀ x ∈ f '' s, ‖x‖ ≤ r) ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖f x‖ ≤ r
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖f x‖ ≤ r

Tactic:
simp_rw [isVonNBounded_iff', Set.forall_mem_image]

Premises used: NormedSpace.isVonNBounded_iff', Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
rw : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology

Tactic:
rw [Bornology.ext_iff_isBounded]

Premises used: Bornology.ext_iff_isBounded
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
rw : Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
rw [Bornology.isBounded_iff_isVonNBounded]

Premises used: Bornology.isBounded_iff_isVonNBounded
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
isVonNBounded_iff _

Premises used: NormedSpace.isVonNBounded_iff
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
exact isVonNBounded_iff _

Premises used: NormedSpace.isVonNBounded_iff
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
rw : Bornology.IsVonNBounded 𝕜 s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
⊢ Bornology.IsBounded s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)

Tactic:
rw [← isVonNBounded_iff 𝕜]

Premises used: NormedSpace.isVonNBounded_iff
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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)
mpr : (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)) → Bornology.IsVonNBounded 𝕜 s
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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
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)
⊢ ∃ (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⟩

Premises used: Metric.ball_mem_nhds, zero_lt_one, Absorbs.exists_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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)
mp : ∀ (a : 𝕜) (ha : ρ < ‖a‖), ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
⊢ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)

Tactic:
rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩

Premises used: NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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 : 𝕜
ha : ρ < ‖a‖
⊢ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)

Tactic:
⟨a, hρball a ha.le⟩

Premises used: LT.lt.le, Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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 : 𝕜
ha : ρ < ‖a‖
⊢ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)

Tactic:
exact ⟨a, hρball a ha.le⟩
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Premises used: NormedSpace.isVonNBounded_ball, Bornology.IsVonNBounded.subset, HSMul.hSMul, Bornology.IsVonNBounded.image, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Premises used: NormedSpace.isVonNBounded_ball, Bornology.IsVonNBounded.subset, HSMul.hSMul, Bornology.IsVonNBounded.image, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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)
mpr : (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)) → Bornology.IsBounded s
⊢ Bornology.IsBounded s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
mp :
  (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)) →
    ∃ (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)

Tactic:
rw [isBounded_iff_subset_smul_ball 𝕜]

Premises used: NormedSpace.isBounded_iff_subset_smul_ball
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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.ball 0 1)) →
    ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)

Tactic:
Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, HasSubset.Subset.trans, Set.smul_set_mono, Exists.imp
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
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.ball 0 1)) →
    ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)

Tactic:
exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall

Premises used: Exists.imp
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
mpr : (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)) → Bornology.IsVonNBounded 𝕜 s
⊢ (∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)) → Bornology.IsBounded s

Tactic:
rw [← isVonNBounded_iff 𝕜]

Premises used: NormedSpace.isVonNBounded_iff
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Premises used: NormedSpace.isVonNBounded_closedBall, Bornology.IsVonNBounded.subset, HSMul.hSMul, Bornology.IsVonNBounded.image, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ HSMul.hSMul (β := Set E) a (Metric.closedBall 0 1)
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
exact ((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Premises used: NormedSpace.isVonNBounded_closedBall, Bornology.IsVonNBounded.subset, HSMul.hSMul, Bornology.IsVonNBounded.image, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : QuasiCompleteSpace 𝕜 E
s : Set E
hs : TotallyBounded s
⊢ IsCompact (closure[inst_3.toTopologicalSpace] s)

Tactic:
hs.closure.isCompact_of_isComplete
    (QuasiCompleteSpace.quasiComplete (TotallyBounded.isVonNBounded 𝕜 (TotallyBounded.closure hs))
    isClosed_closure)

Premises used: TotallyBounded.isVonNBounded, TotallyBounded.isCompact_of_isComplete, TotallyBounded.closure, isClosed_closure, QuasiCompleteSpace.quasiComplete
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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

Tactic:
continuous_of_continuousAt_zero f ?_

Premises used: continuous_of_continuousAt_zero
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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)
refine : ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0
⊢ Continuous[inst_1, inst_4] f.toFun

Tactic:
refine continuous_of_continuousAt_zero f ?_

Premises used: continuous_of_continuousAt_zero
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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)
rw :
  ∀ (A : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) A → Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' A)
⊢ ContinuousAt.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F) 0

Tactic:
rw [continuousAt_def, f.map_zero]

Premises used: LinearMap.map_zero, continuousAt_def
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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
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)
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)

Tactic:
rcases h with ⟨V, hV, h⟩
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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)
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)
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)

Tactic:
rcases (h hU).exists_pos with ⟨r, hr, h⟩

Premises used: Absorbs.exists_pos
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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
rcases : ∀ (x : 𝕜) (hx : r < ‖x‖), Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((⇑f : (a : E) → F) ⁻¹' U)

Tactic:
rcases NormedField.exists_lt_norm 𝕜 r with ⟨x, hx⟩

Premises used: NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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‖
⊢ r ≤ norm.{u_2} (E := 𝕜') ((σ : (a : 𝕜) → 𝕜') x : 𝕜')

Tactic:
simpa using hx.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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‖
⊢ (⇑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)

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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 ≠ 0

Tactic:
have x_ne := norm_pos_iff.mp (hr.trans hx)
-- Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
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
rw₁ rw₂ : Eq.{u_3 + 1} (α := Set E) ((⇑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

Tactic:
rw [x_ne.isUnit.preimage_smul_setₛₗ _, inv_smul_smul₀ x_ne _]

Premises used: inv_smul_smul₀, Ne.isUnit, IsUnit.preimage_smul_setₛₗ