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 : CommSemiring k
inst_1 : CommMonoid G
inst_2 : MulSemiringAction G k
inst_3 : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
x : G
h : x ∈ b.toFinsupp.support
y : G
h_1 : y ∈ a.toFinsupp.support
rw :
  Eq (α := SkewMonoidAlgebra k G)
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((a.toFinsupp : (a : G) → k) y : k) ((b.toFinsupp : (a : G) → k) x : k)))
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))
⊢ Eq (α := SkewMonoidAlgebra k G)
    (single (y * x)
      (HMul.hMul (α := k) (β := k) ((a.toFinsupp : (a : G) → k) y : k) ((b.toFinsupp : (a : G) → k) x : k)))
    (single (x * y)
      (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))
have rw₁ : Eq (α := SkewMonoidAlgebra k G)
  (single (x * y) (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))
  (single (x * y) (HMul.hMul (α := k) (β := k) ((b.toFinsupp : (a : G) → k) x : k) ((a.toFinsupp : (a : G) → k) y : k)))
Tactic: rw [mul_comm, mul_comm (a.toFinsupp y) _]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst : AddMonoid k
inst_1 : SMulZeroClass S k
inst_2 : FaithfulSMul S k
inst_3 : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
⊢ _s₁ = _s₂
have apply : ∀ (a : G →₀ k), { toFinsupp := _s₁ • a : SkewMonoidAlgebra k G } = { toFinsupp := _s₂ • a }
Tactic: apply eq_of_smul_eq_smul fun a : G →₀ k ↦ congr_arg toFinsupp _
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g g' : G
f : SkewMonoidAlgebra M α
⊢ (g * g') • f = g • g' • f
have rw : (mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = g • g' • f
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g g' : G
f : SkewMonoidAlgebra M α
rw : (mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = g • g' • f
⊢ (g * g') • f = g • g' • f
have rw₁ : Eq (α := SkewMonoidAlgebra M α)
  ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
    SkewMonoidAlgebra M α)
  ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) (g' • f) :
    SkewMonoidAlgebra M α)
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g g' : G
f : SkewMonoidAlgebra M α
rw : (mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = g • g' • f
rw₁ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) (g' • f) :
      SkewMonoidAlgebra M α)
⊢ (g * g') • f = g • g' • f
have rw₂ : Eq (α := SkewMonoidAlgebra M α)
  ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
    SkewMonoidAlgebra M α)
  ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
      ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
    SkewMonoidAlgebra M α)
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g g' : G
f : SkewMonoidAlgebra M α
rw : (mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = g • g' • f
rw₁ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) (g' • f) :
      SkewMonoidAlgebra M α)
rw₂ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
      SkewMonoidAlgebra M α)
