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 : 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)
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))
⊢ 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)) (domCongr R A (MulEquiv.trans x_1 x))
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
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
f : M →* N
⊢ Eq (α := R →+* A[N]) (RingHom.comp (mapDomainRingHom A f) (algebraMap R A[M])) (algebraMap R A[N])
have a : ∀ (x : R) (m : N),
  Eq.{u_4 + 1} (α := A)
    ((((RingHom.comp (mapDomainRingHom A f) (algebraMap R A[M]) : (a : R) → A[N]) x : A[N]) : (a : N) → A) m : A)
    (((((algebraMap R A[N] : 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
S : Type u_2
M : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Monoid M
f : R →+* S
⊢ Eq (α := R →+* S[M]) (RingHom.comp (mapRingHom M f) (algebraMap R R[M])) (RingHom.comp (algebraMap S S[M]) f)
have a : ∀ (x : R) (m : M),
  Eq.{u_2 + 1} (α := S)
    ((((RingHom.comp (mapRingHom M f) (algebraMap R R[M]) : (a : R) → S[M]) x : S[M]) : (a : M) → S) m : S)
    (((((RingHom.comp (algebraMap S S[M]) f : R →+* S[M]) : (a : R) → S[M]) x : S[M]) : (a : M) → S) m : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
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
f : A →ₐ[R] B
m : M
a : A
⊢ Eq (α := B[M]) ((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) (single m ((f : (a : A) → B) a) : B[M])
have hfg : ∀ (m_1 : M),
  Eq.{u_5 + 1} (α := B) ((((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) : (a : M) → B) m_1 : B)
    (((single m ((f : (a : A) → B) a) : B[M]) : (a : M) → B) m_1 : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
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
f : A →ₐ[R] B
m : M
a : A
⊢ Eq (α := B[M]) ((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) (single m ((f : (a : A) → B) a) : B[M])
have hfg : ∀ (m_1 : M),
  Eq.{u_5 + 1} (α := B) ((((mapAlgHom M f : (a : A[M]) → B[M]) (single m a) : B[M]) : (a : M) → B) m_1 : B)
    (((single m ((f : (a : A) → B) a) : B[M]) : (a : M) → B) m_1 : B)
Tactic: classical ext; simp [single_apply, apply_ite f]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
k : Type u_10
R : Type u_11
G : Type u_12
inst : CommSemiring k
inst_1 : Semiring R
inst_2 : Algebra k R
inst_3 : Monoid G
⊢ Eq (α := R[G] →ₐ[k] R[G]) (mapAlgHom G (AlgHom.id k R)) (AlgHom.id k R[G])
have H : ∀ (x : R[G]) (m : G),
  Eq.{u_11 + 1} (α := R) ((((mapAlgHom G (AlgHom.id k R) : (a : R[G]) → R[G]) x : R[G]) : (a : G) → R) m : R)
    ((((AlgHom.id k R[G] : (a : R[G]) → R[G]) x : R[G]) : (a : G) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
k : Type u_10
R : Type u_11
S : Type u_12
T : Type u_13
G : Type u_14
inst : CommSemiring k
inst_1 : Semiring R
inst_2 : Algebra k R
inst_3 : Semiring S
inst_4 : Algebra k S
inst_5 : Semiring T
inst_6 : Algebra k T
inst_7 : Monoid G
f : R →ₐ[k] S
g : S →ₐ[k] T
⊢ Eq (α := R[G] →ₐ[k] T[G]) (mapAlgHom G (g.comp f)) (AlgHom.comp (mapAlgHom G g) (mapAlgHom G f))
have H : ∀ (x : R[G]) (m : G),
  Eq.{u_13 + 1} (α := T) ((((mapAlgHom G (g.comp f) : (a : R[G]) → T[G]) x : T[G]) : (a : G) → T) m : T)
    ((((AlgHom.comp (mapAlgHom G g) (mapAlgHom G f) : (a : R[G]) → T[G]) x : T[G]) : (a : G) → T) m : T)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : Monoid M
e₁ : A ≃ₐ[R] B
e₂ : B ≃ₐ[R] C
⊢ Eq (α := A[M] ≃ₐ[R] C[M]) (mapAlgEquiv R M (e₁.trans e₂)) (AlgEquiv.trans (mapAlgEquiv R M e₁) (mapAlgEquiv R M e₂))
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_6 + 1} (α := C) ((((mapAlgEquiv R M (e₁.trans e₂) : (a : A[M]) → C[M]) a : C[M]) : (a : M) → C) m : C)
    ((((AlgEquiv.trans (mapAlgEquiv R M e₁) (mapAlgEquiv R M e₂) : (a : A[M]) → C[M]) a : C[M]) : (a : M) → C) m : C)
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 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M 1) 1
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M 1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((1 : (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
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 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Semiring C
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Monoid M
inst_9 : Monoid N
x y : A ≃ₐ[R] A
⊢ mapAlgEquiv R M (x * y) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M x) (mapAlgEquiv R M y)
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M (x * y) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M x) (mapAlgEquiv R M y) : (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
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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
⊢ (f : (a : V) → W) (c • v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) c : R[M]) ((f : (a : V) → W) v : W)
have refine_1 : (f : (a : V) → W) (HSMul.hSMul (α := R[M]) 0 v) =
  HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) 0) ((f : (a : V) → W) v : W)
Tactic: refine Finsupp.induction c ?_ ?_
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
refine_1 :
  (f : (a : V) → W) (HSMul.hSMul (α := R[M]) 0 v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) 0) ((f : (a : V) → W) v : W)
⊢ (f : (a : V) → W) (c • v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) c : R[M]) ((f : (a : V) → W) v : W)
have refine_2 : ∀ (a : M) (b : R) (f_1 : M →₀ R),
  a ∉ f_1.support →
    b ≠ 0 →
      (f : (a : V) → W) (f_1 • v) =
          HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) f_1 : R[M])
            ((f : (a : V) → W) v : W) →
        (f : (a : V) → W) ((Finsupp.single a b + f_1) • v) =
          HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) (Finsupp.single a b + f_1) : R[M])
            ((f : (a : V) → W) v : W)
Tactic: refine Finsupp.induction c ?_ ?_
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : r ≠ 0
w :
  (f : (a : V) → W) (c' • v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) c' : R[M]) ((f : (a : V) → W) v : W)
⊢ (f : (a : V) → W) ((Finsupp.single g r + c') • v) =
    HSMul.hSMul (α := R[M]) (β := W) ((RingHom.id R[M] : (a : R[M]) → R[M]) (Finsupp.single g r + c') : R[M])
      ((f : (a : V) → W) v : W)
have refine_2 : (f : (a : V) → W) ((Finsupp.single g r + c') • v) =
  HSMul.hSMul (β := W) (Finsupp.single g r + c') ((f : (a : V) → W) v : W)
Tactic: dsimp at *
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ (f : (a : V) → W) ((Finsupp.single g r + c') • v) =
    HSMul.hSMul (β := W) (Finsupp.single g r + c') ((f : (a : V) → W) v : W)
have refine_2 : HAdd.hAdd (α := W)
    ((f : (a : V) → W)
        (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
          (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
      W)
    (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
  HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
      (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
Tactic: simp only [add_smul, f.map_add, w, single_eq_algebraMap_mul_of, ← smul_smul]
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ HAdd.hAdd (α := W)
      ((f : (a : V) → W)
          (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
            (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
        W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
have refine_2 : HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
    (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
  HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
      (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
Tactic: rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2 :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ HAdd.hAdd (α := W)
      ((f : (a : V) → W)
          (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
            (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
        W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
have refine_2₁ : HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
    (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
  r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
Tactic: rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2 :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₁ :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ HAdd.hAdd (α := W)
      ((f : (a : V) → W)
          (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
            (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
        W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
have refine_2₂ : HSMul.hSMul (β := W) r ((f : (a : V) → W) (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
  r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
Tactic: rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2 :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₁ :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₂ :
  HSMul.hSMul (β := W) r ((f : (a : V) → W) (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
    r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ HAdd.hAdd (α := W)
      ((f : (a : V) → W)
          (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
            (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
        W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
have refine_2₃ : HSMul.hSMul (β := W) r ((f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) : W) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
  r • HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
Tactic: rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]
-- 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 : Monoid M
inst_1 : CommSemiring R
V : Type u_10
W : Type u_11
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module R[M] V
inst_5 : IsScalarTower R R[M] V
inst_6 : AddCommMonoid W
inst_7 : Module R W
inst_8 : Module R[M] W
inst_9 : IsScalarTower R R[M] W
f : V →ₗ[R] W
h :
  ∀ (g : M) (v : V),
    (f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) =
      HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W)
c : R[M]
v : V
g : M
r : R
c' : M →₀ R
_nm : g ∉ c'.support
_nz : ¬r = 0
w : (f : (a : V) → W) (c' • v) = HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2 :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₁ :
  HAdd.hAdd (α := W) ((f : (a : V) → W) (r • HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₂ :
  HSMul.hSMul (β := W) r ((f : (a : V) → W) (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v) : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
    r • HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
refine_2₃ :
  HSMul.hSMul (β := W) r ((f : (a : V) → W) (HSMul.hSMul (α := R[M]) (single g 1) v) : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
    r • HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
⊢ HAdd.hAdd (α := W)
      ((f : (a : V) → W)
          (HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
            (HSMul.hSMul (α := R[M]) ((of R M : (a : M) → R[M]) g : R[M]) v)) :
        W)
      (HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)) =
    HSMul.hSMul (α := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
        (HSMul.hSMul (α := R[M]) (β := W) ((of R M : (a : M) → R[M]) g : R[M]) ((f : (a : V) → W) v : W)) +
      HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
have refine_2₄ : r • HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W) =
  r • HSMul.hSMul (α := R[M]) (β := W) (single g 1) ((f : (a : V) → W) v : W) +
    HSMul.hSMul (β := W) c' ((f : (a : V) → W) v : W)
Tactic: rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]