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

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ s ∈ nhds 0 ↔ ∃ i, ↑(B i) ∈ nhds 0 ∧ ↑(B i) ⊆ s
Tactic:
simp only [AddGroupFilterBasis.nhds_eq, AddGroupFilterBasis.N_zero,
  Filter.IsBasis.mem_filter_iff, FilterBasis.mem_filter_iff]
State after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) ↔
    ∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s

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

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

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

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

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

State before:
case mpr
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
⊢ (∃ i, (∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)) ∧ ↑(B i) ⊆ s) →
    ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
rintro ⟨i, _, his⟩
State after:
case mpr.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
s : Set α
i : ι
left✝ : ∃ s ∈ AddGroupFilterBasis.toFilterBasis, s ⊆ ↑(B i)
his : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

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