awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ 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)
h₃ : ∀ (n : σ →₀ ℕ), embDomain e n = x → r = 0
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e ((monomial x : (a : R) → MvPowerSeries τ R) r)) 0

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

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 : σ ↪ τ
p q : MvPowerSeries τ R
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)
⊢ killComplFun e (p * q) = killComplFun e p * killComplFun e q

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p q : MvPowerSeries τ R
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:
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⟩)))]

Premises used: Finsupp.image_prodMap_embDomain_antidiagonal, Iff.mpr, Function.Injective.injOn, Finsupp.embDomain_injective, And.intro, Prod.map_injective, _private.0.MvPowerSeries.coeff_killComplFun, Finset.sum_image, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p q : MvPowerSeries τ R
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)
⊢ killComplFun e (p * q) = killComplFun e p * killComplFun e q

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

Premises used: Finsupp.image_prodMap_embDomain_antidiagonal, Iff.mpr, Function.Injective.injOn, Finsupp.embDomain_injective, And.intro, Prod.map_injective, _private.0.MvPowerSeries.coeff_killComplFun, Finset.sum_image, MvPowerSeries.coeff_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_1 e : σ ↪ τ
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e 1) 1

Tactic:
simpa using killComplFun_monomial_embDomain 0 1

Premises used: _private.0.MvPowerSeries.killComplFun_monomial_embDomain, OfNat.ofNat
-- 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_1 e : σ ↪ τ
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)
⊢ Eq (α := MvPowerSeries σ R) (killComplFun e 0) 0

Tactic:
ext
-- 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_1 e : σ ↪ τ
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:
simp [coeff_killComplFun]

Premises used: _private.0.MvPowerSeries.coeff_killComplFun
-- 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_1 e : σ ↪ τ
x x_1 : MvPowerSeries τ R
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)
⊢ killComplFun e (x + x_1) = killComplFun e x + killComplFun e x_1

Tactic:
ext
-- 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_1 e : σ ↪ τ
x x_1 : MvPowerSeries τ R
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:
simp [coeff_killComplFun]

Premises used: _private.0.MvPowerSeries.coeff_killComplFun
-- 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_1 e : σ ↪ τ
⊢ ∀ (r : R),
    Eq (α := MvPowerSeries σ R) (killComplFun e ((algebraMap R (MvPowerSeries τ R) : (a : R) → MvPowerSeries τ R) r))
      ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r)

Tactic:
simpa using killComplFun_monomial_embDomain 0

Premises used: _private.0.MvPowerSeries.killComplFun_monomial_embDomain, OfNat.ofNat
-- 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)
        ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) p : MvPowerSeries σ R) :
      R)
    ((coeff (embDomain e x) : (a : MvPowerSeries τ R) → R) p : R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries σ R)
    ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R)
        ((monomial (embDomain e x) : (a : R) → MvPowerSeries τ R) r) :
      MvPowerSeries σ R)
    ((monomial x : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)

Tactic:
killComplFun_monomial_embDomain x r

Premises used: Function.update, Multiset.map, _private.0.MvPowerSeries.killComplFun_monomial_embDomain, Pi.single, dite, MvPowerSeries.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)
⊢ Eq (α := MvPowerSeries σ R)
    ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) ((monomial x : (a : R) → MvPowerSeries τ R) r) :
      MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
killComplFun_monomial_eq_zero r h

Premises used: _private.0.MvPowerSeries.killComplFun_monomial_eq_zero, Function.update, Multiset.map, Pi.single, dite, MvPowerSeries.killComplFun
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
r : R
⊢ Eq (α := MvPowerSeries σ R)
    ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries τ R) r) :
      MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)

Tactic:
simpa using killCompl_monomial_embDomain 0 r

Premises used: MvPowerSeries.killCompl_monomial_embDomain, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
i : σ
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) (X ((e : (a : σ) → τ) i)) : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R) (X i) : R)
⊢ Eq (α := MvPowerSeries σ R)
    ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) (X ((e : (a : σ) → τ) i)) : MvPowerSeries σ R)
    (X i : MvPowerSeries σ R)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
i : σ
n : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) (X ((e : (a : σ) → τ) i)) : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (X i) : R)

Tactic:
simp [coeff_X, coeff_killCompl, ← embDomain_single]

Premises used: MvPowerSeries.coeff_X, Finsupp.embDomain_single, MvPowerSeries.coeff_killCompl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
i : σ
h h₁ :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) (X ((e : (a : σ) → τ) i)) : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R) (X i) : R)
⊢ Eq (α := MvPowerSeries σ R)
    ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) (X ((e : (a : σ) → τ) i)) : MvPowerSeries σ R)
    (X i : MvPowerSeries σ R)

Tactic:
classical
  ext; simp [coeff_X, coeff_killCompl, ← embDomain_single]

