awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (1 + HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₁ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) 1 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (if n + 1 = 0 then 1 else 0 : ℕ)
      ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (0 : ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ) =
    (coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries
h₄ :
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₅ :
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₆ :
  Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (catalanSeries * catalanSeries) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
h₇ :
  Eq (α := ℕ)
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := ℕ) (β := ℕ) ((coeff p.1 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
          ((coeff p.2 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ) :
      ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
⊢ Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₈ : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan x.1 * catalan x.2 = catalan (n + 1)
Tactic: simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h : Eq (α := ℕ) ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
  ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: cases n with
  | zero => simp
  | succ n =>
    simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Catalan (goal)
Goal:
n : ℕ
h :
  Eq (α := ℕ) ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff 0 : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
⊢ Eq (α := ℕ) ((coeff n : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff n : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
have h₁ : ∀ (n : ℕ),
  Eq (α := ℕ) ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) (HPow.hPow (β := ℕ) catalanSeries 2 * X + 1) : ℕ)
    ((coeff (n + 1) : (a : ℕ⟦X⟧) → ℕ) catalanSeries : ℕ)
Tactic: cases n with
  | zero => simp
  | succ n =>
    simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.CoeffMulMem (goal)
Goal:
A : Type u_1
inst : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
hg : ∀ i ≤ n, Membership.mem (α := A) J ((coeff i : (a : A⟦X⟧) → A) g : A)
i : ℕ
hi : i ≤ n
⊢ Membership.mem (α := A) (I * J) ((coeff i : (a : A⟦X⟧) → A) (f * g) : A)
have rw : ∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i,
    HMul.hMul (α := A) (β := A) ((coeff p.1 : (a : A⟦X⟧) → A) f : A) ((coeff p.2 : (a : A⟦X⟧) → A) g : A) ∈
  I * J
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
S : Type u_3
inst : CommRing S
a : S
t u : TopologicalSpace S
h : t ≤ u
ha : HasEval a
⊢ HasEval a
have simp : ∀ (ha : MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a),
  MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a
Tactic: simp only [hasEval_iff] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
⊢ HasEval.{u_2} (S := S) 0
have rw : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ 0
Tactic: rw [hasEval_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
S : Type u_2
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
⊢ HasEval (a + b)
have simp : ∀ (ha : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a)
  (hb : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ b),
  MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a + b
Tactic: simp only [hasEval_iff] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : HasEval x
⊢ HasEval (c * x)
have simp : ∀ (hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x),
  MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ c * x
Tactic: simp only [hasEval_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : HasEval x
⊢ HasEval (x * c)
have simp : ∀ (hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x),
  MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x * c
Tactic: simp only [hasEval_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
a : R
ha : HasEval a
⊢ HasEval.{u_2} (S := S) ((φ : (a : R) → S) a : S)
have simp : ∀ (ha : MvPowerSeries.HasEval.{0, u_1} (S := R) fun (x : Unit) ↦ a),
  MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ (φ : (a : R) → S) a
Tactic: simp only [hasEval_iff] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
⊢ HasEval.{u_1} (S := R⟦X⟧) X
have rw : MvPowerSeries.HasEval.{0, u_1} (S := R⟦X⟧) fun (x : Unit) ↦ X
Tactic: rw [hasEval_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
f : Polynomial R
⊢ eval₂ φ a (↑f : R⟦X⟧) = Polynomial.eval₂ φ a f
have rw : eval₂ φ a
    (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
          ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
      R⟦X⟧) =
  Polynomial.eval₂ φ a
    ((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f))
Tactic: rw [← (MvPolynomial.uniqueAlgEquiv R Unit).apply_symm_apply f]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
f : Polynomial R
⊢ eval₂ φ a
      (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
            ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
        R⟦X⟧) =
    Polynomial.eval₂ φ a
      ((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
        ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f))
have simp : MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
    (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
          ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
      R⟦X⟧) =
  MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
    ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
Tactic: simp only [PowerSeries.eval₂, MvPolynomial.eval₂_const_uniqueAlgEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
f : Polynomial R
⊢ MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
      (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
            ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
        R⟦X⟧) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
have rw : MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
    (↑((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f) :
      MvPowerSeries PUnit.{1} R) =
  MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
    ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
Tactic: rw [← MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPowerSeries.eval₂_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
f : Polynomial R
rw :
  MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
      (↑((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f) :
        MvPowerSeries PUnit.{1} R) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
⊢ MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
      (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
            ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
        R⟦X⟧) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
have rw₁ : MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
    ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f) =
  MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
    ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
Tactic: rw [← MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPowerSeries.eval₂_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
r : R
⊢ eval₂ φ a ((C : (a : R) → R⟦X⟧) r) = (φ : (a : R) → S) r
have rw : eval₂ φ a (↑((Polynomial.C : (a : R) → Polynomial R) r) : R⟦X⟧) = (φ : (a : R) → S) r
Tactic: rw [← Polynomial.coe_C, eval₂_coe, Polynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
r : R
rw : eval₂ φ a (↑((Polynomial.C : (a : R) → Polynomial R) r) : R⟦X⟧) = (φ : (a : R) → S) r
⊢ eval₂ φ a ((C : (a : R) → R⟦X⟧) r) = (φ : (a : R) → S) r
have rw₁ : Polynomial.eval₂ φ a ((Polynomial.C : (a : R) → Polynomial R) r) = (φ : (a : R) → S) r
Tactic: rw [← Polynomial.coe_C, eval₂_coe, Polynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
r : R
rw : eval₂ φ a (↑((Polynomial.C : (a : R) → Polynomial R) r) : R⟦X⟧) = (φ : (a : R) → S) r
rw₁ : Polynomial.eval₂ φ a ((Polynomial.C : (a : R) → Polynomial R) r) = (φ : (a : R) → S) r
⊢ eval₂ φ a ((C : (a : R) → R⟦X⟧) r) = (φ : (a : R) → S) r
have rw₂ : Eq.{u_2 + 1} (α := S) ((φ : (a : R) → S) r : S) ((φ : (a : R) → S) r : S)
Tactic: rw [← Polynomial.coe_C, eval₂_coe, Polynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
⊢ eval₂ φ a X = a
have rw : eval₂ φ a (↑Polynomial.X : R⟦X⟧) = a
Tactic: rw [← Polynomial.coe_X, eval₂_coe, Polynomial.eval₂_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
rw : eval₂ φ a (↑Polynomial.X : R⟦X⟧) = a
⊢ eval₂ φ a X = a
have rw₁ : Polynomial.eval₂ φ a Polynomial.X = a
Tactic: rw [← Polynomial.coe_X, eval₂_coe, Polynomial.eval₂_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
rw : eval₂ φ a (↑Polynomial.X : R⟦X⟧) = a
rw₁ : Polynomial.eval₂ φ a Polynomial.X = a
⊢ eval₂ φ a X = a
have rw₂ : a = a
Tactic: rw [← Polynomial.coe_X, eval₂_coe, Polynomial.eval₂_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
⊢ HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (eval₂ φ a f)
have this : HasSum
  (fun (d : Unit →₀ ℕ) ↦
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
      (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
  (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
Tactic: have := MvPowerSeries.hasSum_eval₂ hφ (hasEval ha) f
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
⊢ HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
have rw : ∀
  (this :
    HasSum
      ((fun (d : Unit →₀ ℕ) ↦
          HMul.hMul (α := S) (β := S)
            ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
            (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
        Finsupp.single ())
      (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)),
  HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
Tactic: rw [← (Finsupp.single_injective ()).hasSum_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
rw :
  ∀
    (this :
      HasSum
        ((fun (d : Unit →₀ ℕ) ↦
            HMul.hMul (α := S) (β := S)
              ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
              (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
          Finsupp.single ())
        (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)),
    HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
      (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
⊢ HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
have rw₁ : ∀ x ∉ Set.range (Finsupp.single ()),
  HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R) : S)
      (x.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S) =
    0
Tactic: rw [← (Finsupp.single_injective ()).hasSum_iff] at this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    ((fun (d : Unit →₀ ℕ) ↦
        HMul.hMul (α := S) (β := S)
          ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
          (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
      Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
⊢ HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
have h : ∀ (x : ℕ),
  HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (a ^ x) =
    ((fun (d : Unit →₀ ℕ) ↦
          HMul.hMul (α := S) (β := S)
            ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
            (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
        Finsupp.single ())
      x
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    ((fun (d : Unit →₀ ℕ) ↦
        HMul.hMul (α := S) (β := S)
          ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
          (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
      Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
x : ℕ
⊢ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (a ^ x) =
    ((fun (d : Unit →₀ ℕ) ↦
          HMul.hMul (α := S) (β := S)
            ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
            (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
        Finsupp.single ())
      x
have h : HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (a ^ x) =
  HMul.hMul (α := S)
    ((φ : (a : R) → S) ((MvPowerSeries.coeff (Finsupp.single () x) : (a : MvPowerSeries Unit R) → R) f : R) : S) (a ^ x)
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ Finsupp.single () ((d : (a : Unit) → ℕ) ()) = d
have h : Eq (α := ℕ) (((Finsupp.single () ((d : (a : Unit) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
  ((d : (a : Unit) → ℕ) default : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε (↑p : R⟦X⟧) = Polynomial.eval₂ φ a p
⊢ ε = eval₂ φ a
have refine : ∀ (p : MvPolynomial Unit R), ε (↑p : MvPowerSeries Unit R) = MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
Tactic: refine MvPowerSeries.eval₂_unique hφ (hasEval ha) hε (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Evaluation (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε (↑p : R⟦X⟧) = Polynomial.eval₂ φ a p
p : MvPolynomial Unit R
⊢ ε (↑p : MvPowerSeries Unit R) = MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
have rw : ε (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → Polynomial R) p) : R⟦X⟧) =
  MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a) p
Tactic: rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_uniqueAlgEquiv]