internlm/Lean-Github huggingface dataset:
Theorem: Ideal.IsBasis.mem_nhds_zero_iff
Proof 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⟩
Proof state after:
no goals
Theorem: Ideal.IsBasis.mem_nhds_zero_iff
Proof 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⟩
Proof 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
Theorem: Ideal.IsBasis.mem_nhds_zero_iff
Proof 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
Proof state after:
no goals
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
⊢ ⋯.topology = hB.topology
Tactic:
rw [TopologicalSpace.ext_iff_nhds]
Proof state after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
⊢ ∀ (x : α), nhds x = nhds x
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
⊢ ∀ (x : α), nhds x = nhds x
Tactic:
intro a
Proof state after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ nhds a = nhds a
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ nhds a = nhds a
Tactic:
simp [AddGroupFilterBasis.nhds_eq]
Proof state after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ RingFilterBasis.toAddGroupFilterBasis.N a = RingFilterBasis.toAddGroupFilterBasis.N a
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ RingFilterBasis.toAddGroupFilterBasis.N a = RingFilterBasis.toAddGroupFilterBasis.N a
Tactic:
simp only [AddGroupFilterBasis.N]
Proof state after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter =
    Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter =
    Filter.map (fun y => a + y) AddGroupFilterBasis.toFilterBasis.filter
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ AddGroupFilterBasis.toFilterBasis.filter = AddGroupFilterBasis.toFilterBasis.filter
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
⊢ AddGroupFilterBasis.toFilterBasis.filter = AddGroupFilterBasis.toFilterBasis.filter
Tactic:
ext s
Proof state after:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ s ∈ AddGroupFilterBasis.toFilterBasis.filter ↔ s ∈ AddGroupFilterBasis.toFilterBasis.filter
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ s ∈ AddGroupFilterBasis.toFilterBasis.filter ↔ s ∈ AddGroupFilterBasis.toFilterBasis.filter
Tactic:
simp only [FilterBasis.mem_filter_iff]
Proof state after:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) ↔ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) ↔ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
constructor
Proof state after:
case a.mp
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s

case a.mpr
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a.mp
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
rintro ⟨u, ⟨⟨v, ⟨i, rfl⟩⟩, rfl⟩, hus⟩
Proof state after:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup ((fun x => ↑x) i)) ⟨B i, ⋯⟩) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup ((fun x => ↑x) i)) ⟨B i, ⋯⟩) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
simp only [Submodule.coe_toAddSubgroup] at hus
Proof state after:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a.mp.intro.intro.intro.mk.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
exact ⟨B i, ⟨i, rfl⟩, hus⟩
Proof state after:
no goals
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a.mpr
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
⊢ (∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s) → ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
rintro ⟨u, ⟨i, rfl⟩, hus⟩
Proof state after:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup (B i)) i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑((fun i => Submodule.toAddSubgroup (B i)) i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
simp only [Submodule.coe_toAddSubgroup] at hus
Proof state after:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Theorem: Ideal.IsBasis.ofIdealBasis_topology_eq
Proof state before:
case a.mpr.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
a : α
s : Set α
i : ι
hus : ↑(B i) ⊆ s
⊢ ∃ s_1 ∈ AddGroupFilterBasis.toFilterBasis, s_1 ⊆ s
Tactic:
refine ⟨B i, ⟨⟨B i, ⟨i, rfl⟩⟩, rfl⟩, hus⟩
Proof state after:
no goals
Theorem: IdealBasis.mem_nhds_zero_iff
Proof 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]
Proof 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
Theorem: IdealBasis.mem_nhds_zero_iff
Proof 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]
Proof 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
Theorem: IdealBasis.mem_nhds_zero_iff
Proof 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
Proof 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
Theorem: IdealBasis.mem_nhds_zero_iff
Proof 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⟩
Proof 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
Theorem: IdealBasis.mem_nhds_zero_iff
Proof 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⟩
Proof state after:
no goals
Theorem: IdealBasis.mem_nhds_zero_iff
Proof 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⟩
Proof 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
Theorem: IdealBasis.mem_nhds_zero_iff
Proof 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⟩
Proof state after:
no goals
Theorem: LinearTopology.mem_nhds_zero_iff
Proof state before:
α : Type u
inst✝¹ : Ring α
inst✝ : TopologicalSpace α
hL : LinearTopology α
s : Set α
⊢ s ∈ nhds 0 ↔ ∃ i ∈ toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ s
Tactic:
rw [TopologicalSpace.ext_iff_nhds.mp hL.isTopology,
  hL.toIdealBasis.mem_nhds_zero_iff]
