awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : Mul M
e₁ : R ≃+ S
e₂ : S ≃+ T
h :
  ∀ (x : R[M]) (m : M),
    Eq.{u_5 + 1} (α := T) ((((mapAddEquiv M (e₁.trans e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
      ((((AddEquiv.trans (mapAddEquiv M e₁) (mapAddEquiv M e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
⊢ Eq (α := R[M] ≃+ T[M]) (mapAddEquiv M (e₁.trans e₂)) (AddEquiv.trans (mapAddEquiv M e₁) (mapAddEquiv M e₂))

Tactic:
ext
-- 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
inst_3 : Mul M
e₁ : R ≃+ S
e₂ : S ≃+ T
x : R[M]
m : M
⊢ Eq.{u_5 + 1} (α := T) ((((mapAddEquiv M (e₁.trans e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
    ((((AddEquiv.trans (mapAddEquiv M e₁) (mapAddEquiv M e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)

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
f : R →+* S
x y : R[M]
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) (x * y) : (a : M) → S) m : S)
      ((HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y) : (a : M) → S) m : S)
⊢ map (↑f : R →+ S) (x * y) = HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y)

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
inst_2 : Mul M
f : R →+* S
x y : R[M]
m : M
hfg :
  Eq.{u_4 + 1} (α := S)
    ((f : (a : R) → S)
        (sum x fun (a₁ : M) (b : R) ↦
          sum y fun (a₁_1 : M) (b_1 : R) ↦ (coeff (single (a₁ * a₁_1) (b * b_1)) : (a : M) → R) m) :
      S)
    ((sum (map (↑f : R →+ S) x) fun (m₁ : M) (r₁ : S) ↦
            sum (map (↑f : R →+ S) y) fun (m₂ : M) (r₂ : S) ↦ single (m₁ * m₂) (r₁ * r₂) :
          (a : M) → S)
        m :
      S)
⊢ Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) (x * y) : (a : M) → S) m : S)
    ((HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y) : (a : M) → S) m : S)

Tactic:
simp [mul_def]

Premises used: MonoidAlgebra.mul_def
-- 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
f : R →+* S
x y : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := S)
    ((f : (a : R) → S)
        (sum x fun (a₁ : M) (b : R) ↦
          sum y fun (a₁_1 : M) (b_1 : R) ↦ (coeff (single (a₁ * a₁_1) (b * b_1)) : (a : M) → R) m) :
      S)
    ((sum (map (↑f : R →+ S) x) fun (m₁ : M) (r₁ : S) ↦
            sum (map (↑f : R →+ S) y) fun (m₂ : M) (r₂ : S) ↦ single (m₁ * m₂) (r₁ * r₂) :
          (a : M) → S)
        m :
      S)

Tactic:
simp [MonoidAlgebra, sum_mapRange_index, map_finsuppSum, single_apply, apply_ite, map,
    coeff, ofCoeff]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, apply_ite, MonoidAlgebra.map, map_finsuppSum, MonoidAlgebra, Finsupp.sum_mapRange_index, MonoidAlgebra.single_apply
-- 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
f : R →+* S
x y : R[M]
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) (x * y) : (a : M) → S) m : S)
      ((HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y) : (a : M) → S) m : S)
hfg₁ :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := S)
      ((f : (a : R) → S)
          (sum x fun (a₁ : M) (b : R) ↦
            sum y fun (a₁_1 : M) (b_1 : R) ↦ (coeff (single (a₁ * a₁_1) (b * b_1)) : (a : M) → R) m) :
        S)
      ((sum (map (↑f : R →+ S) x) fun (m₁ : M) (r₁ : S) ↦
              sum (map (↑f : R →+ S) y) fun (m₂ : M) (r₂ : S) ↦ single (m₁ * m₂) (r₁ * r₂) :
            (a : M) → S)
          m :
        S)
⊢ map (↑f : R →+ S) (x * y) = HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y)

Tactic:
classical
  ext
  simp [mul_def]
  simp [MonoidAlgebra, sum_mapRange_index, map_finsuppSum, single_apply, apply_ite, map,
    coeff, ofCoeff]

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.mul_def, MonoidAlgebra.ofCoeff, apply_ite, MonoidAlgebra.map, map_finsuppSum, MonoidAlgebra, Finsupp.sum_mapRange_index, MonoidAlgebra.single_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
h₁ :
  ∀ (r : R) (m : M),
    Eq.{u_3 + 1} (α := R)
      ((((mapDomainRingHom R (MonoidHom.id M) : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)
      ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)
h_of :
  ∀ (m m_1 : M),
    Eq.{u_3 + 1} (α := R)
      ((((mapDomainRingHom R (MonoidHom.id M) : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : R)
      ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : R)
⊢ Eq (α := R[M] →+* R[M]) (mapDomainRingHom R (MonoidHom.id M)) (RingHom.id R[M])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
r : R
m : M
⊢ Eq.{u_3 + 1} (α := R)
    ((((mapDomainRingHom R (MonoidHom.id M) : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)
    ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
m m_1 : M
⊢ Eq.{u_3 + 1} (α := R)
    ((((mapDomainRingHom R (MonoidHom.id M) : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : R)
    ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : 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 : Monoid M
inst_2 : Monoid N
inst_3 : Monoid O
f : N →* O
g : M →* N
h₁ :
  ∀ (r : R) (m : O),
    Eq.{u_3 + 1} (α := R)
      ((((mapDomainRingHom R (f.comp g) : (a : R[M]) → R[O]) (single 1 r) : R[O]) : (a : O) → R) m : R)
      ((((RingHom.comp (mapDomainRingHom R f) (mapDomainRingHom R g) : (a : R[M]) → R[O]) (single 1 r) : R[O]) :
            (a : O) → R)
          m :
        R)
h_of :
  ∀ (m : M) (m_1 : O),
    Eq.{u_3 + 1} (α := R)
      ((((mapDomainRingHom R (f.comp g) : (a : R[M]) → R[O]) (single m 1) : R[O]) : (a : O) → R) m_1 : R)
      ((((RingHom.comp (mapDomainRingHom R f) (mapDomainRingHom R g) : (a : R[M]) → R[O]) (single m 1) : R[O]) :
            (a : O) → R)
          m_1 :
        R)
⊢ Eq (α := R[M] →+* R[O]) (mapDomainRingHom R (f.comp g)) (RingHom.comp (mapDomainRingHom R f) (mapDomainRingHom 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 : Monoid M
inst_2 : Monoid N
inst_3 : Monoid O
f : N →* O
g : M →* N
r : R
m : O
⊢ Eq.{u_3 + 1} (α := R)
    ((((mapDomainRingHom R (f.comp g) : (a : R[M]) → R[O]) (single 1 r) : R[O]) : (a : O) → R) m : R)
    ((((RingHom.comp (mapDomainRingHom R f) (mapDomainRingHom R g) : (a : R[M]) → R[O]) (single 1 r) : R[O]) :
          (a : O) → 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 : Monoid M
inst_2 : Monoid N
inst_3 : Monoid O
f : N →* O
g : M →* N
m : M
m_1 : O
⊢ Eq.{u_3 + 1} (α := R)
    ((((mapDomainRingHom R (f.comp g) : (a : R[M]) → R[O]) (single m 1) : R[O]) : (a : O) → R) m_1 : R)
    ((((RingHom.comp (mapDomainRingHom R f) (mapDomainRingHom R g) : (a : R[M]) → R[O]) (single m 1) : R[O]) :
          (a : O) → R)
        m_1 :
      R)

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 : Monoid M
f : R →+* S
hfg : ∀ (m : M), Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) 1 : (a : M) → S) m : S) ((1 : (a : M) → S) m : S)
⊢ Eq (α := S[M]) (map (↑f : R →+ S) 1) 1

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
inst_2 : Monoid M
f : R →+* S
m : M
⊢ Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) 1 : (a : M) → S) m : S) ((1 : (a : M) → S) m : S)

Tactic:
simp [one_def]

Premises used: MonoidAlgebra.one_def
-- 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 : Monoid M
f : R →+* S
⊢ Eq (α := (a : R[M]) → S[M]) (⇑(mapRingHom M f) : (a : R[M]) → S[M]) (map (↑f : R →+ S))

Tactic:
rfl

Premises used: MonoidAlgebra.ofCoeff, Finsupp.onFinset, MonoidAlgebra.map, Finsupp.mapRange, rfl
-- 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 : Monoid M
f : R →+* S
x : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := S) ((((mapRingHom M f : (a : R[M]) → S[M]) x : S[M]) : (a : M) → S) m : S)
    ((f : (a : R) → S) ((x : (a : M) → R) m : R) : S)

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

Premises used: MonoidAlgebra.coeff, MonoidAlgebra.ofCoeff, MonoidAlgebra.map, MonoidAlgebra.mapRingHom
-- 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 : Monoid M
f : R →+* S
a : M
b : R
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := S) ((((mapRingHom M f : (a : R[M]) → S[M]) (single a b) : S[M]) : (a : M) → S) m : S)
      (((single a ((f : (a : R) → S) b) : S[M]) : (a : M) → S) m : S)
⊢ Eq (α := S[M]) ((mapRingHom M f : (a : R[M]) → S[M]) (single a b) : S[M]) (single a ((f : (a : R) → S) b) : S[M])

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
inst_2 : Monoid M
f : R →+* S
a : M
b : R
m : M
⊢ Eq.{u_4 + 1} (α := S) ((((mapRingHom M f : (a : R[M]) → S[M]) (single a b) : S[M]) : (a : M) → S) m : S)
    (((single a ((f : (a : R) → S) b) : S[M]) : (a : M) → S) m : S)

Tactic:
simp [single_apply, apply_ite f]

Premises used: apply_ite, MonoidAlgebra.single_apply, DFunLike.coe
-- 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 : Monoid M
f : R →+* S
a : M
b : R
hfg hfg₁ :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := S) ((((mapRingHom M f : (a : R[M]) → S[M]) (single a b) : S[M]) : (a : M) → S) m : S)
      (((single a ((f : (a : R) → S) b) : S[M]) : (a : M) → S) m : S)
⊢ Eq (α := S[M]) ((mapRingHom M f : (a : R[M]) → S[M]) (single a b) : S[M]) (single a ((f : (a : R) → S) b) : S[M])

Tactic:
classical ext; simp [single_apply, apply_ite f]

Premises used: apply_ite, MonoidAlgebra.single_apply, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
h₁ :
  ∀ (r : R) (m : M),
    Eq.{u_3 + 1} (α := R)
      ((((mapRingHom M (RingHom.id R) : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)
      ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)
h_of :
  ∀ (m m_1 : M),
    Eq.{u_3 + 1} (α := R)
      ((((mapRingHom M (RingHom.id R) : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : R)
      ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : R)
⊢ Eq (α := R[M] →+* R[M]) (mapRingHom M (RingHom.id R)) (RingHom.id R[M])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
r : R
m : M
⊢ Eq.{u_3 + 1} (α := R) ((((mapRingHom M (RingHom.id R) : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)
    ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M]) : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
m m_1 : M
⊢ Eq.{u_3 + 1} (α := R)
    ((((mapRingHom M (RingHom.id R) : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : R)
    ((((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M]) : (a : M) → R) m_1 : R)

Tactic:
simp
-- 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
inst_3 : Monoid M
f : S →+* T
g : R →+* S
h₁ :
  ∀ (r : R) (m : M),
    Eq.{u_5 + 1} (α := T) ((((mapRingHom M (f.comp g) : (a : R[M]) → T[M]) (single 1 r) : T[M]) : (a : M) → T) m : T)
      ((((RingHom.comp (mapRingHom M f) (mapRingHom M g) : (a : R[M]) → T[M]) (single 1 r) : T[M]) : (a : M) → T) m : T)
h_of :
  ∀ (m m_1 : M),
    Eq.{u_5 + 1} (α := T) ((((mapRingHom M (f.comp g) : (a : R[M]) → T[M]) (single m 1) : T[M]) : (a : M) → T) m_1 : T)
      ((((RingHom.comp (mapRingHom M f) (mapRingHom M g) : (a : R[M]) → T[M]) (single m 1) : T[M]) : (a : M) → T) m_1 :
        T)
⊢ Eq (α := R[M] →+* T[M]) (mapRingHom M (f.comp g)) (RingHom.comp (mapRingHom M f) (mapRingHom M g))

Tactic:
ext
-- 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
inst_3 : Monoid M
f : S →+* T
g : R →+* S
r : R
m : M
⊢ Eq.{u_5 + 1} (α := T) ((((mapRingHom M (f.comp g) : (a : R[M]) → T[M]) (single 1 r) : T[M]) : (a : M) → T) m : T)
    ((((RingHom.comp (mapRingHom M f) (mapRingHom M g) : (a : R[M]) → T[M]) (single 1 r) : T[M]) : (a : M) → T) m : T)

Tactic:
simp
-- 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
inst_3 : Monoid M
f : S →+* T
g : R →+* S
m m_1 : M
⊢ Eq.{u_5 + 1} (α := T) ((((mapRingHom M (f.comp g) : (a : R[M]) → T[M]) (single m 1) : T[M]) : (a : M) → T) m_1 : T)
    ((((RingHom.comp (mapRingHom M f) (mapRingHom M g) : (a : R[M]) → T[M]) (single m 1) : T[M]) : (a : M) → T) m_1 : T)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
S : Type u_4
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : Monoid M
inst_3 : Monoid N
f : R →+* S
g : M →* N
⊢ RingHom.comp (mapRingHom N f) (mapDomainRingHom R g) = RingHom.comp (mapDomainRingHom S g) (mapRingHom M f)

Tactic:
aesop
-- 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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
h₁ :
  ∀ (r : R),
    Eq (α := R[N])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e : M →* N))
              (mapDomainRingHom R (↑e.symm : N →* M)) :
            (a : R[N]) → R[N])
          (single 1 r) :
        R[N])
      ((RingHom.id R[N] : (a : R[N]) → R[N]) (single 1 r) : R[N])
h_of :
  ∀ (m : N),
    Eq (α := R[N])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e : M →* N))
              (mapDomainRingHom R (↑e.symm : N →* M)) :
            (a : R[N]) → R[N])
          (single m 1) :
        R[N])
      ((RingHom.id R[N] : (a : R[N]) → R[N]) (single m 1) : R[N])
⊢ Eq (α := R[N] →+* R[N])
    (@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e : M →* N))
      (mapDomainRingHom R (↑e.symm : N →* M)))
    (RingHom.id R[N])

Tactic:
apply MonoidAlgebra.ringHom_ext

Premises used: MonoidAlgebra.ringHom_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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
⊢ ∀ (r : R),
    Eq (α := R[N])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e : M →* N))
              (mapDomainRingHom R (↑e.symm : N →* M)) :
            (a : R[N]) → R[N])
          (single 1 r) :
        R[N])
      ((RingHom.id R[N] : (a : R[N]) → R[N]) (single 1 r) : R[N])

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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
⊢ ∀ (m : N),
    Eq (α := R[N])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e : M →* N))
              (mapDomainRingHom R (↑e.symm : N →* M)) :
            (a : R[N]) → R[N])
          (single m 1) :
        R[N])
      ((RingHom.id R[N] : (a : R[N]) → R[N]) (single m 1) : R[N])

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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
h₁ :
  ∀ (r : R),
    Eq (α := R[M])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e.symm : N →* M))
              (mapDomainRingHom R (↑e : M →* N)) :
            (a : R[M]) → R[M])
          (single 1 r) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M])
