awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
x y : R[M]
⊢ map f (x + y) = map f x + map f y

Tactic:
mapRange_add (hf := f.map_zero) f.map_add ..

Premises used: MonoidAlgebra.ofCoeff, Finsupp.onFinset, MonoidAlgebra.map, MonoidAlgebra, Finsupp.mapRange_add, Finsupp.mapRange, AddMonoidHom.map_add
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
s : Finset ι
x : ι → R[M]
⊢ Eq (α := S[M]) (map f (∑ i ∈ s, x i)) (∑ i ∈ s, map f (x i))

Tactic:
mapRange_finsetSum ..

Premises used: MonoidAlgebra.ofCoeff, Finsupp.mapRange_finsetSum, Finsupp.onFinset, MonoidAlgebra.map, MonoidAlgebra, Finsupp.mapRange
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
r : R
m : M
⊢ map f (single m r) = single m ((f : (a : R) → S) r)

Tactic:
mapRange_single (hf := f.map_zero)

Premises used: MonoidAlgebra.ofCoeff, Finsupp.onFinset, MonoidAlgebra.map, MonoidAlgebra, Finsupp.mapRange, Finsupp.mapRange_single
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
x : R[M]
⊢ map (AddMonoidHom.id R) x = x

Tactic:
simp [map, coeff, ofCoeff]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.map
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : S →+ T
g : R →+ S
x : R[M]
⊢ map f (map g x) = map (f.comp g) x

Tactic:
simp [map, coeff, ofCoeff]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.map
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
simp_rw :
  Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x)))
simp_rw₁ :
  Eq (α := Set (M →₀ S)) (Set.image (α := S[M]) (⇑coeffEquiv : (a : S[M]) → M →₀ S) (Set.range (map f)))
    (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x))
simp_rw₂ :
  Eq (α := Set (M →₀ S)) (Set.range fun (x : R[M]) ↦ (coeffEquiv : (a : S[M]) → M →₀ S) (map f x))
    (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ ((coeffEquiv : (a : R[M]) → M →₀ R) x))
simp_rw₃ :
  Eq (α := Set (M →₀ S)) (Set.range fun (x : R[M]) ↦ (map f x).coeff)
    (Set.range fun (x : R[M]) ↦ mapRange (⇑f : (a : R) → S) ⋯ x.coeff)
⊢ Eq (α := Set S[M]) (Set.range (map f))
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range (ι := R[M]) (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R))))

Tactic:
simp_rw [comp_def, Equiv.eq_preimage_iff_image_eq, ← Set.range_comp', coeffEquiv_apply,
        coeff_map]

Premises used: Equiv.eq_preimage_iff_image_eq, Function.comp_def, MonoidAlgebra.coeff_map, MonoidAlgebra.coeffEquiv_apply, Set.range_comp'
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
⊢ Eq (α := Set S[M])
    (Set.preimage (β := M →₀ S) (⇑coeffEquiv : (a : S[M]) → M →₀ S)
      (Set.range (ι := R[M]) (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R))))
    {x : S[M] |
      ∀ (i : M),
        Membership.mem.{u_4, u_4} (α := S) (γ := Set S) (Set.range.{u_4, u_3 + 1} (ι := R) (⇑f : (a : R) → S))
          ((x.coeff : (a : M) → S) i : S)}

Tactic:
simp [Finsupp.range_mapRange]

Premises used: Finsupp.range_mapRange
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  ∀ (x : R[M]) (m : M),
    Eq.{u_4 + 1} (α := S) ((map f x : (a : M) → S) m : S)
      ((comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
              (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)) x :
            (a : M) → S)
          m :
        S)
⊢ Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := S) ((map f x : (a : M) → S) m : S)
    ((comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
            (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)) x :
          (a : M) → S)
        m :
      S)

Tactic:
simp [ofCoeff_mapRange]

Premises used: MonoidAlgebra.ofCoeff_mapRange
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))

Tactic:
have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this :
  Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))
⊢ Injective (α := R[M]) (map f)

Tactic:
simpa [this] using mapRange_injective _ (map_zero f) he

