-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.firstCountableTopology (hp : WithSeminorms p) :
    FirstCountableTopology E

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝² : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 E).IsCountablyGenerated
⊢ FirstCountableTopology E

Tactic:
exact UniformSpace.firstCountableTopology E

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ FirstCountableTopology E

Tactic:
have := hp.topologicalAddGroup

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ FirstCountableTopology E

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ FirstCountableTopology E

Tactic:
let _ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
⊢ FirstCountableTopology E

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ (𝓝 0).IsCountablyGenerated

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ (⨅ i, comap (⇑(p i)) (𝓝 0)).IsCountablyGenerated

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ FirstCountableTopology E

Tactic:
have : (𝓝 (0 : E)).IsCountablyGenerated := by
  rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
  exact Filter.iInf.isCountablyGenerated _

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝¹ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (𝓝 0).IsCountablyGenerated
⊢ FirstCountableTopology E

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
⊢ FirstCountableTopology E

Tactic:
have : UniformAddGroup E := uniformAddGroup_of_addCommGroup

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ FirstCountableTopology E

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ (⨅ i, comap (⇑(p i)) (𝓝 0)).IsCountablyGenerated

Tactic:
exact Filter.iInf.isCountablyGenerated _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝¹ : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (𝓝 0).IsCountablyGenerated
⊢ FirstCountableTopology E

Tactic:
have : (uniformity E).IsCountablyGenerated := UniformAddGroup.uniformity_countably_generated

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Nonempty ι
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
this✝² : IsTopologicalAddGroup E
x✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 E).IsCountablyGenerated
⊢ FirstCountableTopology E