Premises used: MvPowerSeries.coeff_X, Finsupp.embDomain_single, MvPowerSeries.coeff_killCompl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range.{u_2, u_1 + 1} (ι := σ) (⇑e : (a : σ) → τ)
⊢ Ne (α := ℕ) 1 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range.{u_2, u_1 + 1} (ι := σ) (⇑e : (a : σ) → τ)
rwa : ¬(↑(support (M := ℕ) (single t 1)) : Set τ) ⊆ Set.range.{u_2, u_1 + 1} (ι := σ) (⇑e : (a : σ) → τ)
rwa₁ : ¬(↑{t} : Set τ) ⊆ Set.range.{u_2, u_1 + 1} (ι := σ) (⇑e : (a : σ) → τ)
rwa₂ : ¬Subset (α := Set τ) {t} (Set.range.{u_2, u_1 + 1} (ι := σ) (⇑e : (a : σ) → τ))
rwa₃ rwa₄ rwa₅ rwa₆ : t ∉ Set.range.{u_2, u_1 + 1} (ι := σ) (⇑e : (a : σ) → τ)
⊢ single t 1 ∉ Set.range (embDomain e)

Tactic:
rwa [mem_range_embDomain_iff, support_single _ (by simp), Finset.coe_singleton,
      Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Finsupp.support_single, Finset.coe_singleton, Finsupp.mem_range_embDomain_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range.{u_2, u_1 + 1} (ι := σ) (⇑e : (a : σ) → τ)
⊢ single t 1 ∉ Set.range (embDomain e)

Tactic:
replace h : single t 1 ∉ Set.range (embDomain e) := by
    rwa [mem_range_embDomain_iff, support_single _ (by simp), Finset.coe_singleton,
      Set.singleton_subset_iff]
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
t : τ
h : single t 1 ∉ Set.range (embDomain e)
⊢ Eq (α := MvPowerSeries σ R) ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) (X t) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
simpa using killCompl_monomial_eq_zero (1 : R) h

