awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p_1 : SeminormFamily 𝕜 E ι
hp_1 : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p_1 i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p_1 i) : (a : E) → ℝ)
p : Seminorm 𝕜 E
hp : Continuous[t, _] (⇑p : (a : E) → ℝ)
⊢ Tendsto (α := E) (β := ℝ)
    (⇑(↑(Subtype.mk (p := fun (p : Seminorm 𝕜 E) ↦ Continuous[t, _] (⇑p : (a : E) → ℝ)) p hp) : Seminorm 𝕜 E) :
      (a : E) → ℝ)
    (𝓝 0) (𝓝 0)

Tactic:
exact hp.tendsto' 0 0 (map_zero _)

Premises used: map_zero, Continuous.tendsto', OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
refine_2 :
  ∀ (i : ι),
    LE.le (α := Filter E)
      (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
        comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
      (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
⊢ LE.le.{u_6} (α := Filter E)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
    (𝓝 0)

Tactic:
simp_rw [hp, le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
i : ι
⊢ LE.le (α := Filter E)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
    (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))

Tactic:
iInf_le (ι := {p : Seminorm 𝕜 E // Continuous p}) _ ⟨p i, hp' i⟩

Premises used: Set.Mem, setOf, Subtype.mk, iInf_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
i : ι
⊢ LE.le (α := Filter E)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
    (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))

Tactic:
exact iInf_le (ι := {p : Seminorm 𝕜 E // Continuous p}) _ ⟨p i, hp' i⟩

Premises used: Subtype.mk, iInf_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
u : UniformSpace E
inst_3 : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
rw :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)
⊢ WithSeminorms p ↔ u = ⨅ (i : ι), PseudoMetricSpace.toUniformSpace

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsUniformAddGroup.ext_iff inferInstance (isUniformAddGroup_iInf fun i => inferInstance),
    UniformSpace.toTopologicalSpace_iInf, nhds_iInf]

Premises used: IsUniformAddGroup.ext_iff, nhds_iInf, inferInstance, UniformSpace.toTopologicalSpace_iInf, isUniformAddGroup_iInf, SeminormFamily.withSeminorms_iff_nhds_eq_iInf
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
u : UniformSpace E
inst_3 : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
a : ∀ (i : ι), Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)

Tactic:
congrm _ = ⨅ i, ?_
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
u : UniformSpace E
inst_3 : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)

Tactic:
@comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup

Premises used: comap_norm_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
u : UniformSpace E
inst_3 : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)

Tactic:
exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup

