awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 ι
⊢ WithSeminorms p ↔ u = ⨅ (i : ι), PseudoMetricSpace.toUniformSpace
have rw : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)
Tactic: rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsUniformAddGroup.ext_iff inferInstance (isUniformAddGroup_iInf fun i => inferInstance),
    UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 ι
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)
have a : ∀ (i : ι), Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)
Tactic: congrm _ = ⨅ i, ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ WithSeminorms.{u_11, u_12, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ normSeminorm 𝕜 E
have rw : Eq.{u_12 + 1} (α := Filter E) (𝓝 0) (⨅ (i : Fin 1), comap (β := ℝ) (⇑(normSeminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
Tactic: rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm,
    comap_norm_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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))
⊢ WithSeminorms.{u_11, u_12, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ normSeminorm 𝕜 E
have rw₁ : Eq (α := Filter E) (𝓝 0) (comap (β := ℝ) (⇑(normSeminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
Tactic: rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm,
    comap_norm_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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))
⊢ WithSeminorms.{u_11, u_12, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ normSeminorm 𝕜 E
have rw₂ : Eq.{u_12 + 1} (α := Filter E) (𝓝 0) (comap norm (𝓝 0))
Tactic: rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm,
    comap_norm_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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))
⊢ WithSeminorms.{u_11, u_12, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ normSeminorm 𝕜 E
have rw₃ : Eq.{u_12 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
Tactic: rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm,
    comap_norm_nhds_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have rw : (∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
Tactic: rw [hp.hasBasis.isVonNBounded_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 ∈ p.basisSets, Absorbs 𝕜 (id i) s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have mp : (∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) → ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ (∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have mpr : (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r) → ∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
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 ι
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have h₁ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
Tactic: specialize h ((I.sup p).ball 0 1) (p.basisSets_mem I zero_lt_one)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have 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
Tactic: rcases h.exists_pos with ⟨r, hr, h⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have mp : ∀ (a : 𝕜) (ha : r < ‖a‖), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
Tactic: obtain ⟨a, ha⟩ := NormedField.exists_lt_norm 𝕜 r
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
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‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have h₁ : s ⊆ a • (I.sup p).ball 0 1
Tactic: specialize h a (le_of_lt ha)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
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
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have h₁ : s ⊆ (I.sup p).ball 0 ‖a‖
Tactic: rw [Seminorm.smul_ball_zero (norm_pos_iff.1 <| hr.trans ha), mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
have mp : ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < ‖a‖
Tactic: refine ⟨‖a‖, lt_trans hr ha, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
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
⊢ (I.sup p : (a : E) → ℝ) x < ‖a‖
have h₁ : x ∈ (I.sup p).ball 0 ‖a‖
Tactic: specialize h hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ Absorbs 𝕜 (id s') s
have mpr : ∀ (I : Finset ι) (r : ℝ) (hr : 0 < r) (hs' : s' = (I.sup p).ball 0 r), Absorbs 𝕜 (id s') s
Tactic: rcases p.basisSets_iff.mp hs' with ⟨I, r, hr, hs'⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ Absorbs 𝕜 (id s') s
have mpr : Absorbs 𝕜 ((I.sup p).ball 0 r) s
Tactic: rw [id, hs']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s
have mpr : ∀ r' > 0, ∀ (h' : ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r'), Absorbs 𝕜 ((I.sup p).ball 0 r) s
Tactic: rcases h I with ⟨r', _, h'⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
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'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s
have h'₁ : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
Tactic: simp_rw [← (I.sup p).mem_ball_zero] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
have mpr : Absorbs 𝕜 ((I.sup p).ball 0 r) ((I.sup p).ball 0 r')
Tactic: refine Absorbs.mono_right ?_ h'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ IsVonNBounded 𝕜 (f '' s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) (f x) < r
have 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
Tactic: simp_rw [hp.isVonNBounded_iff_finset_seminorm_bounded, Set.forall_mem_image]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
have 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
Tactic: rw [hp.isVonNBounded_iff_finset_seminorm_bounded]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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, (p i : (a : E) → ℝ) x < r
have h : ∀ (x : ℝ), ∀ a ∈ s, p i = Finset.sup {i} p
Tactic: convert! hI { i }
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 : a ∈ s
⊢ p i = Finset.sup {i} p
have h : p i = p i
Tactic: rw [Finset.sup_singleton]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 ι
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have pos : ∀ (hI : I.Nonempty), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
Tactic: by_cases! hI : I.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have neg : ∀ (hI : I = ∅), ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
Tactic: by_cases! hI : I.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have 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
Tactic: choose r hr h using hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ 0 < I.sup' hI r
have rcases : ∀ (i : ι) (hi : i ∈ I), 0 < I.sup' sorry r
Tactic: rcases hI with ⟨i, hi⟩
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
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
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have h' : 0 < I.sup' hI r
Tactic: have h' : 0 < I.sup' hI r := by
      rcases hI with ⟨i, hi⟩
      exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
h' : 0 < I.sup' hI r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have pos : ∀ (x : E) (hx : x ∈ s) (i : ι) (hi : i ∈ I), (p i : (a : E) → ℝ) x < I.sup' hI r
Tactic: refine ⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ (p i : (a : E) → ℝ) x < I.sup' hI r
have pos : r i ≤ I.sup' hI r
Tactic: refine lt_of_lt_of_le (h i x hx) ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ r i ≤ I.sup' hI r
have pos : ∃ b ∈ I, r i ≤ r b
Tactic: simp only [Finset.le_sup'_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 = ∅
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r
have neg : ∃ r > 0, ∀ x ∈ s, 0 < r
Tactic: simp only [hI, Finset.sup_empty, coe_bot, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) (f x) < r
have simp_rw : (∀ (i : ι), ∃ r > 0, ∀ x ∈ f '' s, (p i : (a : E) → ℝ) x < r) ↔
  ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) (f x) < r
Tactic: simp_rw [hp.isVonNBounded_iff_seminorm_bounded, Set.forall_mem_image]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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
⊢ IsVonNBounded 𝕜 s ↔ ∀ (i : ι), BddAbove (α := ℝ) ((⇑(p i) : (a : E) → ℝ) '' s)
have simp_rw : (∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔
  ∀ (i : ι), ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
Tactic: simp_rw [hp.isVonNBounded_iff_seminorm_bounded, bddAbove_def, forall_mem_image]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
have a : ∀ (i : ι), (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔ ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
Tactic: congrm ∀ i, ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 : ι
⊢ (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔ ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
have a : (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) → ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
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 : ι
a : (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) → ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
⊢ (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔ ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
have a₁ : (∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x) → ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
Tactic: constructor