Premises used: MvPowerSeries.killCompl_monomial_eq_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
H :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((AlgHom.comp (killCompl e) (rename (⇑e : (a : σ) → τ)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x :
            MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (AlgHom.comp (killCompl e) (rename (⇑e : (a : σ) → τ)))
    (AlgHom.id R (MvPowerSeries σ R))

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
x : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((AlgHom.comp (killCompl e) (rename (⇑e : (a : σ) → τ)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x :
          MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)

Tactic:
simp [coeff_killCompl]

Premises used: MvPowerSeries.coeff_killCompl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
⊢ (killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R)
      ((rename (⇑e : (a : σ) → τ) : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p) =
    p

Tactic:
AlgHom.congr_fun (killCompl_comp_rename) p

Premises used: Multiset.sum, Multiset.foldr, MvPowerSeries.killCompl_comp_rename, MvPowerSeries.renameFun, Filter.TendstoCofinite.mapDomain, AlgHom.congr_fun, MvPowerSeries.killComplFun, Finset.sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
e : σ ↪ τ
φ : R →+* S
p : MvPowerSeries τ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_5 + 1} (α := S)
      ((coeff n : (a : MvPowerSeries σ S) → S)
          ((killCompl e : (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)
              ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) p) :
            MvPowerSeries σ S) :
        S)
⊢ Eq (α := MvPowerSeries σ S)
    ((killCompl e : (a : MvPowerSeries τ S) → MvPowerSeries σ S)
        ((map φ : (a : MvPowerSeries τ R) → MvPowerSeries τ S) p) :
      MvPowerSeries σ S)
    ((map φ : (a : MvPowerSeries σ R) → MvPowerSeries σ S)
        ((killCompl e : (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
inst : CommSemiring R
inst_1 : CommSemiring S
e : σ ↪ τ
φ : R →+* S
p : MvPowerSeries τ R
n : σ →₀ ℕ
⊢ Eq.{u_5 + 1} (α := S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        ((killCompl e : (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)
            ((killCompl e : (a : MvPowerSeries τ R) → MvPowerSeries σ R) p) :
          MvPowerSeries σ S) :
      S)

Tactic:
simp [coeff_killCompl]

Premises used: MvPowerSeries.coeff_killCompl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
⊢ ∀ (s : σ), IsNilpotent.{u_6} (R := R) ((constantCoeff : (a : MvPowerSeries τ R) → R) ((X ∘ f) s) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
d : τ →₀ ℕ
x : σ
contrapose :
  x ∉ ⋃ i ∈ (↑d.support : Set τ), f ⁻¹' {i} →
    x ∉ {s : σ | Ne.{u_6 + 1} (α := R) ((coeff d : (a : MvPowerSeries τ R) → R) ((X ∘ f) s) : R) (0 : R)}
⊢ Membership.mem (γ := Set σ)
      {s : σ | Ne.{u_6 + 1} (α := R) ((coeff d : (a : MvPowerSeries τ R) → R) ((X ∘ f) s) : R) (0 : R)} x →
    Membership.mem (γ := Set σ) (⋃ i ∈ (↑d.support : Set τ), f ⁻¹' {i}) x

Tactic:
contrapose
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
d : τ →₀ ℕ
x : σ
h : x ∉ ⋃ i ∈ (↑d.support : Set τ), f ⁻¹' {i}
_ :
  Membership.mem (γ := Set σ)
      {s : σ | Ne.{u_6 + 1} (α := R) ((coeff d : (a : MvPowerSeries τ R) → R) ((X ∘ f) s) : R) (0 : R)} x →
    False
⊢ x ∉ {s : σ | Ne.{u_6 + 1} (α := R) ((coeff d : (a : MvPowerSeries τ R) → R) ((X ∘ f) s) : R) (0 : R)}

Tactic:
_
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
d : τ →₀ ℕ
x : σ
h : x ∉ ⋃ i ∈ (↑d.support : Set τ), f ⁻¹' {i}
h_1 :
  Membership.mem (γ := Set σ)
    {s : σ | Ne.{u_6 + 1} (α := R) ((coeff d : (a : MvPowerSeries τ R) → R) ((X ∘ f) s) : R) (0 : R)} x
⊢ False

Tactic:
simp_all [coeff_X]

Premises used: MvPowerSeries.coeff_X
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
d : τ →₀ ℕ
x : σ
h : x ∉ ⋃ i ∈ (↑d.support : Set τ), f ⁻¹' {i}
h_1 :
  Membership.mem (γ := Set σ)
    {s : σ | Ne.{u_6 + 1} (α := R) ((coeff d : (a : MvPowerSeries τ R) → R) ((X ∘ f) s) : R) (0 : R)} x
⊢ False

Tactic:
classical simp_all [coeff_X]

Premises used: MvPowerSeries.coeff_X
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
h :
  ∀ (n : τ →₀ ℕ),
    Eq.{u_6 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries τ R) → R)
          ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
        R)
      ((coeff n : (a : MvPowerSeries τ R) → R) (subst (X ∘ f) p) : R)
⊢ Eq (α := MvPowerSeries τ R) ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R)
    (subst (X ∘ f) p : MvPowerSeries τ R)

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
h :
  Eq.{u_6 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯,
      HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (i.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R))
⊢ Eq.{u_6 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((coeff n : (a : MvPowerSeries τ R) → R) (subst (X ∘ f) p) : R)

Tactic:
rw [coeff_rename, coeff_subst (HasSubst.X_comp _) p n, finsum_eq_sum _
    (coeff_subst_finite (HasSubst.X_comp _) p n)]

Premises used: finsum_eq_sum, MvPowerSeries.coeff_subst, MvPowerSeries.HasSubst.X_comp, MvPowerSeries.coeff_subst_finite, MvPowerSeries.coeff_rename
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
d : σ →₀ ℕ
hd :
  HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
      ((coeff n : (a : MvPowerSeries τ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
        R) ≠
    0
⊢ HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
      ((coeff n : (a : MvPowerSeries τ R) → R) ((monomial (mapDomain f d) : (a : R) → MvPowerSeries τ R) 1) : R) ≠
    0

Tactic:
simp_rw [← monomial_mapDomain_apply_one] at hd

Premises used: MvPowerSeries.monomial_mapDomain_apply_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
d : σ →₀ ℕ
hd :
  HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
      ((coeff n : (a : MvPowerSeries τ R) → R) ((monomial (mapDomain f d) : (a : R) → MvPowerSeries τ R) 1) : R) ≠
    0
⊢ mapDomain f d = n

Tactic:
(eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm

Premises used: right_ne_zero_of_mul, Eq.symm, MvPowerSeries.eq_of_coeff_monomial_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
d : σ →₀ ℕ
hd :
  HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
      ((coeff n : (a : MvPowerSeries τ R) → R) ((monomial (mapDomain f d) : (a : R) → MvPowerSeries τ R) 1) : R) ≠
    0
⊢ mapDomain f d = n

Tactic:
exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm

Premises used: right_ne_zero_of_mul, Eq.symm, MvPowerSeries.eq_of_coeff_monomial_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n

Tactic:
have (d : σ →₀ ℕ) (hd : (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0) :
      mapDomain f d = n := by
    simp_rw [← monomial_mapDomain_apply_one] at hd
    exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
R : Type u_6
inst_1 : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this :
  ∀ (d : σ →₀ ℕ)
    (hd :
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff n : (a : MvPowerSeries τ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) (X (f s)) e) :
            R) ≠
        0),
    mapDomain f d = n
⊢ Eq.{u_6 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {n}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_6} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R)
              ((coeff n : (a : MvPowerSeries τ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
                R))
          ⋯,
      HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R)
        ((coeff n : (a : MvPowerSeries τ R) → R)
            (i.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries τ R) ((X ∘ f) s) e) :
          R))

Tactic:
(Finset.sum_subset_zero_on_sdiff ?_ ?_ (fun x hx => ?_)).symm

Premises used: Eq.symm, Finset.sum_subset_zero_on_sdiff