awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
have rw : Eq (α := SkewMonoidAlgebra β α₂)
  (x.sum fun (a : α) (b : β) ↦
    y.sum fun (a₂ : α) (b₂ : β) ↦
      single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
  (x.sum fun (a : α) (m : β) ↦
    sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
      fun (a₂ : α₂) (b₂ : β) ↦
      single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
        (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))
Tactic: rw [sum_mapDomain_index (by simp) (by simp [add_mul, single_add, sum_add])]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    (x.sum fun (a : α) (m : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
          (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))
have e_g : Eq (α := α → β → SkewMonoidAlgebra β α₂)
  (fun (a : α) (b : β) ↦
    y.sum fun (a₂ : α) (b₂ : β) ↦
      single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
  fun (a : α) (m : β) ↦
  sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
    fun (a₂ : α₂) (b₂ : β) ↦
    single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
      (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
⊢ Eq (α := α → β → SkewMonoidAlgebra β α₂)
    (fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    fun (a : α) (m : β) ↦
    sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
      fun (a₂ : α₂) (b₂ : β) ↦
      single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
        (m * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂)
have e_g : ∀ (a : α) (b : β) (c : α₂),
  Eq.{u_5 + 1} (α := β)
    (coeff
      (y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
      c)
    (coeff
      (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
          (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))
      c)
Tactic: ext a b c
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
a : α
b : β
c : α₂
⊢ Eq.{u_5 + 1} (α := β)
    (coeff
      (y.sum fun (a₂ : α) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
      c)
    (coeff
      (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦
        single (HMul.hMul (α := α₂) ((f : (a : α) → α₂) a : α₂) a₂)
          (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) b₂))
      c)
have e_g : Eq.{u_5 + 1} (α := β)
  (coeff
    (y.sum fun (a₂ : α) (b₂ : β) ↦
      single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a₂ : α₂)) (b * a • b₂))
    c)
  (coeff
    (y.sum fun (a_1 : α) (m : β) ↦
      single (HMul.hMul (α := α₂) (β := α₂) ((f : (a : α) → α₂) a : α₂) ((f : (a : α) → α₂) a_1 : α₂))
        (b * HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) m))
    c)
Tactic: rw [sum_mapDomain_index (by simp) (by simp [smul_add, mul_add, single_add])]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (hypothesis)
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
⊢ (x.sum fun (a : α) (b : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (y.sum fun (a₂ : α) (b₂ : β) ↦ single (a * a₂) (b * a • b₂))) =
    HMul.hMul (α := SkewMonoidAlgebra β α₂) (β := SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x :
        SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y :
        SkewMonoidAlgebra β α₂)
have this : Eq (α := SkewMonoidAlgebra β α₂)
  (x.sum fun (a : α) (b : β) ↦
    y.sum fun (a₂ : α) (b₂ : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (single (a * a₂) (b * a • b₂)))
  (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
    fun (a₁ : α₂) (b₁ : β) ↦
    sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
      fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
Tactic: have : (sum x fun a b ↦ sum y fun a₂ b₂ ↦ mapDomain (↑f) (single (a * a₂) (b * a • b₂))) =
      sum (mapDomain (↑f) x) fun a₁ b₁ ↦
        sum (mapDomain (↑f) y) fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂) := by
    simp_rw [mapDomain_single, map_mul]
    rw [sum_mapDomain_index (by simp) (by simp [add_mul, single_add, sum_add])]
    congr
    ext a b c
    rw [sum_mapDomain_index (by simp) (by simp [smul_add, mul_add, single_add])]
    simp_rw [hf]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
this :
  Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
⊢ (x.sum fun (a : α) (b : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (y.sum fun (a₂ : α) (b₂ : β) ↦ single (a * a₂) (b * a • b₂))) =
    HMul.hMul (α := SkewMonoidAlgebra β α₂) (β := SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x :
        SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y :
        SkewMonoidAlgebra β α₂)
have h : ∀ (x : α) (x_1 : β),
  Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
      (y.sum fun (a₂ : α) (b₂ : β) ↦ single (x * a₂) (x_1 * x • b₂)))
    (y.sum fun (a₂ : α) (b₂ : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (single (x * a₂) (x_1 * x • b₂)))
Tactic: convert! this using 4
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst : Semiring β
inst_1 : Monoid α
inst_2 : Monoid α₂
inst_3 : FunLike F α α₂
inst_4 : MulSemiringAction α β
inst_5 : MulSemiringAction α₂ β
inst_6 : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = HSMul.hSMul.{u_4, u_5, u_5} (α := α₂) ((f : (a : α) → α₂) a : α₂) x
this :
  Eq (α := SkewMonoidAlgebra β α₂)
    (x.sum fun (a : α) (b : β) ↦
      y.sum fun (a₂ : α) (b₂ : β) ↦
        (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
          (single (a * a₂) (b * a • b₂)))
    (sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x)
      fun (a₁ : α₂) (b₁ : β) ↦
      sum ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y)
        fun (a₂ : α₂) (b₂ : β) ↦ single (a₁ * a₂) (b₁ * a₁ • b₂))
x_1 : α
x_2 : β
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
      (y.sum fun (a₂ : α) (b₂ : β) ↦ single (x_1 * a₂) (x_2 * x_1 • b₂)))
    (y.sum fun (a₂ : α) (b₂ : β) ↦
      (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
        (single (x_1 * a₂) (x_2 * x_1 • b₂)))
have h : Eq (α := SkewMonoidAlgebra β α₂)
  (y.sum fun (a : α) (b : β) ↦
    (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
      (single (x_1 * a) (x_2 * x_1 • b)))
  (y.sum fun (a₂ : α) (b₂ : β) ↦
    (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂)
      (single (x_1 * a₂) (x_2 * x_1 • b₂)))
Tactic: rw [map_sum]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
r : k
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) r ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G) =
    single g r
have rw : HSMul.hSMul (β := SkewMonoidAlgebra k G) r (single g 1) = single g r
Tactic: rw [of_apply, smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
r : k
rw : HSMul.hSMul (β := SkewMonoidAlgebra k G) r (single g 1) = single g r
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) r ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G) =
    single g r
have rw₁ : Eq (α := SkewMonoidAlgebra k G) (single g (HSMul.hSMul (β := k) r 1)) (single g r)
Tactic: rw [of_apply, smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
r : k
rw : HSMul.hSMul (β := SkewMonoidAlgebra k G) r (single g 1) = single g r
rw₁ : Eq (α := SkewMonoidAlgebra k G) (single g (HSMul.hSMul (β := k) r 1)) (single g r)
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) r ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G) =
    single g r
have rw₂ : Eq (α := SkewMonoidAlgebra k G) (single g (r * 1)) (single g r)
Tactic: rw [of_apply, smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
g : G
r : k
rw : HSMul.hSMul (β := SkewMonoidAlgebra k G) r (single g 1) = single g r
rw₁ : Eq (α := SkewMonoidAlgebra k G) (single g (HSMul.hSMul (β := k) r 1)) (single g r)
rw₂ : Eq (α := SkewMonoidAlgebra k G) (single g (r * 1)) (single g r)
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) r ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G) =
    single g r
have rw₃ : Eq (α := SkewMonoidAlgebra k G) (single g r) (single g r)
Tactic: rw [of_apply, smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (hypothesis)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : Nontrivial k
a b : G
h :
  Eq (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) a : SkewMonoidAlgebra k G)
    ((of k G : (a : G) → SkewMonoidAlgebra k G) b : SkewMonoidAlgebra k G)
⊢ a = b
have h₁ : Eq (α := G →₀ k) (toFinsupp (single a 1)) (toFinsupp (single b 1))
Tactic: simp_rw [of_apply, ← toFinsupp_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : MulOneClass G
R : Type u_3
inst_2 : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
⊢ (liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) (c • φ) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) c : R)
      ((liftNC (↑f : k →+ R) (⇑g : (a : G) → R) : (a : SkewMonoidAlgebra k G) → R) φ : R)
