awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
f : MonoidHom.{u_7, u_4} (Multiplicative M) A
⊢ (fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
      ((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A)) f) =
    f
have h : ∀ (x : M),
  Eq.{u_4 + 1} (α := A)
    ((Additive.toMul : (a : Additive A) → A)
        (((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                ((fun (f : R[M] →ₐ[R] A) ↦
                    (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
                  ((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦
                      (liftNCAlgHom (Algebra.ofId R A) F sorry : R[M] →ₐ[R] A))
                    f)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      A)
    ((Additive.toMul : (a : Additive A) → A)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A) f :
                AddMonoidHom.{u_7, u_4} M (Additive A)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
F : R[M] →ₐ[R] A
⊢ (fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦ (liftNCAlgHom (Algebra.ofId R A) F ⋯ : R[M] →ₐ[R] A))
      ((fun (f : R[M] →ₐ[R] A) ↦ (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
        F) =
    F
have h : ∀ (x : M),
  Eq.{u_4 + 1} (α := A)
    ((Additive.toMul : (a : Additive A) → A)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                  (MonoidHom.comp
                    (↑((fun (F : MonoidHom.{u_7, u_4} (Multiplicative M) A) ↦
                            (liftNCAlgHom (Algebra.ofId R A) F sorry : R[M] →ₐ[R] A))
                          ((fun (f : R[M] →ₐ[R] A) ↦
                              (MonoidHom.comp (↑f : R[M] →* A) (of R M) : MonoidHom.{u_7, u_4} (Multiplicative M) A))
                            F)) :
                      R[M] →* A)
                    (of R M)) :
                AddMonoidHom.{u_7, u_4} M (Additive A)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      A)
    ((Additive.toMul : (a : Additive A) → A)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* A) → M →+ Additive A)
                  (MonoidHom.comp (↑F : R[M] →* A) (of R M)) :
                AddMonoidHom.{u_7, u_4} M (Additive A)) :
              (a : M) → Additive A)
            x :
          Additive A) :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
| ((F : (a : R[M]) → A) f : A)
have rw : ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) (MonoidHom.comp (↑F : R[M] →* A) (of R M)) :
        R[M] →ₐ[R] A) :
      (a : R[M]) → A)
    f :
  A)
Tactic: rw [lift_unique' F]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
| ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) (MonoidHom.comp (↑F : R[M] →* A) (of R M)) :
          R[M] →ₐ[R] A) :
        (a : R[M]) → A)
      f :
    A)
have simp : sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A)
Tactic: simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
| ((F : (a : R[M]) → A) f : A)
have rw : sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A)
Tactic: rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
⊢ Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
have conv_lhs : Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
  (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
Tactic: conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
conv_lhs :
  Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
⊢ Eq.{u_4 + 1} (α := A) ((F : (a : R[M]) → A) f : A)
    (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A) : A)
have conv_lhs₁ : Eq.{u_4 + 1} (α := A) (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A))
  (sum f fun (a : M) (b : R) ↦ HSMul.hSMul (β := A) b ((F : (a : R[M]) → A) (single a 1) : A))
Tactic: conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f : MonoidHom.{u_7, u_4} (Multiplicative M) A
x : R[M]
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) x : S[M]) :
      A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) x : A)
have zero : Eq.{u_4 + 1} (α := A)
  ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
      ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) 0) :
    A)
  ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) 0 : A)
Tactic: induction x using Finsupp.induction with
  | zero => simp
  | single_add a b f _ _ ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : CommSemiring S
inst_5 : Algebra S A
inst_6 : Algebra R S
inst_7 : IsScalarTower R S A
f : MonoidHom.{u_7, u_4} (Multiplicative M) A
x : R[M]
zero :
  Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) 0) :
      A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) 0 : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
        ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) x : S[M]) :
      A)
    ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) x : A)
