awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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 : ℕ)))
          ⊤)
have 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))
Tactic: simp only [Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, Ideal.Quotient.mk_out]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ (↑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))
have a : (AdicCompletion.transitionMap (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R) sorry :
      (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: rw [← AdicCompletion.transitionMap_ideal_mk _ (Nat.lt_iff_add_one_le.mp h), eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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) ⋯ :
        (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 : ℕ))
have 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
Tactic: convert! f.prop h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Equiv (goal)
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)
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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 (𝓝 0)
have rw : Tendsto (a + b) cofinite (𝓝 (HAdd.hAdd (α := S) 0 0))
Tactic: rw [← add_zero 0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
⊢ UniformContinuous (α := MvPolynomial σ R) (β := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S)
have hf : ContinuousAt (X := MvPolynomial σ R) (Y := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S) 0
Tactic: apply uniformContinuous_of_continuousAt_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
⊢ ContinuousAt (X := MvPolynomial σ R) (Y := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S) 0
have 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)
Tactic: rw [ContinuousAt, map_zero, IsLinearTopology.hasBasis_ideal.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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}
have rcases : ∀ (n : ℕ) (hn : ∀ b ≥ n, a s ^ b ∈ (↑I : Set S)), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
Tactic: rcases ha.hpow s |>.eventually_mem hI |>.exists_forall_of_atTop with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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)
⊢ Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
have h : Membership.mem (γ := Set ℕ) {n : ℕ | a s ^ n.succ ∈ I} n
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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}
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
have hn_ne : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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}
⊢ n =ᶠ[cofinite] 0
have h : ∀ (s : σ) (has : a s ∈ (↑I : Set S)), n s = 0 s
Tactic: filter_upwards [ha.tendsto_zero.eventually_mem hI] with s has
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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}
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
have hn : (Function.support n).Finite
Tactic: have hn : Set.Finite (n.support) := by
    change n =ᶠ[cofinite] 0
    filter_upwards [ha.tendsto_zero.eventually_mem hI] with s has
    simpa [n, Pi.zero_apply, Nat.sInf_eq_zero, or_iff_left (hn_ne s).ne_empty] using has
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
have hD : D.Finite
Tactic: have hD : Set.Finite D := finite_Iic _
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
have this : Tendsto (α := MvPolynomial σ R) (β := S)
  (Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries)) (𝓝 0) (𝓝 0)
Tactic: have : Tendsto (φ ∘ coeff d ∘ toMvPowerSeries) (𝓝 0) (𝓝 0) :=
      hφ.comp (continuous_coeff R d) |>.comp continuous_induced_dom |>.tendsto' 0 0 (map_zero _)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
this :
  Tendsto (α := MvPolynomial σ R) (β := S)
    (Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries)) (𝓝 0)
    (𝓝 0)
⊢ ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
have h : ∀ (f : MvPolynomial σ R)
  (hf :
    Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries) f ∈
      (↑I : Set S)),
  Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d f) : S)
Tactic: filter_upwards [this.eventually_mem hI] with f hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
have this : ∀ d ∈ D, ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
Tactic: have : ∀ d ∈ D, ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, φ (p.coeff d) ∈ I := fun d hd ↦ by
    have : Tendsto (φ ∘ coeff d ∘ toMvPowerSeries) (𝓝 0) (𝓝 0) :=
      hφ.comp (continuous_coeff R d) |>.comp continuous_induced_dom |>.tendsto' 0 0 (map_zero _)
    filter_upwards [this.eventually_mem hI] with f hf
    simpa using hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ d ∈ D, ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
have this₁ : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
Tactic: rw [← hD.eventually_all] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
have h : ∀ (p : MvPolynomial σ R) (hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)),
  Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S)
Tactic: filter_upwards [this] with p hp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
⊢ Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S)
have h : ∑ d ∈ p.support,
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
  I
Tactic: rw [coe_eval₂Hom, SetLike.mem_coe, eval₂_eq]