have suffices : Eq (α := SkewMonoidAlgebra k G →+ R)
  (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
    ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
  (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))
Tactic: suffices this :
    (liftNC ↑f g).comp (smulAddHom k (SkewMonoidAlgebra k G) c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f g) by simpa using congr($this φ)
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : MulOneClass G
R : Type u_3
inst_2 : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
⊢ Eq (α := SkewMonoidAlgebra k G →+ R)
    (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
      ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))
have refine : ∀ (a : G) (b : k),
  Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := SkewMonoidAlgebra k G) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R))
              ((smulAddHom k (SkewMonoidAlgebra k G) : (a : k) → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G) c))
            (singleAddHom a) :
          (a : k) → R)
        b :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : k) → R) c)) (liftNC (↑f : k →+ R) (⇑g : (a : G) → R)))
              (singleAddHom a) :
            k →+ R) :
          (a : k) → R)
        b :
      R)
Tactic: refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ t • a * b = t • (a * b)
have refine_1 : ∀ (i : G), Eq (α := SkewMonoidAlgebra k G) (b.sum fun (a₂ : G) (b₂ : k) ↦ single (i * a₂) (0 * i • b₂)) 0
Tactic: refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
refine_1 : ∀ (i : G), Eq (α := SkewMonoidAlgebra k G) (b.sum fun (a₂ : G) (b₂ : k) ↦ single (i * a₂) (0 * i • b₂)) 0
⊢ t • a * b = t • (a * b)
have refine_2 : (a.sum fun (x1 : G) (x2 : k) ↦ b.sum fun (a₂ : G) (b₂ : k) ↦ single (x1 * a₂) (t • x2 * x1 • b₂)) = t • (a * b)
Tactic: refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ (a.sum fun (x1 : G) (x2 : k) ↦ b.sum fun (a₂ : G) (b₂ : k) ↦ single (x1 * a₂) (t • x2 * x1 • b₂)) = t • (a * b)
have refine_2 : HSMul.hSMul (β := SkewMonoidAlgebra k G) t
    (a.sum fun (a : G) (b_1 : k) ↦ b.sum fun (a_1 : G) (b : k) ↦ single (a * a_1) (b_1 * a • b)) =
  t • (a * b)
