internlm/Lean-Github huggingface dataset:
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq'
Proof state before:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N (Subalgebra.inclusion hB_le).toLinearMap)
      ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'
Tactic:
simp only [← LinearMap.rTensor_comp, ← LinearMap.comp_apply] at h
Proof state after:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA_le).toLinearMap)) t =
    (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA'_le).toLinearMap)) t'
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq'
Proof state before:
case right
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
hj' : A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
h✝ :
  (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA_le).toLinearMap) t) =
    (LinearMap.rTensor N A''.val.toLinearMap) ((LinearMap.rTensor N (Subalgebra.inclusion hA'_le).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA_le).toLinearMap)) t =
    (LinearMap.rTensor N ((Subalgebra.inclusion hB_le).toLinearMap ∘ₗ (Subalgebra.inclusion hA'_le).toLinearMap)) t'
⊢ (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t =
    (LinearMap.rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'
Tactic:
exact h
Proof state after:
no goals
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
⊢ A''.val.comp (Subalgebra.inclusion hA_le) = A.val
Tactic:
ext
Proof state after:
case H
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
x✝ : ↥A
⊢ (A''.val.comp (Subalgebra.inclusion hA_le)) x✝ = A.val x✝
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq'
Proof state before:
case H
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
x✝ : ↥A
⊢ (A''.val.comp (Subalgebra.inclusion hA_le)) x✝ = A.val x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq'
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
⊢ A''.val.comp (Subalgebra.inclusion hA'_le) = A'.val
Tactic:
ext
Proof state after:
case H
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
x✝ : ↥A'
⊢ (A''.val.comp (Subalgebra.inclusion hA'_le)) x✝ = A'.val x✝
Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq'
Proof state before:
case H
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t'
A'' : Subalgebra R S := A ⊔ A'
hA_le : A ≤ A ⊔ A' := le_sup_left
hA'_le : A' ≤ A ⊔ A' := le_sup_right
hj : A''.val.comp (Subalgebra.inclusion hA_le) = A.val
x✝ : ↥A'
⊢ (A''.val.comp (Subalgebra.inclusion hA'_le)) x✝ = A'.val x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.IsTopologicallyNilpotent.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 ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : IsTopologicallyNilpotent a
⊢ IsTopologicallyNilpotent (φ a)
Tactic:
unfold IsTopologicallyNilpotent at ha ⊢
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
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ a ^ n) Filter.atTop (nhds 0)
Theorem: MvPowerSeries.IsTopologicallyNilpotent.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 ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ a ^ n) Filter.atTop (nhds 0)
Tactic:
simp_rw [← map_pow]
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
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ (a ^ n)) Filter.atTop (nhds 0)
Theorem: MvPowerSeries.IsTopologicallyNilpotent.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 ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ (a ^ n)) Filter.atTop (nhds 0)
Tactic:
apply Filter.Tendsto.comp _ ha
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
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑φ) (nhds 0) (nhds 0)
Theorem: MvPowerSeries.IsTopologicallyNilpotent.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 ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑φ) (nhds 0) (nhds 0)
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 ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ 0 = φ 0
Theorem: MvPowerSeries.IsTopologicallyNilpotent.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 ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ 0 = φ 0
Tactic:
rw [map_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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 : α
ha : IsTopologicallyNilpotent a
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 : α
ha : IsTopologicallyNilpotent a
b : α
v : Set α
hv : v ∈ nhds 0
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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 : α
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
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 : α
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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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 : α
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⟩
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 : α
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
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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 : α
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
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
⊢ v ∈ Filter.map (fun n => (a * b) ^ n) Filter.atTop
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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
⊢ 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 ⊢
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
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v
Tactic:
rcases ha with ⟨n, 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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → (a * b) ^ b_1 ∈ v
Tactic:
use n
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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∀ (b_1 : ℕ), n ≤ b_1 → (a * b) ^ b_1 ∈ v
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
⊢ ∀ (b_1 : ℕ), n ≤ 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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ (a * b) ^ m ∈ v
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ (a * b) ^ m ∈ v
Tactic:
rw [mul_pow]
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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ a ^ m * b ^ m ∈ v
Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_right
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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ a ^ m * 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
n : ℕ
ha : ∀ (b : ℕ), n ≤ b → a ^ b ∈ I
m : ℕ
hm : n ≤ m
⊢ a ^ m * b ^ m ∈ ↑I