-- Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
/-- If the ring `R` is endowed with a linear topology, then the sets `↑basis σ R (J, d)`,
for `J : TwoSidedIdeal R` which are neighborhoods of `0 : R` and `d : σ →₀ ℕ`,
constitute a basis of neighborhoods of `0 : MvPowerSeries σ R` for the product topology. -/
lemma hasBasis_nhds_zero [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
    (𝓝 0 : Filter (MvPowerSeries σ R)).HasBasis
      (fun Id : TwoSidedIdeal R × (σ →₀ ℕ) ↦ (Id.1 : Set R) ∈ 𝓝 0)
      (fun Id ↦ basis _ _ Id)

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
f : (σ →₀ ℕ) → R
hf : ∀ e ≤ (I, hD.toFinset.sup id).2, (coeff R e) f ∈ (I, hD.toFinset.sup id).1
d : σ →₀ ℕ
hd : d ∈ (D, I).1
⊢ f d ∈ (fun x => ↑(D, I).2) d

Tactic:
convert hf _ <| Finset.le_sup (hD.mem_toFinset.mpr hd)

Result:
no goals

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : ↑(I, d).1 ∈ 𝓝 0
⊢ ∃ i, (i.1.Finite ∧ ↑i.2 ∈ 𝓝 0) ∧ (i.1.pi fun x => ↑i.2) ⊆ ↑(basis σ R (I, d))

Tactic:
refine ⟨⟨Iic d, I⟩, ⟨finite_Iic d, hI⟩, ?_⟩

Result:
case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : ↑(I, d).1 ∈ 𝓝 0
⊢ ((Iic d, I).1.pi fun x => ↑(Iic d, I).2) ⊆ ↑(basis σ R (I, d))

Proof state:
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ (𝓝 0).HasBasis (fun Id => ↑Id.1 ∈ 𝓝 0) fun Id => ↑(basis σ R Id)

Tactic:
rw [nhds_pi]

Result:
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ (Filter.pi fun i => 𝓝 (0 i)).HasBasis (fun Id => ↑Id.1 ∈ 𝓝 0) fun Id => ↑(basis σ R Id)

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i' : TwoSidedIdeal R × (σ →₀ ℕ)),
    ↑i'.1 ∈ 𝓝 0 → ∃ i, (i.1.Finite ∧ ↑i.2 ∈ 𝓝 0) ∧ (i.1.pi fun x => ↑i.2) ⊆ ↑(basis σ R i')

Tactic:
intro ⟨I, d⟩ hI

Result:
case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : ↑(I, d).1 ∈ 𝓝 0
⊢ ∃ i, (i.1.Finite ∧ ↑i.2 ∈ 𝓝 0) ∧ (i.1.pi fun x => ↑i.2) ⊆ ↑(basis σ R (I, d))

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : ↑(I, d).1 ∈ 𝓝 0
⊢ ((Iic d, I).1.pi fun x => ↑(Iic d, I).2) ⊆ ↑(basis σ R (I, d))

Tactic:
simpa [basis, coeff_apply, Iic, pi] using subset_rfl

Result:
no goals

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
⊢ ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ (D, I).1.pi fun x => ↑(D, I).2

Tactic:
refine ⟨⟨I, Finset.sup hD.toFinset id⟩, hI, fun f hf d hd ↦ ?_⟩

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
f : (σ →₀ ℕ) → R
hf : f ∈ ↑(basis σ R (I, hD.toFinset.sup id))
d : σ →₀ ℕ
hd : d ∈ (D, I).1
⊢ f d ∈ (fun x => ↑(D, I).2) d

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
f : (σ →₀ ℕ) → R
hf : f ∈ ↑(basis σ R (I, hD.toFinset.sup id))
d : σ →₀ ℕ
hd : d ∈ (D, I).1
⊢ f d ∈ (fun x => ↑(D, I).2) d

Tactic:
rw [SetLike.mem_coe, mem_basis_iff] at hf

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
f : (σ →₀ ℕ) → R
hf : ∀ e ≤ (I, hD.toFinset.sup id).2, (coeff R e) f ∈ (I, hD.toFinset.sup id).1
d : σ →₀ ℕ
hd : d ∈ (D, I).1
⊢ f d ∈ (fun x => ↑(D, I).2) d

Proof state:
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ (Filter.pi fun i => 𝓝 (0 i)).HasBasis (fun Id => ↑Id.1 ∈ 𝓝 0) fun Id => ↑(basis σ R Id)

Tactic:
refine IsLinearTopology.hasBasis_twoSidedIdeal.pi_self.to_hasBasis ?_ ?_

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i : Set (σ →₀ ℕ) × TwoSidedIdeal R),
    i.1.Finite ∧ ↑i.2 ∈ 𝓝 0 → ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ i.1.pi fun x => ↑i.2

case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i' : TwoSidedIdeal R × (σ →₀ ℕ)),
    ↑i'.1 ∈ 𝓝 0 → ∃ i, (i.1.Finite ∧ ↑i.2 ∈ 𝓝 0) ∧ (i.1.pi fun x => ↑i.2) ⊆ ↑(basis σ R i')

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i : Set (σ →₀ ℕ) × TwoSidedIdeal R),
    i.1.Finite ∧ ↑i.2 ∈ 𝓝 0 → ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ i.1.pi fun x => ↑i.2

Tactic:
intro ⟨D, I⟩ ⟨hD, hI⟩

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : ↑(D, I).2 ∈ 𝓝 0
⊢ ∃ i', ↑i'.1 ∈ 𝓝 0 ∧ ↑(basis σ R i') ⊆ (D, I).1.pi fun x => ↑(D, I).2