awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
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)
⊢ Membership.mem (γ := Filter E) (𝓝 0) U

Tactic:
obtain ⟨s, r, hr, rfl⟩ := p.basisSets_iff.mp hU

Premises used: Iff.mp, SeminormFamily.basisSets_iff, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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)

Tactic:
Seminorm.ball_mem_nhds ?_ hr

Premises used: Seminorm.ball_mem_nhds
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
refine : Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)
⊢ Membership.mem (γ := Filter E) (𝓝 0) ((s.sup p).ball 0 r)

Tactic:
refine Seminorm.ball_mem_nhds ?_ hr

Premises used: Seminorm.ball_mem_nhds
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
⊢ Continuous[inst_3, _] (⇑(Finset.sup ∅ p) : (a : E) → ℝ)

Tactic:
simpa using continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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) → ℝ)
insert : Continuous[inst_3, _] ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ))
⊢ Continuous[inst_3, _] (⇑((Insert.insert a s).sup p) : (a : E) → ℝ)

Tactic:
simp only [Finset.sup_insert, coe_sup]

Premises used: Finset.sup_insert, Seminorm.coe_sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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, _] ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ))

Tactic:
Continuous.max (hp a) hs

Premises used: Continuous.max
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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, _] ((⇑(p a) : (a : E) → ℝ) ⊔ (⇑(s.sup p) : (a : E) → ℝ))

Tactic:
exact Continuous.max (hp a) hs

Premises used: Continuous.max
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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) → ℝ)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∀ (hs : Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)),
        Continuous[inst_3, _] (⇑((Insert.insert a s).sup p) : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⇑(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

Premises used: Finset.sup_insert, Seminorm.coe_sup, Insert.insert, continuous_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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) → ℝ)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∀ (hs : Continuous[inst_3, _] (⇑(s.sup p) : (a : E) → ℝ)),
        Continuous[inst_3, _] (⇑((Insert.insert a s).sup p) : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⇑(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

Premises used: Finset.sup_insert, Seminorm.coe_sup, Insert.insert, continuous_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ℝ)
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
⊢ ∀ (i : ι'), ∃ (s : Finset ι) (C : ℝ≥0), (q i).comp f ≤ C • s.sup p

Tactic:
peel H with i s H
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ℝ)
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
⊢ ∃ (C : ℝ≥0), (q i).comp f ≤ C • s.sup p

Tactic:
obtain ⟨C, hC⟩ := H
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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

Tactic:
⟨C.toNNReal, fun x ↦ show q i (f x) ≤ C.toNNReal • ((s.sup p) x) from ?_⟩

Premises used: Exists.intro, Real.toNNReal
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ℝ)
h :
  ∀ (x : E),
    (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HSMul.hSMul (β := ℝ) C.toNNReal ((s.sup p : (a : E) → ℝ) x : ℝ)
⊢ ∃ (C : ℝ≥0), (q i).comp f ≤ C • s.sup p

Tactic:
refine ⟨C.toNNReal, fun x ↦ show q i (f x) ≤ C.toNNReal • ((s.sup p) x) from ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ℝ)
x : E
⊢ (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HSMul.hSMul (β := ℝ) C.toNNReal ((s.sup p : (a : E) → ℝ) x : ℝ)

Tactic:
(hC x).trans <| mul_le_mul_of_nonneg_right C.le_coe_toNNReal (apply_nonneg _ _)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, NonnegHomClass.apply_nonneg, Real.le_coe_toNNReal
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ℝ)
x : E
⊢ (q i : (a : F) → ℝ) ((f : (a : E) → F) x : F) ≤ HSMul.hSMul (β := ℝ) C.toNNReal ((s.sup p : (a : E) → ℝ) x : ℝ)

Tactic:
exact (hC x).trans <| mul_le_mul_of_nonneg_right C.le_coe_toNNReal (apply_nonneg _ _)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, NonnegHomClass.apply_nonneg, Real.le_coe_toNNReal
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
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 p (fun (x : ι') ↦ q) f ↔ ∃ (s : Finset ι) (C : ℝ≥0), q.comp f ≤ C • s.sup p

Tactic:
simp only [IsBounded, forall_const]

Premises used: Seminorm.IsBounded, forall_const
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
mpr : (∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p) → IsBounded (fun (x : ι) ↦ p) q f
⊢ IsBounded (fun (x : ι) ↦ p) q f ↔ ∀ (i : ι'), ∃ (C : ℝ≥0), (q i).comp f ≤ C • p

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ι'
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
⊢ ∃ (C : ℝ≥0), (q i).comp f ≤ C • p

Tactic:
rcases h i with ⟨s, C, h⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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_1 : IsBounded (fun (x : ι) ↦ p) q f
i : ι'
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:
⟨C, le_trans h (smul_le_smul (Finset.sup_le fun _ _ => le_rfl) le_rfl)⟩

Premises used: le_rfl, Finset.sup_le, Exists.intro, Seminorm.smul_le_smul, le_trans
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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_1 : IsBounded (fun (x : ι) ↦ p) q f
i : ι'
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:
exact ⟨C, le_trans h (smul_le_smul (Finset.sup_le fun _ _ => le_rfl) le_rfl)⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ι'
h₁ : ∃ (C : ℝ≥0), (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (Finset.sup {Classical.arbitrary ι} fun (x : ι) ↦ p)
⊢ ∃ (s : Finset ι) (C : ℝ≥0), (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (s.sup fun (x : ι) ↦ p)

Tactic:
use {Classical.arbitrary ι}

Premises used: Classical.arbitrary
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 : ι'
⊢ ∃ (C : ℝ≥0), (q i).comp f ≤ HSMul.hSMul (β := Seminorm 𝕜 E) C (Finset.sup {Classical.arbitrary ι} fun (x : ι) ↦ p)

Tactic:
simp only [h, Finset.sup_singleton]

Premises used: Finset.sup_singleton
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
inr : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p

Tactic:
obtain rfl | _ := s'.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
⊢ (Finset.sup ∅ q).comp f ≤ HSMul.hSMul (α := ℝ≥0) 1 (Finset.sup ∅ p)

Tactic:
simp [Seminorm.bot_eq_zero]

Premises used: Seminorm.bot_eq_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p

Tactic:
exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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
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
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p

Tactic:
choose fₛ fC hf using hf
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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_1 : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
h : (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p

Tactic:
use s'.card • s'.sup fC, Finset.biUnion s' fₛ

Premises used: Finset.biUnion, Finset.card, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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

Tactic:
(hf i).trans (smul_le_smul ?_ (Finset.le_sup hi))

Premises used: LE.le.trans, Seminorm.smul_le_smul, Finset.le_sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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'
refine : (fₛ i).sup p ≤ (s'.biUnion fₛ).sup p
⊢ (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p

Tactic:
refine (hf i).trans (smul_le_smul ?_ (Finset.le_sup hi))

Premises used: LE.le.trans, Seminorm.smul_le_smul, Finset.le_sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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'
⊢ (fₛ i).sup p ≤ (s'.biUnion fₛ).sup p

Tactic:
Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)

Premises used: Finset.subset_biUnion_of_mem, Finset.sup_mono
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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'
⊢ (fₛ i).sup p ≤ (s'.biUnion fₛ).sup p

Tactic:
exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)

Premises used: Finset.subset_biUnion_of_mem, Finset.sup_mono
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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 ∈ 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)
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
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

Tactic:
(comp_mono f (finset_sup_le_sum q s')).trans ?_

Premises used: Seminorm.comp_mono, LE.le.trans, Seminorm.finset_sup_le_sum