awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq τ
x : τ →₀ ℕ
a : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))
ht :
  a.1.1 + a.1.2 = x →
    mapDomain f a.2.1 = a.1.1 →
      mapDomain f a.2.2 = a.1.2 →
        ∃ (a_4 : σ →₀ ℕ) (b : σ →₀ ℕ),
          mapDomain f a_4 + mapDomain f b = x ∧ ((mapDomain f a_4, mapDomain f b), a_4, b) = a
⊢ Membership.mem (γ := Set (Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))))
      {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
        p.1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ x ∧
          p.2 ∈
            Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯}
      a →
    a ∈
      (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
            Finset.product {q}
              (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) ⋯ ×ˢ
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) ⋯)) :
        Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq τ
x : τ →₀ ℕ
a : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))
⊢ a.1.1 + a.1.2 = x →
    mapDomain f a.2.1 = a.1.1 →
      mapDomain f a.2.2 = a.1.2 →
        ∃ (a_4 : σ →₀ ℕ) (b : σ →₀ ℕ),
          mapDomain f a_4 + mapDomain f b = x ∧ ((mapDomain f a_4, mapDomain f b), a_4, b) = a

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq τ
x : τ →₀ ℕ
hs :
  (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
          Finset.product {q}
            (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) ⋯ ×ˢ
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) ⋯)) :
      Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite
ht ht₁ :
  {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
      p.1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ x ∧
        p.2 ∈
          Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
            Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯} ⊆
    (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
          Finset.product {q}
            (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) ⋯ ×ˢ
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) ⋯)) :
      Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
⊢ Set.Finite (α := Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)))
    {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
      p.1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ x ∧
        p.2 ∈
          Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯}

Tactic:
classical
  apply Set.Finite.subset (s := ↑((Finset.antidiagonal x).sup (fun q ↦ Finset.product {q}
    ((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.1).toFinset ×ˢ
      (TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.2).toFinset))))
  · exact Finset.finite_toSet ..
  · intro; simp
    grind

Premises used: Finset.finite_toSet
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
inst_2 : DecidableEq τ
x : τ →₀ ℕ
h :
  ∀ (fst fst_1 snd : σ →₀ ℕ),
    Membership.mem (γ := Finset ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        (Finset.image
          (fun (x : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))) ↦
            match (motive :=
              Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)) x with
            | (fst, b) => (b.1 + b.2, b))
          (Set.Finite.toFinset (s :=
            {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
              p.1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ x ∧
                p.2 ∈
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                    Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
            ⋯))
        (fst, fst_1, snd) ↔
      (fst, fst_1, snd) ∈
        Set.Finite.toFinset (s :=
          {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
            mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1})
          ⋯
⊢ Finset.image
      (fun (x : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))) ↦
        match (motive := Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
          x with
        | (fst, b) => (b.1 + b.2, b))
      (Set.Finite.toFinset (s :=
        {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
          p.1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ x ∧
            p.2 ∈
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
        ⋯) =
    Set.Finite.toFinset (s :=
      {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
        mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1})
      ⋯

Tactic:
ext ⟨_, _, _⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
inst_2 : DecidableEq τ
x : τ →₀ ℕ
fst fst_1 snd : σ →₀ ℕ
h : fst_1 + snd = fst → (mapDomain f fst_1 + mapDomain f snd = x ↔ mapDomain f fst = x)
⊢ Membership.mem (γ := Finset ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)))
      (Finset.image
        (fun (x : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))) ↦
          match (motive := Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
            x with
          | (fst, b) => (b.1 + b.2, b))
        (Set.Finite.toFinset (s :=
          {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
            p.1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ x ∧
              p.2 ∈
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
          ⋯))
      (fst, fst_1, snd) ↔
    (fst, fst_1, snd) ∈
      Set.Finite.toFinset (s :=
        {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
          mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1})
        ⋯

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
inst_2 : DecidableEq τ
x : τ →₀ ℕ
fst fst_1 snd : σ →₀ ℕ
⊢ fst_1 + snd = fst → (mapDomain f fst_1 + mapDomain f snd = x ↔ mapDomain f fst = x)

Tactic:
grind [Finsupp.mapDomain_add]

Premises used: Finsupp.mapDomain_add
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
h :
  ∀ (x : τ →₀ ℕ),
    Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries τ R) → R) (renameFun f (p * q)) : R)
      ((coeff x : (a : MvPowerSeries τ R) → R) (renameFun f p * renameFun f q) : R)
