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
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ (s : Finset ι) (C : ℝ≥0),
    (p i).comp LinearMap.id ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (i : ι) ↦ (Finset.Iic i).sup p)
have refine_2 : (p i).comp LinearMap.id ≤
  HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {i} fun (i : ι) ↦ (Finset.Iic i).sup p)
Tactic: refine ⟨{i}, 1, ?_⟩
-- 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
inst_3 : Preorder ι
inst_4 : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst_5 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {i} fun (i : ι) ↦ (Finset.Iic i).sup p)
have refine_2 : (p i).comp LinearMap.id ≤ (Finset.Iic i).sup p
Tactic: rw [Finset.sup_singleton, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ WithSeminorms.{u_2, u_6, u_10} (ι := ι') (p ∘ (⇑e : (a : ι') → ι))
have refine_1 : Seminorm.IsBounded.{u_2, u_2, u_6, u_6, u_9, u_10} (ι' := ι') p (p ∘ (⇑e : (a : ι') → ι)) LinearMap.id
Tactic: refine hp.congr ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
refine_1 : Seminorm.IsBounded.{u_2, u_2, u_6, u_6, u_9, u_10} (ι' := ι') p (p ∘ (⇑e : (a : ι') → ι)) LinearMap.id
⊢ WithSeminorms.{u_2, u_6, u_10} (ι := ι') (p ∘ (⇑e : (a : ι') → ι))
have refine_2 : Seminorm.IsBounded.{u_2, u_2, u_6, u_6, u_10, u_9} (ι := ι') (p ∘ (⇑e : (a : ι') → ι)) p LinearMap.id
Tactic: refine hp.congr ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι'
⊢ ∃ (s : Finset ι) (C : ℝ≥0), ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤ C • s.sup p
have h : ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤
  HSMul.hSMul (α := ℝ≥0) 1 (Finset.sup (singleton (α := ι) ((e : (a : ι') → ι) i : ι)) p)
Tactic: use {e i}, 1
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι
⊢ ∃ (s : Finset ι') (C : ℝ≥0), (p i).comp LinearMap.id ≤ C • s.sup (p ∘ (⇑e : (a : ι') → ι))
have h : (p i).comp LinearMap.id ≤
  HSMul.hSMul (α := ℝ≥0) 1
    (Finset.sup (β := ι') (singleton (α := ι') ((e.symm : (a : ι) → ι') i : ι')) (p ∘ (⇑e : (a : ι') → ι)))
Tactic: use {e.symm i}, 1
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ WithSeminorms.{u_2, u_6, u_10} (ι := ι') (p ∘ (⇑e : (a : ι') → ι))
have h : ∀ (i : ι'),
  ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) 1 (Finset.sup (singleton (α := ι) ((e : (a : ι') → ι) i : ι)) p)
Tactic: refine hp.congr ?_ ?_ <;>
  intro i <;>
  [use {e i}, 1; use {e.symm i}, 1]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
h :
  ∀ (i : ι'),
    ((p ∘ (⇑e : (a : ι') → ι)) i).comp LinearMap.id ≤
      HSMul.hSMul (α := ℝ≥0) 1 (Finset.sup (singleton (α := ι) ((e : (a : ι') → ι) i : ι)) p)
⊢ WithSeminorms.{u_2, u_6, u_10} (ι := ι') (p ∘ (⇑e : (a : ι') → ι))
have h₁ : ∀ (i : ι),
  (p i).comp LinearMap.id ≤
    HSMul.hSMul (α := ℝ≥0) 1
      (Finset.sup (β := ι') (singleton (α := ι') ((e.symm : (a : ι) → ι') i : ι')) (p ∘ (⇑e : (a : ι') → ι)))
Tactic: refine hp.congr ?_ ?_ <;>
  intro i <;>
  [use {e i}, 1; use {e.symm i}, 1]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
have hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
Tactic: have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
have rcases : ∀ (ε : ℝ) (ε_pos : 0 < ε) (hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))),
  ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
Tactic: rcases NormedAddGroup.nhds_zero_basis_norm_lt.mem_iff.mp (hq' <| Iio_mem_nhds one_pos)
    with ⟨ε, ε_pos, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
have this : 0 < ‖c‖ / ε
Tactic: have : 0 < ‖c‖ / ε := by positivity
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : F), (q : (a : F) → ℝ) x ≤ C * ‖x‖
have refine : ∀ (x : F), (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
Tactic: refine ⟨‖c‖ / ε, this, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x : F
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
have pos : ∀ (hx : ‖x‖ = 0), (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
Tactic: by_cases hx : ‖x‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x : F
pos : ∀ (hx : ‖x‖ = 0), (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
have neg : ∀ (hx : ¬‖x‖ = 0), (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
Tactic: by_cases hx : ‖x‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x : F
hx : ‖x‖ = 0
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
have pos : LE.le (α := ℝ) ((q : (a : F) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [hx, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x : F
hx : ¬‖x‖ = 0
⊢ (q : (a : F) → ℝ) x ≤ ‖c‖ / ε * ‖x‖
have neg : ∀ (x : F) (hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x) (hlt : (normSeminorm 𝕜 F : (a : F) → ℝ) x < ε),
  (q : (a : F) → ℝ) x ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)
Tactic: refine (normSeminorm 𝕜 F).bound_of_shell q ε_pos hc (fun x hle hlt ↦ ?_) hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x_1 : F
hx : ¬‖x_1‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
hlt : (normSeminorm 𝕜 F : (a : F) → ℝ) x < ε
⊢ (q : (a : F) → ℝ) x ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)
have neg : 1 ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)
Tactic: refine (le_of_lt <| show q x < _ from hε hlt).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : F) → ℝ)
hq' : Tendsto (α := F) (β := ℝ) (⇑q : (a : F) → ℝ) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : Subset (α := Set F) {y : F | ‖y‖ < ε} (preimage (β := ℝ) (⇑q : (a : F) → ℝ) (Iio 1))
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x_1 : F
hx : ¬‖x_1‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
hlt : (normSeminorm 𝕜 F : (a : F) → ℝ) x < ε
⊢ 1 ≤ HMul.hMul (β := ℝ) (‖c‖ / ε) ((normSeminorm 𝕜 F : (a : F) → ℝ) x : ℝ)
have neg : 1 / (‖c‖ / ε) ≤ (normSeminorm 𝕜 F : (a : F) → ℝ) x
Tactic: rwa [← div_le_iff₀' this, one_div_div]
-- 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 ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous[t, _] (⇑q : (a : E) → ℝ)
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
have rcases : ∀ (V : Set E) (hV : V ∈ p.basisSets) (hε : id V ⊆ q.ball 0 1), ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
Tactic: rcases hp.hasBasis.mem_iff.mp (ball_mem_nhds hq one_pos) with ⟨V, hV, 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 ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous[t, _] (⇑q : (a : E) → ℝ)
V : Set E
hV : V ∈ p.basisSets
hε : id V ⊆ q.ball 0 1
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
have rcases : ∀ (s : Finset ι) (ε : ℝ) (ε_pos : 0 < ε) (hV : (s.sup p).ball 0 ε ∈ p.basisSets)
  (hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1), ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
Tactic: rcases p.basisSets_iff.mp hV with ⟨s, ε, ε_pos, rfl⟩
Cleared hypotheses: V, hV, 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 ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)
have apply : Metric.ball 0 ε ⊆ q.ball 0 1
Tactic: apply Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) ?_)
-- 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 ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
⊢ Metric.ball 0 ε ⊆ q.ball 0 1
have rw : (s.sup p).ball 0 ε ⊆ q.ball 0 1
Tactic: rw [← ball_eq_metric]
-- 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 ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
have this : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)
Tactic: have : Continuous q := by
    apply Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) ?_)
    rw [← ball_eq_metric]
    exact 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 ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x_1 : NormedSpace 𝕜 E := { toModule := inst_2, norm_smul_le := ⋯ }
this : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑q : (a : E) → ℝ)
⊢ ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
have rcases : ∀ (C : ℝ) (C_pos : 0 < C) (hC : ∀ (x_2 : E), (q : (a : E) → ℝ) x_2 ≤ C * ‖x_2‖),
  ∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ q ≤ C • s.sup p
Tactic: rcases bound_of_continuous_normedSpace q this with ⟨C, C_pos, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ LocallyConvexSpace ℝ E
have this : IsTopologicalAddGroup E
Tactic: have := hp.topologicalAddGroup
-- 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 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ LocallyConvexSpace ℝ E
have hbasis : HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
Tactic: apply ofBasisZero ℝ E id fun s => s ∈ p.basisSets
-- 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 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
hbasis : HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
⊢ LocallyConvexSpace ℝ E
have hconvex : ∀ i ∈ p.basisSets, Convex ℝ (id i)
Tactic: apply ofBasisZero ℝ E id fun s => s ∈ p.basisSets
-- 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 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
have hbasis : HasBasis (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
  (fun (s : Set E) ↦ s ∈ p.basisSets) id
Tactic: rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : s ∈ p.basisSets
⊢ Convex ℝ (id s)
have hs₁ : Membership.mem (γ := Set (Set E)) (⋃ (s : Finset ι), ⋃ (r : ℝ), ⋃ (_ : 0 < r), {(s.sup p).ball 0 r}) s
Tactic: change s ∈ Set.iUnion _ at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : Membership.mem (γ := Set (Set E)) (⋃ (s : Finset ι), ⋃ (r : ℝ), ⋃ (_ : 0 < r), {(s.sup p).ball 0 r}) s
⊢ Convex ℝ (id s)
have hs₁ : ∃ (i : Finset ι) (i_1 : ℝ) (_ : 0 < i_1), s = (i.sup p).ball 0 i_1
Tactic: simp_rw [Set.mem_iUnion, Set.mem_singleton_iff] at hs
Cleared hypotheses: hs
-- 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 : NormedSpace ℝ 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : ∃ (i : Finset ι) (i_1 : ℝ) (_ : 0 < i_1), s = (i.sup p).ball 0 i_1
⊢ Convex ℝ (id s)
have hconvex : ∀ (I : Finset ι) (r : ℝ), 0 < r → Convex ℝ (id ((I.sup p).ball 0 r))
Tactic: rcases hs with ⟨I, r, _, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
⊢ (s.sup q).comp f = s.sup (q.comp f)
have h : ∀ (x : E), Eq (α := ℝ) (((s.sup q).comp f : (a : E) → ℝ) x : ℝ) ((s.sup (q.comp f) : (a : E) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ Eq (α := ℝ) (((s.sup q).comp f : (a : E) → ℝ) x : ℝ) ((s.sup (q.comp f) : (a : E) → ℝ) x : ℝ)
have h : (↑(s.sup fun (i : ι) ↦ NNReal.mk ((q i : (a : F) → ℝ) ((f : (a : E) → F) x : F)) sorry) : ℝ) =
  (↑(s.sup fun (i : ι) ↦ NNReal.mk ((q.comp f i : (a : E) → ℝ) x) sorry) : ℝ)
Tactic: rw [Seminorm.comp_apply, Seminorm.finset_sup_apply, Seminorm.finset_sup_apply]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
⊢ WithSeminorms (q.comp f)
have this : IsTopologicalAddGroup F
Tactic: have := hq.topologicalAddGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this : IsTopologicalAddGroup F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
⊢ WithSeminorms (q.comp f)
have this₁ : IsTopologicalAddGroup E
Tactic: have : IsTopologicalAddGroup E := topologicalAddGroup_induced f