awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
d' : σ →₀ ℕ
hd'_le : d' ≤ d
rw : (if d' = e then x else 0) ∈ J
⊢ Membership.mem (α := R) J
    ((coeff d' : (a : MvPowerSeries σ R) → R) ((monomial e : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) : R)

Tactic:
rw [coeff_monomial]

Premises used: MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
d' : σ →₀ ℕ
hd'_le : d' ≤ d
pos : ∀ (hd' : d' = e), x ∈ J
neg : ∀ (hd' : ¬d' = e), 0 ∈ J
⊢ (if d' = e then x else 0) ∈ J

Tactic:
split_ifs with hd'
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
d' : σ →₀ ℕ
hd'_le : d' ≤ d
hd' : d' = e
⊢ x ∈ J

Tactic:
(h' (hd' ▸ hd'_le)).elim

Premises used: False.elim, Eq.rec
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
d' : σ →₀ ℕ
hd'_le : d' ≤ d
hd' : d' = e
⊢ x ∈ J

Tactic:
exact (h' (hd' ▸ hd'_le)).elim

Premises used: False.elim, Eq.rec
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
d' : σ →₀ ℕ
hd'_le : d' ≤ d
hd' : ¬d' = e
⊢ 0 ∈ J

Tactic:
J.zero_mem

Premises used: Set.Mem, setOf, TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
d' : σ →₀ ℕ
hd'_le : d' ≤ d
hd' : ¬d' = e
⊢ 0 ∈ J

Tactic:
exact J.zero_mem

Premises used: TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
d' : σ →₀ ℕ
hd'_le : d' ≤ d
pos : ∀ (hd' : d' = e), x ∈ J
neg : ∀ (hd' : ¬d' = e), 0 ∈ J
pos₁ : ∀ (hd' : d' = e), x ∈ J
neg₁ : ∀ (hd' : ¬d' = e), 0 ∈ J
⊢ (if d' = e then x else 0) ∈ J

Tactic:
split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]

Premises used: TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
⊢ ∀ (d' : σ →₀ ℕ) (hd'_le : d' ≤ d),
    Membership.mem (α := R) J
      ((coeff d' : (a : MvPowerSeries σ R) → R) ((monomial e : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) : R)

Tactic:
have (d') (hd'_le : d' ≤ d) : coeff d' (monomial e x) ∈ J := by
        rw [coeff_monomial]
        split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
this :
  ∀ (d' : σ →₀ ℕ) (hd'_le : d' ≤ d),
    Membership.mem (α := R) J
      ((coeff d' : (a : MvPowerSeries σ R) → R) ((monomial e : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) : R)
⊢ x ∈ K

Tactic:
simpa using h (monomial e x) this _ le_rfl

Premises used: le_rfl, MvPowerSeries.monomial, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
hJK : J ≤ K
hed : e ≤ d
⊢ basis σ R (J, d) ≤ basis σ R (K, e)

Tactic:
basis_le hJK hed

Premises used: MvPowerSeries.LinearTopology.basis_le
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
hJK : J ≤ K
hed : e ≤ d
⊢ basis σ R (J, d) ≤ basis σ R (K, e)

Tactic:
exact basis_le hJK hed

Premises used: MvPowerSeries.LinearTopology.basis_le
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
mp : basis σ R (J, d) ≤ basis σ R (K, e) → J ≤ K ∧ e ≤ d
mpr mpr₁ : J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d

Tactic:
classical
  constructor
  · simp only [basis, TwoSidedIdeal.le_iff, TwoSidedIdeal.coe_mk', setOf_subset_setOf]
    intro h
    constructor
    · intro x hx
      have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by
        rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]
      simpa using h (C x) (fun _ _ ↦ this _) _ zero_le
    · by_contra h'
      apply hK
      rw [eq_top_iff]
      intro x _
      have (d') (hd'_le : d' ≤ d) : coeff d' (monomial e x) ∈ J := by
        rw [coeff_monomial]
        split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
      simpa using h (monomial e x) this _ le_rfl
  · rintro ⟨hJK, hed⟩
    exact basis_le hJK hed

Premises used: eq_top_iff, TwoSidedIdeal.coe_mk', MvPowerSeries.LinearTopology.basis, TwoSidedIdeal.le_iff, Set.setOf_subset_setOf
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
rw :
  HasBasis (α := MvPowerSeries σ R) (Filter.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (i : σ →₀ ℕ) ↦ 𝓝 (0 i))
    (fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑Id.1 : Set R))
    fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ (↑(basis σ R Id) : Set (MvPowerSeries σ R))
⊢ HasBasis (α := MvPowerSeries σ R) (𝓝 0)
    (fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑Id.1 : Set R))
    fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ (↑(basis σ R Id) : Set (MvPowerSeries σ R))

Tactic:
rw [nhds_pi]

Premises used: nhds_pi
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
⊢ HasBasis (α := MvPowerSeries σ R) (Filter.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (i : σ →₀ ℕ) ↦ 𝓝 (0 i))
    (fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑Id.1 : Set R))
    fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ (↑(basis σ R Id) : Set (MvPowerSeries σ R))

Tactic:
IsLinearTopology.hasBasis_twoSidedIdeal.pi_self.to_hasBasis ?_ ?_

Premises used: Filter.HasBasis.pi_self, IsLinearTopology.hasBasis_twoSidedIdeal, MvPowerSeries, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
refine_1 :
  ∀ (i : Prod.{u_1, u_2} (Set (σ →₀ ℕ)) (TwoSidedIdeal R)),
    i.1.Finite ∧ Membership.mem (γ := Filter R) (𝓝 0) (↑i.2 : Set R) →
      ∃ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
        Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) ∧
          (↑(basis σ R i') : Set (MvPowerSeries σ R)) ⊆
            i.1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑i.2 : Set R)
refine_2 :
  ∀ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
    Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) →
      ∃ (i : Prod.{u_1, u_2} (Set (σ →₀ ℕ)) (TwoSidedIdeal R)),
        (i.1.Finite ∧ Membership.mem (γ := Filter R) (𝓝 0) (↑i.2 : Set R)) ∧
          (i.1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑i.2 : Set R)) ⊆
            (↑(basis σ R i') : Set (MvPowerSeries σ R))
⊢ HasBasis (α := MvPowerSeries σ R) (Filter.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (i : σ →₀ ℕ) ↦ 𝓝 (0 i))
    (fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑Id.1 : Set R))
    fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ (↑(basis σ R Id) : Set (MvPowerSeries σ R))

Tactic:
refine IsLinearTopology.hasBasis_twoSidedIdeal.pi_self.to_hasBasis ?_ ?_

Premises used: Filter.HasBasis.pi_self, IsLinearTopology.hasBasis_twoSidedIdeal, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
refine_1 :
  ∀ (hD : (D, I).1.Finite) (hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(D, I).2 : Set R)),
    ∃ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
      Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) ∧
        (↑(basis σ R i') : Set (MvPowerSeries σ R)) ⊆
          (D, I).1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)
⊢ (D, I).1.Finite ∧ Membership.mem (γ := Filter R) (𝓝 0) (↑(D, I).2 : Set R) →
    ∃ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
      Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) ∧
        (↑(basis σ R i') : Set (MvPowerSeries σ R)) ⊆
          (D, I).1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)

Tactic:
⟨hD, hI⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(D, I).2 : Set R)
⊢ ∃ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
    Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) ∧
      (↑(basis σ R i') : Set (MvPowerSeries σ R)) ⊆
        (D, I).1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)

Tactic:
⟨⟨I, Finset.sup hD.toFinset id⟩, hI, fun f hf d hd ↦ ?_⟩

Premises used: id, Prod.mk, Set.Finite.toFinset, And.intro, Exists.intro, Finset.sup
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(D, I).2 : Set R)
refine_1 :
  ∀ (f : (i : σ →₀ ℕ) → R) (hf : f ∈ (↑(basis σ R (I, hD.toFinset (s := (D, I).1).sup id)) : Set (MvPowerSeries σ R)))
    (d : σ →₀ ℕ) (hd : d ∈ (D, I).1),
    Membership.mem (γ := Set ((fun (i : σ →₀ ℕ) ↦ R) d)) ((fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)) d) (f d)
⊢ ∃ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
    Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) ∧
      (↑(basis σ R i') : Set (MvPowerSeries σ R)) ⊆
        (D, I).1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)

Tactic:
refine ⟨⟨I, Finset.sup hD.toFinset id⟩, hI, fun f hf d hd ↦ ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(D, I).2 : Set R)
f : (i : σ →₀ ℕ) → R
hf : f ∈ (↑(basis σ R (I, hD.toFinset (s := (D, I).1).sup id)) : Set (MvPowerSeries σ R))
d : σ →₀ ℕ
hd : d ∈ (D, I).1
refine_1 :
  ∀
    (hf :
      ∀ e ≤ (I, hD.toFinset (s := (D, I).1).sup id).2,
        Membership.mem (α := R) (I, hD.toFinset (s := (D, I).1).sup id).1
          ((coeff e : (a : MvPowerSeries σ R) → R) f : R))
    (d : σ →₀ ℕ) (hd : d ∈ (D, I).1),
    Membership.mem (γ := Set ((fun (i : σ →₀ ℕ) ↦ R) d)) ((fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)) d) (f d)
⊢ Membership.mem (γ := Set ((fun (i : σ →₀ ℕ) ↦ R) d)) ((fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)) d) (f d)

Tactic:
rw [SetLike.mem_coe, mem_basis_iff] at hf

Premises used: MvPowerSeries.LinearTopology.mem_basis_iff, SetLike.mem_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(D, I).2 : Set R)
f : (i : σ →₀ ℕ) → R
hf :
  ∀ e ≤ (I, hD.toFinset (s := (D, I).1).sup id).2,
    Membership.mem (α := R) (I, hD.toFinset (s := (D, I).1).sup id).1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : d ∈ (D, I).1
⊢ Membership.mem (α := R) (I, hD.toFinset (s := (D, I).1).sup id).1 ((coeff (id d) : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
hf _ <| Finset.le_sup (hD.mem_toFinset.mpr hd)

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Finset.le_sup
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
D : Set (σ →₀ ℕ)
I : TwoSidedIdeal R
hD : (D, I).1.Finite
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(D, I).2 : Set R)
f : (i : σ →₀ ℕ) → R
hf :
  ∀ e ≤ (I, hD.toFinset (s := (D, I).1).sup id).2,
    Membership.mem (α := R) (I, hD.toFinset (s := (D, I).1).sup id).1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : d ∈ (D, I).1
⊢ Membership.mem (γ := Set ((fun (i : σ →₀ ℕ) ↦ R) d)) ((fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)) d) (f d)

Tactic:
convert! hf _ <| Finset.le_sup (hD.mem_toFinset.mpr hd)

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Finset.le_sup
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(I, d).1 : Set R)
⊢ ∃ (i : Prod.{u_1, u_2} (Set (σ →₀ ℕ)) (TwoSidedIdeal R)),
    (i.1.Finite ∧ Membership.mem (γ := Filter R) (𝓝 0) (↑i.2 : Set R)) ∧
      (i.1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑i.2 : Set R)) ⊆
        (↑(basis σ R (I, d)) : Set (MvPowerSeries σ R))

