awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (s.sup p).ball 0 (r / ‖x‖)
have h₁ : Membership.mem (γ := Set (Set F)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    ((s.sup p).ball 0 (r / ‖x‖)) ∧
  (s.sup p).ball 0 (r / ‖x‖) ⊆ (s.sup p).ball 0 (r / ‖x‖)
Tactic: use (s.sup p).ball 0 (r / ‖x‖)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
have neg : (s.sup p).ball 0 r ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
Tactic: refine ⟨(s.sup p).ball 0 r, p.basisSets_mem s hr, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ Eq.{u_7 + 1} (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
have refine_1 : ∀ (i : ι),
  LE.le (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
Tactic: refine le_antisymm (le_iInf fun i => ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
refine_1 :
  ∀ (i : ι),
    LE.le (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      (comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
⊢ Eq.{u_7 + 1} (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
have refine_2 : LE.le.{u_7} (α := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
  (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
Tactic: refine le_antisymm (le_iInf fun i => ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
⊢ LE.le (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
have refine_1 : ∀ (i' : ℝ),
  0 < i' →
    ∃ (i_1 : Set F),
      Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i_1 ∧
        id i_1 ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 i')
Tactic: rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff
        (Metric.nhds_basis_ball.comap _)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ∃ (i_1 : Set F),
    Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i_1 ∧
      id i_1 ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
have refine_1 : Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) ((p i).ball 0 ε)
Tactic: refine ⟨(p i).ball 0 ε, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
refine_1 :
  Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) ((p i).ball 0 ε)
⊢ ∃ (i_1 : Set F),
    Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i_1 ∧
      id i_1 ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
have refine_1₁ : id ((p i).ball 0 ε) ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
Tactic: refine ⟨(p i).ball 0 ε, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) ((p i).ball 0 ε)
have refine_1 : Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)
  ((Finset.sup {i} p).ball 0 ε)
Tactic: rw [← (Finset.sup_singleton : _ = p i)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ id ((p i).ball 0 ε) ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
have refine_1 : (p i).ball 0 ε ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
Tactic: rw [id, (p i).ball_zero_eq_preimage_ball]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
refine_1 : (p i).ball 0 ε ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
⊢ id ((p i).ball 0 ε) ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
have refine_1₁ : Subset (α := Set F) (preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε))
  (preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε))
Tactic: rw [id, (p i).ball_zero_eq_preimage_ball]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ LE.le.{u_7} (α := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
have refine_2 : ∀ (i' : Set F),
  Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i' →
    Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id i')
Tactic: rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
U : Set F
hU : U ∈ p.basisSets
⊢ Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id U)
have refine_2 : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : (s.sup p).ball 0 r ∈ p.basisSets),
  Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id ((s.sup p).ball 0 r))
Tactic: rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id ((s.sup p).ball 0 r))
have refine_2 : ∀ i ∈ s, Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) ((p i).ball 0 r)
Tactic: rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
U : Set E
hU : U ∈ p.basisSets
⊢ Membership.mem (γ := Filter E) (𝓝 0) U
have obtain : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : (s.sup p).ball 0 r ∈ p.basisSets),
  Membership.mem (γ := Filter E) (𝓝 0) ((s.sup p).ball 0 r)
Tactic: obtain ⟨s, r, hr, rfl⟩ := p.basisSets_iff.mp hU
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((s.sup p).ball 0 r)
have refine : Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)
Tactic: refine Seminorm.ball_mem_nhds ?_ hr
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
r : ℝ
hr : 0 < r
a : ι
s : Finset ι
h : a ∉ s
hs : Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⇑((insert a s).sup p) : (a : E) → ℝ)
have insert : Continuous[inst_3, _] ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ))
Tactic: simp only [Finset.sup_insert, coe_sup]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)
have empty : Continuous[inst_3, _] (⇑(Finset.sup ∅ p) : (a : E) → ℝ)
Tactic: induction s using Finset.induction_on with
  | empty => simpa using continuous_zero
  | insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
s : Finset ι
r : ℝ
hr : 0 < r
empty : Continuous[inst_3, _] (⇑(Finset.sup ∅ p) : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∀ (hs : Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)),
      Continuous[inst_3, _] (⇑((insert a s).sup p) : (a : E) → ℝ)
Tactic: induction s using Finset.induction_on with
  | empty => simpa using continuous_zero
  | insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)
have empty : Continuous[inst_3, _] (⇑(Finset.sup ∅ p) : (a : E) → ℝ)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simpa using continuous_zero
  | insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
s : Finset ι
r : ℝ
hr : 0 < r
empty : Continuous[inst_3, _] (⇑(Finset.sup ∅ p) : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∀ (hs : Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)),
      Continuous[inst_3, _] (⇑((insert a s).sup p) : (a : E) → ℝ)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simpa using continuous_zero
  | insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs
