awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
induction : ∀ (x : Finset A) (hg : g₁.support ∪ g₂.support = x), g₁ = g₂
⊢ g₁ = g₂

Tactic:
induction hg : g₁.support ∪ g₂.support using Finset.eraseInduction generalizing g₁ g₂ with
    | _ s ih =>
    obtain h | h := s.eq_empty_or_nonempty <;> subst s
    · simp_rw [Finset.union_eq_empty, support_eq_empty] at h; exact h.1.trans h.2.symm
    obtain ⟨af, haf, ag, hag, uniq⟩ :=
      UniqueProds.uniqueMul_of_nonempty (support_nonempty_iff.2 hf) h
    have h := mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
    dsimp only at eq
    rw [eq, mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
    have := mul_left_cancel₀ (mem_support_iff.mp haf) h
    rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
    simp_rw [mul_add, add_right_cancel_iff] at eq
    rw [ih ag hag eq]
    simp_rw [support_erase, Finset.erase_union_distrib]

Premises used: Finsupp.support, Finsupp.support_erase, Finset.union_eq_empty, Finset.erase_union_distrib, add_right_cancel_iff, Finset.eraseInduction, mul_add, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
induction : ∀ (x : Finset A) (hg : g₁.support ∪ g₂.support = x), g₁ = g₂
⊢ g₁ = g₂

Tactic:
classical
    induction hg : g₁.support ∪ g₂.support using Finset.eraseInduction generalizing g₁ g₂ with
    | _ s ih =>
    obtain h | h := s.eq_empty_or_nonempty <;> subst s
    · simp_rw [Finset.union_eq_empty, support_eq_empty] at h; exact h.1.trans h.2.symm
    obtain ⟨af, haf, ag, hag, uniq⟩ :=
      UniqueProds.uniqueMul_of_nonempty (support_nonempty_iff.2 hf) h
    have h := mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
    dsimp only at eq
    rw [eq, mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
    have := mul_left_cancel₀ (mem_support_iff.mp haf) h
    rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
    simp_rw [mul_add, add_right_cancel_iff] at eq
    rw [ih ag hag eq]
    simp_rw [support_erase, Finset.erase_union_distrib]

Premises used: Finsupp.support, Finsupp.support_erase, Finset.union_eq_empty, Finset.erase_union_distrib, add_right_cancel_iff, Finset.eraseInduction, mul_add, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsRightCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
⊢ IsRightCancelMulZero R[A]

Tactic:
MulOpposite.isLeftCancelMulZero_iff.mp <|
    MonoidAlgebra.opRingEquiv.injective.isLeftCancelMulZero _ (map_zero _) (map_mul _)

Premises used: RingEquiv.injective, map_zero, MonoidAlgebra.opRingEquiv, map_mul, Iff.mp, Function.Injective.isLeftCancelMulZero, MulOpposite.isLeftCancelMulZero_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
⊢ ∀ (x y : R[M]ᵐᵒᵖ),
    (AddEquiv.toAddMonoidHom
            (AddEquiv.trans (AddEquiv.symm opAddEquiv)
              (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
          (a : (M →₀ R)ᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
        (x * y) =
      HMul.hMul (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ) (β := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
        ((AddEquiv.toAddMonoidHom
                (AddEquiv.trans (AddEquiv.symm opAddEquiv)
                  (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
              (a : (M →₀ R)ᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
            x :
          Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ)
        ((AddEquiv.toAddMonoidHom
                (AddEquiv.trans (AddEquiv.symm opAddEquiv)
                  (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
              (a : (M →₀ R)ᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
            y :
          Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ)

Tactic:
(AddMonoidHom.map_mul_iff (R := R[M]ᵐᵒᵖ) (S := Rᵐᵒᵖ[Mᵐᵒᵖ]) _).mpr ?_

Premises used: Iff.mpr, AddMonoidHom.map_mul_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
refine :
  Eq (α := R[M]ᵐᵒᵖ →+ R[M]ᵐᵒᵖ →+ MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
    (AddMonoidHom.compr₂ (P := R[M]ᵐᵒᵖ) AddMonoidHom.mul
      (AddEquiv.toAddMonoidHom
        (AddEquiv.trans (AddEquiv.symm opAddEquiv)
          (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv)))))
    (AddMonoidHom.compl₂ (N := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
      (AddMonoidHom.comp AddMonoidHom.mul
          (AddEquiv.toAddMonoidHom
            (AddEquiv.trans (AddEquiv.symm opAddEquiv)
              (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv)))) :
        R[M]ᵐᵒᵖ →+ MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ →+ MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
      (AddEquiv.toAddMonoidHom
          (AddEquiv.trans (AddEquiv.symm opAddEquiv)
            (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
        (M →₀ R)ᵐᵒᵖ →+ Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ))
⊢ ∀ (x y : R[M]ᵐᵒᵖ),
    (AddEquiv.toAddMonoidHom
            (AddEquiv.trans (AddEquiv.symm opAddEquiv)
              (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
          (a : (M →₀ R)ᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
        (x * y) =
      HMul.hMul (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ) (β := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
        ((AddEquiv.toAddMonoidHom
                (AddEquiv.trans (AddEquiv.symm opAddEquiv)
                  (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
              (a : (M →₀ R)ᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
            x :
          Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ)
        ((AddEquiv.toAddMonoidHom
                (AddEquiv.trans (AddEquiv.symm opAddEquiv)
                  (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
              (a : (M →₀ R)ᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
            y :
          Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ)

Tactic:
refine (AddMonoidHom.map_mul_iff (R := R[M]ᵐᵒᵖ) (S := Rᵐᵒᵖ[Mᵐᵒᵖ]) _).mpr ?_

Premises used: Iff.mpr, AddMonoidHom.map_mul_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
m : M
x : R
m_1 : M
x_1 : R
m_2 : Mᵐᵒᵖ
h :
  Eq.{u_1 + 1} (α := Rᵐᵒᵖ)
    ((((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (HMul.hMul (α := R[M])
                  (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1)))
                  (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x))))) :
            Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
    ((HMul.hMul (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x)))))
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1))))) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ)
    ((((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop
                  (HMul.hMul (α := R[M]ᵐᵒᵖ) (β := R[M]ᵐᵒᵖ)
                    (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x) : R[M]ᵐᵒᵖ)
                    (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1) : R[M]ᵐᵒᵖ)))) :
            Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
    ((HMul.hMul (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x)))))
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1))))) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)

Tactic:
rw [MulOpposite.unop_mul (α := R[M])]

Premises used: MulOpposite.unop_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
m : M
x : R
m_1 : M
x_1 : R
m_2 : Mᵐᵒᵖ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ)
    ((((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (HMul.hMul (α := R[M])
                  (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1)))
                  (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x))))) :
            Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
    ((HMul.hMul (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x)))))
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1))))) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
r : R
x : M
⊢ Eq (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
    ((MonoidAlgebra.opRingEquiv : (a : R[M]ᵐᵒᵖ) → Rᵐᵒᵖ[Mᵐᵒᵖ]) (op (single x r)) : MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
    (single (op x) (op r) : MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
⊢ Eq (α := R[M]ᵐᵒᵖ) ((RingEquiv.symm MonoidAlgebra.opRingEquiv : (a : Rᵐᵒᵖ[Mᵐᵒᵖ]) → R[M]ᵐᵒᵖ) (single x r) : R[M]ᵐᵒᵖ)
    (op (single (unop x) (unop r)) : R[M]ᵐᵒᵖ)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : Zero V
f : R[G]
x : P → V
p : P
gh : G × P
rw :
  gh.1 ∈ (↑f.support : Set G) ∧ gh.2 ∈ Function.support x ∧ gh.1 • gh.2 = p ↔
    Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) gh.1 : R) (0 : R) ∧ x gh.2 ≠ 0 ∧ gh.2 = gh.1⁻¹ • p
rw₁ :
  gh.1 ∈ (↑f.support : Set G) ∧ gh.2 ∈ Function.support x ∧ gh.1 • gh.2 = p ↔
    Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) gh.1 : R) (0 : R) ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p
rw₂ :
  gh.1 ∈ (↑f.support : Set G) ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p ↔
    Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) gh.1 : R) (0 : R) ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p
rw₃ :
  gh.1 ∈ f.support ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p ↔
    Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) gh.1 : R) (0 : R) ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p
