awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
have h : ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: simp_rw [← pullback_apply, map_sum, pullback_apply]
-- 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
⊢ ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
have h : ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: refine (Finset.sum_le_sum hs).trans ?_
-- 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
⊢ ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
have h : s'.card • s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: rw [Finset.sum_const, smul_assoc]
-- 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_1 : 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
h : s'.card • s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
⊢ ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
have h₁ : s'.card • s'.sup fC • (s'.biUnion fₛ).sup p ≤ s'.card • s'.sup fC • (s'.biUnion fₛ).sup p
Tactic: rw [Finset.sum_const, smul_assoc]
-- 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: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
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: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
-- 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
inr 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
have inr₂ : 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
Tactic: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
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
hf : IsBounded p q f
s' : Finset ι'
inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
inr inr₁ : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
inr₂ :
  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
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have 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
Tactic: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
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
hf : IsBounded p q f
s' : Finset ι'
inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
inr inr₁ : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
inr₂ :
  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
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
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have 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: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
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
hf : IsBounded p q f
s' : Finset ι'
inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
inr inr₁ : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
inr₂ :
  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
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
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
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have 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),
    comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
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
hf : IsBounded p q f
s' : Finset ι'
inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
inr inr₁ : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
inr₂ :
  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
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
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
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),
      comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
have 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),
    ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
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
hf : IsBounded p q f
s' : Finset ι'
inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
inr inr₁ : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
inr₂ :
  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
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
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
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),
      comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
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),
      ∑ x ∈ s', (q x).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
have 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),
    ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Tactic: classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  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)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]
Cleared hypotheses: hf
-- 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 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ IsTopologicalAddGroup E
have rw : IsTopologicalAddGroup E
Tactic: rw [hp.withSeminorms_eq]
-- 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 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ ContinuousSMul 𝕜 E
have rw : ContinuousSMul 𝕜 E
Tactic: rw [hp.withSeminorms_eq]
-- 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 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
have rw : HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
Tactic: rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
-- 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 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ HasBasis.{u_6, u_9 + 1} (α := E) (𝓝 0) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2) fun (sr : Finset ι × ℝ) ↦
    (sr.1.sup p).ball 0 sr.2
have refine : ∀ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V ↔ ∃ (i : Finset ι × ℝ), 0 < i.2 ∧ (i.1.sup p).ball 0 i.2 ⊆ V
Tactic: refine ⟨fun V => ?_⟩
-- 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 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
V : Set E
⊢ Membership.mem (γ := Filter E) (𝓝 0) V ↔ ∃ (i : Finset ι × ℝ), 0 < i.2 ∧ (i.1.sup p).ball 0 i.2 ⊆ V
have simp : (∃ (i : Set E), (∃ (i_1 : Finset ι) (r : ℝ), 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ i ⊆ V) ↔
  ∃ (a : Finset ι) (b : ℝ), 0 < b ∧ (a.sup p).ball 0 b ⊆ V
Tactic: simp only [hp.hasBasis.mem_iff, SeminormFamily.basisSets_iff, Prod.exists, id_eq]
-- 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 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
⊢ (𝓝 x).HasBasis (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2) fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2
have this : IsTopologicalAddGroup E
Tactic: have : IsTopologicalAddGroup E := 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 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (𝓝 x).HasBasis (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2) fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2
have rw : HasBasis.{u_6, u_9 + 1} (α := E) (Filter.map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2)
  fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2
Tactic: rw [← map_add_left_nhds_zero]
-- 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 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ HasBasis.{u_6, u_9 + 1} (α := E) (Filter.map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2)
    fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2
have h : Eq (α := Finset ι × ℝ → Set E) (fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2) fun (i : Finset ι × ℝ) ↦
  (fun (x_1 : E) ↦ x + x_1) '' (i.1.sup p).ball 0 i.2
Tactic: convert! hp.hasBasis_zero_ball.map (x + ·) using 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 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ Eq (α := Finset ι × ℝ → Set E) (fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2) fun (i : Finset ι × ℝ) ↦
    (fun (x_1 : E) ↦ x + x_1) '' (i.1.sup p).ball 0 i.2
have h : ∀ (sr : Finset ι × ℝ), (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
Tactic: ext sr : 1
-- 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 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
sr : Finset ι × ℝ
⊢ (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
have this₁ : (sr.1.sup p).ball (HVAdd.hVAdd (β := E) x 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
Tactic: have : (sr.fst.sup p).ball (x +ᵥ (0 : E)) sr.snd = x +ᵥ (sr.fst.sup p).ball 0 sr.snd :=
    Eq.symm (Seminorm.vadd_ball (sr.fst.sup p))