-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem filter_eq_iInf (p : SeminormFamily 𝕜 E ι) :
    p.moduleFilterBasis.toFilterBasis.filter = ⨅ i, (𝓝 0).comap (p i)

Proof state:
case refine_1.refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ({i}.sup p).ball 0 ε ∈ AddGroupFilterBasis.toFilterBasis

Tactic:
exact p.basisSets_mem {i} hε

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
⊢ AddGroupFilterBasis.toFilterBasis.filter = ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
refine le_antisymm (le_iInf fun i => ?_) ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
⊢ AddGroupFilterBasis.toFilterBasis.filter ≤ comap (⇑(p i)) (𝓝 0)

case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
⊢ ⨅ i, comap (⇑(p i)) (𝓝 0) ≤ AddGroupFilterBasis.toFilterBasis.filter

Proof state:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ id ((s.sup p).ball 0 r) ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]

Result:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ ∀ i ∈ s, (p i).ball 0 r ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
⊢ ∀ (i' : ℝ), 0 < i' → ∃ i_1 ∈ AddGroupFilterBasis.toFilterBasis, id i_1 ⊆ ⇑(p i) ⁻¹' Metric.ball 0 i'

Tactic:
intro ε hε

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ∃ i_1 ∈ AddGroupFilterBasis.toFilterBasis, id i_1 ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
⊢ AddGroupFilterBasis.toFilterBasis.filter ≤ comap (⇑(p i)) (𝓝 0)

Tactic:
rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff
    (Metric.nhds_basis_ball.comap _)]

Result:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
⊢ ∀ (i' : ℝ), 0 < i' → ∃ i_1 ∈ AddGroupFilterBasis.toFilterBasis, id i_1 ⊆ ⇑(p i) ⁻¹' Metric.ball 0 i'

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
⊢ ∀ i' ∈ AddGroupFilterBasis.toFilterBasis, id i' ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
rintro U (hU : U ∈ p.basisSets)

Result:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
U : Set E
hU : U ∈ p.basisSets
⊢ id U ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
⊢ ⨅ i, comap (⇑(p i)) (𝓝 0) ≤ AddGroupFilterBasis.toFilterBasis.filter

Tactic:
rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]

Result:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
⊢ ∀ i' ∈ AddGroupFilterBasis.toFilterBasis, id i' ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Proof state:
case refine_1.refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ id ((p i).ball 0 ε) ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε

Tactic:
rw [id, (p i).ball_zero_eq_preimage_ball]

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
U : Set E
hU : U ∈ p.basisSets
⊢ id U ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩

Result:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ id ((s.sup p).ball 0 r) ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Proof state:
case refine_1.refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ (p i).ball 0 ε ∈ AddGroupFilterBasis.toFilterBasis

Tactic:
rw [← (Finset.sup_singleton : _ = p i)]

Result:
case refine_1.refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ({i}.sup p).ball 0 ε ∈ AddGroupFilterBasis.toFilterBasis

Proof state:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ ∀ i ∈ s, (p i).ball 0 r ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
exact fun i _ =>
  Filter.mem_iInf_of_mem i
    ⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr,
      Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ∃ i_1 ∈ AddGroupFilterBasis.toFilterBasis, id i_1 ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε

Tactic:
refine ⟨(p i).ball 0 ε, ?_, ?_⟩

Result:
case refine_1.refine_1
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ (p i).ball 0 ε ∈ AddGroupFilterBasis.toFilterBasis

case refine_1.refine_2
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
p : SeminormFamily 𝕜 E ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ id ((p i).ball 0 ε) ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε