internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
Proof 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)
Proof state after:
no goals
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_left
Proof 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 : α
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (a * b)
Tactic:
rw [mul_comm]
Proof 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 : α
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (b * a)
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_left
Proof 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 : α
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (b * a)
Tactic:
exact mul_right hb a
Proof state after:
no goals
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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⟩
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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⟩
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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⟩
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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]
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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)
Proof 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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.add
Proof 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 _ _)
Proof state after:
no goals
Theorem: MvPowerSeries.IsTopologicallyNilpotent.zero
Proof 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 α
x✝ : ℕ
hi : x✝ ≥ 1
⊢ 0 ^ x✝ = 0
Tactic:
rw [zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)]
Proof state after:
no goals
Theorem: MvPowerSeries.EvalDomain.map
Proof 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => φ (a s)) Filter.cofinite (nhds 0)
Tactic:
apply Filter.Tendsto.comp
Proof state after:
case hg
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto ⇑φ ?y (nhds 0)

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite ?y

case y
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter R
Theorem: MvPowerSeries.EvalDomain.map
Proof state before:
case hg
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto ⇑φ ?y (nhds 0)

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite ?y

case y
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter R
Tactic:
convert hφ.tendsto 0
Proof state after:
case h.e'_5.h.e'_3
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ 0 = φ 0

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 0)
Theorem: MvPowerSeries.EvalDomain.map
Proof state before:
case h.e'_5.h.e'_3
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ 0 = φ 0

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 0)
Tactic:
rw [RingHom.map_zero]
Proof state after:
case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 0)