awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (hypothesis)
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)
x : R
hx : x ∈ (↑J : Set R)
⊢ x ∈ (↑K : Set R)
have this : ∀ (d' : σ →₀ ℕ),
  Membership.mem (α := R) J
    ((coeff d' : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) : R)
Tactic: have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by
        rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
⊢ e ≤ d
have mp : ∀ (h' : ¬e ≤ d), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ False
have mp : K = ⊤
Tactic: apply hK
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ K = ⊤
have mp : ⊤ ≤ K
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
have rw : (if d' = e then x else 0) ∈ J
Tactic: rw [coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ (if d' = e then x else 0) ∈ J
have pos : ∀ (hd' : d' = e), x ∈ J
Tactic: split_ifs with hd'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ (if d' = e then x else 0) ∈ J
have neg : ∀ (hd' : ¬d' = e), 0 ∈ J
Tactic: split_ifs with hd'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ (if d' = e then x else 0) ∈ J
have pos : ∀ (hd' : d' = e), x ∈ J
Tactic: split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ (if d' = e then x else 0) ∈ J
have neg : ∀ (hd' : ¬d' = e), 0 ∈ J
Tactic: split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (hypothesis)
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
⊢ x ∈ K
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d
have mp : 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d
have mpr : J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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) (𝓝 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))
have 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))
Tactic: rw [nhds_pi]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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))
have 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)
Tactic: refine IsLinearTopology.hasBasis_twoSidedIdeal.pi_self.to_hasBasis ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
⊢ 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))
have 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))
Tactic: refine IsLinearTopology.hasBasis_twoSidedIdeal.pi_self.to_hasBasis ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ (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)
have 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)
Tactic: ⟨hD, hI⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
have 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)
Tactic: refine ⟨⟨I, Finset.sup hD.toFinset id⟩, hI, fun f hf d hd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (γ := Set ((fun (i : σ →₀ ℕ) ↦ R) d)) ((fun (x : σ →₀ ℕ) ↦ (↑(D, I).2 : Set R)) d) (f d)
have 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)
Tactic: rw [SetLike.mem_coe, mem_basis_iff] at hf
Cleared hypotheses: hf, d, hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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))
have 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))
Tactic: refine ⟨⟨Iic d, I⟩, ⟨finite_Iic d, hI⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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) (𝓝 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))
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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))
⊢ 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))
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
⊢ 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))
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
⊢ IsTopologicallyNilpotent f
have 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)
Tactic: simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero,
    IsLinearTopology.hasBasis_ideal.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (hypothesis)
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, Membership.mem (α := R) (↑I : Set R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ x) : R)
have hf₁ : ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) x ∈ (↑I : Set R)
Tactic: replace hf := hf.eventually_mem hI
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
⊢ ∀ᶠ (x : ℕ) in atTop, Membership.mem (α := R) (↑I : Set R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ x) : R)
have 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)
Tactic: simp_rw [eventually_atTop, SetLike.mem_coe, ← Ideal.Quotient.eq_zero_iff_mem,
    map_pow, ← coeff_map, ← constantCoeff_map] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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 :
  ∃ (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)
have obtain : ∀ (N : ℕ)
  (hN :
    ∀ b ≥ N,
      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)
Tactic: obtain ⟨N, hN⟩ := hf
Cleared hypotheses: hf