⊢ renameFun f (p * q) = renameFun f p * renameFun f q

Tactic:
ext x
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
h :
  Eq.{u_4 + 1} (α := R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯,
      ∑ p_1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
        HMul.hMul (α := R) (β := R) ((coeff p_1.1 : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff p_1.2 : (a : MvPowerSeries σ R) → R) q : R))
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
      ∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.1}) ⋯ ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.2}) ⋯,
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) p : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) q : R))
⊢ Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries τ R) → R) (renameFun f (p * q)) : R)
    ((coeff x : (a : MvPowerSeries τ R) → R) (renameFun f p * renameFun f q) : R)

Tactic:
simp only [coeff_renameFun, coeff_mul, sum_mul_sum, ← sum_product']

Premises used: _private.0.MvPowerSeries.coeff_renameFun, Finset.sum_product', MvPowerSeries.coeff_mul, Finset.sum_mul_sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈
        Set.Finite.toFinset (s :=
          {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
            mapDomain f p.1 = x ∧ p.2 ∈ @antidiagonal _ Finsupp.instAddMonoid _ p.1})
          ⋯ ↔
      p.1 ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯ ∧ p.2 ∈ @antidiagonal _ Finsupp.instAddMonoid _ p.1

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ ∀ (p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))),
    p ∈
        Set.Finite.toFinset (s :=
          {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
            p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
              p.2 ∈
                Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
          ⋯ ↔
      p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
        p.2 ∈
          Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
x_1 : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))
simp :
  x_1.1.1 + x_1.1.2 = x →
    mapDomain f x_1.2.1 = x_1.1.1 →
      mapDomain f x_1.2.2 = x_1.1.2 →
        ∀ (a b : τ →₀ ℕ) (a_1 b_1 : σ →₀ ℕ),
          a + b = x →
            mapDomain f a_1 = a →
              mapDomain f b_1 = b → x_1.2.1 + x_1.2.2 = a_1 + b_1 → x_1.2 = (a_1, b_1) → x_1 = ((a, b), a_1, b_1)
⊢ x_1 ∈
      (↑(Set.Finite.toFinset (s :=
            {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
              p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
                p.2 ∈
                  Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                    Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
            ⋯) :
        Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))) →
    ∀ ⦃x₂ : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))⦄,
      x₂ ∈
          (↑(Set.Finite.toFinset (s :=
                {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
                  p.1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x ∧
                    p.2 ∈
                      Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ
                        Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯})
                ⋯) :
            Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))) →
        Eq (α := (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
            (match (motive :=
                Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)) x_1 with
              | (fst, b) => (b.1 + b.2, b) :
              (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
            (match (motive :=
                Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) → (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)) x₂ with
              | (fst, b) => (b.1 + b.2, b) :
              (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)) →
          x_1 = x₂

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
x_1 : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ))
⊢ x_1.1.1 + x_1.1.2 = x →
    mapDomain f x_1.2.1 = x_1.1.1 →
      mapDomain f x_1.2.2 = x_1.1.2 →
        ∀ (a b : τ →₀ ℕ) (a_1 b_1 : σ →₀ ℕ),
          a + b = x →
            mapDomain f a_1 = a →
              mapDomain f b_1 = b → x_1.2.1 + x_1.2.2 = a_1 + b_1 → x_1.2 = (a_1, b_1) → x_1 = ((a, b), a_1, b_1)

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p q : MvPowerSeries σ R
h :
  ∀ (x : τ →₀ ℕ),
    Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries τ R) → R) (renameFun f (p * q)) : R)
      ((coeff x : (a : MvPowerSeries τ R) → R) (renameFun f p * renameFun f q) : R)
