awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst : TendstoCofinite f
inst_1 : CommSemiring R
inst_2 : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain g ⁻¹' {y}) ⋯,
      ∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
have h : Eq.{u_4 + 1} (α := R)
  (∑
    p_1 ∈ Finset.image (fun (u : σ →₀ ℕ) ↦ (mapDomain f u, u)) (Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) sorry),
    (coeff p_1.2 : (a : MvPowerSeries σ R) → R) p)
  (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) sorry, (coeff x : (a : MvPowerSeries σ R) → R) p)
Tactic: rw [← Finset.sum_finset_product' ((TendstoCofinite.finite_preimage_singleton
    (Finsupp.mapDomain (g ∘ f)) y).toFinset.image (fun u ↦ (Finsupp.mapDomain f u, u))) _ _
      (by simp; grind [mapDomain_comp]), Finset.sum_image (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst : TendstoCofinite f
inst_1 : CommSemiring R
inst_2 : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
h :
  Eq.{u_4 + 1} (α := R)
    (∑
      p_1 ∈
        Finset.image (fun (u : σ →₀ ℕ) ↦ (mapDomain f u, u)) (Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) ⋯),
      (coeff p_1.2 : (a : MvPowerSeries σ R) → R) p)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
⊢ Eq.{u_4 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain g ⁻¹' {y}) ⋯,
      ∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
have h₁ : Eq.{u_4 + 1} (α := R)
  (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) sorry,
    (coeff (mapDomain f x, x).2 : (a : MvPowerSeries σ R) → R) p)
  (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) sorry, (coeff x : (a : MvPowerSeries σ R) → R) p)
Tactic: rw [← Finset.sum_finset_product' ((TendstoCofinite.finite_preimage_singleton
    (Finsupp.mapDomain (g ∘ f)) y).toFinset.image (fun u ↦ (Finsupp.mapDomain f u, u))) _ _
      (by simp; grind [mapDomain_comp]), Finset.sum_image (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst : TendstoCofinite f
inst_1 : CommSemiring R
inst_2 : TendstoCofinite g
p : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries γ R)
    ((rename g : (a : MvPowerSeries τ R) → MvPowerSeries γ R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p) :
      MvPowerSeries γ R)
    ((rename (g ∘ f) : (a : MvPowerSeries σ R) → MvPowerSeries γ R) p : MvPowerSeries γ R)
have h : ∀ (y : γ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff y : (a : MvPowerSeries γ R) → R)
        ((rename g : (a : MvPowerSeries τ R) → MvPowerSeries γ R)
            ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p) :
          MvPowerSeries γ R) :
      R)
    ((coeff y : (a : MvPowerSeries γ R) → R)
        ((rename (g ∘ f) : (a : MvPowerSeries σ R) → MvPowerSeries γ R) p : MvPowerSeries γ R) :
      R)
Tactic: classical
  ext y; simp only [coeff_rename]
  rw [← Finset.sum_finset_product' ((TendstoCofinite.finite_preimage_singleton
    (Finsupp.mapDomain (g ∘ f)) y).toFinset.image (fun u ↦ (Finsupp.mapDomain f u, u))) _ _
      (by simp; grind [mapDomain_comp]), Finset.sum_image (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst : TendstoCofinite f
inst_1 : CommSemiring R
inst_2 : TendstoCofinite g
p : MvPowerSeries σ R
h h₁ :
  ∀ (y : γ →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      ((coeff y : (a : MvPowerSeries γ R) → R)
          ((rename g : (a : MvPowerSeries τ R) → MvPowerSeries γ R)
              ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p) :
            MvPowerSeries γ R) :
        R)
      ((coeff y : (a : MvPowerSeries γ R) → R)
          ((rename (g ∘ f) : (a : MvPowerSeries σ R) → MvPowerSeries γ R) p : MvPowerSeries γ R) :
        R)
⊢ Eq (α := MvPowerSeries γ R)
    ((rename g : (a : MvPowerSeries τ R) → MvPowerSeries γ R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p) :
      MvPowerSeries γ R)
    ((rename (g ∘ f) : (a : MvPowerSeries σ R) → MvPowerSeries γ R) p : MvPowerSeries γ R)
have h₂ : ∀ (y : γ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain g ⁻¹' {y}) sorry,
      ∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) sorry, (coeff x : (a : MvPowerSeries σ R) → R) p)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) sorry, (coeff x : (a : MvPowerSeries σ R) → R) p)
