-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem withSeminorms_iInf {κ : ι → Type*} [Nonempty ((i : ι) × κ i)] [∀ i, Nonempty (κ i)]
    {p : (i : ι) → SeminormFamily 𝕜 E (κ i)} {t : ι → TopologicalSpace E}
    (hp : ∀ i, WithSeminorms (topology := t i) (p i)) :
    WithSeminorms (topology := ⨅ i, t i) (SeminormFamily.sigma p)

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this : ∀ (i : ι), IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)

Tactic:
have : @IsTopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf inferInstance

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, UniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, ⨅ j, UniformSpace.toTopologicalSpace

Tactic:
exact iInf_congr hp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)

Tactic:
simp_rw [@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)] at hp ⊢

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, UniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, UniformSpace.toTopologicalSpace

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, UniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, UniformSpace.toTopologicalSpace

Tactic:
rw [iInf_sigma]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, UniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, ⨅ j, UniformSpace.toTopologicalSpace

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
⊢ WithSeminorms (SeminormFamily.sigma p)

Tactic:
have : ∀ i, @IsTopologicalAddGroup E (t i) _ :=
  fun i ↦ @WithSeminorms.topologicalAddGroup _ _ _ _ _ _ _ (t i) _ (hp i)

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
κ : ι → Type u_10
inst✝¹ : Nonempty ((i : ι) × κ i)
inst✝ : ∀ (i : ι), Nonempty (κ i)
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this : ∀ (i : ι), IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)