have single_add : ∀ (a : M) (b : R) (f_1 : M →₀ R),
  a ∉ f_1.support →
    b ≠ 0 →
      ∀
        (ih :
          Eq.{u_4 + 1} (α := A)
            ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
                ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) f_1 : S[M]) :
              A)
            ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A) f_1 : A)),
        Eq.{u_4 + 1} (α := A)
          ((((lift S A M : (a : Multiplicative M →* A) → S[M] →ₐ[S] A) f : S[M] →ₐ[S] A) : (a : S[M]) → A)
              ((mapRingHom M (algebraMap R S) : (a : R[M]) → S[M]) (Finsupp.single a b + f_1) : S[M]) :
            A)
          ((((lift R A M : (a : Multiplicative M →* A) → R[M] →ₐ[R] A) f : R[M] →ₐ[R] A) : (a : R[M]) → A)
              (Finsupp.single a b + f_1) :
            A)
Tactic: induction x using Finsupp.induction with
  | zero => simp
  | single_add a b f _ _ ih => simp [ih]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (domCongr R A 1) 1
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((domCongr R A 1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x x_1 : AddAut M
⊢ domCongr R A (x * x_1) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1)
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((domCongr R A (x * x_1) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (domCongr R A x) (domCongr R A x_1) : (a : A[M]) → A[M]) a : A[M]) :
          (a : M) → A)
        m :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
