awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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]
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h_1 : (g₁.support ∪ g₂.support).Nonempty
af : A
haf : af ∈ f.support
ag : A
hag : ag ∈ g₁.support ∪ g₂.support
uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag
h :
  HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₂ : (a : A) → R) ag : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)
this : Eq.{u_1 + 1} (α := R) ((g₂ : (a : A) → R) ag : R) ((g₁ : (a : A) → R) ag : R)
eq : f * Finsupp.erase ag g₁ = f * Finsupp.erase ag g₂
⊢ HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₁) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R) =
    HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₂) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R)
have H : (Finsupp.erase ag g₁).support ∪ (Finsupp.erase ag g₂).support = (g₁.support ∪ g₂.support).erase ag
Tactic: rw [ih ag hag eq]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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₂)
⊢ g₁ = g₂
have induction : ∀ (x : Finset A) (hg : g₁.support ∪ g₂.support = x), 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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₂)
⊢ g₁ = g₂
have induction : ∀ (x : Finset A) (hg : g₁.support ∪ g₂.support = x), 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Opposite (goal)
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ᵐᵒᵖ)
have 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ᵐᵒᵖ))
Tactic: refine (AddMonoidHom.map_mul_iff (R := R[M]ᵐᵒᵖ) (S := Rᵐᵒᵖ[Mᵐᵒᵖ]) _).mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Opposite (goal)
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ᵐᵒᵖ)
                (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ᵐᵒᵖ)
have 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ᵐᵒᵖ)
Tactic: rw [MulOpposite.unop_mul (α := R[M])]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.mem_smulAntidiagonal, eq_inv_smul_iff, Function.mem_support, Finset.mem_coe,
    Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.mem_smulAntidiagonal, eq_inv_smul_iff, Function.mem_support, Finset.mem_coe,
    Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.mem_smulAntidiagonal, eq_inv_smul_iff, Function.mem_support, Finset.mem_coe,
    Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.mem_smulAntidiagonal, eq_inv_smul_iff, Function.mem_support, Finset.mem_coe,
    Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.mem_smulAntidiagonal, eq_inv_smul_iff, Function.mem_support, Finset.mem_coe,
    Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (hypothesis)
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 • x) p = ∑ i ∈ f.support, HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i : R) (x (i⁻¹ • p))
have hp : ((↑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
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ x_1 = x_2
have 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
Tactic: rw [Finset.mem_coe, mem_smulAntidiagonal_of_group] at h₁ h₂
Cleared hypotheses: h₁, x_2, h₂, h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (hypothesis)
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))
⊢ (f • x) p = ∑ i ∈ f.support, HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i : R) (x (i⁻¹ • p))
have h₁ : 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
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (hypothesis)
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
⊢ (f • x) p = ∑ i ∈ f.support, HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i : R) (x (i⁻¹ • p))
have h₂ : Set.MapsTo Prod.fst s (↑f.support : Set G)
Tactic: have h₂ : s.MapsTo Prod.fst ↑f.support := fun g hg ↦ by aesop
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
have 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
Tactic: obtain (h | h) : f g = 0 ∨ ∀ q, ¬ x q = 0 → ¬g • q = p := by aesop
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0
have 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
Tactic: obtain (h | h) : f g = 0 ∨ ∀ q, ¬ x q = 0 → ¬g • q = p := by aesop
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (hypothesis)
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
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) g : R) (x (g⁻¹ • p)) = 0
have this : ¬x (g⁻¹ • p) = 0 → ¬g • g⁻¹ • p = p
Tactic: have := h (g⁻¹ • p)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (hypothesis)
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)
⊢ (f • x) p = ∑ i ∈ f.support, HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i : R) (x (i⁻¹ • p))
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.PointwiseSMul (goal)
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
⊢ (f • x) p = ∑ i ∈ f.support, HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((f : (a : G) → R) i : R) (x (i⁻¹ • p))
have 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))
Tactic: rw [smul_eq, Finset.sum_of_injOn Prod.fst h₁ h₂ h₃]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
a b : k[G]
⊢ (a * b).support ⊆ a.support * b.support
have rw : support.{u₂, u₁} (M := k) (sum a fun (m₁ : G) (r₁ : k) ↦ sum b fun (m₂ : G) (r₂ : k) ↦ single (m₁ * m₂) (r₁ * r₂)) ⊆
  a.support * b.support
Tactic: rw [MonoidAlgebra.mul_def]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
a : G
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) {a} f.support) (image (fun (x : G) ↦ a * x) f.support)
have rw : Subset (α := Finset G) (image (fun (b : G) ↦ a * b) f.support) (image (fun (b : G) ↦ a * b) f.support)
Tactic: rw [Finset.image₂_singleton_left]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
a : G
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) f.support {a}) (image (fun (x : G) ↦ x * a) f.support)
have rw : Subset (α := Finset G) (image (fun (a_1 : G) ↦ a_1 * a) f.support) (image (fun (a_1 : G) ↦ a_1 * a) f.support)
Tactic: rw [Finset.image₂_singleton_right]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
⊢ (single x r * f).support = image (fun (x_1 : G) ↦ x * x_1) f.support
have refine : ∀ (y : G) (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) y),
  y ∈ (single x r * f).support
Tactic: refine subset_antisymm (support_single_mul_subset f _ _) fun y hy => ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Support (goal)
Goal:
k : Type u₁
G : Type u₂
inst : Semiring k
inst_1 : Mul G
inst_2 : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) y
⊢ y ∈ (single x r * f).support
have obtain : ∀ (y : G) (yf : y ∈ f.support)
  (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) (x * y)),
  x * y ∈ (single x r * f).support
Tactic: obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by grind
Cleared hypotheses: y, hy