Premises used: map_zero, Finsupp.mapRange_injective
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  ∀ (x : R[M]) (m : M),
    Eq.{u_4 + 1} (α := S) ((map f x : (a : M) → S) m : S)
      ((comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
              (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)) x :
            (a : M) → S)
          m :
        S)
⊢ Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := S) ((map f x : (a : M) → S) m : S)
    ((comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
            (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)) x :
          (a : M) → S)
        m :
      S)

Tactic:
simp [ofCoeff_mapRange]

Premises used: MonoidAlgebra.ofCoeff_mapRange
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))

Tactic:
have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R →+ S
he : Surjective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this :
  Eq (α := (x : R[M]) → S[M]) (map f)
    (comp (β := M →₀ S) (⇑(Equiv.symm coeffEquiv) : (a : M →₀ S) → S[M])
      (comp (β := M →₀ R) (mapRange (⇑f : (a : R) → S) ⋯) (⇑coeffEquiv : (a : R[M]) → M →₀ R)))
⊢ Surjective (α := R[M]) (map f)

Tactic:
simpa [this] using mapRange_surjective _ (map_zero f) he

Premises used: map_zero, Finsupp.mapRange_surjective
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
hf : Injective f
x : R[N]
⊢ (comapDomain f hf x).coeff = Finsupp.comapDomain f x.coeff ⋯

Tactic:
simp [comapDomain]

Premises used: MonoidAlgebra.comapDomain
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
hf : Injective f
⊢ Eq (α := R[M]) (comapDomain f hf 0) 0

Tactic:
simp [comapDomain]

Premises used: MonoidAlgebra.comapDomain
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
hf : Injective f
x y : R[N]
⊢ comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

Tactic:
simp [comapDomain, comapDomain_add_of_injective hf]

Premises used: MonoidAlgebra.comapDomain, Finsupp.comapDomain_add_of_injective
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
r : R
n : N
hn : n ∉ Set.range f
hf : Injective f
⊢ Eq (α := R[M]) (comapDomain f hf (single n r)) 0

