awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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]
⊢ map (↑f : R →+ S) (x * y) = HMul.hMul (α := S[M]) (map (↑f : R →+ S) x) (map (↑f : R →+ S) y)
have 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)
Tactic: classical
  ext
  simp [mul_def]
  simp [MonoidAlgebra, sum_mapRange_index, map_finsuppSum, single_apply, apply_ite, map,
    coeff, ofCoeff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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)
have 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)
Tactic: classical
  ext
  simp [mul_def]
  simp [MonoidAlgebra, sum_mapRange_index, map_finsuppSum, single_apply, apply_ite, map,
    coeff, ofCoeff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
⊢ Eq (α := R[M] →+* R[M]) (mapDomainRingHom R (MonoidHom.id M)) (RingHom.id R[M])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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)
⊢ Eq (α := R[M] →+* R[M]) (mapDomainRingHom R (MonoidHom.id M)) (RingHom.id R[M])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ Eq (α := R[M] →+* R[O]) (mapDomainRingHom R (f.comp g)) (RingHom.comp (mapDomainRingHom R f) (mapDomainRingHom R g))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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)
⊢ Eq (α := R[M] →+* R[O]) (mapDomainRingHom R (f.comp g)) (RingHom.comp (mapDomainRingHom R f) (mapDomainRingHom R g))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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 (α := S[M]) (map (↑f : R →+ S) 1) 1
have hfg : ∀ (m : M), Eq.{u_4 + 1} (α := S) ((map (↑f : R →+ S) 1 : (a : M) → S) m : S) ((1 : (a : M) → S) m : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ 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])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ 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])
have 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)
Tactic: classical ext; simp [single_apply, apply_ite f]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
Goal:
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : Monoid M
⊢ Eq (α := R[M] →+* R[M]) (mapRingHom M (RingHom.id R)) (RingHom.id R[M])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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)
⊢ Eq (α := R[M] →+* R[M]) (mapRingHom M (RingHom.id R)) (RingHom.id R[M])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ Eq (α := R[M] →+* T[M]) (mapRingHom M (f.comp g)) (RingHom.comp (mapRingHom M f) (mapRingHom M g))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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)
⊢ Eq (α := R[M] →+* T[M]) (mapRingHom M (f.comp g)) (RingHom.comp (mapRingHom M f) (mapRingHom M g))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ Eq (α := R[N] →+* R[N])
    (@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e : M →* N))
      (mapDomainRingHom R (↑e.symm : N →* M)))
    (RingHom.id R[N])
have 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])
Tactic: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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])
⊢ Eq (α := R[N] →+* R[N])
    (@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e : M →* N))
      (mapDomainRingHom R (↑e.symm : N →* M)))
    (RingHom.id R[N])
have 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])
Tactic: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ Eq (α := R[M] →+* R[M])
    (@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e.symm : N →* M))
      (mapDomainRingHom R (↑e : M →* N)))
    (RingHom.id R[M])
have 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])
Tactic: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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])
⊢ Eq (α := R[M] →+* R[M])
    (@RingHom.comp _ _ _ _ nonAssocSemiring _ (mapDomainRingHom R (↑e.symm : N →* M))
      (mapDomainRingHom R (↑e : M →* N)))
    (RingHom.id R[M])
have 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])
Tactic: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ Eq (α := R[M] ≃+* R[O]) (mapDomainRingEquiv R (e₁.trans e₂))
    (RingEquiv.trans (mapDomainRingEquiv R e₁) (mapDomainRingEquiv R e₂))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ Eq (α := S[M] →+* S[M]) (RingHom.comp (β := R[M]) (mapRingHom M (↑e : R →+* S)) (mapRingHom M (↑e.symm : S →+* R)))
    (RingHom.id S[M])
have 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])
Tactic: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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])
⊢ Eq (α := S[M] →+* S[M]) (RingHom.comp (β := R[M]) (mapRingHom M (↑e : R →+* S)) (mapRingHom M (↑e.symm : S →+* R)))
    (RingHom.id S[M])
have 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])
Tactic: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
⊢ Eq (α := R[M] →+* R[M]) (RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)))
    (RingHom.id R[M])
have h₁ : ∀ (r : R),
  Eq (α := R[M])
    ((RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)) : (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: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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 : R),
    Eq (α := R[M])
      ((RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)) : (a : R[M]) → R[M])
          (single 1 r) :
        R[M])
      ((RingHom.id R[M] : (a : R[M]) → R[M]) (single 1 r) : R[M])
⊢ Eq (α := R[M] →+* R[M]) (RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)))
    (RingHom.id R[M])
