awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a m c : G
hc : c ∈ x.support
hfg : a + c = a + m ↔ c = m
⊢ c + a = a + m ↔ c = m

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a m c : G
hc : c ∈ x.support
⊢ a + c = a + m ↔ c = m

Tactic:
add_right_inj _

Premises used: add_right_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a m c : G
hc : c ∈ x.support
⊢ a + c = a + m ↔ c = m

Tactic:
exact add_right_inj _

Premises used: add_right_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
a : G
⊢ Eq (α := k[G]) (of' k G a /ᵒᶠ a) 1

Tactic:
simpa only [one_mul] using mul_of'_divOf (1 : k[G]) a

Premises used: OfNat.ofNat, one_mul, AddMonoidAlgebra.mul_of'_divOf
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
⊢ Eq.{u_1 + 1} (α := k) ((x %ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)

Tactic:
Finsupp.filter_apply_pos _ _ h

Premises used: Finsupp.filter_apply_pos
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
⊢ Eq.{u_1 + 1} (α := k) ((x %ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)

Tactic:
exact Finsupp.filter_apply_pos _ _ h

Premises used: Finsupp.filter_apply_pos
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
⊢ Eq.{u_1 + 1} (α := k) ((x %ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)

Tactic:
classical exact Finsupp.filter_apply_pos _ _ h
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h rwa rwa₁ rwa₂ rwa₃ : ∃ (g₂ : G), g' = g + g₂
⊢ ¬¬∃ (g₂ : G), g' = g + g₂

Tactic:
rwa [Classical.not_not]

Premises used: Classical.not_not
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ∃ (d : G), g' = g + d
⊢ Eq.{u_1 + 1} (α := k) ((x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)

Tactic:
exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]

Premises used: Finsupp.filter_apply_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ∃ (d : G), g' = g + d
⊢ Eq.{u_1 + 1} (α := k) ((x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)

Tactic:
classical exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]

Premises used: Finsupp.filter_apply_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g d : G
⊢ Eq.{u_1 + 1} (α := k) ((x %ᵒᶠ g : (a : G) → k) (d + g) : k) (0 : k)

Tactic:
modOf_apply_of_exists_add _ _ _ ⟨_, add_comm _ _⟩

Premises used: AddMonoidAlgebra.modOf_apply_of_exists_add, add_comm, Exists.intro
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g d : G
⊢ Eq.{u_1 + 1} (α := k) ((x %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)

Tactic:
modOf_apply_of_exists_add _ _ _ ⟨_, rfl⟩

Premises used: AddMonoidAlgebra.modOf_apply_of_exists_add, Exists.intro, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
hfg : ∀ (g' : G), Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
ext g'
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)

Tactic:
rw [Finsupp.zero_apply]

Premises used: Finsupp.zero_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
hfg : ∀ (d : G), Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
hfg₁ : ∀ (h : ¬∃ (d : G), g' = g + d), Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Premises used: Exists, em, HAdd.hAdd, Eq, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
d : G
hfg hfg₁ : Eq.{u_1 + 1} (α := k) 0 0
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)

Tactic:
rw [modOf_apply_self_add]

Premises used: AddMonoidAlgebra.modOf_apply_self_add
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ (d : G), g' = g + d
hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * x : (a : G) → k) g' : k) (0 : k)
hfg₁ : Eq.{u_1 + 1} (α := k) ((single g 1 * x : (a : G) → k) g' : k) (0 : k)
hfg₂ hfg₃ : Eq.{u_1 + 1} (α := k) 0 0
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)

Tactic:
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]

Premises used: AddMonoidAlgebra.modOf_apply_of_not_exists_add, AddMonoidAlgebra.single_mul_apply_of_not_exists_add, AddMonoidAlgebra.of'_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g : G
hfg : ∀ (g' : G), Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)
⊢ x * of' k G g %ᵒᶠ g = 0

Tactic:
ext g'
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
hfg : Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)

Tactic:
rw [Finsupp.zero_apply]

Premises used: Finsupp.zero_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
hfg : ∀ (d : G), Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
hfg₁ : ∀ (h : ¬∃ (d : G), g' = g + d), Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Premises used: Exists, em, HAdd.hAdd, Eq, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g d : G
hfg hfg₁ : Eq.{u_1 + 1} (α := k) 0 0
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)

Tactic:
rw [modOf_apply_self_add]

Premises used: AddMonoidAlgebra.modOf_apply_self_add
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
hfg : ¬∃ (d : G), g' = d + g
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)

Tactic:
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]

Premises used: AddMonoidAlgebra.modOf_apply_of_not_exists_add, AddMonoidAlgebra.of'_apply, AddMonoidAlgebra.mul_single_apply_of_not_exists_add
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
⊢ ¬∃ (d : G), g' = d + g

Tactic:
simpa only [add_comm] using h

Premises used: add_comm
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
⊢ Eq (α := k[G]) (of' k G g %ᵒᶠ g) 0

Tactic:
simpa only [one_mul] using mul_of'_modOf (1 : k[G]) g

Premises used: AddMonoidAlgebra.mul_of'_modOf, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
hfg :
  ∀ (g' : G), Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)
⊢ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x

Tactic:
ext g'
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
hfg :
  HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)

Tactic:
rw [Finsupp.add_apply]

Premises used: Finsupp.add_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
hfg :
  ∀ (d : G),
    HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k)
        ((x %ᵒᶠ g : (a : G) → k) (g + d) : k) =
      (x : (a : G) → k) (g + d)
hfg₁ :
  ∀ (h : ¬∃ (d : G), g' = g + d),
    HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
      (x : (a : G) → k) g'
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Premises used: Exists, em, HAdd.hAdd, Eq, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
hfg :
  HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
hfg₁ :
  HAdd.hAdd (α := k) (β := k) ((single g 1 * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
hfg₂ : HAdd.hAdd (α := k) (β := k) (0 : k) ((x : (a : G) → k) g' : k) = (x : (a : G) → k) g'
hfg₃ hfg₄ : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'

Tactic:
rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
      zero_add]

Premises used: AddMonoidAlgebra.modOf_apply_of_not_exists_add, zero_add, AddMonoidAlgebra.single_mul_apply_of_not_exists_add, AddMonoidAlgebra.of'_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g d : G
hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k) ((x : (a : G) → k) (g + d) : k)
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k)
      ((x %ᵒᶠ g : (a : G) → k) (g + d) : k) =
    (x : (a : G) → k) (g + d)

Tactic:
rw [modOf_apply_self_add, add_zero]

Premises used: AddMonoidAlgebra.modOf_apply_self_add, add_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g d : G
hfg : ∀ m' ∈ (x /ᵒᶠ g).support, g + m' = g + d ↔ m' = d
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k) ((x : (a : G) → k) (g + d) : k)

Tactic:
rw [of'_apply, single_mul_apply_aux, one_mul, divOf_apply]

Premises used: AddMonoidAlgebra.divOf_apply, AddMonoidAlgebra.of'_apply, AddMonoidAlgebra.single_mul_apply_aux, one_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g d a : G
ha : a ∈ (x /ᵒᶠ g).support
⊢ g + a = g + d ↔ a = d

Tactic:
add_right_inj _

Premises used: add_right_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g d a : G
ha : a ∈ (x /ᵒᶠ g).support
⊢ g + a = g + d ↔ a = d

Tactic:
exact add_right_inj _

Premises used: add_right_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
rw : of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x
rw₁ rw₂ : x = x
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x

Tactic:
rw [add_comm, divOf_add_modOf]

Premises used: add_comm, AddMonoidAlgebra.divOf_add_modOf
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
mp : of' k G g ∣ x → x %ᵒᶠ g = 0
mpr : x %ᵒᶠ g = 0 → of' k G g ∣ x
⊢ of' k G g ∣ x ↔ x %ᵒᶠ g = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
g : G
x : k[G]
mp mp₁ : Eq (α := k[G]) 0 0
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
rw [of'_mul_modOf]

Premises used: AddMonoidAlgebra.of'_mul_modOf
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
mpr : of' k G g ∣ of' k G g * (x /ᵒᶠ g)
⊢ of' k G g ∣ x

Tactic:
rw [← divOf_add_modOf x g, h, add_zero]

Premises used: AddMonoidAlgebra.divOf_add_modOf, add_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : CommSemiring R
f : M → ι
i : ι
a b : R[M]
ha : Membership.mem (γ := Set R[M]) {a : R[M] | ∀ m ∈ a.support, f m = i} a
hb : Membership.mem (γ := Set R[M]) {a : R[M] | ∀ m ∈ a.support, f m = i} b
m : M
h : m ∈ (a + b).support
⊢ f m = i

Tactic:
(Finset.mem_union.mp (Finsupp.support_add h)).elim (ha m) (hb m)

Premises used: Finsupp.support_add, Iff.mp, Finset.mem_union, Or.elim
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : CommSemiring R
f : M → ι
i : ι
a b : R[M]
ha : Membership.mem (γ := Set R[M]) {a : R[M] | ∀ m ∈ a.support, f m = i} a
hb : Membership.mem (γ := Set R[M]) {a : R[M] | ∀ m ∈ a.support, f m = i} b
m : M
h : m ∈ (a + b).support
⊢ f m = i

Tactic:
exact (Finset.mem_union.mp (Finsupp.support_add h)).elim (ha m) (hb m)

Premises used: Finsupp.support_add, Iff.mp, Finset.mem_union, Or.elim
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : CommSemiring R
f : M → ι
i : ι
a b : R[M]
ha : Membership.mem (γ := Set R[M]) {a : R[M] | ∀ m ∈ a.support, f m = i} a
hb : Membership.mem (γ := Set R[M]) {a : R[M] | ∀ m ∈ a.support, f m = i} b
m : M
h : m ∈ (a + b).support
⊢ f m = i

Tactic:
classical exact (Finset.mem_union.mp (Finsupp.support_add h)).elim (ha m) (hb m)
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : CommSemiring R
f : M → ι
i : ι
m : M
h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) 0) m
⊢ f m = i

Tactic:
cases h
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := (i : M) → Submodule R R[M]) (gradeBy R id) (grade R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : CommSemiring R
f : M → ι
i : ι
a : R[M]
⊢ Membership.mem (γ := Submodule R R[M]) (gradeBy R f i) a ↔ (↑a.support : Set M) ⊆ f ⁻¹' {i}

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
rw : Membership.mem (γ := Submodule R R[M]) (grade R m) a ↔ (↑a.support : Set M) ⊆ {m}
⊢ Membership.mem (γ := Submodule R R[M]) (grade R m) a ↔ a.support ⊆ {m}

Tactic:
rw [← Finset.coe_subset, Finset.coe_singleton]

Premises used: Finset.coe_singleton, Finset.coe_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
⊢ Membership.mem (γ := Submodule R R[M]) (grade R m) a ↔ (↑a.support : Set M) ⊆ {m}

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
rw :
  (∃ (b : R), a = Finsupp.single m b) ↔ Membership.mem (γ := Submodule R R[M]) (LinearMap.range (Finsupp.lsingle m)) a
⊢ Membership.mem (γ := Submodule R R[M]) (grade R m) a ↔
    Membership.mem (γ := Submodule R R[M]) (LinearMap.range (Finsupp.lsingle m)) a

Tactic:
rw [mem_grade_iff, Finsupp.support_subset_singleton']

Premises used: AddMonoidAlgebra.mem_grade_iff, Finsupp.support_subset_singleton'
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
h : ∀ (a_1 : R), a = Finsupp.single m a_1 ↔ (Finsupp.lsingle m : (a : R) → R[M]) a_1 = a
⊢ (∃ (b : R), a = Finsupp.single m b) ↔ Membership.mem (γ := Submodule R R[M]) (LinearMap.range (Finsupp.lsingle m)) a

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
r : R
h : a = Finsupp.single m r → (Finsupp.lsingle m : (a : R) → R[M]) r = a
h₁ : (Finsupp.lsingle m : (a : R) → R[M]) r = a → a = Finsupp.single m r
⊢ a = Finsupp.single m r ↔ (Finsupp.lsingle m : (a : R) → R[M]) r = a

Tactic:
constructor
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
r : R
⊢ a = Finsupp.single m r → (Finsupp.lsingle m : (a : R) → R[M]) r = a

Tactic:
Eq.symm

Premises used: AddMonoidAlgebra, Eq.symm, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
r : R
⊢ a = Finsupp.single m r → (Finsupp.lsingle m : (a : R) → R[M]) r = a

Tactic:
exact Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
r : R
⊢ (Finsupp.lsingle m : (a : R) → R[M]) r = a → a = Finsupp.single m r

Tactic:
Eq.symm

Premises used: AddMonoidAlgebra, Eq.symm, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
r : R
⊢ (Finsupp.lsingle m : (a : R) → R[M]) r = a → a = Finsupp.single m r

Tactic:
exact Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
⊢ Eq (α := Submodule R R[M]) (grade R m) (LinearMap.range (Finsupp.lsingle m))

Tactic:
Submodule.ext (mem_grade_iff' R m)

Premises used: AddMonoidAlgebra.mem_grade_iff', Submodule.ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_4
inst : CommSemiring R
f : M → ι
m : M
r : R
x : M
hx : x ∈ Finsupp.support (single m r)
rw rw₁ : f m = f m
⊢ f x = f m

Tactic:
rw [Finset.mem_singleton.mp (Finsupp.support_single_subset hx)]

Premises used: Finset.mem_singleton, Iff.mp, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
i : M
r : R
⊢ Membership.mem (γ := Submodule R R[M]) (grade R i) (single i r)

Tactic:
single_mem_gradeBy _ _ _

Premises used: Set.Mem, setOf, AddMonoidAlgebra.single_mem_gradeBy
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
m : M
h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) 1) m
⊢ Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) m