⊢ (g * g') • f = g • g' • f
have rw₃ : Eq (α := SkewMonoidAlgebra M α)
  ((mapDomain ((fun (x : α) ↦ g • x) ∘ fun (x : α) ↦ g' • x) : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
    SkewMonoidAlgebra M α)
  ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
      ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
    SkewMonoidAlgebra M α)
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
g g' : G
f : SkewMonoidAlgebra M α
rw : (mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = g • g' • f
rw₁ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) (g' • f) :
      SkewMonoidAlgebra M α)
rw₂ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ (g * g') • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
      SkewMonoidAlgebra M α)
rw₃ :
  Eq (α := SkewMonoidAlgebra M α)
    ((mapDomain ((fun (x : α) ↦ g • x) ∘ fun (x : α) ↦ g' • x) : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        f :
      SkewMonoidAlgebra M α)
    ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
        ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
      SkewMonoidAlgebra M α)
⊢ (g * g') • f = g • g' • f
have rw₄ : Eq (α := SkewMonoidAlgebra M α)
  ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
      ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
    SkewMonoidAlgebra M α)
  ((mapDomain fun (x : α) ↦ g • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
      ((mapDomain fun (x : α) ↦ g' • x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) :
    SkewMonoidAlgebra M α)
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
f : SkewMonoidAlgebra M α
⊢ HSMul.hSMul (α := G) 1 f = f
have rw : (mapDomain fun (x : α) ↦ HSMul.hSMul.{u_2, u_7, u_7} (α := G) 1 x : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
    f =
  f
Tactic: rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
f : SkewMonoidAlgebra M α
rw :
  (mapDomain fun (x : α) ↦ HSMul.hSMul.{u_2, u_7, u_7} (α := G) 1 x :
        (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
      f =
    f
⊢ HSMul.hSMul (α := G) 1 f = f
have rw₁ : (mapDomain id : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = f
Tactic: rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
f : SkewMonoidAlgebra M α
rw :
  (mapDomain fun (x : α) ↦ HSMul.hSMul.{u_2, u_7, u_7} (α := G) 1 x :
        (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α)
      f =
    f
rw₁ : (mapDomain id : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f = f
⊢ HSMul.hSMul (α := G) 1 f = f
have rw₂ : f = f
Tactic: rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
inst_3 : AddCommMonoid k
g : G
⊢ HSMul.hSMul (β := SkewMonoidAlgebra k G) g 0 = 0
have a : ∀ (a : G), (HSMul.hSMul (β := SkewMonoidAlgebra k G) g 0).coeff a = coeff 0 a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst : Monoid G
inst_1 : AddCommMonoid M
inst_2 : MulAction G α
inst_3 : AddCommMonoid k
g : G
f f' : SkewMonoidAlgebra k G
⊢ g • (f + f') = g • f + g • f'
have a : ∀ (a : G), (g • (f + f')).coeff a = (g • f + g • f').coeff a
Tactic: ext
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
have rw : Eq (α := k) (f.sum fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
  (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0)
Tactic: rw [mul_def, coeff_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 : Mul G
inst_2 : SMulZeroClass G k
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ Eq (α := k) (f.sum fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
    (f.sum fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0)
have e_g : Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
  fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
Tactic: congr
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (a₁ * a₂) (b * a₁ • b₂)) x)
    fun (a₁ : G) (b₁ : k) ↦ g.sum fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
have e_g : ∀ (x_1 : G) (x_2 : k),
  Eq (α := k) (coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (x_1 * a₂) (x_2 * x_1 • b₂)) x)
    (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)
Tactic: ext
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
⊢ Eq (α := k) (coeff (g.sum fun (a₂ : G) (b₂ : k) ↦ single (x_1 * a₂) (x_2 * x_1 • b₂)) x)
    (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)
have e_g : Eq (α := k) (g.sum fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x)
  (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)
Tactic: rw [coeff_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 : Mul G
inst_2 : SMulZeroClass G k
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
⊢ Eq (α := k) (g.sum fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x)
    (g.sum fun (a₂ : G) (b₂ : k) ↦ if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0)
have e_g : Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x) fun (a₂ : G) (b₂ : k) ↦
  if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0
Tactic: congr
-- 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
inst_3 : DecidableEq G
f g : SkewMonoidAlgebra k G
x x_1 : G
x_2 : k
⊢ Eq (α := G → k → k) (fun (a₁ : G) (b : k) ↦ coeff (single (x_1 * a₁) (x_2 * x_1 • b)) x) fun (a₂ : G) (b₂ : k) ↦
    if x_1 * a₂ = x then x_2 * x_1 • b₂ else 0
have e_g : ∀ (x_3 : G) (x_4 : k), coeff (single (x_1 * x_3) (x_2 * x_1 • x_4)) x = if x_1 * x_3 = x then x_2 * x_1 • x_4 else 0
Tactic: ext
-- 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)
have rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ f.support ×ˢ g.support, F x) (∑ p ∈ f.support ×ˢ g.support, F p)
Tactic: rw [← Finset.sum_product _ _ _]
-- 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} = {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
have h : ∀ (a : G × G), a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} ↔ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (hypothesis)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
have hp₁ : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
Tactic: simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
Cleared hypotheses: hp
-- 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
have pos : ∀ (h1 : f.coeff p.1 = 0), f.coeff p.1 * p.1 • g.coeff p.2 = 0
Tactic: by_cases h1 : f.coeff p.1 = 0
-- 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
pos : ∀ (h1 : f.coeff p.1 = 0), f.coeff p.1 * p.1 • g.coeff p.2 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
have neg : ∀ (h1 : ¬f.coeff p.1 = 0), f.coeff p.1 * p.1 • g.coeff p.2 = 0
Tactic: by_cases h1 : f.coeff p.1 = 0
-- 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
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ (f * g).coeff x = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2
have x₁ : Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)
Tactic: calc
    (f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [← Finset.sum_product _ _ _]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 :=
      (Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm])
        fun _ _ ↦ rfl)
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all
-- 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
f g : SkewMonoidAlgebra k G
x : G
⊢ Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
have hs : Set.Finite.{u_2} (α := G × G) (Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
Tactic: apply Set.Finite.inter_of_right
-- 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
f g : SkewMonoidAlgebra k G
x : G
⊢ Set.Finite.{u_2} (α := G × G) (Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
have hs : (Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2) ⊆
  (↑(f.support.product g.support) : Set (G × G))
Tactic: apply Set.Finite.subset (Finset.finite_toSet ((f.support).product (g.support)))
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (hypothesis)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x =
    ∑ᶠ (p : G × G) (_ : Membership.mem (γ := Set (G × G)) {p : G × G | p.1 * p.2 = x} p),
      f.coeff p.1 * p.1 • g.coeff p.2
have this : Set.Finite.{u_2} (α := G × G)
  ({p : G × G | p.1 * p.2 = x} ∩ Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
Tactic: have : ({p : G × G | p.1 * p.2 = x}
      ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite := by
    apply Set.Finite.inter_of_right
    apply Set.Finite.subset (Finset.finite_toSet ((f.support).product (g.support)))
    aesop
-- 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
f g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
⊢ (f * g).coeff x =
    ∑ᶠ (p : G × G) (_ : Membership.mem (γ := Set (G × G)) {p : G × G | p.1 * p.2 = x} p),
      f.coeff p.1 * p.1 • g.coeff p.2
have rw : (f * g).coeff x =
  ∑
    i ∈
      this.toFinset (s :=
        {p : G × G | p.1 * p.2 = x} ∩
          Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2),
    f.coeff i.1 * i.1 • g.coeff i.2
Tactic: rw [← finsum_mem_inter_support, finsum_mem_eq_finite_toFinset_sum _ 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 : Mul G
inst_2 : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
s : Finset (G × G) :=
  this.toFinset (s :=
    {p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)
have rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ f.support ×ˢ g.support, F x) (∑ p ∈ f.support ×ˢ g.support, F p)
Tactic: rw [← Finset.sum_product _ _ _]
-- 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
f g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
s : Finset (G × G) :=
  this.toFinset (s :=
    {p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ Eq.{u_1 + 1} (α := k) (∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2)
    (∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f.coeff p.1 * p.1 • g.coeff p.2)
have h₁ : ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
  a ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = 0
Tactic: apply Finset.sum_congr_of_eq_on_inter
-- 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
f g : SkewMonoidAlgebra k G
x : G
this :
  Set.Finite.{u_2} (α := G × G)
    ({p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
s : Finset (G × G) :=
  this.toFinset (s :=
    {p : G × G | p.1 * p.2 = x} ∩
      Function.support.{u_2, u_1} (M := k) fun (p : G × G) ↦ f.coeff p.1 * p.1 • g.coeff p.2)
F : G × G → k := fun (p : G × G) ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
h₁ :
  ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2)
    (∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f.coeff p.1 * p.1 • g.coeff p.2)
have h₂ : ∀ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support},
  a ∉ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} → f.coeff a.1 * a.1 • g.coeff a.2 = 0
Tactic: apply Finset.sum_congr_of_eq_on_inter