Premises used: comap_norm_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_11
E : Type u_12
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
rw : Eq.{u_12 + 1} (α := Filter E) (𝓝 0) (⨅ (i : Fin 1), comap (β := ℝ) (⇑(normSeminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
rw₁ : Eq (α := Filter E) (𝓝 0) (comap (β := ℝ) (⇑(normSeminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
rw₂ : Eq.{u_12 + 1} (α := Filter E) (𝓝 0) (comap norm (𝓝 0))
rw₃ rw₄ : Eq.{u_12 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ WithSeminorms.{u_11, u_12, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ normSeminorm 𝕜 E

Tactic:
rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm,
    comap_norm_nhds_zero]

Premises used: comap_norm_nhds_zero, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, coe_normSeminorm, iInf_const
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
𝕜 : Type u_2
𝕜₂ : Type u_3
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
norm_withSeminorms 𝕜 E |>.toPolynormableSpace

Premises used: norm_withSeminorms, WithSeminorms.toPolynormableSpace
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
rw : (∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
⊢ IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
rw [hp.hasBasis.isVonNBounded_iff]

Premises used: Filter.HasBasis.isVonNBounded_iff, WithSeminorms.hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
mp : (∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) → ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
mpr : (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r) → ∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s
⊢ (∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ i ∈ p.basisSets, Absorbs 𝕜 i s
I : Finset ι
⊢ Absorbs 𝕜 ((I.sup p).ball 0 1) s

Tactic:
specialize h ((I.sup p).ball 0 1) (p.basisSets_mem I zero_lt_one)

Premises used: zero_lt_one, Seminorm.ball, Finset.sup, OfNat.ofNat, SeminormFamily.basisSets_mem
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h : Absorbs 𝕜 ((I.sup p).ball 0 1) s
mp :
  ∀ (r : ℝ) (hr : r > 0) (h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1),
    ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

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

Premises used: Absorbs.exists_pos
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
mp : ∀ (a : 𝕜) (ha : r < ‖a‖), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
obtain ⟨a, ha⟩ := NormedField.exists_lt_norm 𝕜 r

Premises used: NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
a : 𝕜
ha : r < ‖a‖
⊢ s ⊆ a • (I.sup p).ball 0 1

Tactic:
specialize h a (le_of_lt ha)

Premises used: le_of_lt
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ a • (I.sup p).ball 0 1
⊢ s ⊆ (I.sup p).ball 0 ‖a‖

Tactic:
rw [Seminorm.smul_ball_zero (norm_pos_iff.1 <| hr.trans ha), mul_one] at h

Premises used: norm_pos_iff, Iff.mp, LT.lt.trans, Seminorm.smul_ball_zero, mul_one
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
⟨‖a‖, lt_trans hr ha, ?_⟩

Premises used: Norm.norm, lt_trans, And.intro, Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
mp : ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
refine ⟨‖a‖, lt_trans hr ha, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
x : E
hx : x ∈ s
⊢ x ∈ (I.sup p).ball 0 ‖a‖

Tactic:
specialize h hx
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
x : E
hx : x ∈ s
h : x ∈ (I.sup p).ball 0 ‖a‖
⊢ (I.sup p : (a : E) → ℝ) x < ‖a‖

Tactic:
(Finset.sup I p).mem_ball_zero.mp h

Premises used: Seminorm.mem_ball_zero, Iff.mp, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h_1 : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
x : E
hx : x ∈ s
h : x ∈ (I.sup p).ball 0 ‖a‖
⊢ (I.sup p : (a : E) → ℝ) x < ‖a‖

Tactic:
exact (Finset.sup I p).mem_ball_zero.mp h

Premises used: Seminorm.mem_ball_zero, Iff.mp, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs' : s' ∈ p.basisSets
mpr : ∀ (I : Finset ι) (r : ℝ) (hr : 0 < r) (hs' : s' = (I.sup p).ball 0 r), Absorbs 𝕜 (id s') s
⊢ Absorbs 𝕜 (id s') s

Tactic:
rcases p.basisSets_iff.mp hs' with ⟨I, r, hr, hs'⟩

Premises used: Iff.mp, SeminormFamily.basisSets_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs'_1 : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
mpr : Absorbs 𝕜 ((I.sup p).ball 0 r) s
⊢ Absorbs 𝕜 (id s') s

Tactic:
rw [id, hs']

Premises used: id
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs'_1 : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
mpr : ∀ r' > 0, ∀ (h' : ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r'), Absorbs 𝕜 ((I.sup p).ball 0 r) s
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s

Tactic:
rcases h I with ⟨r', _, h'⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs'_1 : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left : r' > 0
h' : ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r'
⊢ ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'

Tactic:
simp_rw [← (I.sup p).mem_ball_zero] at h'

Premises used: Seminorm.mem_ball_zero, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs'_1 : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left : r' > 0
h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s

Tactic:
Absorbs.mono_right ?_ h'

Premises used: Absorbs.mono_right
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs'_1 : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left : r' > 0
h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
mpr : Absorbs 𝕜 ((I.sup p).ball 0 r) ((I.sup p).ball 0 r')
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s

Tactic:
refine Absorbs.mono_right ?_ h'

Premises used: Absorbs.mono_right
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs'_1 : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left : r' > 0
h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) ((I.sup p).ball 0 r')

Tactic:
(Finset.sup I p).ball_zero_absorbs_ball_zero hr

Premises used: Seminorm.ball_zero_absorbs_ball_zero, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
s' : Set E
hs'_1 : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left : r' > 0
h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) ((I.sup p).ball 0 r')

Tactic:
exact (Finset.sup I p).ball_zero_absorbs_ball_zero hr

Premises used: Seminorm.ball_zero_absorbs_ball_zero, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
G : Type u_8
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
f : G → E
s : Set G
hp : WithSeminorms p
simp_rw :
  (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ f '' s, (I.sup p : (a : E) → ℝ) x < r) ↔
    ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) (f x) < r
⊢ IsVonNBounded 𝕜 (f '' s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) (f x) < r

Tactic:
simp_rw [hp.isVonNBounded_iff_finset_seminorm_bounded, Set.forall_mem_image]

Premises used: WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded, Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
rw :
  (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
⊢ IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r

Tactic:
rw [hp.isVonNBounded_iff_finset_seminorm_bounded]

Premises used: WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
mp :
  (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r) →
    ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
mpr :
  (∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) →
    ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
⊢ (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
i : ι
⊢ ∃ r > 0, ∀ x ∈ s, (Finset.sup {i} p : (a : E) → ℝ) x < r

Tactic:
hI { i }

Premises used: Singleton.singleton
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
i : ι
h : ∀ (x : ℝ), ∀ a ∈ s, p i = Finset.sup {i} p
⊢ ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r

Tactic:
convert! hI { i }

Premises used: Singleton.singleton
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
i : ι
x : ℝ
a : E
h_1 : a ∈ s
h h₁ : p i = p i
⊢ p i = Finset.sup {i} p

Tactic:
rw [Finset.sup_singleton]

Premises used: Finset.sup_singleton
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
I : Finset ι
pos : ∀ (hI : I.Nonempty), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
neg : ∀ (hI : I = ∅), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
by_cases! hI : I.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
I : Finset ι
hI : I.Nonempty
pos :
  ∀ (r : (i : ι) → ℝ) (hr : ∀ (i : ι), r i > 0) (h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i),
    ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
choose r hr h using hi
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
rcases : ∀ (i : ι) (hi : i ∈ I), 0 < I.sup' ⋯ r
⊢ 0 < I.sup' hI r

Tactic:
rcases hI with ⟨i, hi⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
i : ι
hi : i ∈ I
⊢ 0 < I.sup' ⋯ r

Tactic:
lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)

Premises used: Finset.le_sup', lt_of_lt_of_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
i : ι
hi : i ∈ I
⊢ 0 < I.sup' ⋯ r

Tactic:
exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)

Premises used: Finset.le_sup', lt_of_lt_of_le