awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
a :
  (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)) =
    (Ideal.Quotient.mk
          (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
            (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
              (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
            ⊤) :
        (a : MvPolynomial σ R) →
          MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
      (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n))
⊢ Eq (α :=
    MvPolynomial σ R ⧸
      HSMul.hSMul (β := Ideal (MvPolynomial σ R))
        (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
          (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
        ⊤)
    ((Ideal.Quotient.mk
            (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
                (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
              ⊤) :
          (a : MvPolynomial σ R) →
            MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
        (Quotient.out
          ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))) :
      MvPolynomial σ R ⧸
        HSMul.hSMul (β := Ideal (MvPolynomial σ R))
          (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
          ⊤)
    ((Ideal.Quotient.mk
            (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
                (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
              ⊤) :
          (a : MvPolynomial σ R) →
            MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
        (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) :
      MvPolynomial σ R ⧸
        HSMul.hSMul (β := Ideal (MvPolynomial σ R))
          (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
            (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
          ⊤)

Tactic:
simp only [Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, Ideal.Quotient.mk_out]

Premises used: Submodule.factor_eq_factor, Submodule.mapQ_eq_factor, Ideal.Quotient.mk_out
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
a :
  (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) ⋯ :
        (a : MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) →
          MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
      ((Ideal.Quotient.mk
            (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
        (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n))) =
    (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))
⊢ (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)) =
    (Ideal.Quotient.mk
          (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
            (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R)
              (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)))
            ⊤) :
        (a : MvPolynomial σ R) →
          MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
      (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n))

Tactic:
rw [← AdicCompletion.transitionMap_ideal_mk _ (Nat.lt_iff_add_one_le.mp h), eq_comm]

Premises used: eq_comm, Nat.lt_iff_add_one_le, Iff.mp, AdicCompletion.transitionMap_ideal_mk
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) h :
        (a : MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) →
          MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x).succ • ⊤)
      ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n) =
    (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) (Nat.succ ((degree : (a : σ →₀ ℕ) → ℕ) x))

Tactic:
f.prop h

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
h₁ :
  (Ideal.Quotient.mk
          (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
            (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤) :
        (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) =
    (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n
⊢ (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) ⋯ :
        (a : MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) →
          MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ ((degree : (a : σ →₀ ℕ) → ℕ) x + 1) • ⊤)
      ((Ideal.Quotient.mk
            (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
              (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
        (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n))) =
    (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      (HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ))

Tactic:
convert! f.prop h

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ (Ideal.Quotient.mk
          (HSMul.hSMul (β := Ideal (MvPolynomial σ R))
            (HPow.hPow (α := Ideal (MvPolynomial σ R)) (MvPolynomial.idealOfVars σ R) n) ⊤) :
        (a : MvPolynomial σ R) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      (Quotient.out ((↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n * ⊤) n)) =
    (↑f : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
n : ℕ
f : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : (degree : (a : σ →₀ ℕ) → ℕ) x < n
⊢ (degree : (a : σ →₀ ℕ) → ℕ) x < HAdd.hAdd (α := ℕ) (β := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) x : ℕ) (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ_1 : Type u_1
R_1 : Type u_2
n : ℕ
inst : CommRing R_1
inst_1 : Finite σ_1
σ : Type u_3
R : Type u_4
inst_2 : Finite σ
inst_3 : CommRing R
x : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (toAdicCompletionInv σ R
            (OneHom.toFun
              (↑(↑(AlgHom.toRingHom (toAdicCompletion σ R)) :
                    MvPowerSeries σ R →* AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) :
                OneHom (MvPowerSeries σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
              x)) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R) x : R)
⊢ toAdicCompletionInv σ R
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (toAdicCompletion σ R)) :
              MvPowerSeries σ R →* AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) :
          OneHom (MvPowerSeries σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ_1 : Type u_1
R_1 : Type u_2
n : ℕ
inst : CommRing R_1
inst_1 : Finite σ_1
σ : Type u_3
R : Type u_4
inst_2 : Finite σ
inst_3 : CommRing R
x : MvPowerSeries σ R
n_1 : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R)
    ((coeff n_1 : (a : MvPowerSeries σ R) → R)
        (toAdicCompletionInv σ R
          (OneHom.toFun
            (↑(↑(AlgHom.toRingHom (toAdicCompletion σ R)) :
                  MvPowerSeries σ R →* AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) :
              OneHom (MvPowerSeries σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
            x)) :
      R)
    ((coeff n_1 : (a : MvPowerSeries σ R) → R) x : R)

Tactic:
simp [coeff_toAdicCompletionInv, coeff_toAdicCompletion_val_apply_out]

Premises used: MvPowerSeries.coeff_toAdicCompletionInv, MvPowerSeries.coeff_toAdicCompletion_val_apply_out
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ_1 : Type u_1
R_1 : Type u_2
n : ℕ
inst : CommRing R_1
inst_1 : Finite σ_1
σ : Type u_3
R : Type u_4
inst_2 : Finite σ
inst_3 : CommRing R
x : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
h :
  ∀ (n : ℕ),
    (↑(OneHom.toFun
              (↑(↑(AlgHom.toRingHom (toAdicCompletion σ R)) :
                    MvPowerSeries σ R →* AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) :
                OneHom (MvPowerSeries σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
              (toAdicCompletionInv σ R x)) :
          (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
        n =
      (↑x : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n
⊢ OneHom.toFun
      (↑(↑(AlgHom.toRingHom (toAdicCompletion σ R)) :
            MvPowerSeries σ R →* AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) :
        OneHom (MvPowerSeries σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (toAdicCompletionInv σ R x) =
    x

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ_1 : Type u_1
R_1 : Type u_2
n : ℕ
inst : CommRing R_1
inst_1 : Finite σ_1
σ : Type u_3
R : Type u_4
inst_2 : Finite σ
inst_3 : CommRing R
x : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
n_1 : ℕ
⊢ (↑(OneHom.toFun
            (↑(↑(AlgHom.toRingHom (toAdicCompletion σ R)) :
                  MvPowerSeries σ R →* AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) :
              OneHom (MvPowerSeries σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
            (toAdicCompletionInv σ R x)) :
        (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤)
      n_1 =
    (↑x : (n : ℕ) → MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n • ⊤) n_1

Tactic:
simpa using mk_truncTotal_toAdicCompletionInv

Premises used: MvPowerSeries.mk_truncTotal_toAdicCompletionInv
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
p : MvPowerSeries σ R
⊢ Eq (α := AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((toAdicCompletionAlgEquiv σ R :
          (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        p :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    ((toAdicCompletion σ R : (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        p :
      AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Equiv
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Finite σ
x : AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (AlgEquiv.symm (toAdicCompletionAlgEquiv σ R) :
        (a : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) → MvPowerSeries σ R)
      x =
    toAdicCompletionInv σ R x

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
S : Type u_4
inst : CommRing S
a : σ → S
t u : TopologicalSpace S
h : t ≤ u
ha : HasEval a
⊢ HasEval a

Tactic:
⟨fun s ↦ Filter.Tendsto.mono_right (@HasEval.hpow _ _ _ t a ha s) (nhds_mono h),
   Filter.Tendsto.mono_right (@HasEval.tendsto_zero σ _ _ t a ha) (nhds_mono h)⟩

Premises used: MvPowerSeries.HasEval.hpow, nhds_mono, Filter.Tendsto.mono_right, MvPowerSeries.HasEval.mk, MvPowerSeries.HasEval.tendsto_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
S : Type u_3
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : ContinuousAdd S
inst_3 : IsLinearTopology S S
a b : σ → S
ha : HasEval a
hb : HasEval b
rw : Tendsto (a + b) cofinite (𝓝 (HAdd.hAdd (α := S) 0 0))
⊢ Tendsto (a + b) cofinite (𝓝 0)

Tactic:
rw [← add_zero 0]

Premises used: add_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
S : Type u_3
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : ContinuousAdd S
inst_3 : IsLinearTopology S S
a b : σ → S
ha : HasEval a
hb : HasEval b
⊢ Tendsto (a + b) cofinite (𝓝 (HAdd.hAdd (α := S) 0 0))

Tactic:
ha.tendsto_zero.add hb.tendsto_zero

Premises used: Filter.Tendsto.add, MvPowerSeries.HasEval.tendsto_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
S : Type u_3
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : ContinuousAdd S
inst_3 : IsLinearTopology S S
a b : σ → S
ha : HasEval a
hb : HasEval b
⊢ Tendsto (a + b) cofinite (𝓝 (HAdd.hAdd (α := S) 0 0))

Tactic:
exact ha.tendsto_zero.add hb.tendsto_zero

Premises used: Filter.Tendsto.add, MvPowerSeries.HasEval.tendsto_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
S : Type u_3
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : σ → S
hx : HasEval x
⊢ HasEval (x * c)

Tactic:
mul_comm x c ▸ HasEval.mul_left c hx

Premises used: Eq.rec, MvPowerSeries.HasEval.mul_left, mul_comm, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
S : Type u_3
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsTopologicalRing S
inst_3 : IsLinearTopology S S
a : σ → S
⊢ Membership.mem (γ := Ideal (σ → S)) hasEvalIdeal a ↔ HasEval a

Tactic:
simp [hasEvalIdeal]

Premises used: MvPowerSeries.hasEvalIdeal
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
S : Type u_3
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsTopologicalRing S
inst_3 : IsLinearTopology S S
x : σ → S
ha : HasEval x
p : ℕ
hp : 0 < p
⊢ HasEval (x ^ p)

Tactic:
mem_hasEvalIdeal_iff.mp <| Ideal.pow_mem_of_mem hasEvalIdeal ha p hp

Premises used: MvPowerSeries.mem_hasEvalIdeal_iff, Ideal.pow_mem_of_mem, Iff.mp, MvPowerSeries.hasEvalIdeal
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
inst_4 : IsUniformAddGroup R
⊢ IsUniformAddGroup (MvPolynomial σ R)

Tactic:
IsUniformAddGroup.comap coeToMvPowerSeries.ringHom

Premises used: MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, IsUniformAddGroup.comap, MvPolynomial.coeToMvPowerSeries.ringHom
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
⊢ IsUniformInducing (α := MvPolynomial σ R) toMvPowerSeries

Tactic:
(isUniformInducing_iff toMvPowerSeries).mpr rfl

Premises used: Iff.mpr, MvPolynomial.toMvPowerSeries, isUniformInducing_iff, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
⊢ IsDenseInducing (α := MvPolynomial σ R) toMvPowerSeries

Tactic:
toMvPowerSeries_isUniformInducing.isDenseInducing denseRange_toMvPowerSeries

Premises used: MvPolynomial.toMvPowerSeries_isUniformInducing, IsUniformInducing.isDenseInducing, MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
hf : ContinuousAt (X := MvPolynomial σ R) (Y := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S) 0
⊢ UniformContinuous (α := MvPolynomial σ R) (β := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S)

Tactic:
apply uniformContinuous_of_continuousAt_zero

Premises used: uniformContinuous_of_continuousAt_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
hf :
  ∀ (i : Ideal S),
    Membership.mem (γ := Filter S) (𝓝 0) (↑i : Set S) →
      ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
        Membership.mem (α := S) (↑i : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
⊢ ContinuousAt (X := MvPolynomial σ R) (Y := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S) 0

Tactic:
rw [ContinuousAt, map_zero, IsLinearTopology.hasBasis_ideal.tendsto_right_iff]

Premises used: ContinuousAt, map_zero, Filter.HasBasis.tendsto_right_iff, IsLinearTopology.hasBasis_ideal
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
s : σ
rcases : ∀ (n : ℕ) (hn : ∀ b ≥ n, a s ^ b ∈ (↑I : Set S)), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
⊢ Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}

Tactic:
rcases ha.hpow s |>.eventually_mem hI |>.exists_forall_of_atTop with ⟨n, hn⟩

Premises used: Filter.Tendsto.eventually_mem, MvPowerSeries.HasEval.hpow, Filter.Eventually.exists_forall_of_atTop
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n_1 : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
s : σ
n : ℕ
hn : ∀ b ≥ n, a s ^ b ∈ (↑I : Set S)
h : Membership.mem (γ := Set ℕ) {n : ℕ | a s ^ n.succ ∈ I} n
⊢ Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}

Tactic:
use n
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n_1 : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
s : σ
n : ℕ
hn : ∀ b ≥ n, a s ^ b ∈ (↑I : Set S)
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | a s ^ n.succ ∈ I} n

Tactic:
simpa using hn n.succ n.le_succ

Premises used: Nat.le_succ, Nat.succ
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
⊢ ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}

Tactic:
have hn_ne : ∀ s, Set.Nonempty {n : ℕ | (a s) ^ n.succ ∈ I} := fun s ↦ by
    rcases ha.hpow s |>.eventually_mem hI |>.exists_forall_of_atTop with ⟨n, hn⟩
    use n
    simpa using hn n.succ n.le_succ
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
h : ∀ (s : σ) (has : a s ∈ (↑I : Set S)), n s = 0 s
⊢ n =ᶠ[cofinite] 0

Tactic:
filter_upwards [ha.tendsto_zero.eventually_mem hI] with s has

Premises used: Filter.Tendsto.eventually_mem, MvPowerSeries.HasEval.tendsto_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
s : σ
has : a s ∈ (↑I : Set S)
⊢ n s = 0 s

Tactic:
simpa [n, Pi.zero_apply, Nat.sInf_eq_zero, or_iff_left (hn_ne s).ne_empty] using has

Premises used: Nat.sInf_eq_zero, Set.Nonempty.ne_empty, Pi.zero_apply, or_iff_left