Cleared hypotheses: s
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
H :
  ∀ (i : ι'),
    ∃ (s : Finset ι) (C : ℝ),
      ∀ (x : E), (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HMul.hMul (β := ℝ) C ((s.sup p : (a : E) → ℝ) x : ℝ)
⊢ ∀ (i : ι'), ∃ (s : Finset ι) (C : ℝ≥0), (q i).comp f ≤ C • s.sup p
have h : ∀ (i : ι') (s : Finset ι)
  (H :
    ∃ (C : ℝ),
      ∀ (x : E), (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HMul.hMul (β := ℝ) C ((s.sup p : (a : E) → ℝ) x : ℝ)),
  ∃ (C : ℝ≥0), (q i).comp f ≤ C • s.sup p
Tactic: peel H with i s H
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
H_1 :
  ∀ (i : ι'),
    ∃ (s : Finset ι) (C : ℝ),
      ∀ (x : E), (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HMul.hMul (β := ℝ) C ((s.sup p : (a : E) → ℝ) x : ℝ)
i : ι'
s : Finset ι
H :
  ∃ (C : ℝ),
    ∀ (x : E), (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HMul.hMul (β := ℝ) C ((s.sup p : (a : E) → ℝ) x : ℝ)
⊢ ∃ (C : ℝ≥0), (q i).comp f ≤ C • s.sup p
have h : ∀ (C : ℝ)
  (hC :
    ∀ (x : E), (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HMul.hMul (β := ℝ) C ((s.sup p : (a : E) → ℝ) x : ℝ)),
  ∃ (C : ℝ≥0), (q i).comp f ≤ C • s.sup p
Tactic: obtain ⟨C, hC⟩ := H
Cleared hypotheses: H
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
H :
  ∀ (i : ι'),
    ∃ (s : Finset ι) (C : ℝ),
      ∀ (x : E), (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HMul.hMul (β := ℝ) C ((s.sup p : (a : E) → ℝ) x : ℝ)
i : ι'
s : Finset ι
C : ℝ
hC : ∀ (x : E), (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HMul.hMul (β := ℝ) C ((s.sup p : (a : E) → ℝ) x : ℝ)
⊢ ∃ (C : ℝ≥0), (q i).comp f ≤ C • s.sup p
have h : ∀ (x : E),
  (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HSMul.hSMul (β := ℝ) C.toNNReal ((s.sup p : (a : E) → ℝ) x : ℝ)
Tactic: refine ⟨C.toNNReal, fun x ↦ show q i (f x) ≤ C.toNNReal • ((s.sup p) x) from ?_⟩
-- 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_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_11
inst_7 : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ IsBounded (fun (x : ι) ↦ p) q f ↔ ∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p
have mp : IsBounded (fun (x : ι) ↦ p) q f → ∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p
Tactic: constructor
-- 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_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_11
inst_7 : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
mp : IsBounded (fun (x : ι) ↦ p) q f → ∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p
⊢ IsBounded (fun (x : ι) ↦ p) q f ↔ ∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p
have mpr : (∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p) → IsBounded (fun (x : ι) ↦ p) q f
Tactic: constructor
-- 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_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_11
inst_7 : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : IsBounded (fun (x : ι) ↦ p) q f
i : ι'
⊢ ∃ (C : ℝ≥0), (q i).comp f ≤ C • p
have mp : ∀ (s : Finset ι) (C : ℝ≥0) (h : (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (x : ι) ↦ p)),
  ∃ (C : ℝ≥0), (q i).comp f ≤ C • p
Tactic: rcases h i with ⟨s, C, h⟩
-- 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_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
ι : Type u_11
inst_7 : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : ∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p
i : ι'
⊢ ∃ (s : Finset ι) (C : ℝ≥0), (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (x : ι) ↦ p)
have h₁ : ∃ (C : ℝ≥0), (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (Finset.sup {Classical.arbitrary ι} fun (x : ι) ↦ p)
Tactic: use {Classical.arbitrary ι}
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
Tactic: obtain rfl | _ := s'.eq_empty_or_nonempty
Cleared hypotheses: s'
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have inr : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
Tactic: obtain rfl | _ := s'.eq_empty_or_nonempty
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
h : s'.Nonempty
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have inr : ∀ (fₛ : (i : ι') → Finset ι) (fC : (i : ι') → ℝ≥0) (hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p),
  ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
Tactic: choose fₛ fC hf using hf
Cleared hypotheses: hf
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have h : (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: use s'.card • s'.sup fC, Finset.biUnion s' fₛ
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
i : ι'
hi : i ∈ s'
⊢ (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
have refine : (fₛ i).sup p ≤ (s'.biUnion fₛ).sup p
Tactic: refine (hf i).trans (smul_le_smul ?_ (Finset.le_sup hi))
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
⊢ (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
have hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
Tactic: have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • (Finset.biUnion s' fₛ).sup p := by
    intro i hi
    refine (hf i).trans (smul_le_smul ?_ (Finset.le_sup hi))
    exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)
-- 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
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
have h : comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: refine (comp_mono f (finset_sup_le_sum q s')).trans ?_