Theorem: MvPowerSeries.IsTopologicallyNilpotent.add (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 b : α
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent 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 b : α
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent 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 b : α
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent 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 b : α
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent 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 b : α
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent 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 b : α
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent 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 b : α
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent 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 : α
hb : IsTopologicallyNilpotent 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 : α
hb : IsTopologicallyNilpotent 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:
specialize hb 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
hb : ↑I ∈ Filter.map (fun n => b ^ 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
hb : ↑I ∈ Filter.map (fun n => b ^ 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 hb
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
hb : ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → b ^ b_1 ∈ I
⊢ 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 : ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a ^ b ∈ I
hb : ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → b ^ b_1 ∈ I
⊢ v ∈ Filter.map (fun n => (a + b) ^ n) Filter.atTop
Tactic:
rcases ha with ⟨na, 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
hb : ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → b ^ b_1 ∈ I
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
⊢ v ∈ Filter.map (fun n => (a + b) ^ n) Filter.atTop

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
hb : ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → b ^ b_1 ∈ I
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
⊢ v ∈ Filter.map (fun n => (a + b) ^ n) Filter.atTop
Tactic:
rcases hb with ⟨nb, hb⟩
State after:
case intro.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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
⊢ v ∈ Filter.map (fun n => (a + b) ^ n) Filter.atTop

State before:
case intro.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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
⊢ 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]
State after:
case intro.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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a + b) ^ b_1 ∈ v

State before:
case intro.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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a + b) ^ b_1 ∈ v
Tactic:
use na + nb
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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
⊢ ∀ (b_1 : ℕ), na + nb ≤ 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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
⊢ ∀ (b_1 : ℕ), na + nb ≤ 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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
m : ℕ
hm : na + nb ≤ 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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
m : ℕ
hm : na + nb ≤ m
⊢ (a + 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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
m : ℕ
hm : na + nb ≤ m
⊢ (a + 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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
m : ℕ
hm : na + nb ≤ m
⊢ (a + b) ^ m ∈ ↑I
Tactic:
apply I.add_pow_mem_of_pow_mem_of_le (ha na le_rfl) (hb nb le_rfl)
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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
m : ℕ
hm : na + nb ≤ m
⊢ na + nb ≤ m + 1

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
na : ℕ
ha : ∀ (b : ℕ), na ≤ b → a ^ b ∈ I
nb : ℕ
hb : ∀ (b_1 : ℕ), nb ≤ b_1 → b ^ b_1 ∈ I
m : ℕ
hm : na + nb ≤ m
⊢ na + nb ≤ m + 1
Tactic:
apply le_trans hm (Nat.le_add_right _ _)
State after:
no goals