Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq (DividedPowers/ForMathlib/Topology/LinearTopology.lean)

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
⊢ ⋯.topology = hB.topology
Tactic:
rw [TopologicalSpace.ext_iff_nhds]
State after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
⊢ ∀ (x : α), nhds x = nhds x

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
⊢ ∀ (x : α), nhds x = nhds x
Tactic:
intro a
State after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ nhds a = nhds a

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ nhds a = nhds a
Tactic:
simp [AddGroupFilterBasis.nhds_eq]
State after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ RingFilterBasis.toAddGroupFilterBasis.N a = RingFilterBasis.toAddGroupFilterBasis.N a

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ RingFilterBasis.toAddGroupFilterBasis.N a = RingFilterBasis.toAddGroupFilterBasis.N a
Tactic:
simp only [AddGroupFilterBasis.N]
State after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter =
    Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter =
    Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter
Tactic:
apply congr_arg₂ _ rfl
State after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ AddGroupFilterBasis.toFilterBasis.filter = AddGroupFilterBasis.toFilterBasis.filter

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ AddGroupFilterBasis.toFilterBasis.filter = AddGroupFilterBasis.toFilterBasis.filter
Tactic:
ext s
State after:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ s ∈ AddGroupFilterBasis.toFilterBasis.filter ↔ s ∈ AddGroupFilterBasis.toFilterBasis.filter

State before:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ s ∈ AddGroupFilterBasis.toFilterBasis.filter ↔ s ∈ AddGroupFilterBasis.toFilterBasis.filter
Tactic:
simp only [FilterBasis.mem_filter_iff]
State after:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) ↔ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

State before:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) ↔ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

case a.mpr
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

State before:
case a.mp
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
rintro ⟨u, ⟨⟨v, ⟨i, rfl⟩⟩, rfl⟩, hus⟩
State after:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup ((fun x => ↑x) i)) ⟨B i, ⋯⟩) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

State before:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup ((fun x => ↑x) i)) ⟨B i, ⋯⟩) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
simp only [Submodule.coe_toAddSubgroup] at hus
State after:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

State before:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
exact ⟨B i, ⟨i, rfl⟩, hus⟩
State after:
no goals

State before:
case a.mpr
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
rintro ⟨u, ⟨i, rfl⟩, hus⟩
State after:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup (B i)) i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

State before:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup (B i)) i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
simp only [Submodule.coe_toAddSubgroup] at hus
State after:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

State before:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
refine ⟨B i, ⟨⟨B i, ⟨i, rfl⟩⟩, rfl⟩, hus⟩
State after:
no goals