awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
⊢ (single g r * x).coeff g' = 0
have rw : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
Tactic: rw [coeff_mul, sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
rw : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
⊢ (single g r * x).coeff g' = 0
have rw₁ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then 0 * g • b₂ else 0) 0
Tactic: rw [coeff_mul, sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
⊢ Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
have h₁ : ∀ x_1 ∈ x.toFinsupp.support,
  Eq.{u_1 + 1} (α := k)
    ((fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
Tactic: apply Finset.sum_eq_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 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
⊢ ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
have h₁ : ∀ x_1 ∈ x.toFinsupp.support, g * x_1 = g' → r * HSMul.hSMul (β := k) g ((x.toFinsupp : (a : G) → k) x_1 : k) = 0
Tactic: simp_rw [ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
⊢ (single g r * x).coeff g' = 0
have rw : Eq (α := k)
  (sum (single g r) fun (a₁ : G) (b₁ : k) ↦ x.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = g' then b₁ * a₁ • b₂ else 0) 0
Tactic: classical
  rw [coeff_mul, sum_single_index]
  · apply Finset.sum_eq_zero
    simp_rw [ite_eq_right_iff]
    rintro g'' _hg'' rfl
    exact absurd ⟨_, rfl⟩ h
  · simp
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
rw :
  Eq (α := k)
    (sum (single g r) fun (a₁ : G) (b₁ : k) ↦ x.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = g' then b₁ * a₁ • b₂ else 0) 0
⊢ (single g r * x).coeff g' = 0
have rw₁ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
Tactic: classical
  rw [coeff_mul, sum_single_index]
  · apply Finset.sum_eq_zero
    simp_rw [ite_eq_right_iff]
    rintro g'' _hg'' rfl
    exact absurd ⟨_, rfl⟩ h
  · simp
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ (d : G), g' = g * d
rw :
  Eq (α := k)
    (sum (single g r) fun (a₁ : G) (b₁ : k) ↦ x.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = g' then b₁ * a₁ • b₂ else 0) 0
rw₁ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then r * g • b₂ else 0) 0
⊢ (single g r * x).coeff g' = 0
have rw₂ : Eq (α := k) (x.sum fun (a₂ : G) (b₂ : k) ↦ if g * a₂ = g' then 0 * g • b₂ else 0) 0
Tactic: classical
  rw [coeff_mul, sum_single_index]
  · apply Finset.sum_eq_zero
    simp_rw [ite_eq_right_iff]
    rintro g'' _hg'' rfl
    exact absurd ⟨_, rfl⟩ h
  · simp
-- 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
f : SkewMonoidAlgebra k G
r : k
x a : G
⊢ a * 1 = x ↔ a = x
have rw : a = x ↔ a = x
Tactic: rw [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 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun (a : G) (b : k) ↦ (single a b * g).coeff x
have rw : (f * g).coeff x = coeff (f.sum fun (a : G) (b : k) ↦ single a b * g) x
Tactic: rw [← coeff_sum, ← sum_mul g f, f.sum_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
rw : (f * g).coeff x = coeff (f.sum fun (a : G) (b : k) ↦ single a b * g) x
⊢ (f * g).coeff x = f.sum fun (a : G) (b : k) ↦ (single a b * g).coeff x
have rw₁ : (f * g).coeff x = (f.sum single * g).coeff x
Tactic: rw [← coeff_sum, ← sum_mul g f, f.sum_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
rw : (f * g).coeff x = coeff (f.sum fun (a : G) (b : k) ↦ single a b * g) x
rw₁ : (f * g).coeff x = (f.sum single * g).coeff x
⊢ (f * g).coeff x = f.sum fun (a : G) (b : k) ↦ (single a b * g).coeff x
have rw₂ : (f * g).coeff x = (f * g).coeff x
Tactic: rw [← coeff_sum, ← sum_mul g f, f.sum_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = g.sum fun (a : G) (b : k) ↦ (f * single a b).coeff x
have rw : (f * g).coeff x = coeff (g.sum fun (a : G) (b : k) ↦ f * single a b) x
Tactic: rw [← coeff_sum, ← mul_sum f g, g.sum_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
rw : (f * g).coeff x = coeff (g.sum fun (a : G) (b : k) ↦ f * single a b) x
⊢ (f * g).coeff x = g.sum fun (a : G) (b : k) ↦ (f * single a b).coeff x
have rw₁ : (f * g).coeff x = (f * g.sum single).coeff x
Tactic: rw [← coeff_sum, ← mul_sum f g, g.sum_single]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Group G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
x : G
rw : (f * g).coeff x = coeff (g.sum fun (a : G) (b : k) ↦ f * single a b) x
rw₁ : (f * g).coeff x = (f * g.sum single).coeff x
⊢ (f * g).coeff x = g.sum fun (a : G) (b : k) ↦ (f * single a b).coeff x
have rw₂ : (f * g).coeff x = (f * g).coeff x
Tactic: rw [← coeff_sum, ← mul_sum f g, g.sum_single]
-- 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
f g : SkewMonoidAlgebra k G →+* k
h₁ :
  ∀ (b : k),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
h_of :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
this : ∀ {a : G} {b₁ b₂ : k}, HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b₁) (single a b₂) = single a (b₁ * b₂)
a : G
b : k
⊢ Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
have rw : Eq.{u_1 + 1} (α := k)
  (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
        (a : SkewMonoidAlgebra k G) → k)
      (single a (b * 1)) :
    k)
  (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
        (a : SkewMonoidAlgebra k G) → k)
      (single a (b * 1)) :
    k)
Tactic: rw [← mul_one b, ← this, AddMonoidHom.coe_coe f,
      AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]
-- 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
f g : SkewMonoidAlgebra k G →+* k
h₁ :
  ∀ (b : k),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
h_of :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
this : ∀ {a : G} {b₁ b₂ : k}, HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b₁) (single a b₂) = single a (b₁ * b₂)
a : G
b : k
rw :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
⊢ Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
have rw₁ : Eq.{u_1 + 1} (α := k)
  (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
        (a : SkewMonoidAlgebra k G) → k)
      (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
    k)
  (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
        (a : SkewMonoidAlgebra k G) → k)
      (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
    k)
Tactic: rw [← mul_one b, ← this, AddMonoidHom.coe_coe f,
      AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]
-- 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
f g : SkewMonoidAlgebra k G →+* k
h₁ :
  ∀ (b : k),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
h_of :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
this : ∀ {a : G} {b₁ b₂ : k}, HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b₁) (single a b₂) = single a (b₁ * b₂)
a : G
b : k
rw :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
rw₁ :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
⊢ Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
have rw₂ : Eq.{u_1 + 1} (α := k)
  ((f : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
  (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
        (a : SkewMonoidAlgebra k G) → k)
      (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
    k)
Tactic: rw [← mul_one b, ← this, AddMonoidHom.coe_coe f,
      AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]
-- 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
f g : SkewMonoidAlgebra k G →+* k
h₁ :
  ∀ (b : k),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
h_of :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
this : ∀ {a : G} {b₁ b₂ : k}, HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b₁) (single a b₂) = single a (b₁ * b₂)
a : G
b : k
rw :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
rw₁ :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
rw₂ :
  Eq.{u_1 + 1} (α := k)
    ((f : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
⊢ Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
have rw₃ : Eq.{u_1 + 1} (α := k)
  ((f : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
  ((g : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
Tactic: rw [← mul_one b, ← this, AddMonoidHom.coe_coe f,
      AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]
-- 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
f g : SkewMonoidAlgebra k G →+* k
h₁ :
  ∀ (b : k),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
h_of :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
this : ∀ {a : G} {b₁ b₂ : k}, HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b₁) (single a b₂) = single a (b₁ * b₂)
a : G
b : k
rw :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
rw₁ :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
rw₂ :
  Eq.{u_1 + 1} (α := k)
    ((f : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
rw₃ :
  Eq.{u_1 + 1} (α := k)
    ((f : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
    ((g : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
⊢ Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
have rw₄ : HMul.hMul (α := k) (β := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
    ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k) =
  (g : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1))
Tactic: rw [← mul_one b, ← this, AddMonoidHom.coe_coe f,
      AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]
-- 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 : MonoidHomClass F α α₂
f : F
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) 1) 1
have simp_rw : Eq (α := SkewMonoidAlgebra β α₂)
  ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) (single 1 1) :
    SkewMonoidAlgebra β α₂)
  (single 1 1 : SkewMonoidAlgebra β α₂)
Tactic: simp_rw [one_def, mapDomain_single, map_one]
-- 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 : MonoidHomClass F α α₂
f : F
simp_rw :
  Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) (single 1 1) :
      SkewMonoidAlgebra β α₂)
    (single 1 1 : SkewMonoidAlgebra β α₂)
⊢ Eq (α := SkewMonoidAlgebra β α₂)
    ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) 1) 1
have simp_rw₁ : Eq (α := SkewMonoidAlgebra β α₂) (single ((f : (a : α) → α₂) 1) 1 : SkewMonoidAlgebra β α₂)
  (single 1 1 : SkewMonoidAlgebra β α₂)
Tactic: simp_rw [one_def, mapDomain_single, map_one]
-- 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
⊢ (mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) (x * y) =
    HMul.hMul (α := SkewMonoidAlgebra β α₂) (β := SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) x :
        SkewMonoidAlgebra β α₂)
      ((mapDomain (⇑f : (a : α) → α₂) : (a : SkewMonoidAlgebra β α) → SkewMonoidAlgebra β α₂) y :
        SkewMonoidAlgebra β α₂)
have rw : (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 β α₂)
Tactic: rw [mul_def, map_sum]
-- 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₂ : β) ↦
        (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₂))
have simp_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₂))
  (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: simp_rw [mapDomain_single, map_mul]