awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
r : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((eval₂Hom (φ := algebraMap R S) ⋯ ha : (a : MvPowerSeries σ R) → S)
        ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
      S)
    ((algebraMap R S : (a : R) → S) r : S)
⊢ Eq.{u_3 + 1} (α := S)
    ((eval₂Hom (φ := algebraMap R S) ⋯ ha : (a : MvPowerSeries σ R) → S)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
      S)
    ((algebraMap R S : (a : R) → S) r : S)
have rw₁ : eval₂ (algebraMap R S) a ((C : (a : R) → MvPowerSeries σ R) r) = (algebraMap R S : (a : R) → S) r
Tactic: rw [← c_eq_algebraMap, coe_eval₂Hom, eval₂_C]
-- 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 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
r : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((eval₂Hom (φ := algebraMap R S) ⋯ ha : (a : MvPowerSeries σ R) → S)
        ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
      S)
    ((algebraMap R S : (a : R) → S) r : S)
rw₁ : eval₂ (algebraMap R S) a ((C : (a : R) → MvPowerSeries σ R) r) = (algebraMap R S : (a : R) → S) r
⊢ Eq.{u_3 + 1} (α := S)
    ((eval₂Hom (φ := algebraMap R S) ⋯ ha : (a : MvPowerSeries σ R) → S)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
      S)
    ((algebraMap R S : (a : R) → S) r : S)