h_of :
  ∀ (m : M),
    Eq (α := R[M])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e.symm : N →* M))
              (mapDomainRingHom R (↑e : M →* N)) :
            (a : R[M]) → R[M])
          (single m 1) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M])
⊢ Eq (α := R[M] →+* R[M])
    (@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e.symm : N →* M))
      (mapDomainRingHom R (↑e : M →* N)))
    (RingHom.id R[M])

Tactic:
apply MonoidAlgebra.ringHom_ext

Premises used: MonoidAlgebra.ringHom_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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
⊢ ∀ (r : R),
    Eq (α := R[M])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e.symm : N →* M))
              (mapDomainRingHom R (↑e : M →* N)) :
            (a : R[M]) → R[M])
          (single 1 r) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M])

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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
⊢ ∀ (m : M),
    Eq (α := R[M])
      ((@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e.symm : N →* M))
              (mapDomainRingHom R (↑e : M →* N)) :
            (a : R[M]) → R[M])
          (single m 1) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single m 1) : R[M])

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 : Monoid M
inst_2 : Monoid N
e : M ≃* N
x : R[M]
n : N
⊢ Eq.{u_3 + 1} (α := R) ((((mapDomainRingEquiv 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:
mapDomainAddEquiv_apply ..

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

Tactic:
simp [mapDomainRingEquiv]

Premises used: MonoidAlgebra.mapDomainRingEquiv
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
e : M ≃* N
⊢ Eq (α := R[M] →+* R[N]) (RingEquiv.toRingHom (mapDomainRingEquiv R e)) (mapDomainRingHom R (↑e : M →* N))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, MulEquiv.toMonoidHom, RingEquiv.toRingHom, MonoidAlgebra.mapDomainRingHom, Finset.sum, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.MapDomain
Goal:
R : Type u_3
M : Type u_6
N : Type u_7
inst : Semiring R
inst_1 : Monoid M
inst_2 : Monoid N
e : M ≃* N
⊢ Eq (α := R[N] ≃+* R[M]) (RingEquiv.symm (mapDomainRingEquiv R e)) (mapDomainRingEquiv R e.symm)

Tactic:
rfl

Premises used: RingEquiv.ofRingHom, MonoidAlgebra.mapDomainRingEquiv, Equiv.symm, MulEquiv.symm, RingEquiv.symm, rfl
-- 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 : Monoid M
inst_2 : Monoid N
inst_3 : Monoid O
e₁ : M ≃* N
e₂ : N ≃* O
h :
  ∀ (x : R[M]) (m : O),
    Eq.{u_3 + 1} (α := R) ((((mapDomainRingEquiv R (e₁.trans e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
      ((((RingEquiv.trans (mapDomainRingEquiv R e₁) (mapDomainRingEquiv R e₂) : (a : R[M]) → R[O]) x : R[O]) :
            (a : O) → R)
          m :
        R)
⊢ Eq (α := R[M] ≃+* R[O]) (mapDomainRingEquiv R (e₁.trans e₂))
    (RingEquiv.trans (mapDomainRingEquiv R e₁) (mapDomainRingEquiv 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 : Monoid M
inst_2 : Monoid N
inst_3 : Monoid O
e₁ : M ≃* N
e₂ : N ≃* O
x : R[M]
m : O
⊢ Eq.{u_3 + 1} (α := R) ((((mapDomainRingEquiv R (e₁.trans e₂) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
    ((((RingEquiv.trans (mapDomainRingEquiv R e₁) (mapDomainRingEquiv 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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : R ≃+* S
h₁ :
  ∀ (r : S),
    Eq (α := S[M])
      ((RingHom.comp (β := R[M]) (mapRingHom M (↑e : R →+* S)) (mapRingHom M (↑e.symm : S →+* R)) : (a : S[M]) → S[M])
          (single 1 r) :
        S[M])
      ((RingHom.id S[M] : (a : S[M]) → S[M]) (single 1 r) : S[M])
h_of :
  ∀ (m : M),
    Eq (α := S[M])
      ((RingHom.comp (β := R[M]) (mapRingHom M (↑e : R →+* S)) (mapRingHom M (↑e.symm : S →+* R)) : (a : S[M]) → S[M])
          (single m 1) :
        S[M])
      ((RingHom.id S[M] : (a : S[M]) → S[M]) (single m 1) : S[M])
⊢ Eq (α := S[M] →+* S[M]) (RingHom.comp (β := R[M]) (mapRingHom M (↑e : R →+* S)) (mapRingHom M (↑e.symm : S →+* R)))
    (RingHom.id S[M])

Tactic:
apply MonoidAlgebra.ringHom_ext

Premises used: MonoidAlgebra.ringHom_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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : R ≃+* S
⊢ ∀ (r : S),
    Eq (α := S[M])
      ((RingHom.comp (β := R[M]) (mapRingHom M (↑e : R →+* S)) (mapRingHom M (↑e.symm : S →+* R)) : (a : S[M]) → S[M])
          (single 1 r) :
        S[M])
      ((RingHom.id S[M] : (a : S[M]) → S[M]) (single 1 r) : S[M])

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 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : R ≃+* S
⊢ ∀ (m : M),
    Eq (α := S[M])
      ((RingHom.comp (β := R[M]) (mapRingHom M (↑e : R →+* S)) (mapRingHom M (↑e.symm : S →+* R)) : (a : S[M]) → S[M])
          (single m 1) :
        S[M])
      ((RingHom.id S[M] : (a : S[M]) → S[M]) (single m 1) : S[M])

Tactic:
simp