h₁ :
  ∀ (x : τ →₀ ℕ),
    Eq.{u_4 + 1} (α := R)
      (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯,
        ∑ p_1 ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
          HMul.hMul (α := R) (β := R) ((coeff p_1.1 : (a : MvPowerSeries σ R) → R) p : R)
            ((coeff p_1.2 : (a : MvPowerSeries σ R) → R) q : R))
      (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ x,
        ∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.1}) ⋯ ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x.2}) ⋯,
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) p : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) q : R))
⊢ renameFun f (p * q) = renameFun f p * renameFun f q

Tactic:
classical
  ext x
  simp only [coeff_renameFun, coeff_mul, sum_mul_sum, ← sum_product']
  rw [← sum_finset_product' (renameFunAux f x).toFinset _ _ (by simp),
    ← sum_finset_product' (renameFunAux' f x).toFinset _ _ (by simp),
    ← renameFunAuxImage f x, sum_image fun _ ↦ by simp; grind]

Premises used: _private.0.MvPowerSeries.coeff_renameFun, Finset.sum_product', Finset.sum_image, MvPowerSeries.coeff_mul, Finset.sum_mul_sum
-- 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
h :
  ∀ (n : τ →₀ ℕ),
    Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f 0) : R)
      ((coeff n : (a : MvPowerSeries τ R) → R) 0 : R)
⊢ Eq (α := MvPowerSeries τ R) (renameFun f 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
n : τ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f 0) : R)
    ((coeff n : (a : MvPowerSeries τ R) → R) 0 : R)

Tactic:
simp [coeff_renameFun]

Premises used: _private.0.MvPowerSeries.coeff_renameFun
-- 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
x x_1 : MvPowerSeries σ R
h :
  ∀ (n : τ →₀ ℕ),
    Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f (x + x_1)) : R)
      ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f x + renameFun f x_1) : R)
⊢ renameFun f (x + x_1) = renameFun f x + renameFun f 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
x x_1 : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R) ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f (x + x_1)) : R)
    ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f x + renameFun f x_1) : R)

Tactic:
simp [coeff_renameFun, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, _private.0.MvPowerSeries.coeff_renameFun
-- 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
x : τ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯, (coeff 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
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
x : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) ((monomial x : (a : R) → MvPowerSeries σ R) r) :
      MvPowerSeries τ R)
    ((monomial (mapDomain f x) : (a : R) → MvPowerSeries τ R) r : MvPowerSeries τ R)

Tactic:
renameFun_monomial f ..

Premises used: Multiset.sum, Multiset.foldr, MvPowerSeries.renameFun, _private.0.MvPowerSeries.renameFun_monomial, Filter.TendstoCofinite.mapDomain, Finset.sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ x ∉ Set.Finite.toFinset (s := Set.preimage (β := τ →₀ ℕ) (mapDomain (⇑e : (a : σ) → τ)) {embDomain e x}) ⋯ →
    Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simp [← embDomain_eq_mapDomain]

