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

State before:
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ s ∈ nhds 0 ↔ ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ s
Tactic:
rw [Ideal.IsBasis.mem_nhds_zero_iff]
State after:
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ i, ↑↑i ∈ nhds 0 ∧ ↑↑i ⊆ s) ↔ ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ s

State before:
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ i, ↑↑i ∈ nhds 0 ∧ ↑↑i ⊆ s) ↔ ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ s
Tactic:
simp only [Subtype.exists, exists_and_left, exists_prop, Set.le_eq_subset]
State after:
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s) ↔ ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s

State before:
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s) ↔ ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s) → ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s

case mpr
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s) → ∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s

State before:
case mp
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s) → ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s
Tactic:
rintro ⟨a, mem_nhds, mem_sets, subset_s⟩
State after:
case mp.intro.intro.intro
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
a : Ideal α
mem_nhds : ↑a ∈ nhds 0
mem_sets : a ∈ B.sets
subset_s : ↑a ⊆ s
⊢ ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s

State before:
case mp.intro.intro.intro
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
a : Ideal α
mem_nhds : ↑a ∈ nhds 0
mem_sets : a ∈ B.sets
subset_s : ↑a ⊆ s
⊢ ∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s
Tactic:
exact ⟨a, mem_sets, mem_nhds, subset_s⟩
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
⊢ (∃ i ∈ B.sets, ↑i ∈ nhds 0 ∧ ↑i ⊆ s) → ∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s
Tactic:
rintro ⟨i, hi, mem_nhds, subset_s⟩
State after:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
i : Ideal α
hi : i ∈ B.sets
mem_nhds : ↑i ∈ nhds 0
subset_s : ↑i ⊆ s
⊢ ∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s

State before:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
B : IdealBasis α
s : Set α
i : Ideal α
hi : i ∈ B.sets
mem_nhds : ↑i ∈ nhds 0
subset_s : ↑i ⊆ s
⊢ ∃ a, ↑a ∈ nhds 0 ∧ a ∈ B.sets ∧ ↑a ⊆ s
Tactic:
exact ⟨i, mem_nhds, hi, subset_s⟩
State after:
no goals