Tactic: classical
  ext y; simp only [coeff_rename]
  rw [← Finset.sum_finset_product' ((TendstoCofinite.finite_preimage_singleton
    (Finsupp.mapDomain (g ∘ f)) y).toFinset.image (fun u ↦ (Finsupp.mapDomain f u, u))) _ _
      (by simp; grind [mapDomain_comp]), Finset.sum_image (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (rename id) (AlgHom.id R (MvPowerSeries σ R))
have H : ∀ (x : MvPowerSeries σ R) (y : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff y : (a : MvPowerSeries σ R) → R)
        ((rename id : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff y : (a : MvPowerSeries σ R) → R)
        ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
Tactic: ext _ y
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPowerSeries σ R
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
have rw : Eq.{u_4 + 1} (α := R)
  ((coeff 0 : (a : MvPowerSeries τ R) → R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
    R)
  ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, ← coeff_zero_eq_constantCoeff_apply,
    coeff_rename, Finset.sum_eq_single 0 (by
      simp [mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits]) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPowerSeries σ R
rw :
  Eq.{u_4 + 1} (α := R)
    ((coeff 0 : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
have rw₁ : Eq.{u_4 + 1} (α := R)
  ((coeff 0 : (a : MvPowerSeries τ R) → R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
    R)
  ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, ← coeff_zero_eq_constantCoeff_apply,
    coeff_rename, Finset.sum_eq_single 0 (by
      simp [mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits]) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPowerSeries σ R
rw :
  Eq.{u_4 + 1} (α := R)
    ((coeff 0 : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
rw₁ :
  Eq.{u_4 + 1} (α := R)
    ((coeff 0 : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
have rw₂ : Eq.{u_4 + 1} (α := R)
  (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {0}) sorry, (coeff x : (a : MvPowerSeries σ R) → R) p : R)
  ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, ← coeff_zero_eq_constantCoeff_apply,
    coeff_rename, Finset.sum_eq_single 0 (by
      simp [mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits]) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPowerSeries σ R
rw :
  Eq.{u_4 + 1} (α := R)
    ((coeff 0 : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
rw₁ :
  Eq.{u_4 + 1} (α := R)
    ((coeff 0 : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R)
rw₂ :
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {0}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p : R)
    ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) p : R)
have rw₃ : Eq.{u_4 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R) ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, ← coeff_zero_eq_constantCoeff_apply,
    coeff_rename, Finset.sum_eq_single 0 (by
      simp [mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits]) (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
a₁ a₂ : MvPowerSeries σ R
h :
  Eq (α := MvPowerSeries τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPowerSeries σ R) → MvPowerSeries τ R) a₁ : MvPowerSeries τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPowerSeries σ R) → MvPowerSeries τ R) a₂ : MvPowerSeries τ R)
⊢ a₁ = a₂
have h₁ : ∀ (x : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) a₁ : R)
    ((coeff x : (a : MvPowerSeries σ R) → R) a₂ : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
inst_2 : CommSemiring S
φ : R →+* S
p : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries τ S)
    ((rename f : (a : MvPowerSeries σ S) → MvPowerSeries τ S)
        ((map φ : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p) :
      MvPowerSeries τ S)
    ((map φ : (a : MvPowerSeries τ R) → MvPowerSeries τ S)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p) :
      MvPowerSeries τ S)
have h : ∀ (n : τ →₀ ℕ),
  Eq.{u_5 + 1} (α := S)
    ((coeff n : (a : MvPowerSeries τ S) → S)
        ((rename f : (a : MvPowerSeries σ S) → MvPowerSeries τ S)
            ((map φ : (a : MvPowerSeries σ R) → MvPowerSeries σ S) p) :
          MvPowerSeries τ S) :
      S)
    ((coeff n : (a : MvPowerSeries τ S) → S)
        ((map φ : (a : MvPowerSeries τ R) → MvPowerSeries τ S)
            ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p) :
          MvPowerSeries τ S) :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPolynomial σ R
⊢ Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑p : MvPowerSeries σ R) : MvPowerSeries τ R)
    ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) : MvPowerSeries τ R) : MvPowerSeries τ R)
have C : ∀ (a : R),
  Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R)
        (↑((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R) :
      MvPowerSeries τ R)
    ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
            ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPowerSeries τ R) :
      MvPowerSeries τ R)
Tactic: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add P Q hP hQ => simp [hP, hQ]
  | mul_X P n hP => simp only [MvPolynomial.coe_mul, MvPolynomial.coe_X, map_mul, hP, rename_X,
    MvPolynomial.rename_X]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPowerSeries τ R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R)
          (↑((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R) :
        MvPowerSeries τ R)
      ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
          MvPowerSeries τ R) :
        MvPowerSeries τ R)
⊢ Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑p : MvPowerSeries σ R) : MvPowerSeries τ R)
    ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) : MvPowerSeries τ R) : MvPowerSeries τ R)
have add : ∀ (P Q : MvPolynomial σ R)
  (hP :
    Eq (α := MvPowerSeries τ R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑P : MvPowerSeries σ R) : MvPowerSeries τ R)
      ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) P) : MvPowerSeries τ R) :
        MvPowerSeries τ R))
  (hQ :
    Eq (α := MvPowerSeries τ R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑Q : MvPowerSeries σ R) : MvPowerSeries τ R)
      ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) Q) : MvPowerSeries τ R) :
        MvPowerSeries τ R)),
  Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑(P + Q) : MvPowerSeries σ R) : MvPowerSeries τ R)
    ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (P + Q)) : MvPowerSeries τ R) :
      MvPowerSeries τ R)
