internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e = e
Tactic:
apply le_antisymm
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e ≤ e

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e ≤ e

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Tactic:
. exact inf_le_right
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Tactic:
. by_contra h'
  simp only [AddSubsemigroup.mk_le_mk, setOf_subset_setOf] at h
  specialize h (monomial α e 1) _
  . intro e' he'
    apply coeff_monomial_ne
    intro hee'
    rw [hee'] at he'
    apply h'
    exact le_inf_iff.mpr ⟨he', le_rfl⟩
  apply one_ne_zero' α
  convert h e le_rfl
  rw [coeff_monomial_same]
Proof state after:
no goals
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e ≤ e
Tactic:
exact inf_le_right
Proof state after:
no goals
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Tactic:
by_contra h'
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
h' : ¬e ≤ d ⊓ e
⊢ False
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
h' : ¬e ≤ d ⊓ e
⊢ False
Tactic:
simp only [AddSubsemigroup.mk_le_mk, setOf_subset_setOf] at h
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ False
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ False
Tactic:
specialize h (monomial α e 1) _
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ ∀ e_1 ≤ d, (coeff α e_1) ((monomial α e) 1) = 0

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ ∀ e_1 ≤ d, (coeff α e_1) ((monomial α e) 1) = 0

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False
Tactic:
. intro e' he'
  apply coeff_monomial_ne
  intro hee'
  rw [hee'] at he'
  apply h'
  exact le_inf_iff.mpr ⟨he', le_rfl⟩
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False
Tactic:
apply one_ne_zero' α
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = 0
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = 0
Tactic:
convert h e le_rfl
Proof state after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = (coeff α e) ((monomial α e) 1)
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = (coeff α e) ((monomial α e) 1)
Tactic:
rw [coeff_monomial_same]
Proof state after:
no goals
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ ∀ e_1 ≤ d, (coeff α e_1) ((monomial α e) 1) = 0
Tactic:
intro e' he'
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ (coeff α e') ((monomial α e) 1) = 0
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ (coeff α e') ((monomial α e) 1) = 0
Tactic:
apply coeff_monomial_ne
Proof state after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ e' ≠ e
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ e' ≠ e
Tactic:
intro hee'
Proof state after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
hee' : e' = e
⊢ False
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
hee' : e' = e
⊢ False
Tactic:
rw [hee'] at he'
Proof state after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ False
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ False
Tactic:
apply h'
Proof state after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ e ≤ d ⊓ e
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ e ≤ d ⊓ e
Tactic:
exact le_inf_iff.mpr ⟨he', le_rfl⟩
Proof state after:
no goals
Theorem: MvPowerSeries.idealIsBasis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ⊓ basis σ α e
Tactic:
use d ⊔ e
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
d e : σ →₀ ℕ
⊢ basis σ α (d ⊔ e) ≤ basis σ α d ⊓ basis σ α e
Theorem: MvPowerSeries.idealIsBasis
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
d e : σ →₀ ℕ
⊢ basis σ α (d ⊔ e) ≤ basis σ α d ⊓ basis σ α e
Tactic:
apply Antitone.map_sup_le (basis_antitone σ α)
Proof state after:
no goals
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ↑(basis σ α d) ∈ nhds 0
Tactic:
rw [nhds_pi, Filter.mem_pi]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ ↑(basis σ α d)
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ ↑(basis σ α d)
Tactic:
use Finset.Iic d, Finset.finite_toSet _, (fun e => if e ≤ d then {0} else univ)
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)) ∧
    ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)) ∧
    ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)
Tactic:
constructor
Proof state after:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)

case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)
Tactic:
intro e
Proof state after:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ (if e ≤ d then {0} else univ) ∈ nhds (0 e)
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ (if e ≤ d then {0} else univ) ∈ nhds (0 e)
Tactic:
split_ifs with h
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ {0} ∈ nhds (0 e)

case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ {0} ∈ nhds (0 e)

case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Tactic:
. simp only [nhds_discrete, Filter.mem_pure, mem_singleton_iff]
  rfl
Proof state after:
case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Tactic:
. simp only [Filter.univ_mem]
Proof state after:
no goals
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ {0} ∈ nhds (0 e)
Tactic:
simp only [nhds_discrete, Filter.mem_pure, mem_singleton_iff]
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ OfNat.ofNat 0 e = 0
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ OfNat.ofNat 0 e = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Tactic:
simp only [Filter.univ_mem]
Proof state after:
no goals
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)
Tactic:
intro f
Proof state after:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (f ∈ (↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) → f ∈ ↑(basis σ α d)
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (f ∈ (↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) → f ∈ ↑(basis σ α d)
Tactic:
simp only [Finset.coe_Iic, mem_pi, mem_Iic, mem_ite_univ_right, mem_singleton_iff, mem_coe]
Proof state after:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (∀ i ≤ d, i ≤ d → f i = 0) → f ∈ basis σ α d
Theorem: MvPowerSeries.basis_mem_nhds_zero
Proof state before:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (∀ i ≤ d, i ≤ d → f i = 0) → f ∈ basis σ α d
Tactic:
exact forall_imp (fun e h he => h he he)
Proof state after:
no goals
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ := MvPowerSeries.WithPiTopology.topologicalSpace σ α
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ' := (toRingSubgroupsBasis σ α).topology
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
erw [TopologicalAddGroup.ext_iff_nhds_zero τ τ']
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0
Tactic:
ext s
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0
Tactic:
rw [(RingSubgroupsBasis.hasBasis_nhds (toRingSubgroupsBasis σ α) 0).mem_iff]
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s
Tactic:
simp only [sub_zero, Submodule.mem_toAddSubgroup, exists_true_left, true_and]
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
refine' ⟨_, fun ⟨d, hd⟩ => (@nhds _ τ 0).sets_of_superset (basis_mem_nhds_zero σ α d) hd⟩
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 → ∃ i, {b | b ∈ basis σ α i} ⊆ s
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 → ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
rw [nhds_pi, Filter.mem_pi]
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ s) → ∃ i, {b | b ∈ basis σ α i} ⊆ s
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ s) → ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
rintro ⟨D, hD, t, ht, ht'⟩
Proof state after:
case a.intro.intro.intro.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Theorem: MvPowerSeries.topology_eq_ideals_basis_topology
Proof state before:
case a.intro.intro.intro.intro
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
use Finset.sup hD.toFinset id
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
D : Set (σ →₀ ℕ)
hD : D.Finite
t : (σ →₀ ℕ) → Set α
ht : ∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)
ht' : D.pi t ⊆ s
⊢ {b | b ∈ basis σ α (hD.toFinset.sup id)} ⊆ s