rw₄ rw₅ :
  Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) gh.1 : R) (0 : R) ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p ↔
    Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) gh.1 : R) (0 : R) ∧ x gh.2 ≠ 0 ∧ gh.1 • gh.2 = p
⊢ gh ∈ Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p ⋯ ↔
    Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) gh.1 : R) (0 : R) ∧ x gh.2 ≠ 0 ∧ gh.2 = gh.1⁻¹ • p

Tactic:
rw [Finset.mem_smulAntidiagonal, eq_inv_smul_iff, Function.mem_support, Finset.mem_coe,
    Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, Function.mem_support, Finset.mem_smulAntidiagonal, Finset.mem_coe, eq_inv_smul_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : SMul G P
inst_1 : IsLeftCancelSMul G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
⊢ (f • x) p =
    ∑ gh ∈ Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp,
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) gh.1 : R) (x gh.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
⊢ ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite

Tactic:
have hp : ((f.support : Set G).smulAntidiagonal (Function.support x) p).Finite :=
    Set.SMulAntidiagonal.finite_of_finite_fst f.support.finite_toSet x.support p
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
x_1 : G × P
h₁ : x_1 ∈ s
x_2 : G × P
h₂ : x_2 ∈ s
h : x_1.1 = x_2.1
rw :
  ∀ (h₁ : Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) x_1.1 : R) (0 : R) ∧ x x_1.2 ≠ 0 ∧ x_1.2 = x_1.1⁻¹ • p) (x_3 : G × P)
    (h₂ : Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) x_3.1 : R) (0 : R) ∧ x x_3.2 ≠ 0 ∧ x_3.2 = x_3.1⁻¹ • p)
    (h : x_1.1 = x_3.1), x_1 = x_3
