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
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
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
⊢ 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 = f.coeff a.1 * a.1 • g.coeff a.2
Tactic: apply Finset.sum_congr_of_eq_on_inter
-- 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
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
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
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
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
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
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
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
⊢ (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
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 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ 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
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
x₁ : Eq.{u_1 + 1} (α := k) (∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂)) (∑ p ∈ f.support ×ˢ g.support, F p)
⊢ (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
have x₂ : 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)
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 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ 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 (hypothesis)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
⊢ (f * single x r).coeff z = f.coeff y * y • r
have A : ∀ (a₁ : G) (b₁ : k),
  (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
    if a₁ * x = z then b₁ * a₁ • r else 0
Tactic: have A : ∀ a₁ b₁, ((single x r).sum fun a₂ b₂ ↦ ite (a₁ * a₂ = z) (b₁ * a₁ • b₂) 0) =
      ite (a₁ * x = z) (b₁ * a₁ • r) 0 :=
    fun a₁ b₁ ↦ sum_single_index <| by 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
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
⊢ (if y ∈ f.support then f.coeff y * y • r else 0) = f.coeff y * y • r
have pos : ∀ (h : y ∈ f.support), f.coeff y * y • r = f.coeff y * y • r
Tactic: split_ifs with 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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
pos : ∀ (h : y ∈ f.support), f.coeff y * y • r = f.coeff y * y • r
⊢ (if y ∈ f.support then f.coeff y * y • r else 0) = f.coeff y * y • r
have neg : ∀ (h : y ∉ f.support), 0 = f.coeff y * y • r
Tactic: split_ifs with h
-- 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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∈ f.support
⊢ f.coeff y * y • r = f.coeff y * y • r
have h₁ : ¬f.coeff y = 0
Tactic: simp [support] at h
Cleared hypotheses: h
-- 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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
h : y ∉ f.support
⊢ 0 = f.coeff y * y • r
have h₁ : f.coeff y = 0
Tactic: simp [support] 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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
⊢ (f * single x r).coeff z = f.coeff y * y • r
have x₁ : (f * single x r).coeff z = f.sum fun (a : G) (b : k) ↦ if a = y then b * y • r else 0
Tactic: calc
    (f * (single x r)).coeff z =
        sum f fun a b ↦ if a = y then b * y • r else 0 := by simp [coeff_mul, A, H, sum_ite_eq']
    _ = if y ∈ f.support then f.coeff y * y • r else 0 := (f.support.sum_ite_eq' _ _)
    _ = f.coeff y * y • r := by
      split_ifs with h <;> simp [support] at h <;> simp [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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
A :
  ∀ (a₁ : G) (b₁ : k),
    (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
      if a₁ * x = z then b₁ * a₁ • r else 0
x₁ : (f * single x r).coeff z = f.sum fun (a : G) (b : k) ↦ if a = y then b * y • r else 0
⊢ (f * single x r).coeff z = f.coeff y * y • r
have x₂ : (if y ∈ f.support then f.coeff y * y • r else 0) = f.coeff y * y • r
Tactic: calc
    (f * (single x r)).coeff z =
        sum f fun a b ↦ if a = y then b * y • r else 0 := by simp [coeff_mul, A, H, sum_ite_eq']
    _ = if y ∈ f.support then f.coeff y * y • r else 0 := (f.support.sum_ite_eq' _ _)
    _ = f.coeff y * y • r := by
      split_ifs with h <;> simp [support] at h <;> simp [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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
⊢ (f * single x r).coeff z = f.coeff y * y • r
have have : ∀
  (A :
    ∀ (a₁ : G) (b₁ : k),
      (sum (single x r) fun (a₂ : G) (b₂ : k) ↦ if a₁ * a₂ = z then b₁ * a₁ • b₂ else 0) =
        if a₁ * x = z then b₁ * a₁ • r else 0),
  (f * single x r).coeff z = f.coeff y * y • r
Tactic: classical
  have A : ∀ a₁ b₁, ((single x r).sum fun a₂ b₂ ↦ ite (a₁ * a₂ = z) (b₁ * a₁ • b₂) 0) =
      ite (a₁ * x = z) (b₁ * a₁ • r) 0 :=
    fun a₁ b₁ ↦ sum_single_index <| by simp
  calc
    (f * (single x r)).coeff z =
        sum f fun a b ↦ if a = y then b * y • r else 0 := by simp [coeff_mul, A, H, sum_ite_eq']
    _ = if y ∈ f.support then f.coeff y * y • r else 0 := (f.support.sum_ite_eq' _ _)
    _ = f.coeff y * y • r := by
      split_ifs with h <;> simp [support] at h <;> simp [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 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
⊢ (x * single g r).coeff g' = 0
have simp : Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
Tactic: simp only [coeff_mul, smul_zero, mul_zero, ite_self, 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 : ∀ (x : G), ¬g' = x * g
⊢ Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
have h₁ : ∀ x_1 ∈ x.toFinsupp.support,
  Eq.{u_1 + 1} (α := k)
    ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r 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 : ∀ (x : G), ¬g' = x * g
⊢ ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
have h₁ : ∀ x_1 ∈ x.toFinsupp.support, x_1 * g = g' → HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 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 : ∀ (x : G), ¬g' = x * g
⊢ (x * single g r).coeff g' = 0
have simp : Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
Tactic: classical
  simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ 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 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
simp : Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
⊢ (x * single g r).coeff g' = 0
have h₁ : ∀ x_1 ∈ x.toFinsupp.support,
  Eq.{u_1 + 1} (α := k)
    ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
Tactic: classical
  simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ 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 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
simp : Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
h₁ :
  ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
⊢ (x * single g r).coeff g' = 0
have h₂ : ∀ x_1 ∈ x.toFinsupp.support, x_1 * g = g' → HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0
Tactic: classical
  simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ 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 : Mul G
inst_2 : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ∀ (x : G), ¬g' = x * g
simp : Eq (α := k) (x.sum fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) 0
h₁ :
  ∀ x_1 ∈ x.toFinsupp.support,
    Eq.{u_1 + 1} (α := k)
      ((fun (a₁ : G) (b₁ : k) ↦ if a₁ * g = g' then b₁ * a₁ • r else 0) x_1 ((x.toFinsupp : (a : G) → k) x_1)) 0
h₂ : ∀ x_1 ∈ x.toFinsupp.support, x_1 * g = g' → HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0
⊢ (x * single g r).coeff g' = 0
have h₃ : ∀ x_1 ∈ x.toFinsupp.support,
  ∀ (h : ∀ (x : G), ¬x_1 * g = x * g), HMul.hMul (α := k) ((x.toFinsupp : (a : G) → k) x_1 : k) (x_1 • r) = 0
Tactic: classical
  simp only [coeff_mul, smul_zero, mul_zero, ite_self, sum_single_index]
  apply Finset.sum_eq_zero
  simp_rw [ite_eq_right_iff]
  rintro _ _ rfl
  exact False.elim (h _ rfl)
Cleared hypotheses: g', h
-- 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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
⊢ (single x r * f).coeff y = r * x • f.coeff z
have this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
Tactic: have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by 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
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
⊢ (if z ∈ f.support then r * x • f.coeff z else 0) = r * x • f.coeff z
have pos : ∀ (h : z ∈ f.support), r * x • f.coeff z = r * x • f.coeff z
Tactic: split_ifs with 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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
pos : ∀ (h : z ∈ f.support), r * x • f.coeff z = r * x • f.coeff z
⊢ (if z ∈ f.support then r * x • f.coeff z else 0) = r * x • f.coeff z
have neg : ∀ (h : z ∉ f.support), 0 = r * x • f.coeff z
Tactic: split_ifs with h
-- 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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
h : z ∈ f.support
⊢ r * x • f.coeff z = r * x • f.coeff z
have h₁ : ¬f.coeff z = 0
Tactic: simp [support] at h
Cleared hypotheses: h
-- 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 : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
h : z ∉ f.support
⊢ 0 = r * x • f.coeff z
have h₁ : f.coeff z = 0
Tactic: simp [support] 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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
⊢ (single x r * f).coeff y = r * x • f.coeff z
have x₁ : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then r * x • b else 0)
  (f.sum fun (a : G) (b : k) ↦ if a = z then r * x • b else 0)
Tactic: calc
    (single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
x₁ :
  Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then r * x • b else 0)
    (f.sum fun (a : G) (b : k) ↦ if a = z then r * x • b else 0)
⊢ (single x r * f).coeff y = r * x • f.coeff z
have x₂ : (if z ∈ f.support then r * x • f.coeff z else 0) = r * x • f.coeff z
Tactic: calc
    (single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
⊢ (single x r * f).coeff y = r * x • f.coeff z
have have : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
Tactic: classical
  have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by simp
  calc
    (single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [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 : Mul G
inst_2 : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
have : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0
⊢ (single x r * f).coeff y = r * x • f.coeff z
have have₁ : ∀ (this : Eq (α := k) (f.sum fun (a : G) (b : k) ↦ if x * a = y then 0 * x • b else 0) 0),
  (single x r * f).coeff y = r * x • f.coeff z
Tactic: classical
  have : (f.sum fun a b ↦ ite (x * a = y) (0 * x • b) 0) = 0 := by simp
  calc
    (single x r * f).coeff y =
        sum f fun a b ↦ ite (x * a = y) (r * x • b) 0 :=
      (coeff_mul _ _ _).trans <| sum_single_index this
    _ = f.sum fun a b ↦ ite (a = z) (r * x • b) 0 := by simp [H]
    _ = if z ∈ f.support then r * x • f.coeff z else 0 := (f.support.sum_ite_eq' _ _)
    _ = _ := by split_ifs with h <;> simp [support] at h <;> simp [h]