-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem partial_sups [Preorder ι] [LocallyFiniteOrderBot ι] {p : SeminormFamily 𝕜 E ι}
    [TopologicalSpace E] (hp : WithSeminorms p) : WithSeminorms (fun i ↦ (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded (fun i => (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup fun i => (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ((fun i => (Finset.Iic i).sup p) i).comp LinearMap.id ≤ (Finset.Iic i).sup p

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁶ : Nonempty ι
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms fun i => (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded p (fun i => (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded (fun i => (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded p (fun i => (Finset.Iic i).sup p) LinearMap.id

Tactic:
intro i

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁶ : Nonempty ι
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, ((fun i => (Finset.Iic i).sup p) i).comp LinearMap.id ≤ C • 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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, ((fun i => (Finset.Iic i).sup p) i).comp LinearMap.id ≤ C • s.sup p

Tactic:
refine ⟨Finset.Iic i, 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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ((fun i => (Finset.Iic i).sup p) i).comp LinearMap.id ≤ 1 • (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {i}.sup fun i => (Finset.Iic i).sup p

Tactic:
rw [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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ (Finset.Iic i).sup p

Tactic:
exact (Finset.le_sup (Finset.mem_Iic.mpr le_rfl) : p i ≤ (Finset.Iic i).sup p)

Result:
no goals

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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup fun i => (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {i}.sup fun i => (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ((fun i => (Finset.Iic i).sup p) i).comp LinearMap.id ≤ 1 • (Finset.Iic i).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
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ((fun i => (Finset.Iic i).sup p) i).comp LinearMap.id ≤ (Finset.Iic i).sup p