Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right (DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean)

State before:
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a : α
ha : IsTopologicallyNilpotent a
b : α
⊢ IsTopologicallyNilpotent (a * b)
Tactic:
intro v hv
State after:
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a : α
ha : IsTopologicallyNilpotent a
b : α
v : Set α
hv : v ∈ nhds 0
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop

State before:
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a : α
ha : IsTopologicallyNilpotent a
b : α
v : Set α
hv : v ∈ nhds 0
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop
Tactic:
rw [LinearTopology.mem_nhds_zero_iff] at hv
State after:
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a : α
ha : IsTopologicallyNilpotent a
b : α
v : Set α
hv : ∃ i ∈ LinearTopology.toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ v
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop

State before:
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a : α
ha : IsTopologicallyNilpotent a
b : α
v : Set α
hv : ∃ i ∈ LinearTopology.toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ v
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop
Tactic:
rcases hv with ⟨I, _, I_mem_nhds, I_subset⟩
State after:
case intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a : α
ha : IsTopologicallyNilpotent a
b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop

State before:
case intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a : α
ha : IsTopologicallyNilpotent a
b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop
Tactic:
specialize ha I_mem_nhds
State after:
case intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
ha : ↑I ∈ Filter.map (fun n => a ^ n) Filter.atTop
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop

State before:
case intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
ha : ↑I ∈ Filter.map (fun n => a ^ n) Filter.atTop
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop
Tactic:
simp only [Filter.mem_map, Filter.mem_atTop_sets, ge_iff_le, Set.mem_preimage, SetLike.mem_coe] at ha ⊢
State after:
case intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
ha : ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a ^ b ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v

State before:
case intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
ha : ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a ^ b ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v
Tactic:
rcases ha with ⟨n, ha⟩
State after:
case intro.intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v

State before:
case intro.intro.intro.intro
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v
Tactic:
use n
State after:
case h
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∀ (b_1 : ℕ), n ≤ b_1 → (a * b) ^ b_1 ∈ v

State before:
case h
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∀ (b_1 : ℕ), n ≤ b_1 → (a * b) ^ b_1 ∈ v
Tactic:
intro m hm
State after:
case h
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ (a * b) ^ m ∈ v

State before:
case h
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ (a * b) ^ m ∈ v
Tactic:
rw [mul_pow]
State after:
case h
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ a ^ m * b ^ m ∈ v

State before:
case h
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ a ^ m * b ^ m ∈ v
Tactic:
apply I_subset
State after:
case h.a
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ a ^ m * b ^ m ∈ ↑I

State before:
case h.a
σ : Type u_1
inst✝⁹ : DecidableEq σ
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : TopologicalSpace S
inst✝³ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
a b : α
v : Set α
I : Ideal α
left✝ : I ∈ LinearTopology.toIdealBasis.sets
I_mem_nhds : ↑I ∈ nhds 0
I_subset : ↑I ≤ v
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ a ^ m * b ^ m ∈ ↑I
Tactic:
apply I.mul_mem_right _ (ha m hm)
State after:
no goals