-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem finset_sups {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E]
    (hp : WithSeminorms p) : WithSeminorms (fun s : Finset ι ↦ s.sup p)

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms fun s => s.sup p

Tactic:
refine hp.congr ?_ ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded p (fun s => s.sup p) LinearMap.id

case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded (fun s => s.sup p) p LinearMap.id

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded p (fun s => s.sup p) LinearMap.id

Tactic:
intro s

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ∃ s_1 C, ((fun s => s.sup p) s).comp LinearMap.id ≤ C • s_1.sup p

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ p i

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ((fun s => s.sup p) s).comp LinearMap.id ≤ s.sup p

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ((fun s => s.sup p) s).comp LinearMap.id ≤ 1 • s.sup p

Tactic:
rw [one_smul]

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ((fun s => s.sup p) s).comp LinearMap.id ≤ s.sup p

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ∃ s_1 C, ((fun s => s.sup p) s).comp LinearMap.id ≤ C • s_1.sup p

Tactic:
refine ⟨s, 1, ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
s : Finset ι
⊢ ((fun s => s.sup p) s).comp LinearMap.id ≤ 1 • s.sup p

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup fun s => s.sup p

Tactic:
refine ⟨{{i}}, 1, ?_⟩

Result:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {{i}}.sup fun s => s.sup p

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded (fun s => s.sup p) p LinearMap.id

Tactic:
intro i

Result:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup fun s => s.sup p

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {{i}}.sup fun s => s.sup p

Tactic:
rw [Finset.sup_singleton, Finset.sup_singleton, one_smul]

Result:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : Nonempty ι
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ p i