awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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 : γ →₀ ℕ
⊢ Set.InjOn (β := Prod.{u_2, u_1} (τ →₀ ℕ) (σ →₀ ℕ)) (fun (u : σ →₀ ℕ) ↦ (mapDomain f u, u))
    (↑(Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) ⋯) : Set (σ →₀ ℕ))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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)
h₁ h₂ :
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) ⋯,
      (coeff (mapDomain f x, x).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)

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)]

Premises used: Filter.TendstoCofinite.finite_preimage_singleton, Finsupp.mapDomain, Function.comp, Prod.mk, Set.Finite.toFinset, Finset.sum_image, Finset.image, Finset.sum_finset_product'
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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)
h₂ :
  ∀ (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)
⊢ 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)

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)]

Premises used: Finset.sum_image, MvPowerSeries.coeff_rename
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries γ R) (AlgHom.comp (rename g) (rename f)) (rename (g ∘ f))

Tactic:
AlgHom.ext fun p ↦ rename_rename f g p

Premises used: MvPowerSeries.rename_rename, AlgHom.ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
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)
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (rename id) (AlgHom.id R (MvPowerSeries σ R))

Tactic:
ext _ y
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
x : MvPowerSeries σ R
y : σ →₀ ℕ
⊢ ∀ b ∈ Set.Finite.toFinset (s := mapDomain id ⁻¹' {y}) ⋯,
    b ≠ y → Eq.{u_4 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) x : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
x : MvPowerSeries σ R
y : σ →₀ ℕ
⊢ y ∉ Set.Finite.toFinset (s := mapDomain id ⁻¹' {y}) ⋯ →
    Eq.{u_4 + 1} (α := R) ((coeff y : (a : MvPowerSeries σ R) → R) x : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
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:
simpa [coeff_rename] using Finset.sum_eq_single y (by simp) (by simp)

Premises used: Finset.sum_eq_single, MvPowerSeries.coeff_rename
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPowerSeries σ R
⊢ (rename id : (a : MvPowerSeries σ R) → MvPowerSeries σ R) p = p

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPowerSeries σ R
⊢ ∀ (b : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ)) (Set.Finite.toFinset (s := mapDomain f ⁻¹' {0}) ⋯) b →
      b ≠ 0 → Eq.{u_4 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simp [mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits]

Premises used: Finsupp.mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
p : MvPowerSeries σ R
⊢ 0 ∉ Set.Finite.toFinset (s := mapDomain f ⁻¹' {0}) ⋯ →
    Eq.{u_4 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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)
rw₃ rw₄ :
  Eq.{u_4 + 1} (α := R) ((coeff 0 : (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)

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)]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, Finset.sum_eq_single, MvPowerSeries.coeff_rename, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
a₁ : MvPowerSeries σ R
_ :
  ∀ ⦃a₂ : MvPowerSeries σ R⦄,
    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₂
⊢ ∀ ⦃a₂ : MvPowerSeries σ R⦄,
    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₂

Tactic:
_
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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)
h₁ :
  ∀ (x : σ →₀ ℕ),
    Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) a₁ : R)
      ((coeff x : (a : MvPowerSeries σ R) → R) a₂ : R)
⊢ a₁ = a₂

Tactic:
ext x
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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)
x : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) a₁ : R)
    ((coeff x : (a : MvPowerSeries σ R) → R) a₂ : R)

Tactic:
simpa using MvPowerSeries.ext_iff.mp h (embDomain e x)

Premises used: MvPowerSeries.ext_iff, Iff.mp, Finsupp.embDomain
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p q : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries τ R)
      ((rename (⇑e : (a : σ) → τ) : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R)
      ((rename (⇑e : (a : σ) → τ) : (a : MvPowerSeries σ R) → MvPowerSeries τ R) q : MvPowerSeries τ R) ↔
    p = q

Tactic:
(rename_injective e).eq_iff

Premises used: Function.Injective.eq_iff, MvPowerSeries.rename_injective
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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
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:
simp [coeff_rename]

Premises used: MvPowerSeries.coeff_rename
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
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:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
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:
simp [hP, hQ]
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
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:
simp only [MvPolynomial.coe_mul, MvPolynomial.coe_X, map_mul, hP, rename_X,
    MvPolynomial.rename_X]

Premises used: MvPolynomial.coe_X, map_mul, MvPolynomial.rename_X, MvPowerSeries.rename_X, MvPolynomial.coe_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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)
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)
⊢ 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)

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]