Tactic: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add P Q hP hQ => simp [hP, hQ]
  | mul_X P n hP => simp only [MvPolynomial.coe_mul, MvPolynomial.coe_X, map_mul, hP, rename_X,
    MvPolynomial.rename_X]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPowerSeries τ R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R)
          (↑((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) : MvPowerSeries σ R) :
        MvPowerSeries τ R)
      ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
              ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
          MvPowerSeries τ R) :
        MvPowerSeries τ R)
add :
  ∀ (P Q : MvPolynomial σ R)
    (hP :
      Eq (α := MvPowerSeries τ R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑P : MvPowerSeries σ R) : MvPowerSeries τ R)
        ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) P) : MvPowerSeries τ R) :
          MvPowerSeries τ R))
    (hQ :
      Eq (α := MvPowerSeries τ R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑Q : MvPowerSeries σ R) : MvPowerSeries τ R)
        ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) Q) : MvPowerSeries τ R) :
          MvPowerSeries τ R)),
    Eq (α := MvPowerSeries τ R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑(P + Q) : MvPowerSeries σ R) : MvPowerSeries τ R)
      ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (P + Q)) : MvPowerSeries τ R) :
        MvPowerSeries τ R)
⊢ Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑p : MvPowerSeries σ R) : MvPowerSeries τ R)
    ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) : MvPowerSeries τ R) : MvPowerSeries τ R)
have mul_X : ∀ (P : MvPolynomial σ R) (n : σ)
  (hP :
    Eq (α := MvPowerSeries τ R)
      ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑P : MvPowerSeries σ R) : MvPowerSeries τ R)
      ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) P) : MvPowerSeries τ R) :
        MvPowerSeries τ R)),
  Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (↑(P * MvPolynomial.X n) : MvPowerSeries σ R) :
      MvPowerSeries τ R)
    ((↑((MvPolynomial.rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (P * MvPolynomial.X n)) :
        MvPowerSeries τ R) :
      MvPowerSeries τ R)
Tactic: induction p using MvPolynomial.induction_on with
  | C a => simp
  | add P Q hP hQ => simp [hP, hQ]
  | mul_X P n hP => simp only [MvPolynomial.coe_mul, MvPolynomial.coe_X, map_mul, hP, rename_X,
    MvPolynomial.rename_X]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial (embDomain e x) : (a : R) → MvPowerSeries τ R) r))
    ((monomial x : (a : R) → MvPowerSeries σ R) r)
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (killComplFun e ((monomial (embDomain e x) : (a : R) → MvPowerSeries τ R) r)) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) ((monomial x : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial (embDomain e x) : (a : R) → MvPowerSeries τ R) r))
    ((monomial x : (a : R) → MvPowerSeries σ R) r)
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (killComplFun e ((monomial (embDomain e x) : (a : R) → MvPowerSeries τ R) r)) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) ((monomial x : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) : R)
Tactic: classical
  ext; simp [coeff_killComplFun, coeff_monomial, embDomain_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) 0
have h₁ : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
n : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
have h₁ : embDomain e n = x → r = 0
Tactic: simp [coeff_killComplFun, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) 0
have h₁ : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: classical
  ext; simp [coeff_killComplFun, coeff_monomial]
  grind
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
h₁ h₂ :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) 0
have h₃ : ∀ (n : σ →₀ ℕ), embDomain e n = x → r = 0
Tactic: classical
  ext; simp [coeff_killComplFun, coeff_monomial]
  grind
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p q : MvPowerSeries τ R
⊢ killComplFun e (p * q) = killComplFun e p * killComplFun e q
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e (p * q)) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e p * killComplFun e q) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p q : MvPowerSeries τ R
⊢ killComplFun e (p * q) = killComplFun e p * killComplFun e q
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e (p * q)) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e p * killComplFun e q) : R)
Tactic: classical
  ext
  simp [coeff_killComplFun, coeff_mul, ← image_prodMap_embDomain_antidiagonal, Finset.sum_image
    ((Function.Injective.injOn (Prod.map_injective.mpr ⟨embDomain_injective e,
      embDomain_injective e⟩)))]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst : TendstoCofinite f
inst_1 : CommSemiring R
inst_2 : CommSemiring S
e_1 e : σ ↪ τ
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e 0) 0
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e 0) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst : TendstoCofinite f
inst_1 : CommSemiring R
inst_2 : CommSemiring S
e_1 e : σ ↪ τ
x x_1 : MvPowerSeries τ R
⊢ killComplFun e (x + x_1) = killComplFun e x + killComplFun e x_1
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e (x + x_1)) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (killComplFun e x + killComplFun e x_1) : R)
Tactic: ext