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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
⊢ (eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f = eval₂ φ a f
have h : IsDenseInducing.extend sorry (MvPolynomial.eval₂ φ a) f =
  if H : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f then
    MvPolynomial.eval₂ φ a (H.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
  else IsDenseInducing.extend sorry (MvPolynomial.eval₂ φ a) f
Tactic: simp only [eval₂Hom_eq_extend, eval₂]
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
    if H : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f then
      MvPolynomial.eval₂ φ a (H.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
    else IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f
have pos : ∀ (h : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f),
  IsDenseInducing.extend sorry (MvPolynomial.eval₂ φ a) f =
    MvPolynomial.eval₂ φ a (h.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
Tactic: split_ifs with h
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
pos :
  ∀ (h : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f),
    IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
      MvPolynomial.eval₂ φ a (h.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
    if H : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f then
      MvPolynomial.eval₂ φ a (H.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
    else IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f
have neg : ∀ (h : ¬∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f),
  IsDenseInducing.extend sorry (MvPolynomial.eval₂ φ a) f = IsDenseInducing.extend sorry (MvPolynomial.eval₂ φ a) f
Tactic: split_ifs with h
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
h : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
    MvPolynomial.eval₂ φ a (h.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
have pos : ∀ (p : MvPolynomial σ R),
  IsDenseInducing.extend sorry (MvPolynomial.eval₂ φ a) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ φ a
      (Exists.choose (p := fun (p_1 : MvPolynomial σ R) ↦ (↑p_1 : MvPowerSeries σ R) = (↑p : MvPowerSeries σ R)) sorry)
Tactic: obtain ⟨p, rfl⟩ := h
Cleared hypotheses: f, h
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
h : ¬∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f = IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f
have neg : Eq.{u_3 + 1} (α := S) ((eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f : S)
  ((eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f : S)
Tactic: rw [← eval₂Hom_eq_extend hφ 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
φ : 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
⊢ UniformContinuous (eval₂ φ a)
have rw : UniformContinuous (α := MvPowerSeries σ R) (β := S) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
Tactic: rw [← coe_eval₂Hom hφ 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
φ : 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (eval₂ φ a f)
have rw : HasSum
  (fun (d : σ →₀ ℕ) ↦
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
      (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
  (IsDenseInducing.extend sorry (MvPolynomial.eval₂ φ a) f)
Tactic: rw [← coe_eval₂Hom hφ ha, eval₂Hom_eq_extend hφ 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
φ : 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f)
have h : ∀ (d : σ →₀ ℕ),
  HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
      (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S) =
    Function.comp (β := MvPowerSeries σ R) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
      (fun (d : σ →₀ ℕ) ↦ (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f)) d
Tactic: convert! (hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (?_) with d
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S) =
      Function.comp (β := MvPowerSeries σ R) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
        (fun (d : σ →₀ ℕ) ↦ (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f)) d
⊢ HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f)
have convert! : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
Tactic: convert! (hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (?_) with d
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
f : MvPowerSeries σ R
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
have rw : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ φ a)
Tactic: rw [coe_eval₂Hom]
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε (↑p : MvPowerSeries σ R) = MvPolynomial.eval₂ φ a p
⊢ ε = eval₂ φ a
have rw : ε = (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
Tactic: rw [← coe_eval₂Hom hφ 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
φ : 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ (⇑ε : (a : S) → T) ∘ eval₂ φ a = eval₂ (ε.comp φ) ((⇑ε : (a : S) → T) ∘ a)
have hε₁ : Continuous[instTopologicalSpace R, inst_11.toTopologicalSpace] ((⇑ε : (a : S) → T) ∘ eval₂ φ a)
Tactic: apply eval₂_unique _ (ha.map hε)
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
hε₁ : Continuous[instTopologicalSpace R, inst_11.toTopologicalSpace] ((⇑ε : (a : S) → T) ∘ eval₂ φ a)
⊢ (⇑ε : (a : S) → T) ∘ eval₂ φ a = eval₂ (ε.comp φ) ((⇑ε : (a : S) → T) ∘ a)
have h : ∀ (p : MvPolynomial σ R),
  ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
Tactic: apply eval₂_unique _ (ha.map hε)
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
hε₁ : Continuous[instTopologicalSpace R, inst_11.toTopologicalSpace] ((⇑ε : (a : S) → T) ∘ eval₂ φ a)
h :
  ∀ (p : MvPolynomial σ R),
    ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : MvPowerSeries σ R) =
      MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
⊢ (⇑ε : (a : S) → T) ∘ eval₂ φ a = eval₂ (ε.comp φ) ((⇑ε : (a : S) → T) ∘ a)
have apply : Continuous[inst_1.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑(ε.comp φ) : (a : R) → T)
Tactic: apply eval₂_unique _ (ha.map hε)
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
p : MvPolynomial σ R
⊢ ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
have h : (ε : (a : S) → T) (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
Tactic: simp only [Function.comp_apply, 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
φ : 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
p : MvPolynomial σ R
⊢ (ε : (a : S) → T) (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
have h : (ε : (a : S) → T) ((MvPolynomial.eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S) =
  MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
Tactic: rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom,
      MvPolynomial.coe_eval₂Hom]
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
p : MvPolynomial σ R
h :
  (ε : (a : S) → T) ((MvPolynomial.eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S) =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
⊢ (ε : (a : S) → T) (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
have h₁ : (ε.comp (MvPolynomial.eval₂Hom φ a) : (a : MvPolynomial σ R) → T) p =
  MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
Tactic: rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom,
      MvPolynomial.coe_eval₂Hom]
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
p : MvPolynomial σ R
h :
  (ε : (a : S) → T) ((MvPolynomial.eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S) =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
h₁ :
  (ε.comp (MvPolynomial.eval₂Hom φ a) : (a : MvPolynomial σ R) → T) p =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
⊢ (ε : (a : S) → T) (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
have h₂ : (MvPolynomial.eval₂Hom (ε.comp φ) fun (i : σ) ↦ (ε : (a : S) → T) (a i) : (a : MvPolynomial σ R) → T) p =
  MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
Tactic: rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom,
      MvPolynomial.coe_eval₂Hom]
-- 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
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
p : MvPolynomial σ R
h :
  (ε : (a : S) → T) ((MvPolynomial.eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S) =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
h₁ :
  (ε.comp (MvPolynomial.eval₂Hom φ a) : (a : MvPolynomial σ R) → T) p =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
h₂ :
  (MvPolynomial.eval₂Hom (ε.comp φ) fun (i : σ) ↦ (ε : (a : S) → T) (a i) : (a : MvPolynomial σ R) → T) p =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
⊢ (ε : (a : S) → T) (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
have h₃ : MvPolynomial.eval₂ (ε.comp φ) (fun (i : σ) ↦ (ε : (a : S) → T) (a i)) p =
  MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
Tactic: rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom,
      MvPolynomial.coe_eval₂Hom]
-- 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
⊢ OneHom.toFun (↑(↑(eval₂Hom (φ := algebraMap R S) ⋯ ha) : MvPowerSeries σ R →* S) : OneHom (MvPowerSeries σ R) S)
      ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r) =
    (algebraMap R S : (a : R) → S) r
have simp : Eq.{u_3 + 1} (α := S)
  ((eval₂Hom (φ := algebraMap R S) sorry 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)
Tactic: simp only [toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_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
φ : 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
⊢ 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)
  ((eval₂Hom (φ := algebraMap R S) sorry ha : (a : MvPowerSeries σ R) → S)
      ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
    S)
  ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [← c_eq_algebraMap, coe_eval₂Hom, eval₂_C]