Premises used: MvPolynomial.coe_X, MvPolynomial.induction_on, map_mul, MvPolynomial.rename_X, MvPowerSeries.rename_X, MvPowerSeries.C, MvPolynomial.coe_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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 : σ ≃ τ
x : MvPowerSeries σ R
⊢ (rename (⇑e.symm : (a : τ) → σ) : (a : MvPowerSeries τ R) → MvPowerSeries σ R)
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (rename (⇑e : (a : σ) → τ))) : MvPowerSeries σ R →* MvPowerSeries τ R) :
          OneHom (MvPowerSeries σ R) (MvPowerSeries τ R))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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 : σ ≃ τ
x : MvPowerSeries τ R
⊢ OneHom.toFun (M := MvPowerSeries σ R)
      (↑(↑(AlgHom.toRingHom (rename (⇑e : (a : σ) → τ))) : MvPowerSeries σ R →* MvPowerSeries τ R) :
        OneHom (MvPowerSeries σ R) (MvPowerSeries τ R))
      ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPowerSeries τ R) → MvPowerSeries σ R) x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
⊢ ∀ (a : MvPowerSeries σ R),
    Eq (α := MvPowerSeries σ R)
      ((renameEquiv R (Equiv.refl σ) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
      ((AlgEquiv.refl : (a : MvPowerSeries σ R) → MvPowerSeries σ R) a : MvPowerSeries σ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ ≃ τ
⊢ Eq (α := MvPowerSeries τ R ≃ₐ[R] MvPowerSeries σ R) (AlgEquiv.symm (renameEquiv R f)) (renameEquiv R f.symm)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, AlgEquiv.symm, MvPowerSeries, MvPowerSeries.renameFun, Filter.TendstoCofinite.mapDomain, Equiv.symm, MvPowerSeries.renameEquiv, Finset.sum, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
inst : CommSemiring R
e : σ ≃ τ
f : τ ≃ γ
⊢ Eq (α := MvPowerSeries σ R ≃ₐ[R] MvPowerSeries γ R) (AlgEquiv.trans (renameEquiv R e) (renameEquiv R f))
    (renameEquiv R (e.trans f))

Tactic:
AlgEquiv.ext (rename_rename e f)

Premises used: MvPowerSeries.rename_rename, AlgEquiv.ext, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries τ R
x : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) (killComplFun e p) : R)
    ((coeff (embDomain e x) : (a : MvPowerSeries τ R) → R) p : R)

Tactic:
rfl

Premises used: MvPowerSeries.killComplFun, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
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)
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial (embDomain e x) : (a : R) → MvPowerSeries τ R) r))
    ((monomial x : (a : R) → MvPowerSeries σ R) r)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
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:
simp [coeff_killComplFun, coeff_monomial, embDomain_inj]

Premises used: Finsupp.embDomain_inj, MvPowerSeries.coeff_monomial, _private.0.MvPowerSeries.coeff_killComplFun
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
h 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)
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial (embDomain e x) : (a : R) → MvPowerSeries τ R) r))
    ((monomial x : (a : R) → MvPowerSeries σ R) r)

Tactic:
classical
  ext; simp [coeff_killComplFun, coeff_monomial, embDomain_inj]

Premises used: Finsupp.embDomain_inj, MvPowerSeries.coeff_monomial, _private.0.MvPowerSeries.coeff_killComplFun
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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₁ :
  ∀ (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

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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 : σ →₀ ℕ
h₁ : embDomain e n = x → r = 0
⊢ 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:
simp [coeff_killComplFun, coeff_monomial]

Premises used: MvPowerSeries.coeff_monomial, _private.0.MvPowerSeries.coeff_killComplFun
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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 : σ →₀ ℕ
⊢ embDomain e n = x → r = 0

Tactic:
grind