Proof state after:
no goals
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
⊢ Filter.Tendsto (a * b) f (nhds 0)
Tactic:
intro v hv
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : v ∈ nhds 0
⊢ v ∈ Filter.map (a * b) f
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : v ∈ nhds 0
⊢ v ∈ Filter.map (a * b) f
Tactic:
rw [LinearTopology.mem_nhds_zero_iff] at hv
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : ∃ i ∈ toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ v
⊢ v ∈ Filter.map (a * b) f
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
hv : ∃ i ∈ toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ v
⊢ v ∈ Filter.map (a * b) f
Tactic:
obtain ⟨I, _, I_mem, I_le⟩ := hv
Proof state after:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ≤ v
⊢ v ∈ Filter.map (a * b) f
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ≤ v
⊢ v ∈ Filter.map (a * b) f
Tactic:
simp only [Set.le_eq_subset] at I_le
Proof state after:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ v ∈ Filter.map (a * b) f
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
case intro.intro.intro
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ v ∈ Filter.map (a * b) f
Tactic:
apply Filter.sets_of_superset _ _ I_le
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ ↑I ∈ (Filter.map (a * b) f).sets
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ ↑I ∈ (Filter.map (a * b) f).sets
Tactic:
simp only [Filter.mem_sets, Filter.mem_map]
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : Filter.Tendsto b f (nhds 0)
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f
Tactic:
rw [Filter.tendsto_def] at hb
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : ∀ s ∈ nhds 0, b ⁻¹' s ∈ f
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
hb : ∀ s ∈ nhds 0, b ⁻¹' s ∈ f
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
⊢ (a * b) ⁻¹' ↑I ∈ f
Tactic:
specialize hb _ I_mem
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ (a * b) ⁻¹' ↑I ∈ f
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ (a * b) ⁻¹' ↑I ∈ f
Tactic:
apply Filter.sets_of_superset _ hb
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ b ⁻¹' ↑I ⊆ (a * b) ⁻¹' ↑I
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
⊢ b ⁻¹' ↑I ⊆ (a * b) ⁻¹' ↑I
Tactic:
intro x
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ x ∈ b ⁻¹' ↑I → x ∈ (a * b) ⁻¹' ↑I
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ x ∈ b ⁻¹' ↑I → x ∈ (a * b) ⁻¹' ↑I
Tactic:
simp only [Set.mem_preimage, Pi.mul_apply, SetLike.mem_coe]
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ b x ∈ I → a x * b x ∈ I
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
⊢ b x ∈ I → a x * b x ∈ I
Tactic:
intro hx
Proof state after:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
hx : b x ∈ I
⊢ a x * b x ∈ I
Theorem: LinearTopology.tendsto_zero_mul
Proof state before:
α : Type u
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : LinearTopology α
ι : Type u_1
f : Filter ι
a b : ι → α
v : Set α
I : Ideal α
left✝ : I ∈ toIdealBasis.sets
I_mem : ↑I ∈ nhds 0
I_le : ↑I ⊆ v
hb : b ⁻¹' ↑I ∈ f
x : ι
hx : b x ∈ I
⊢ a x * b x ∈ I
Tactic:
apply Ideal.mul_mem_left _ _ hx
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_pow
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
⊢ (coeff α d) (f ^ n) = ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f
Tactic:
suffices f ^ n = (Finset.range n).prod fun _ => f by
  rw [this, coeff_prod]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = ∏ x ∈ range n, f
Theorem: MvPowerSeries.coeff_pow
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = ∏ x ∈ range n, f
Tactic:
rw [Finset.prod_const, card_range]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_pow
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ (coeff α d) (f ^ n) = ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f
Tactic:
rw [this, coeff_prod]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ (coeff α d) (f ^ n) = 0
Tactic:
rw [coeff_pow]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f = 0
Tactic:
apply sum_eq_zero
Proof state after:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ ∀ x ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (x i)) f = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ ∀ x ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (x i)) f = 0
Tactic:
intro k hk
Proof state after:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k ∈ (range n).piAntidiagonal d
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k ∈ (range n).piAntidiagonal d
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0
Tactic:
rw [mem_piAntidiagonal'] at hk
Proof state after:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0