have h_of : ∀ (m : M),
  Eq (α := R[M])
    ((RingHom.comp (β := S[M]) (mapRingHom M (↑e.symm : S →+* R)) (mapRingHom M (↑e : R →+* S)) : (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: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
e₁ : R ≃+* S
e₂ : S ≃+* T
⊢ Eq (α := R[M] ≃+* T[M]) (mapRingEquiv M (e₁.trans e₂)) (RingEquiv.trans (mapRingEquiv M e₁) (mapRingEquiv M e₂))
have h : ∀ (x : R[M]) (m : M),
  Eq.{u_5 + 1} (α := T) ((((mapRingEquiv M (e₁.trans e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
    ((((RingEquiv.trans (mapRingEquiv M e₁) (mapRingEquiv M e₂) : (a : R[M]) → T[M]) x : T[M]) : (a : M) → T) m : T)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x : k[G]
⊢ (fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
        (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
      ((fun (x : k[G]) ↦
          (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
            AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
        x) =
    x
have hfg : ∀ (m : G),
  Eq.{u_9 + 1} (α := k)
    (((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
              (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
            ((fun (x : k[G]) ↦
                (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
                  AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
              x) :
          (a : G) → k)
        m :
      k)
    ((x : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)
⊢ (fun (x : k[G]) ↦
        (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
          AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
      ((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
          (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
        x) =
    x
have hfg : ∀ (m : Multiplicative G),
  Eq.{u_9 + 1} (α := k)
    (((fun (x : k[G]) ↦
              (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x :
                AddMonoidAlgebra.{u_9, u_10} k (Multiplicative G)))
            ((fun (x : MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) ↦
                (MonoidAlgebra.mapDomain (⇑Multiplicative.toAdd : (a : Multiplicative G) → G) x : MonoidAlgebra k G))
              x) :
          (a : Multiplicative G) → k)
        m :
      k)
    ((x : (a : Multiplicative G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Add G
x y : k[G]
⊢ mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) (x * y) =
    HMul.hMul (α := MonoidAlgebra.{u_9, u_10} k (Multiplicative G))
      (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) x)
      (mapDomain (⇑Multiplicative.ofAdd : (a : G) → Multiplicative G) y)
have dsimp : mapDomain (fun (x : G) ↦ x) (x * y) =
  HMul.hMul (α := MonoidAlgebra.{u_9, u_10} k (Multiplicative G)) (mapDomain (fun (x : G) ↦ x) x)
    (mapDomain (fun (x : G) ↦ x) y)
Tactic: dsimp [Multiplicative.ofAdd]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Mul G
x : k[G]
⊢ (fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
        (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
      ((fun (x : k[G]) ↦
          (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
        x) =
    x
have hfg : ∀ (m : G),
  Eq.{u_9 + 1} (α := k)
    (((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
              (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
            ((fun (x : k[G]) ↦
                (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
              x) :
          (a : G) → k)
        m :
      k)
    ((x : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.MapDomain (goal)
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
k : Type u_9
G : Type u_10
inst : Semiring k
inst_1 : Mul G
x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)
⊢ (fun (x : k[G]) ↦ (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
      ((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
          (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
        x) =
    x
have hfg : ∀ (m : Additive G),
  Eq.{u_9 + 1} (α := k)
    (((fun (x : k[G]) ↦
              (mapDomain (⇑Additive.ofMul : (a : G) → Additive G) x : MonoidAlgebra.{u_9, u_10} k (Additive G)))
            ((fun (x : AddMonoidAlgebra.{u_9, u_10} k (Additive G)) ↦
                (AddMonoidAlgebra.mapDomain (⇑Additive.toMul : (a : Additive G) → G) x : AddMonoidAlgebra k G))
              x) :
          (a : Additive G) → k)
        m :
      k)
    ((x : (a : Additive G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
s : Set M
m : M
inst_2 : Nontrivial R
h :
  Membership.mem (α := R[M]) (γ := Submodule R R[M])
    (Submodule.span R (↑(Submonoid.closure ((⇑(of R M) : (a : M) → R[M]) '' s)) : Set R[M]))
    ((of R M : (a : M) → R[M]) m : R[M])
⊢ Membership.mem (γ := Submonoid M) (Submonoid.closure s) m
have h₁ : Membership.mem (α := R[M]) (γ := Submodule R R[M])
  (Submodule.span R (↑(Submonoid.map (F := M →* R[M]) (of R M) (Submonoid.closure s)) : Set R[M]))
  ((of R M : (a : M) → R[M]) m : R[M])
Tactic: rw [← MonoidHom.map_mclosure] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
⊢ (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (c • φ) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) φ : R)
have suffices : Eq (α := S[M] →+ R)
  (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
    ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
  (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
Tactic: suffices (liftNC (↑f) g).comp (smulAddHom S S[M] c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g) from
    DFunLike.congr_fun this φ