Tactic:
⟨⟨Iic d, I⟩, ⟨finite_Iic d, hI⟩, ?_⟩

Premises used: Set.finite_Iic, Prod.mk, And.intro, Exists.intro, Set.Iic
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(I, d).1 : Set R)
refine_2 :
  ((Iic d, I).1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑(Iic d, I).2 : Set R)) ⊆
    (↑(basis σ R (I, d)) : Set (MvPowerSeries σ R))
⊢ ∃ (i : Prod.{u_1, u_2} (Set (σ →₀ ℕ)) (TwoSidedIdeal R)),
    (i.1.Finite ∧ Membership.mem (γ := Filter R) (𝓝 0) (↑i.2 : Set R)) ∧
      (i.1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑i.2 : Set R)) ⊆
        (↑(basis σ R (I, d)) : Set (MvPowerSeries σ R))

Tactic:
refine ⟨⟨Iic d, I⟩, ⟨finite_Iic d, hI⟩, ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑(I, d).1 : Set R)
⊢ ((Iic d, I).1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑(Iic d, I).2 : Set R)) ⊆
    (↑(basis σ R (I, d)) : Set (MvPowerSeries σ R))

Tactic:
simpa [basis, coeff_apply, Iic, Set.pi] using subset_rfl

Premises used: MvPowerSeries.LinearTopology.basis, MvPowerSeries.coeff_apply, Set.Iic, Set.pi, subset_rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
rw rw₁ rw₂ :
  HasBasis (α := MvPowerSeries σ R) (Filter.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (i : σ →₀ ℕ) ↦ 𝓝 (0 i))
    (fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑Id.1 : Set R))
    fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ (↑(basis σ R Id) : Set (MvPowerSeries σ R))
