awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
a : A[M]
⊢ r • a =
    HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) a
have hfg : ∀ (m : M),
  Eq.{u_4 + 1} (α := A) ((r • a : (a : M) → A) m : A)
    ((HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])
            a :
          (a : M) → A)
        m :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
a : A[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((r • a : (a : M) → A) m : A)
    ((HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])
            a :
          (a : M) → A)
        m :
      A)
have hfg : HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
  (HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) a : (a : M) → A) m
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
a : A[M]
m : M
⊢ HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
    (HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) a : (a : M) → A) m
have hfg : HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((a : (a : M) → A) m : A)
Tactic: rw [single_one_mul_apply, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
a : A[M]
m : M
hfg :
  HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((a : (a : M) → A) m : A)
⊢ HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
    (HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) a : (a : M) → A) m
have hfg₁ : HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((a : (a : M) → A) m : A) =
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((a : (a : M) → A) m : A)
Tactic: rw [single_one_mul_apply, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
⊢ Eq (α := A[M])
    (OneHom.toFun (↑(↑singleOneRingHom : A →* A[M]) : OneHom A A[M]) ((algebraMap R A : (a : R) → A) r) : A[M])
    ((algebraMap R A[M] : (a : R) → A[M]) r : A[M])
have hfg : ∀ (m : M),
  Eq.{u_4 + 1} (α := A)
    (((OneHom.toFun (↑(↑singleOneRingHom : A →* A[M]) : OneHom A A[M]) ((algebraMap R A : (a : R) → A) r) : A[M]) :
          (a : M) → A)
        m :
      A)
    ((((algebraMap R A[M] : (a : R) → A[M]) r : A[M]) : (a : M) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
m : M
⊢ Eq.{u_4 + 1} (α := A)
    (((OneHom.toFun (↑(↑singleOneRingHom : A →* A[M]) : OneHom A A[M]) ((algebraMap R A : (a : R) → A) r) : A[M]) :
          (a : M) → A)
        m :
      A)
    ((((algebraMap R A[M] : (a : R) → A[M]) r : A[M]) : (a : M) → A) m : A)
have hfg : Eq.{u_4 + 1} (α := A) (((single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
  ((((algebraMap R A[M] : (a : R) → A[M]) r : A[M]) : (a : M) → A) m : A)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
⊢ Eq (α := A[N][M]) (Equiv.toFun (RingEquiv.toEquiv curryRingEquiv) ((algebraMap R A[M × N] : (a : R) → A[M × N]) r))
    ((algebraMap R A[N][M] : (a : R) → A[N][M]) r)
have hfg : ∀ (m : M) (m_1 : N),
  Eq.{u_4 + 1} (α := A)
    ((((Equiv.toFun (RingEquiv.toEquiv curryRingEquiv) ((algebraMap R A[M × N] : (a : R) → A[M × N]) r) :
                (a : M) → A[N])
              m :
            A[N]) :
          (a : N) → A)
        m_1 :
      A)
    ((((((algebraMap R A[N][M] : (a : R) → A[N][M]) r : A[N][M]) : (a : M) → A[N]) m : A[N]) : (a : N) → A) m_1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
f : M →* A
⊢ (fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : M →* A))
      ((fun (F : M →* A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A)) f) =
    f
have h : ∀ (x : M),
  Eq.{u_4 + 1} (α := A)
    (((fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : M →* A))
            ((fun (F : M →* A) ↦ (liftNCAlgHom (Algebra.ofId R A) F sorry : R[M] →ₐ[R] A)) f) :
          (a : M) → A)
        x :
      A)
    ((f : (a : M) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
F : R[M] →ₐ[R] A
⊢ (fun (F : M →* A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A))
      ((fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : M →* A)) F) =
    F
have h : ∀ (x : M),
  Eq.{u_4 + 1} (α := A)
    ((MonoidHom.comp
            (↑((fun (F : M →* A) ↦ (liftNCAlgHom (Algebra.ofId R A) F sorry : R[M] →ₐ[R] A))
                  ((fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : M →* A)) F)) :
              R[M] →* A)
            (of R M) :
          (a : M) → A)
        x :
      A)
    ((MonoidHom.comp (↑F : R[M] →* A) (of R M) : (a : M) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : M →* A
a : M
b : R
⊢ (((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
have rw : (liftNC (↑(algebraMap R A) : R →+ A) (⇑F : (a : M) → A) : (a : R[M]) → A) (single a b) =
  HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : M →* A
a : M
b : R
rw :
  (liftNC (↑(algebraMap R A) : R →+ A) (⇑F : (a : M) → A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
⊢ (((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
have rw₁ : HMul.hMul (α := A) (β := A) (((↑(algebraMap R A) : R →+ A) : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
  HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : M →* A
a : M
b : R
rw :
  (liftNC (↑(algebraMap R A) : R →+ A) (⇑F : (a : M) → A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
rw₁ :
  HMul.hMul (α := A) (β := A) (((↑(algebraMap R A) : R →+ A) : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
⊢ (((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
have rw₂ : HMul.hMul (α := A) (β := A) (((↑(algebraMap R A) : R →+ A) : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A) ((F : (a : M) → A) a : A)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : M →* A
a : M
b : R
rw :
  (liftNC (↑(algebraMap R A) : R →+ A) (⇑F : (a : M) → A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
rw₁ :
  HMul.hMul (α := A) (β := A) (((↑(algebraMap R A) : R →+ A) : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
rw₂ :
  HMul.hMul (α := A) (β := A) (((↑(algebraMap R A) : R →+ A) : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A) ((F : (a : M) → A) a : A)
⊢ (((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) F : R[M] →ₐ[R] A) : (a : R[M]) → A) (single a b) =
    HSMul.hSMul (β := A) b ((F : (a : M) → A) a : A)
have rw₃ : HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A) ((F : (a : M) → A) a : A) =
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) b : A) ((F : (a : M) → A) a : A)
Tactic: rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
f : R[M]
| ((F : (a : R[M]) → A) f : A)
have rw : ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) (MonoidHom.comp (↑F : R[M] →* A) (of R M)) : R[M] →ₐ[R] A) :
      (a : R[M]) → A)
    f :
  A)
Tactic: rw [lift_unique' F]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
f : R[M]
| ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) (MonoidHom.comp (↑F : R[M] →* A) (of R M)) : R[M] →ₐ[R] A) :
        (a : R[M]) → A)
      f :
    A)
have simp : sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A)
Tactic: simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
f : R[M]
| ((F : (a : R[M]) → A) f : A)
have rw : sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A)
Tactic: rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
f : R[M]
⊢ Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
have conv_lhs : Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
  (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
Tactic: conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
F : R[M] →ₐ[R] A
f : R[M]
conv_lhs :
  Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
⊢ Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
have conv_lhs₁ : Eq.{u_4 + 1} (α := A) (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A))
  (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A))
Tactic: conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f : M →* A
x : R[M]
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) x : S[M]) :
      A)
    ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) x : A)
have zero : Eq.{u_4 + 1} (α := A)
  ((((lift S A M : (a : M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
      ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) 0) :
    A)
  ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) 0 : A)
Tactic: induction x using Finsupp.induction with
  | zero => simp
  | single_add a b f _ _ ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f : M →* A
x : R[M]
zero :
  Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) 0) :
      A)
    ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) 0 : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) x : S[M]) :
      A)
    ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) x : A)
have single_add : ∀ (a : M) (b : R) (f_1 : M →₀ R),
  a ∉ f_1.support →
    b ≠ 0 →
      ∀
        (ih :
          Eq.{u_4 + 1} (α := A)
            ((((lift S A M : (a : M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
                ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) f_1 : S[M]) :
              A)
            ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) f_1 : A)),
        Eq.{u_4 + 1} (α := A)
          ((((lift S A M : (a : M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
              ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) (Finsupp.single a b + f_1) : S[M]) :
            A)
          ((((lift R A M : (a : M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) (Finsupp.single a b + f_1) :
            A)
Tactic: induction x using Finsupp.induction with
  | zero => simp
  | single_add a b f _ _ ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
⊢ Eq (α := A[M] →ₐ[R] A[M]) (mapDomainAlgHom R A (MonoidHom.id M)) (AlgHom.id R A[M])
have H : ∀ (x : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((mapDomainAlgHom R A (MonoidHom.id M) : (a : A[M]) → A[M]) x : A[M]) : (a : M) → A) m : A)
    ((((AlgHom.id R A[M] : (a : A[M]) → A[M]) x : A[M]) : (a : M) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
f : M →* N
g : N →* O
⊢ Eq (α := A[M] →ₐ[R] A[O]) (mapDomainAlgHom R A (g.comp f))
    (AlgHom.comp (mapDomainAlgHom R A g) (mapDomainAlgHom R A f))
have H : ∀ (x : A[M]) (m : O),
  Eq.{u_4 + 1} (α := A) ((((mapDomainAlgHom R A (g.comp f) : (a : A[M]) → A[O]) x : A[O]) : (a : O) → A) m : A)
    ((((AlgHom.comp (mapDomainAlgHom R A g) (mapDomainAlgHom R A f) : (a : A[M]) → A[O]) x : A[O]) : (a : O) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
e : M ≃* N
x : R
⊢ Eq (α := A[N]) (Equiv.toFun (RingEquiv.toEquiv (mapDomainRingEquiv A e)) ((algebraMap R A[M] : (a : R) → A[M]) x))
    ((algebraMap R A[N] : (a : R) → A[N]) x)
have hfg : ∀ (m : N),
  Eq.{u_4 + 1} (α := A)
    ((Equiv.toFun (RingEquiv.toEquiv (mapDomainRingEquiv A e)) ((algebraMap R A[M] : (a : R) → A[M]) x) : (a : N) → A)
        m :
      A)
    ((((algebraMap R A[N] : (a : R) → A[N]) x : A[N]) : (a : N) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
e : M ≃* N
f : A[M]
⊢ support.{u_8, u_4} (M := A) ((domCongr R A e : (a : A[M]) → A[N]) f) = Finset.map (↑e : M ≃ N).toEmbedding f.support
have h : ∀ (a : N),
  Membership.mem (γ := Finset N) (support.{u_8, u_4} (M := A) ((domCongr R A e : (a : A[M]) → A[N]) f)) a ↔
    a ∈ Finset.map (↑e : M ≃ N).toEmbedding f.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
e : M ≃* N
m : M
⊢ Eq (α := A →ₗ[R] A[N]) (AlgEquiv.toLinearMap (domCongr R A e) ∘ₗ lsingle m) (lsingle ((e : (a : M) → N) m))
have h : ∀ (x : A) (m_1 : N),
  Eq.{u_4 + 1} (α := A)
    ((((AlgEquiv.toLinearMap (domCongr R A e) ∘ₗ lsingle m : (a : A) → A[N]) x : A[N]) : (a : N) → A) m_1 : A)
    (((((lsingle ((e : (a : M) → N) m) : A →ₗ[R] A[N]) : (a : A) → A[N]) x : A[N]) : (a : N) → A) m_1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) AlgEquiv.refl
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((domCongr R A (MulEquiv.refl M) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((AlgEquiv.refl : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
e : M ≃* N
f : N ≃* O
⊢ Eq (α := A[M] ≃ₐ[R] A[O]) (AlgEquiv.trans (domCongr R A e) (domCongr R A f)) (domCongr R A (e.trans f))
have h : ∀ (a : A[M]) (m : O),
  Eq.{u_4 + 1} (α := A)
    ((((AlgEquiv.trans (domCongr R A e) (domCongr R A f) : (a : A[M]) → A[O]) a : A[O]) : (a : O) → A) m : A)
    ((((domCongr R A (e.trans f) : (a : A[M]) → A[O]) a : A[O]) : (a : O) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A 1) 1
have rw : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) 1
Tactic: rw [MulAut.one_def, AlgEquiv.aut_one, domCongr_refl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
rw : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) 1
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A 1) 1
have rw₁ : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) AlgEquiv.refl
Tactic: rw [MulAut.one_def, AlgEquiv.aut_one, domCongr_refl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
rw : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) 1
rw₁ : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.refl M)) AlgEquiv.refl
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A 1) 1
have rw₂ : Eq (α := A[M] ≃ₐ[R] A[M]) AlgEquiv.refl AlgEquiv.refl
Tactic: rw [MulAut.one_def, AlgEquiv.aut_one, domCongr_refl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
x x_1 : MulAut M
⊢ domCongr R A (x * x_1) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1)
have rw : domCongr R A (MulEquiv.trans x_1 x) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1)
Tactic: rw [MulAut.mul_def, AlgEquiv.aut_mul, trans_domCongr_domCongr]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Monoid M
inst_6 : Monoid N
inst_7 : Monoid O
x x_1 : MulAut M
rw : domCongr R A (MulEquiv.trans x_1 x) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1)
⊢ domCongr R A (x * x_1) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1)
have rw₁ : Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A (MulEquiv.trans x_1 x)) (AlgEquiv.trans (domCongr R A x_1) (domCongr R A x))
Tactic: rw [MulAut.mul_def, AlgEquiv.aut_mul, trans_domCongr_domCongr]