Tactic: simp only [← smul_sum, smul_mul_assoc, ← smul_single,
        zero_mul, imp_true_iff, sum_zero, single_zero]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ (t • a) • b = t • a • b
have simp : t • a * b = t • (a * b)
Tactic: classical
    simp only [smul_eq_mul]
    refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_ <;>
      simp only [← smul_sum, smul_mul_assoc, ← smul_single,
        zero_mul, imp_true_iff, sum_zero, single_zero]; rfl
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
inst_3 : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
simp : t • a * b = t • (a * b)
⊢ (t • a) • b = t • a • b
have refine_2 : HSMul.hSMul (β := SkewMonoidAlgebra k G) t
    (a.sum fun (a : G) (b_1 : k) ↦ b.sum fun (a_1 : G) (b : k) ↦ single (a * a_1) (b_1 * a • b)) =
  t • (a * b)
Tactic: classical
    simp only [smul_eq_mul]
    refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_ <;>
      simp only [← smul_sum, smul_mul_assoc, ← smul_single,
        zero_mul, imp_true_iff, sum_zero, single_zero]; rfl
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_6 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
⊢ φ₁ = φ₂
have h₁ : Eq (α := SkewMonoidAlgebra k G →+[k] A) (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (↑φ₂ : SkewMonoidAlgebra k G →+[k] A)
Tactic: apply NonUnitalAlgHom.to_distribMulActionHom_injective
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_6 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
⊢ Eq (α := SkewMonoidAlgebra k G →+[k] A) (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (↑φ₂ : SkewMonoidAlgebra k G →+[k] A)
have h₁ : ∀ (a : G),
  Eq (α := k →+[k] A) (DistribMulActionHom.comp (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))
    (DistribMulActionHom.comp (↑φ₂ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))
Tactic: apply distribMulActionHom_ext'
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
A : Type u_6
inst : NonUnitalNonAssocSemiring A
inst_1 : Monoid G
inst_2 : Semiring k
inst_3 : MulSemiringAction G k
inst_4 : DistribMulAction k A
φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A
h :
  ∀ (x : G),
    Eq.{u_6 + 1} (α := A) ((φ₁ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
      ((φ₂ : (a : SkewMonoidAlgebra k G) → A) (single x 1) : A)
a : G
⊢ Eq (α := k →+[k] A) (DistribMulActionHom.comp (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))
    (DistribMulActionHom.comp (↑φ₂ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a))
have h₁ : Eq.{u_6 + 1} (α := A)
  ((DistribMulActionHom.comp (↑φ₁ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a) : (a : k) → A) 1 : A)
  ((DistribMulActionHom.comp (↑φ₂ : SkewMonoidAlgebra k G →+[k] A) (DistribMulActionHom.single a) : (a : k) → A) 1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
r : k
f : SkewMonoidAlgebra A G
⊢ HMul.hMul (α := SkewMonoidAlgebra A G)
      ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G) f =
    HMul.hMul (β := SkewMonoidAlgebra A G) f
      ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G)
have a : ∀ (a : G),
  (HMul.hMul (α := SkewMonoidAlgebra A G)
          ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G)
          f).coeff
      a =
    (HMul.hMul (β := SkewMonoidAlgebra A G) f
          ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r :
            SkewMonoidAlgebra A G)).coeff
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : CommSemiring k
A : Type u_3
inst_2 : Semiring A
inst_3 : Algebra k A
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G k A
r : k
a : SkewMonoidAlgebra A G
⊢ r • a =
    HMul.hMul (α := SkewMonoidAlgebra A G)
      ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G) a
have a₁ : ∀ (a_1 : G),
  (r • a).coeff a_1 =
    (HMul.hMul (α := SkewMonoidAlgebra A G)
          ((RingHom.comp singleOneRingHom (algebraMap k A) : (a : k) → SkewMonoidAlgebra A G) r : SkewMonoidAlgebra A G)
          a).coeff
      a_1
Tactic: ext