refine_1 :
  ∀ (i : Prod.{u_1, u_2} (Set (σ →₀ ℕ)) (TwoSidedIdeal R)),
    i.1.Finite ∧ Membership.mem (γ := Filter R) (𝓝 0) (↑i.2 : Set R) →
      ∃ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
        Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) ∧
          (↑(basis σ R i') : Set (MvPowerSeries σ R)) ⊆
            i.1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑i.2 : Set R)
refine_2 refine_2₁ :
  ∀ (i' : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)),
    Membership.mem (γ := Filter R) (𝓝 0) (↑i'.1 : Set R) →
      ∃ (i : Prod.{u_1, u_2} (Set (σ →₀ ℕ)) (TwoSidedIdeal R)),
        (i.1.Finite ∧ Membership.mem (γ := Filter R) (𝓝 0) (↑i.2 : Set R)) ∧
          (i.1.pi (α := fun (i : σ →₀ ℕ) ↦ R) fun (x : σ →₀ ℕ) ↦ (↑i.2 : Set R)) ⊆
            (↑(basis σ R i') : Set (MvPowerSeries σ R))
⊢ HasBasis (α := MvPowerSeries σ R) (𝓝 0)
    (fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ Membership.mem (γ := Filter R) (𝓝 0) (↑Id.1 : Set R))
    fun (Id : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)) ↦ (↑(basis σ R Id) : Set (MvPowerSeries σ R))

Tactic:
classical
  rw [nhds_pi]
  refine IsLinearTopology.hasBasis_twoSidedIdeal.pi_self.to_hasBasis ?_ ?_
  · intro ⟨D, I⟩ ⟨hD, hI⟩
    refine ⟨⟨I, Finset.sup hD.toFinset id⟩, hI, fun f hf d hd ↦ ?_⟩
    rw [SetLike.mem_coe, mem_basis_iff] at hf
    convert! hf _ <| Finset.le_sup (hD.mem_toFinset.mpr hd)
  · intro ⟨I, d⟩ hI
    refine ⟨⟨Iic d, I⟩, ⟨finite_Iic d, hI⟩, ?_⟩
    simpa [basis, coeff_apply, Iic, Set.pi] using subset_rfl

Premises used: Filter.HasBasis.pi_self, MvPowerSeries.LinearTopology.mem_basis_iff, IsLinearTopology.hasBasis_twoSidedIdeal, nhds_pi, MvPowerSeries.LinearTopology.basis, MvPowerSeries.coeff_apply, SetLike.mem_coe, Set.Iic, Set.pi, Filter.HasBasis.to_hasBasis, subset_rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
⊢ IsLinearTopology (MvPowerSeries σ R) (MvPowerSeries σ R)

Tactic:
IsLinearTopology.mk_of_hasBasis' _ hasBasis_nhds_zero TwoSidedIdeal.mul_mem_left

Premises used: TwoSidedIdeal.mul_mem_left, IsLinearTopology.mk_of_hasBasis', MvPowerSeries.LinearTopology.hasBasis_nhds_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
inst_3 : IsLinearTopology Rᵐᵒᵖ R
⊢ IsLinearTopology (MvPowerSeries σ R)ᵐᵒᵖ (MvPowerSeries σ R)

Tactic:
IsLinearTopology.mk_of_hasBasis' _ hasBasis_nhds_zero (fun J _ _ hg ↦ J.mul_mem_right _ _ hg)

Premises used: TwoSidedIdeal.mul_mem_right, IsLinearTopology.mk_of_hasBasis', MulOpposite.unop, MvPowerSeries.LinearTopology.hasBasis_nhds_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
simp_rw :
  ∀ (d : σ →₀ ℕ) (i : Ideal R),
    Membership.mem (γ := Filter R) (𝓝 0) (↑i : Set R) →
      ∀ᶠ (x : ℕ) in atTop, Membership.mem (α := R) (↑i : Set R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ x) : R)
⊢ IsTopologicallyNilpotent f

Tactic:
simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero,
    IsLinearTopology.hasBasis_ideal.tendsto_right_iff]

Premises used: MvPowerSeries.coeff_zero, IsTopologicallyNilpotent, Filter.HasBasis.tendsto_right_iff, IsLinearTopology.hasBasis_ideal, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
I : Ideal R
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
⊢ ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) x ∈ (↑I : Set R)

Tactic:
replace hf := hf.eventually_mem hI
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
hf : ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) x ∈ (↑I : Set R)
simp_rw :
  ∀
    (hf :
      ∃ (a : ℕ),
        ∀ b ≥ a,
          HPow.hPow (α := R ⧸ I)
              ((constantCoeff : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
                  ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) f) :
                R ⧸ I)
              b =
            0),
    ∃ (a : ℕ),
      ∀ b ≥ a,
        Eq.{u_3 + 1} (α := R ⧸ I)
          ((coeff d : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
              ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) (f ^ b)) :
            R ⧸ I)
          (0 : R ⧸ I)
⊢ ∀ᶠ (x : ℕ) in atTop, Membership.mem (α := R) (↑I : Set R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ x) : R)

Tactic:
simp_rw [eventually_atTop, SetLike.mem_coe, ← Ideal.Quotient.eq_zero_iff_mem,
    map_pow, ← coeff_map, ← constantCoeff_map] at hf ⊢

Premises used: map_pow, Ideal.Quotient.eq_zero_iff_mem, SetLike.mem_coe, MvPowerSeries.constantCoeff_map, MvPowerSeries.coeff_map, Filter.eventually_atTop