⊢ Eq (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M 1) 1
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M 1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((1 : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : AddMonoid M
inst_2 : Semiring A
inst_3 : Algebra R A
x y : A ≃ₐ[R] A
⊢ mapAlgEquiv R M (x * y) = HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M x) (mapAlgEquiv R M y)
have h : ∀ (a : A[M]) (m : M),
  Eq.{u_4 + 1} (α := A) ((((mapAlgEquiv R M (x * y) : (a : A[M]) → A[M]) a : A[M]) : (a : M) → A) m : A)
    ((((HMul.hMul (α := A[M] ≃ₐ[R] A[M]) (mapAlgEquiv R M x) (mapAlgEquiv R M y) : (a : A[M]) → A[M]) a : A[M]) :
          (a : M) → A)
        m :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
r : R
⊢ Eq (α := R[M]) (erase m (single m r)) 0
have simp : Eq (α := R[M]) 0 0
Tactic: simp [erase, ofCoeff, coeff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
A : Type u_8
inst_1 : SMulZeroClass A R
a : A
m : M
r : R
⊢ HSMul.hSMul (β := R[M]) a (single m r) = single m (a • r)
have hfg : ∀ (m_1 : M),
  Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := R[M]) a (single m r) : (a : M) → R) m_1 : R)
    ((single m (a • r) : (a : M) → R) m_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Mul M
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c
have simp : ∀ (a b c : R[M]),
  (sum a fun (m₁ : M) (r₁ : R) ↦ sum (b + c) fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
    HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum b fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
      (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
Tactic: simp [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Mul M
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c
have classical : ∀ (a b c : R[M]),
  (sum a fun (m₁ : M) (r₁ : R) ↦ sum (b + c) fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
    HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum b fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
      (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
Tactic: classical simp [mul_def]; simp [MonoidAlgebra, sum_add_index, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Mul M
⊢ ∀ (a b c : R[M]), (a + b) * c = a * c + b * c
have simp : ∀ (a b c : R[M]),
  (sum (a + b) fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
    HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
      (sum b fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
Tactic: simp [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Mul M
⊢ ∀ (a b c : R[M]), (a + b) * c = a * c + b * c
have classical : ∀ (a b c : R[M]),
  (sum (a + b) fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
    HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
      (sum b fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
Tactic: classical simp [mul_def]; simp [MonoidAlgebra, sum_add_index, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m : M
⊢ Eq (α := R) ((x * y : (a : M) → R) m : R)
    (sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : R)
have rw : Eq (α := R) (sum x fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
  (sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0)
Tactic: rw [mul_def, Finsupp.sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m : M
⊢ Eq (α := R) (sum x fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
    (sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0)
have e_g : Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
  fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m : M
⊢ Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
    fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
have e_g : ∀ (x : M) (x_1 : R),
  Eq (α := R) ((sum y fun (m₂ : M) (r₂ : R) ↦ single (x * m₂) (x_1 * r₂) : (a : M) → R) m : R)
    (sum y fun (m₂ : M) (r₂ : R) ↦ if x * m₂ = m then x_1 * r₂ else 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m x_1 : M
x_2 : R
⊢ Eq (α := R) ((sum y fun (m₂ : M) (r₂ : R) ↦ single (x_1 * m₂) (x_2 * r₂) : (a : M) → R) m : R)
    (sum y fun (m₂ : M) (r₂ : R) ↦ if x_1 * m₂ = m then x_2 * r₂ else 0 : R)
have e_g : Eq (α := R) (sum y fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m)
  (sum y fun (m₂ : M) (r₂ : R) ↦ if x_1 * m₂ = m then x_2 * r₂ else 0)
Tactic: rw [Finsupp.sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m x_1 : M
x_2 : R
⊢ Eq (α := R) (sum y fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m)
    (sum y fun (m₂ : M) (r₂ : R) ↦ if x_1 * m₂ = m then x_2 * r₂ else 0)
have e_g : Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m) fun (m₂ : M) (r₂ : R) ↦
  if x_1 * m₂ = m then x_2 * r₂ else 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m x_1 : M
x_2 : R
⊢ Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m) fun (m₂ : M) (r₂ : R) ↦
    if x_1 * m₂ = m then x_2 * r₂ else 0
have e_g : ∀ (x : M) (x_3 : R), (single (x_1 * x) (x_2 * x_3) : (a : M) → R) m = if x_1 * x = m then x_2 * x_3 else 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
⊢ Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
    (∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m,
      HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
have rw : Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
  (∑ a ∈ x.support ×ˢ y.support,
    if a.1 * a.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) a.1 : R) ((y : (a : M) → R) a.2 : R) else 0)
Tactic: rw [Finset.sum_filter, Finset.sum_product]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
rw :
  Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
    (∑ a ∈ x.support ×ˢ y.support,
      if a.1 * a.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) a.1 : R) ((y : (a : M) → R) a.2 : R) else 0)
⊢ Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
    (∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m,
      HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
have rw₁ : Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
  (∑ x_1 ∈ x.support,
    ∑ y_1 ∈ y.support,
      if (x_1, y_1).1 * (x_1, y_1).2 = m then
        HMul.hMul (α := R) (β := R) ((x : (a : M) → R) (x_1, y_1).1 : R) ((y : (a : M) → R) (x_1, y_1).2 : R)
      else 0)
Tactic: rw [Finset.sum_filter, Finset.sum_product]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
⊢ Eq.{u_1 + 1} (α := R)
    (∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m,
      HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
    (∑ p ∈ s with p.1 ∈ x.support ∧ p.2 ∈ y.support,
      HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
have h : {p ∈ x.support ×ˢ y.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
⊢ {p ∈ x.support ×ˢ y.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}
have h : ∀ (a : M × M), a ∈ {p ∈ x.support ×ˢ y.support | p.1 * p.2 = m} ↔ a ∈ {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (hypothesis)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
p : M × M
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
have hp₁ : p ∈ s →
  Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R) → Eq.{u_1 + 1} (α := R) ((y : (a : M) → R) p.2 : R) (0 : R)
Tactic: simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
p : M × M
hps : p ∈ s
hp :
  p ∈ s →
    Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R) →
      Eq.{u_1 + 1} (α := R) ((y : (a : M) → R) p.2 : R) (0 : R)
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
have pos : ∀ (h1 : Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R)),
  HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
Tactic: by_cases h1 : x p.1 = 0