Tactic:
simp [comapDomain, coeff, single, *]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.comapDomain, MonoidAlgebra.single
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f_1 : M → N
a : M
r : R
f : M → N
hf : Injective f
⊢ Eq (α := R[M]) (comapDomain f hf 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f_1 : M → N
a : M
r : R
f : M → N
hf : Injective f
⊢ ∀ (x y : R[N]), comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
hf : Injective f
m : M
r : R
⊢ Eq (α := R[M]) (comapDomain f hf (single (f m) r)) (single m r)

Tactic:
simp [comapDomain, single, coeff, ofCoeff]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.comapDomain, MonoidAlgebra.single
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
f : M → N
x : R[N]
hx : (↑x.coeff.support : Set N) ⊆ Set.range f
hf : Injective f
⊢ mapDomain f (comapDomain f hf x) = x

Tactic:
Finsupp.mapDomain_comapDomain _ hf _ hx

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, Finsupp.mapDomain_comapDomain, MonoidAlgebra, MonoidAlgebra.comapDomain, Finsupp.comapDomain
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
F : Type u_2
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
f : F
x y : R[M]
⊢ mapDomain (⇑f : (a : M) → N) (x * y) =
    HMul.hMul (α := R[N]) (mapDomain (⇑f : (a : M) → N) x) (mapDomain (⇑f : (a : M) → N) y)

Tactic:
simp [mul_def, mapDomain_sum, add_mul, mul_add, sum_mapDomain_index]

Premises used: add_mul, MonoidAlgebra.mul_def, Finsupp.sum_mapDomain_index, mul_add, MonoidAlgebra.mapDomain_sum
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Mul M
a :
  ∀ (x : R[M]) (m : M),
    Eq.{u_3 + 1} (α := R)
      ((((mapDomainNonUnitalRingHom R (MulHom.id M) : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)
      ((((NonUnitalRingHom.id R[M] : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)
⊢ Eq (α := R[M] →ₙ+* R[M]) (mapDomainNonUnitalRingHom R (MulHom.id M)) (NonUnitalRingHom.id R[M])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Mul M
x : R[M]
m : M
⊢ Eq.{u_3 + 1} (α := R)
    ((((mapDomainNonUnitalRingHom R (MulHom.id M) : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)
    ((((NonUnitalRingHom.id R[M] : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul O
f : N →ₙ* O
g : M →ₙ* N
a :
  ∀ (x : R[M]) (m : O),
    Eq.{u_3 + 1} (α := R)
      ((((mapDomainNonUnitalRingHom R (f.comp g) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
      ((((NonUnitalRingHom.comp (mapDomainNonUnitalRingHom R f) (mapDomainNonUnitalRingHom R g) : (a : R[M]) → R[O]) x :
              R[O]) :
            (a : O) → R)
          m :
        R)
⊢ Eq (α := R[M] →ₙ+* R[O]) (mapDomainNonUnitalRingHom R (f.comp g))
    (NonUnitalRingHom.comp (mapDomainNonUnitalRingHom R f) (mapDomainNonUnitalRingHom R g))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul O
f : N →ₙ* O
g : M →ₙ* N
x : R[M]
m : O
⊢ Eq.{u_3 + 1} (α := R) ((((mapDomainNonUnitalRingHom R (f.comp g) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
    ((((NonUnitalRingHom.comp (mapDomainNonUnitalRingHom R f) (mapDomainNonUnitalRingHom R g) : (a : R[M]) → R[O]) x :
            R[O]) :
          (a : O) → R)
        m :
      R)

Tactic:
simp [Finsupp.mapDomain_comp]

Premises used: Finsupp.mapDomain_comp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x : R[M]
hfg :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := R)
      (((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M]))
              ((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N])) x) :
            (a : M) → R)
          m :
        R)
      ((x : (a : M) → R) m : R)
⊢ (fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M]))
      ((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N])) x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x : R[M]
m : M
⊢ Eq.{u_3 + 1} (α := R)
    (((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M]))
            ((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N])) x) :
          (a : M) → R)
        m :
      R)
    ((x : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x : R[N]
hfg :
  ∀ (m : N),
    Eq.{u_3 + 1} (α := R)
      (((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N]))
              ((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M])) x) :
            (a : N) → R)
          m :
        R)
      ((x : (a : N) → R) m : R)
⊢ (fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N]))
      ((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M])) x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x : R[N]
m : N
⊢ Eq.{u_3 + 1} (α := R)
    (((fun (x : R[M]) ↦ (mapDomain (⇑e : (a : M) → N) x : R[N]))
            ((fun (x : R[N]) ↦ (mapDomain (⇑e.symm : (a : N) → M) x : R[M])) x) :
          (a : N) → R)
        m :
      R)
    ((x : (a : N) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x y : R[M]
hfg :
  ∀ (m : N),
    Eq.{u_3 + 1} (α := R) ((mapDomain (⇑e : (a : M) → N) (x + y) : (a : N) → R) m : R)
      ((HAdd.hAdd (α := R[N]) (mapDomain (⇑e : (a : M) → N) x) (mapDomain (⇑e : (a : M) → N) y) : (a : N) → R) m : R)
⊢ mapDomain (⇑e : (a : M) → N) (x + y) =
    HAdd.hAdd (α := R[N]) (mapDomain (⇑e : (a : M) → N) x) (mapDomain (⇑e : (a : M) → N) y)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : M ≃ N
x y : R[M]
m : N
⊢ Eq.{u_3 + 1} (α := R) ((mapDomain (⇑e : (a : M) → N) (x + y) : (a : N) → R) m : R)
    ((HAdd.hAdd (α := R[N]) (mapDomain (⇑e : (a : M) → N) x) (mapDomain (⇑e : (a : M) → N) y) : (a : N) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
e : M ≃ N
x : R[M]
n : N
⊢ Eq.{u_3 + 1} (α := R) ((((mapDomainAddEquiv R e : (a : R[M]) → R[N]) x : R[N]) : (a : N) → R) n : R)
    ((x : (a : M) → R) ((e.symm : (a : N) → M) n : M) : R)

Tactic:
simp [mapDomainAddEquiv]

Premises used: MonoidAlgebra.mapDomainAddEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
e : M ≃ N
r : R
m : M
⊢ Eq (α := R[N]) ((mapDomainAddEquiv R e : (a : R[M]) → R[N]) (single m r) : R[N])
    (single ((e : (a : M) → N) m) r : R[N])

Tactic:
simp [mapDomainAddEquiv]

Premises used: MonoidAlgebra.mapDomainAddEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
e : M ≃ N
⊢ Eq (α := R[N] ≃+ R[M]) (AddEquiv.symm (mapDomainAddEquiv R e)) (mapDomainAddEquiv R e.symm)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, MonoidAlgebra.mapDomainAddEquiv, Finsupp.sum, Equiv.symm, Finset.sum, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul O
e₁ : M ≃ N
e₂ : N ≃ O
h :
  ∀ (x : R[M]) (m : O),
    Eq.{u_3 + 1} (α := R) ((((mapDomainAddEquiv R (e₁.trans e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
      ((((AddEquiv.trans (mapDomainAddEquiv R e₁) (mapDomainAddEquiv R e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R)
          m :
        R)
⊢ Eq (α := R[M] ≃+ R[O]) (mapDomainAddEquiv R (e₁.trans e₂))
    (AddEquiv.trans (mapDomainAddEquiv R e₁) (mapDomainAddEquiv R e₂))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Mul M
inst_2 : Mul N
inst_3 : Mul O
e₁ : M ≃ N
e₂ : N ≃ O
x : R[M]
m : O
⊢ Eq.{u_3 + 1} (α := R) ((((mapDomainAddEquiv R (e₁.trans e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
    ((((AddEquiv.trans (mapDomainAddEquiv R e₁) (mapDomainAddEquiv R e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R)
        m :
      R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : R ≃+ S
x : R[M]
hfg :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := R) ((map (↑e.symm : S →+ R) (map (↑e : R →+ S) x) : (a : M) → R) m : R) ((x : (a : M) → R) m : R)
⊢ map (↑e.symm : S →+ R) (map (↑e : R →+ S) x) = x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : R ≃+ S
x : R[M]
m : M
⊢ Eq.{u_3 + 1} (α := R) ((map (↑e.symm : S →+ R) (map (↑e : R →+ S) x) : (a : M) → R) m : R) ((x : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : R ≃+ S
x : S[M]
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := S) ((map (↑e : R →+ S) (map (↑e.symm : S →+ R) x) : (a : M) → S) m : S) ((x : (a : M) → S) m : S)
⊢ map (↑e : R →+ S) (map (↑e.symm : S →+ R) x) = x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : M → N
a : M
r : R
inst_3 : Mul M
inst_4 : Mul N
inst_5 : Mul O
inst_6 : FunLike F M N
inst_7 : MulHomClass F M N
e : R ≃+ S
x : S[M]
m : M
⊢ Eq.{u_4 + 1} (α := S) ((map (↑e : R →+ S) (map (↑e.symm : S →+ R) x) : (a : M) → S) m : S) ((x : (a : M) → S) m : S)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Mul M
e : R ≃+ S
x : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := S) ((((mapAddEquiv M e : (a : R[M]) → S[M]) x : S[M]) : (a : M) → S) m : S)
    ((e : (a : R) → S) ((x : (a : M) → R) m : R) : S)

Tactic:
simp [mapAddEquiv, map, coeff, ofCoeff]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.map, MonoidAlgebra.mapAddEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Mul M
e : R ≃+ S
r : R
m : M
⊢ Eq (α := S[M]) ((mapAddEquiv M e : (a : R[M]) → S[M]) (single m r) : S[M]) (single m ((e : (a : R) → S) r) : S[M])

Tactic:
simp [mapAddEquiv]

Premises used: MonoidAlgebra.mapAddEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : Mul M
e : R ≃+ S
⊢ Eq (α := S[M] ≃+ R[M]) (AddEquiv.symm (mapAddEquiv M e)) (mapAddEquiv M e.symm)

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, Finsupp.onFinset, MonoidAlgebra.map, MonoidAlgebra.mapAddEquiv, Equiv.symm, Finsupp.mapRange, rfl, AddEquiv.symm