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
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
have refine_3 : ∀ (c : 𝕜) (c_pos : 0 < ‖c‖) (hc : ‖c‖ < r), Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
Tactic: obtain ⟨c, c_pos, hc⟩ : ∃ (c : 𝕜), 0 < ‖c‖ ∧ ‖c‖ < r := exists_norm_lt 𝕜 r_pos
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
have c_ne : c ≠ 0
Tactic: have c_ne : c ≠ 0 := (by simpa using c_pos)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ c • p.ball 0 1 ⊆ p.ball 0 r
have rw : p.ball 0 (‖c‖ * 1) ⊆ p.ball 0 r
Tactic: rw [smul_ball_zero c_ne]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
have this₁ : c • p.ball 0 1 ⊆ p.ball 0 r
Tactic: have : c • p.ball 0 1 ⊆ p.ball 0 r := by
      rw [smul_ball_zero c_ne]
      exact ball_mono (by simpa using hc.le)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this_1 : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
this : c • p.ball 0 1 ⊆ p.ball 0 r
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
have refine_3 : Membership.mem (γ := Filter E) (𝓝 0) (c • p.ball 0 1)
Tactic: grw [← this]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
⊢ Continuous[inst_7, inst_9] (⇑f : (a : E) → F)
have this : IsTopologicalAddGroup F
Tactic: have : IsTopologicalAddGroup F := hq.topologicalAddGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
⊢ Continuous[inst_7, inst_9] (⇑f : (a : E) → F)
have refine : ContinuousAt.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F) 0
Tactic: refine continuous_of_continuousAt_zero f ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
⊢ ContinuousAt.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F) 0
have simp_rw : ∀ (i : ι'),
  Tendsto.{u_6, 0} (α := E) (β := ℝ) (Function.comp (β := F) (⇑(q i) : (a : F) → ℝ) (⇑f : (a : E) → F)) (𝓝 0) (𝓝 0)
Tactic: simp_rw [ContinuousAt, f.map_zero, q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.tendsto_iInf,
    Filter.tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
i : ι'
⊢ Tendsto.{u_6, 0} (α := E) (β := ℝ) (Function.comp (β := F) (⇑(q i) : (a : F) → ℝ) (⇑f : (a : E) → F)) (𝓝 0) (𝓝 0)
have h : Eq (α := ℝ) (0 : ℝ) (((q i).comp f : (a : E) → ℝ) 0 : ℝ)
Tactic: convert! (hf i).continuousAt.tendsto
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
⊢ Continuous[x, x_1] (⇑f : (a : E) → F)
have this : IsTopologicalAddGroup E
Tactic: have : IsTopologicalAddGroup E := hp.topologicalAddGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
⊢ Continuous[x, x_1] (⇑f : (a : E) → F)
have refine : ∀ (i : ι'), Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)
Tactic: refine continuous_of_continuous_comp hq _ fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
⊢ Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)
have rcases : ∀ (s : Finset ι) (C : ℝ≥0) (hC : (q i).comp f ≤ C • s.sup p), Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)
Tactic: rcases hf i with ⟨s, C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ C • s.sup p
⊢ Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)
have hC₁ : (q i).comp f ≤ s.sup (C • p)
Tactic: rw [← Seminorm.finset_sup_smul] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x, _] (⇑((q i).comp f) : (a : E) → ℝ)
have refine : Continuous[x, _] (⇑(∑ i ∈ s, (C • p) i) : (a : E) → ℝ)
Tactic: refine Seminorm.continuous_of_le ?_ (hC.trans <| Seminorm.finset_sup_le_sum _ _)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x, _] (⇑(∑ i ∈ s, (C • p) i) : (a : E) → ℝ)
have change : Continuous[x, _] fun (x : E) ↦ (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (∑ i ∈ s, C • p i) x
Tactic: change Continuous (fun x ↦ Seminorm.coeFnAddMonoidHom _ _ (∑ i ∈ s, C • p i) x)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x : TopologicalSpace E
hp : WithSeminorms p
x_1 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x, _] fun (x : E) ↦ (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (∑ i ∈ s, C • p i) x
have simp_rw : Continuous[x, _] fun (x : E) ↦ ∑ c ∈ s, (coeFnAddMonoidHom 𝕝 E : (a : Seminorm 𝕝 E) → E → ℝ) (C • p c) x
Tactic: simp_rw [map_sum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
ι : Type u_9
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : NormedField 𝕝₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
F : Type u_11
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕝₂ F
inst_7 : TopologicalSpace E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : ∃ (s : Finset ι) (C : ℝ≥0), comp (normSeminorm 𝕝₂ F) f ≤ C • s.sup p
⊢ Continuous[inst_7, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : E) → F)
have hf₁ : Seminorm.IsBounded.{u_4, u_5, u_6, u_11, u_9, 0} (𝕜₂ := 𝕝₂) (F := F) (σ₁₂ := τ₁₂) p
  (fun (x : Fin 1) ↦ normSeminorm 𝕝₂ F) f
Tactic: rw [← Seminorm.isBounded_const (Fin 1)] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
F : Type u_7
ι : Type u_9
inst : NormedField 𝕝
inst_1 : AddCommGroup F
inst_2 : NormedField 𝕝₂
inst_3 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_4 : RingHomIsometric τ₁₂
E : Type u_11
inst_5 : SeminormedAddCommGroup E
inst_6 : NormedSpace 𝕝 E
inst_7 : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι), ∃ (C : ℝ≥0), (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕝 E) C (normSeminorm 𝕝 E)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_7] (⇑f : (a : E) → F)
have hf₁ : Seminorm.IsBounded.{u_4, u_5, u_11, u_7, 0, u_9} (𝕜 := 𝕝) (E := E) (σ₁₂ := τ₁₂) (fun (x : Fin 1) ↦ normSeminorm 𝕝 E) q f
Tactic: rw [← Seminorm.const_isBounded (Fin 1)] at hf
Cleared hypotheses: hf
-- 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 ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ WithSeminorms q
have topology_eq_withSeminorms : t = q.moduleFilterBasis.topology
Tactic: constructor
-- 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 ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ t = q.moduleFilterBasis.topology
have topology_eq_withSeminorms : p.moduleFilterBasis.topology = q.moduleFilterBasis.topology
Tactic: rw [hp.topology_eq_withSeminorms]
-- 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 ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology
have topology_eq_withSeminorms : p.moduleFilterBasis.topology ≤ q.moduleFilterBasis.topology
Tactic: refine le_antisymm ?_ ?_
-- 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 ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
topology_eq_withSeminorms : p.moduleFilterBasis.topology ≤ q.moduleFilterBasis.topology
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology
have topology_eq_withSeminorms₁ : q.moduleFilterBasis.topology ≤ p.moduleFilterBasis.topology
Tactic: refine le_antisymm ?_ ?_
-- 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 ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology ≤ q.moduleFilterBasis.topology
have topology_eq_withSeminorms : Continuous[p.moduleFilterBasis.topology, q.moduleFilterBasis.topology] id
Tactic: rw [← continuous_id_iff_le]
-- 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 ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ q.moduleFilterBasis.topology ≤ p.moduleFilterBasis.topology
have topology_eq_withSeminorms : Continuous[q.moduleFilterBasis.topology, p.moduleFilterBasis.topology] id
Tactic: rw [← continuous_id_iff_le]
-- 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
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := Finset ι) fun (s : Finset ι) ↦ s.sup p
have refine_1 : Seminorm.IsBounded p (fun (s : Finset ι) ↦ s.sup 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
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
refine_1 : Seminorm.IsBounded p (fun (s : Finset ι) ↦ s.sup p) LinearMap.id
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := Finset ι) fun (s : Finset ι) ↦ s.sup p
have refine_2 : Seminorm.IsBounded (fun (s : Finset ι) ↦ s.sup p) 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
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ∃ (s_1 : Finset ι) (C : ℝ≥0), comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id ≤ C • s_1.sup p
have refine_1 : comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 (s.sup p)
Tactic: refine ⟨s, 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
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 (s.sup p)
have refine_1 : LE.le.{u_6} (α := Seminorm 𝕜 E) (comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id)
  (comp ((fun (s : Finset ι) ↦ s.sup p) s) LinearMap.id)