Tactic:
rw [one_def] at h

Premises used: AddMonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
m : M
h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) m
⊢ m = 0

Tactic:
Finset.mem_singleton.1 <| Finsupp.support_single_subset h

Premises used: Finset.mem_singleton, Iff.mp, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
m : M
h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) m
obtain :
  ∀ (h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) 0),
    Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) 0 : ι) (0 : ι)
⊢ Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) m : ι) (0 : ι)

Tactic:
obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h

Premises used: Finset.mem_singleton, Iff.mp, Finsupp.support_single_subset, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
h : Membership.mem (γ := Finset M) (Finsupp.support.{u_1, u_3} (M := R) (single 0 1)) 0
⊢ Eq.{u_2 + 1} (α := ι) ((f : (a : M) → ι) 0 : ι) (0 : ι)

Tactic:
apply map_zero

Premises used: map_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) a
hb : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) j) b
c : M
hc : c ∈ (a * b).support
⊢ ∃ y ∈ a.support, ∃ z ∈ b.support, y + z = c

Tactic:
Finset.mem_add.1 <| support_mul a b hc

Premises used: AddMonoidAlgebra.support_mul, Finset.mem_add, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.Grading
Goal:
M : Type u_1
ι : Type u_2
R : Type u_3
inst : AddMonoid M
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
f : M →+ ι
i j : ι
a b : R[M]
ha : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) i) a
hb : Membership.mem (γ := Submodule R R[M]) (gradeBy R (⇑f : (a : M) → ι) j) b
c : M
hc : c ∈ (a * b).support
obtain :
  ∀ (ma : M) (hma : ma ∈ a.support) (mb : M) (hmb : mb ∈ b.support) (hc : ma + mb ∈ (a * b).support),
    (f : (a : M) → ι) (ma + mb) = i + j
⊢ (f : (a : M) → ι) c = i + j

Tactic:
obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.support, ∃ z ∈ b.support, y + z = c :=
      Finset.mem_add.1 <| support_mul a b hc

Premises used: Finsupp.support, AddMonoidAlgebra.support_mul, Finset.mem_add, Iff.mp, rfl