Premises used: Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
rw :
  ∀ (b : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ))
        (Set.Finite.toFinset (s := Set.preimage (β := τ →₀ ℕ) (mapDomain (⇑e : (a : σ) → τ)) {embDomain e x}) ⋯) b →
      b ≠ x → Eq.{u_4 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) p : R) (0 : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((coeff (embDomain e x) : (a : MvPowerSeries τ R) → R)
        ((rename (⇑e : (a : σ) → τ) : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    ((coeff x : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
rw [coeff_rename, Finset.sum_eq_single x _ (by simp [← embDomain_eq_mapDomain])]

Premises used: Finset.sum_eq_single, MvPowerSeries.coeff_rename
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x x_1 : σ →₀ ℕ
h : mapDomain (⇑e : (a : σ) → τ) x_1 = embDomain e x
h' : ¬x_1 = x
⊢ Eq.{u_4 + 1} (α := R) ((coeff x_1 : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simp [← embDomain_eq_mapDomain, embDomain_inj, h'] at h

Premises used: Finsupp.embDomain_inj, Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ ∀ (b : σ →₀ ℕ),
    Membership.mem (γ := Finset (σ →₀ ℕ))
        (Set.Finite.toFinset (s := Set.preimage (β := τ →₀ ℕ) (mapDomain (⇑e : (a : σ) → τ)) {embDomain e x}) ⋯) b →
      b ≠ x → Eq.{u_4 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simpa using fun _ h h' ↦ by simp [← embDomain_eq_mapDomain, embDomain_inj, h'] at h
-- 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
x : τ →₀ ℕ
h' : x ∉ Set.range (mapDomain f)
⊢ Eq.{u_4 + 1} (α := R)
    ((coeff x : (a : MvPowerSeries τ R) → R)
        ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) p : MvPowerSeries τ R) :
      R)
    (0 : R)

Tactic:
simp [coeff_rename, Set.Finite.toFinset, Set.preimage_singleton_eq_empty.mpr h']

Premises used: Iff.mpr, Set.preimage_singleton_eq_empty, Set.Finite.toFinset, 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
r : R
⊢ Eq (α := MvPowerSeries τ R)
    ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) ((C : (a : R) → MvPowerSeries σ R) r) : MvPowerSeries τ R)
    ((C : (a : R) → MvPowerSeries τ R) r : MvPowerSeries τ R)

Tactic:
rename_monomial f 0 r

Premises used: Multiset.sum, Multiset.foldr, Function.update, Finsupp.mapDomain, Finsupp.sum, MvPowerSeries.rename_monomial, Multiset.zero, Finset.empty, Pi.single, dite, Multiset.ofList, OfNat.ofNat, List.foldr, Finset.sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : CommSemiring R
i : σ
⊢ Eq (α := MvPowerSeries τ R) ((rename f : (a : MvPowerSeries σ R) → MvPowerSeries τ R) (X i) : MvPowerSeries τ R)
    (X (f i) : MvPowerSeries τ R)

Tactic:
simpa using rename_monomial f (single i 1) 1

Premises used: MvPowerSeries.rename_monomial, OfNat.ofNat, Finsupp.single
-- 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 :
  ∀ (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)

Tactic:
ext y
-- 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)
    (∑ 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.{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:
simp only [coeff_rename]

Premises used: 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
p : MvPowerSeries σ R
y : γ →₀ ℕ
simp : ∀ (a : τ →₀ ℕ) (b : σ →₀ ℕ), mapDomain f b = a → (mapDomain (g ∘ f) b = y ↔ mapDomain g a = y)
⊢ ∀ (p : Prod.{u_2, u_1} (τ →₀ ℕ) (σ →₀ ℕ)),
    Membership.mem (γ := Finset (Prod.{u_2, u_1} (τ →₀ ℕ) (σ →₀ ℕ)))
        (Finset.image (fun (u : σ →₀ ℕ) ↦ (mapDomain f u, u)) (Set.Finite.toFinset (s := mapDomain (g ∘ f) ⁻¹' {y}) ⋯))
        p ↔
      p.1 ∈ Set.Finite.toFinset (s := mapDomain g ⁻¹' {y}) ⋯ ∧ p.2 ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1}) ⋯

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 : γ →₀ ℕ
⊢ ∀ (a : τ →₀ ℕ) (b : σ →₀ ℕ), mapDomain f b = a → (mapDomain (g ∘ f) b = y ↔ mapDomain g a = y)

Tactic:
grind [mapDomain_comp]

Premises used: Finsupp.mapDomain_comp