Tactic: rw [one_smul]
-- 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
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ (s : Finset (Finset ι)) (C : ℝ≥0),
    (p i).comp LinearMap.id ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (s : Finset ι) ↦ s.sup p)
have refine_2 : (p i).comp LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {{i}} fun (s : Finset ι) ↦ s.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
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 E) 1 (Finset.sup {{i}} fun (s : Finset ι) ↦ s.sup p)
have refine_2 : (p i).comp LinearMap.id ≤ (p i).comp LinearMap.id
Tactic: rw [Finset.sup_singleton, 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
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
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (Finset.Iic i).sup p
have refine_1 : Seminorm.IsBounded p (fun (i : ι) ↦ (Finset.Iic i).sup 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
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
refine_1 : Seminorm.IsBounded p (fun (i : ι) ↦ (Finset.Iic i).sup p) LinearMap.id
⊢ WithSeminorms.{u_2, u_6, u_9} (𝕜 := 𝕜) (E := E) (ι := ι) fun (i : ι) ↦ (Finset.Iic i).sup p
have refine_2 : Seminorm.IsBounded (fun (i : ι) ↦ (Finset.Iic i).sup p) 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
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), comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id ≤ C • s.sup p
have refine_1 : comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 ((Finset.Iic i).sup p)
Tactic: refine ⟨Finset.Iic 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 : ι
⊢ comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id ≤ HSMul.hSMul (α := ℝ≥0) 1 ((Finset.Iic i).sup p)
have refine_1 : LE.le.{u_6} (α := Seminorm 𝕜 E) (comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id)
  (comp ((fun (i : ι) ↦ (Finset.Iic i).sup p) i) LinearMap.id)
Tactic: rw [one_smul]