have rw₂ : Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [← c_eq_algebraMap, coe_eval₂Hom, eval₂_C]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑(aeval ha) : (a : MvPowerSeries σ R) → S)
have rw : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ (algebraMap R S) a)
Tactic: rw [coe_aeval]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
p : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := S) ((aeval ha : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
    ((MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p : S)
have rw : eval₂ (algebraMap R S) a (↑p : MvPowerSeries σ R) = (MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p
Tactic: rw [coe_aeval, aeval_def, eval₂_coe]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
p : MvPolynomial σ R
rw : eval₂ (algebraMap R S) a (↑p : MvPowerSeries σ R) = (MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p
⊢ Eq.{u_3 + 1} (α := S) ((aeval ha : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
    ((MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p : S)
have rw₁ : eval₂ (algebraMap R S) a (↑p : MvPowerSeries σ R) = MvPolynomial.eval₂ (algebraMap R S) a p
Tactic: rw [coe_aeval, aeval_def, eval₂_coe]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
p : MvPolynomial σ R
rw : eval₂ (algebraMap R S) a (↑p : MvPowerSeries σ R) = (MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p
rw₁ : eval₂ (algebraMap R S) a (↑p : MvPowerSeries σ R) = MvPolynomial.eval₂ (algebraMap R S) a p
⊢ Eq.{u_3 + 1} (α := S) ((aeval ha : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
    ((MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p : S)
have rw₂ : MvPolynomial.eval₂ (algebraMap R S) a p = MvPolynomial.eval₂ (algebraMap R S) a p
Tactic: rw [coe_aeval, aeval_def, eval₂_coe]
-- 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
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
⊢ aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) ⋯ = ε
have h : Eq (α := (a : MvPowerSeries σ R) → S)
  (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) sorry) : (a : MvPowerSeries σ R) → S)
  (⇑ε : (a : MvPowerSeries σ R) → S)
Tactic: apply DFunLike.ext'
-- 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
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
⊢ Eq (α := (a : MvPowerSeries σ R) → S)
    (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) ⋯) : (a : MvPowerSeries σ R) → S)
    (⇑ε : (a : MvPowerSeries σ R) → S)
have h : Eq (α := (a : MvPowerSeries σ R) → S)
  (eval₂ (algebraMap R S) fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s))
  (⇑ε : (a : MvPowerSeries σ R) → S)
Tactic: rw [coe_aeval]
-- 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
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
⊢ Eq (α := (a : MvPowerSeries σ R) → S)
    (eval₂ (algebraMap R S) fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s))
    (⇑ε : (a : MvPowerSeries σ R) → S)
have h : ∀ (p : MvPolynomial σ R),
  (ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
Tactic: refine (eval₂_unique (continuous_algebraMap R S) (HasEval.X.map hε) hε ?_).symm
-- 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
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
⊢ (ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
have trans : Eq.{u_3 + 1} (α := S) ((ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
  ((ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p : S)
Tactic: trans ε.comp (coeToMvPowerSeries.algHom R) p
-- 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
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
trans :
  Eq.{u_3 + 1} (α := S) ((ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
    ((ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p : S)
⊢ (ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
have trans₁ : (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p =
  MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
Tactic: trans ε.comp (coeToMvPowerSeries.algHom R) p
-- 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
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
| (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p
have rw : MvPolynomial.eval₂ (algebraMap R S)
  (fun (i : σ) ↦ (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) (MvPolynomial.X i)) p
Tactic: rw [← p.aeval_X_left_apply, MvPolynomial.comp_aeval_apply, MvPolynomial.aeval_def]
-- 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
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
⊢ (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
have conv_lhs : MvPolynomial.eval₂ (algebraMap R S)
    (fun (i : σ) ↦ (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) (MvPolynomial.X i)) p =
  MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
Tactic: conv_lhs => rw [← p.aeval_X_left_apply, MvPolynomial.comp_aeval_apply, MvPolynomial.aeval_def]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum.{u_3, u_1} (α := S)
    (fun (d : σ →₀ ℕ) ↦
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e))
    ((aeval ha : (a : MvPowerSeries σ R) → S) f : S)
have simp_rw : HasSum
  (fun (d : σ →₀ ℕ) ↦
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
      (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
  (eval₂ (algebraMap R S) a f)
Tactic: simp_rw [coe_aeval, ← algebraMap_smul (R := R) S, smul_eq_mul]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ ε.comp (aeval ha) = aeval ⋯
have h : Eq (α := (a : MvPowerSeries σ R) → T) (⇑(ε.comp (aeval ha)) : (a : MvPowerSeries σ R) → T)
  (⇑(aeval sorry) : (a : MvPowerSeries σ R) → T)
Tactic: apply DFunLike.ext'
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ Eq (α := (a : MvPowerSeries σ R) → T) (⇑(ε.comp (aeval ha)) : (a : MvPowerSeries σ R) → T)
    (⇑(aeval ⋯) : (a : MvPowerSeries σ R) → T)
have h : Eq (α := (a : MvPowerSeries σ R) → T) ((⇑ε : (a : S) → T) ∘ eval₂ (algebraMap R S) a)
  (⇑(aeval sorry) : (a : MvPowerSeries σ R) → T)
Tactic: simp only [AlgHom.coe_comp, coe_aeval ha]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ Eq (α := (a : MvPowerSeries σ R) → T) ((⇑ε : (a : S) → T) ∘ eval₂ (algebraMap R S) a)
    (⇑(aeval ⋯) : (a : MvPowerSeries σ R) → T)
have h : eval₂ (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑ε : S →+* T) (algebraMap R S))
    ((⇑(↑ε : S →+* T) : (a : S) → T) ∘ a) =
  eval₂ (algebraMap R T) fun (s : σ) ↦ (ε.toRingHom : (a : S) → T) (a s)
Tactic: rw [← RingHom.coe_coe,
    comp_eval₂ (continuous_algebraMap R S) ha (show Continuous (ε : S →+* T) from hε), coe_aeval]
-- 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
a : σ → S
inst_4 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
T : Type u_4
inst_13 : CommRing T
inst_14 : UniformSpace T
inst_15 : IsUniformAddGroup T
inst_16 : IsTopologicalRing T
inst_17 : IsLinearTopology T T
inst_18 : T2Space T
inst_19 : Algebra R T
inst_20 : ContinuousSMul R T
inst_21 : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst_3.toTopologicalSpace, inst_14.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ eval₂ (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑ε : S →+* T) (algebraMap R S))
      ((⇑(↑ε : S →+* T) : (a : S) → T) ∘ a) =
    eval₂ (algebraMap R T) fun (s : σ) ↦ (ε.toRingHom : (a : S) → T) (a s)
have h : Eq (α := R →+* T) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑ε : S →+* T) (algebraMap R S)) (algebraMap R T)
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
    MvPowerSeries σ R)
have rw : ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
Tactic: rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
⊢ Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
have conv_lhs : Eq (α := MvPowerSeries σ R)
  ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
    MvPowerSeries σ R)
  ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
Tactic: conv_lhs => rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
conv_lhs :
  Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
have conv_lhs₁ : Eq (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
  ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
Tactic: conv_lhs => rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((monomial d : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
have rw : HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
    ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
    (∏ a ∈ d.support, HPow.hPow (β := ℕ) (HPow.hPow (α := MvPowerSeries σ R) (X a) p) ((d : (a : σ) → ℕ) a : ℕ) :
      MvPowerSeries σ R) =
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
    (∏ x ∈ d.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X x) ((p • d : (a : σ) → ℕ) x : ℕ) :
      MvPowerSeries σ R)
Tactic: rw [expand, substAlgHom_monomial (HasSubst.X_pow hp), monomial_eq', Finsupp.prod,
    Finsupp.prod_of_support_subset _ Finsupp.support_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
rw :
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (∏ a ∈ d.support, HPow.hPow (β := ℕ) (HPow.hPow (α := MvPowerSeries σ R) (X a) p) ((d : (a : σ) → ℕ) a : ℕ) :
        MvPowerSeries σ R) =
    HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      (∏ x ∈ d.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X x) ((p • d : (a : σ) → ℕ) x : ℕ) :
        MvPowerSeries σ R)
⊢ Eq (α := MvPowerSeries σ R)
    ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) ((monomial d : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries σ R)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
have h : ∀ i ∈ d.support, HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X i) 0 = 1
Tactic: rw [expand, substAlgHom_monomial (HasSubst.X_pow hp), monomial_eq', Finsupp.prod,
    Finsupp.prod_of_support_subset _ Finsupp.support_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (expand 1 ⋯) (AlgHom.id R (MvPowerSeries σ R))
have H : ∀ (i : MvPowerSeries σ R),
  Eq (α := MvPowerSeries σ R) ((expand 1 sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
    ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
⊢ AlgHom.comp (expand p hp) (substAlgHom hf) = substAlgHom ⋯
have H : ∀ (i : MvPowerSeries σ S),
  Eq (α := MvPowerSeries τ S)
    ((AlgHom.comp (expand p hp) (substAlgHom hf) : (a : MvPowerSeries σ S) → MvPowerSeries τ S) i : MvPowerSeries τ S)
    ((substAlgHom sorry : (a : MvPowerSeries σ S) → MvPowerSeries τ S) i : MvPowerSeries τ S)
Tactic: ext1 i