⊢ x_1 = x_2

Tactic:
rw [Finset.mem_coe, mem_smulAntidiagonal_of_group] at h₁ h₂

Premises used: MonoidAlgebra.mem_smulAntidiagonal_of_group, Finset.mem_coe
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
x_1 : G × P
h₁ : Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) x_1.1 : R) (0 : R) ∧ x x_1.2 ≠ 0 ∧ x_1.2 = x_1.1⁻¹ • p
x_2 : G × P
h₂ : Ne.{u_3 + 1} (α := R) ((f : (a : G) → R) x_2.1 : R) (0 : R) ∧ x x_2.2 ≠ 0 ∧ x_2.2 = x_2.1⁻¹ • p
h : x_1.1 = x_2.1
⊢ x_1 = x_2

Tactic:
aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
⊢ Set.InjOn Prod.fst s

Tactic:
have h₁ : s.InjOn Prod.fst := fun _ h₁ _ h₂ h ↦ by
    rw [Finset.mem_coe, mem_smulAntidiagonal_of_group] at h₁ h₂
    aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
g : G × P
hg : g ∈ s
⊢ g.1 ∈ (↑f.support : Set G)

Tactic:
aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
⊢ Set.MapsTo Prod.fst s (↑f.support : Set G)

Tactic:
have h₂ : s.MapsTo Prod.fst ↑f.support := fun g hg ↦ by aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
g : G
hg : g ∈ f.support
hgn : g ∉ Prod.fst '' s
⊢ Eq.{u_3 + 1} (α := R) ((f : (a : G) → R) g : R) (0 : R) ∨ ∀ (q : P), ¬x q = 0 → ¬g • q = p

Tactic:
aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
g : G
hg : g ∈ f.support
hgn : g ∉ Prod.fst '' s
inl :
  ∀ (h : Eq.{u_3 + 1} (α := R) ((f : (a : G) → R) g : R) (0 : R)),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0
inr :
  ∀ (h : ∀ (q : P), ¬x q = 0 → ¬g • q = p),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0

Tactic:
obtain (h | h) : f g = 0 ∨ ∀ q, ¬ x q = 0 → ¬g • q = p := by aesop

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
g : G
hg : g ∈ f.support
hgn : g ∉ Prod.fst '' s
h : Eq.{u_3 + 1} (α := R) ((f : (a : G) → R) g : R) (0 : R)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
g : G
hg : g ∈ f.support
hgn : g ∉ Prod.fst '' s
h : ∀ (q : P), ¬x q = 0 → ¬g • q = p
⊢ ¬x (g⁻¹ • p) = 0 → ¬g • g⁻¹ • p = p

Tactic:
have := h (g⁻¹ • p)
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
g : G
hg : g ∈ f.support
hgn : g ∉ Prod.fst '' s
h : ∀ (q : P), ¬x q = 0 → ¬g • q = p
this : ¬x (g⁻¹ • p) = 0 → ¬g • g⁻¹ • p = p
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
⊢ ∀ (g : G) (hg : g ∈ f.support) (hgn : g ∉ Prod.fst '' s),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0

Tactic:
have h₃ (g : G) (hg : g ∈ f.support) (hgn : g ∉ Prod.fst '' s) : f g • x (g⁻¹ • p) = 0 := by
    obtain (h | h) : f g = 0 ∨ ∀ q, ¬ x q = 0 → ¬g • q = p := by aesop
    · simp [h]
    · have := h (g⁻¹ • p)
      aesop
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
h₃ :
  ∀ (g : G) (hg : g ∈ f.support) (hgn : g ∉ Prod.fst '' s),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0
rw :
  ∀ i ∈ Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp,
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i.1 : R) (x i.2) =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i.1 : R) (x (i.1⁻¹ • p))
⊢ (f • x) p = ∑ i ∈ f.support, HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i : R) (x (i⁻¹ • p))

Tactic:
rw [smul_eq, Finset.sum_of_injOn Prod.fst h₁ h₂ h₃]

Premises used: Finset.sum_of_injOn, Finsupp.support, Set.SMulAntidiagonal.finite_of_finite_fst, Prod.fst, MonoidAlgebra.smul_eq, Function.support, Finset.finite_toSet
-- Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
Goal:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst : Group G
inst_1 : MulAction G P
inst_2 : Semiring R
inst_3 : AddCommMonoid V
inst_4 : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.support : Set G).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := (↑(Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp) : Set (G × P))
h₁ : Set.InjOn Prod.fst s
h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
h₃ :
  ∀ (g : G) (hg : g ∈ f.support) (hgn : g ∉ Prod.fst '' s),
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0
⊢ ∀ i ∈ Finset.SMulAntidiagonal (s := (↑f.support : Set G)) (t := Function.support x) p hp,
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i.1 : R) (x i.2) =
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i.1 : R) (x (i.1⁻¹ • p))

Tactic:
aesop