awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s_1 : Finset ι
hf : f.support ⊆ s_1
h : ∀ i ∈ s_1, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
s : ι
H : s ∉ f.support
⊢ LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)

Tactic:
exact notMem_support_iff.1 H ▸ zero_le
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ f ≤ g ↔ ∀ i ∈ f.support, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)

Tactic:
le_iff' f g <| Subset.refl _

Premises used: Finset.Subset.refl, Finsupp.le_iff'
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : a ∈ f.support
rw :
  ∀ (ha : LT.lt.{u_3} (α := α) (0 : α) ((f : (a : ι) → α) a : α)),
    LT.lt.{u_3} (α := α) (0 : α) ((g : (a : ι) → α) a : α)
⊢ a ∈ g.support

Tactic:
rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢

Premises used: Finsupp.mem_support_iff, pos_iff_ne_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : LT.lt.{u_3} (α := α) (0 : α) ((f : (a : ι) → α) a : α)
⊢ LT.lt.{u_3} (α := α) (0 : α) ((g : (a : ι) → α) a : α)

Tactic:
ha.trans_le (h _)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : LT.lt.{u_3} (α := α) (0 : α) ((f : (a : ι) → α) a : α)
⊢ LT.lt.{u_3} (α := α) (0 : α) ((g : (a : ι) → α) a : α)

Tactic:
exact ha.trans_le (h _)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
f g : ι →₀ α
inst_2 : CanonicallyOrderedAdd α
hfg : f ≤ g
⊢ f.support ⊆ g.support

Tactic:
support_monotone hfg

Premises used: Finsupp.support_monotone
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
i : ι
x : α
f : ι →₀ α
⊢ (∀ (i_1 : ι),
      Membership.mem (γ := Finset ι) {i} i_1 →
        LE.le.{u_3} (α := α) ((single i x : (a : ι) → α) i_1 : α) ((f : (a : ι) → α) i_1 : α)) ↔
    x ≤ (f : (a : ι) → α) i

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
f_1 g_1 : ι →₀ α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ OrderedSub (ι →₀ α)

Tactic:
⟨fun _n _m _k => forall_congr' fun _x => tsub_le_iff_right⟩

Premises used: OrderedSub.mk, tsub_le_iff_right, forall_congr'
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f g : ι →₀ α
⊢ (⇑(f - g) : (a : ι) → α) = HSub.hSub (α := (a : ι) → α) (⇑f : (a : ι) → α) (⇑g : (a : ι) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f g : ι →₀ α
a : ι
⊢ (f - g : (a : ι) → α) a = HSub.hSub (α := α) (β := α) ((f : (a : ι) → α) a : α) ((g : (a : ι) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
h :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
      ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
⊢ single i (a - b) = HSub.hSub (α := ι →₀ α) (single i a) (single i b)

Tactic:
ext j
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h :
  Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)
h₁ :
  ∀ (h : j ≠ i),
    Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
      ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)

Tactic:
obtain rfl | h := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
j : ι
h :
  (single j (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
h₁ : a - b = HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
h₂ : a - b = HSub.hSub (β := α) a ((single j b : (a : ι) → α) j : α)
h₃ h₄ : a - b = a - b
⊢ Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)

Tactic:
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.tsub_apply
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
h₁ :
  (single i (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
h₂ : 0 = HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
h₃ : 0 = HSub.hSub (α := α) (β := α) (0 : α) ((single i b : (a : ι) → α) j : α)
h₄ : 0 = HSub.hSub (α := α) 0 0
h₅ h₆ : Eq.{u_3 + 1} (α := α) 0 0
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)

Tactic:
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]

Premises used: tsub_self, Finsupp.single_eq_of_ne, Finsupp.tsub_apply
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support

Tactic:
simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
    Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

Premises used: zero_le, Finsupp.mem_support_iff, Ne, tsub_eq_zero_iff_le, imp_true_iff, Finset.subset_iff, Finsupp.coe_tsub, Pi.sub_apply, not_imp_not
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : DecidableEq ι
f1 f2 : ι →₀ α
⊢ f1.support \ f2.support ⊆ (f1 - f2).support

Tactic:
simp +contextual [subset_iff]

Premises used: Finset.subset_iff
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
h₁ :
  ∀ (y : κ),
    Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
      ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
⊢ mapDomain f (f1 - f2) = mapDomain f f1 - mapDomain f f2

Tactic:
ext y
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
pos :
  ∀ (hy : y ∉ Set.range f),
    Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
      ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
neg :
  ∀ (hy : y ∈ Set.range f),
    Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
      ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
⊢ Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)

Tactic:
by_cases! hy : y ∉ Set.range f

Premises used: Set.range
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
hy : y ∉ Set.range f
⊢ Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)

Tactic:
simp [mapDomain_notin_range _ _ hy]

Premises used: Finsupp.mapDomain_notin_range
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
hy : y ∈ Set.range f
neg :
  ∀ (x : ι),
    Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) (f x) : α)
      ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) (f x) : α)
⊢ Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)

Tactic:
obtain ⟨x, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
x : ι
⊢ Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) (f x) : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) (f x) : α)

Tactic:
simp [mapDomain_apply h]

Premises used: Finsupp.mapDomain_apply
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι ↪ κ
f1 f2 : ι →₀ α
simp_rw :
  mapDomain (⇑f : (a : ι) → κ) (f1 - f2) =
    HSub.hSub (α := κ →₀ α) (mapDomain (⇑f : (a : ι) → κ) f1) (mapDomain (⇑f : (a : ι) → κ) f2)
⊢ embDomain f (f1 - f2) = embDomain f f1 - embDomain f f2

Tactic:
simp_rw [embDomain_eq_mapDomain, mapDomain_tsub f.injective]

Premises used: Finsupp.embDomain_eq_mapDomain, Function.Embedding.injective, Finsupp.mapDomain_tsub
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
inst_3 : DecidableEq ι
f g : ι →₀ α
h : ∀ (a : ι), a ∈ (f ⊓ g).support ↔ a ∈ f.support ∩ g.support
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
inst_3 : DecidableEq ι
f g : ι →₀ α
a : ι
⊢ a ∈ (f ⊓ g).support ↔ a ∈ f.support ∩ g.support

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
inst_3 : DecidableEq ι
f g : ι →₀ α
h : ∀ (a : ι), a ∈ (f ⊔ g).support ↔ a ∈ f.support ∪ g.support
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
inst_3 : DecidableEq ι
f g : ι →₀ α
a : ι
⊢ a ∈ (f ⊔ g).support ↔ a ∈ f.support ∪ g.support

Tactic:
simp [imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
simp [disjoint_iff, bot_eq_zero, ← Finsupp.support_eq_empty]

Premises used: disjoint_iff, Finsupp.support_eq_empty, bot_eq_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
classical
  simp [disjoint_iff, bot_eq_zero, ← Finsupp.support_eq_empty]

Premises used: Finsupp.disjoint_iff, Finsupp.support_eq_empty, bot_eq_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
a : ι
u u' : ι →₀ ℕ
h : Ne (α := ℕ) ((u : (a : ι) → ℕ) a : ℕ) (0 : ℕ)
⊢ u - single a 1 + u' = u + u' - single a 1

Tactic:
tsub_add_eq_add_tsub <| single_le_iff.mpr <| Nat.one_le_iff_ne_zero.mpr h

Premises used: Iff.mpr, tsub_add_eq_add_tsub, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
a : ι
u u' : ι →₀ ℕ
h : Ne (α := ℕ) ((u' : (a : ι) → ℕ) a : ℕ) (0 : ℕ)
⊢ u + (u' - single a 1) = u + u' - single a 1

Tactic:
(add_tsub_assoc_of_le (single_le_iff.mpr <| Nat.one_le_iff_ne_zero.mpr h) _).symm

Premises used: Iff.mpr, add_tsub_assoc_of_le, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Eq.symm
-- Module: Mathlib.Data.Finsupp.Order
Goal:
ι : Type u_1
u : ι →₀ ℕ
i : ι
h : Ne (α := ℕ) ((u : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
rw : u + single i 1 - single i 1 = u
rw₁ rw₂ : u = u
⊢ u - single i 1 + single i 1 = u

Tactic:
rw [sub_single_one_add h, add_tsub_cancel_right]

Premises used: add_tsub_cancel_right, Finsupp.sub_single_one_add
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
obtain : ∀ (w : β →₀ ℕ) (hw : embDomain f z = y + w), Membership.mem (γ := Set (β →₀ ℕ)) (Set.range (embDomain f)) y
⊢ Membership.mem (γ := Set (β →₀ ℕ)) (Set.range (embDomain f)) y

Tactic:
obtain ⟨w, hw⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
rw : (↑y.support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Membership.mem (γ := Set (β →₀ ℕ)) (Set.range (embDomain f)) y

Tactic:
rw [mem_range_embDomain_iff]

Premises used: Finsupp.mem_range_embDomain_iff
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
trans : (↑y.support : Set β) ⊆ (↑(y + w).support : Set β)
trans₁ : (↑(y + w).support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ (↑y.support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
trans ↑(y + w).support

Premises used: Finsupp.support, HAdd.hAdd
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x : β
simp :
  ¬Eq (α := ℕ) ((y : (a : β) → ℕ) x : ℕ) (0 : ℕ) →
    Eq (α := ℕ) ((y : (a : β) → ℕ) x : ℕ) (0 : ℕ) → ¬Eq (α := ℕ) ((w : (a : β) → ℕ) x : ℕ) (0 : ℕ)
⊢ x ∈ (↑y.support : Set β) → x ∈ (↑(y + w).support : Set β)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x : β
⊢ ¬Eq (α := ℕ) ((y : (a : β) → ℕ) x : ℕ) (0 : ℕ) →
    Eq (α := ℕ) ((y : (a : β) → ℕ) x : ℕ) (0 : ℕ) → ¬Eq (α := ℕ) ((w : (a : β) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ (↑y.support : Set β) ⊆ (↑(y + w).support : Set β)

Tactic:
exact fun _ ↦ by simp; grind
-- Module: Mathlib.Data.Finsupp.Order
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ (↑(y + w).support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
simp [← hw]
-- Module: Mathlib.Data.Finsupp.PWO
Goal:
α : Type u_1
σ : Type u_2
inst : Zero α
inst_1 : Preorder α
inst_2 : WellQuasiOrderedLE α
inst_3 : Finite σ
⊢ WellQuasiOrderedLE (σ →₀ α)

Tactic:
orderIsoFunOnFinite.wellQuasiOrderedLE_iff.2 inferInstance

Premises used: Iff.mpr, OrderIso.wellQuasiOrderedLE_iff, inferInstance, Finsupp.orderIsoFunOnFinite
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
inst : MulZeroClass β
g₁ g₂ : α →₀ β
⊢ (⇑(g₁ * g₂) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑g₁ : (a : α) → β) (⇑g₂ : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
inst : MulZeroClass β
g₁ g₂ : α →₀ β
a : α
⊢ (g₁ * g₂ : (a : α) → β) a = HMul.hMul (α := β) (β := β) ((g₁ : (a : α) → β) a : β) ((g₂ : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
inst : MulZeroClass β
a : α
b₁ b₂ : β
⊢ single a (b₁ * b₂) = HMul.hMul (α := α →₀ β) (single a b₁) (single a b₂)

Tactic:
(zipWith_single_single _ _ _ _ _).symm

Premises used: Finsupp.zipWith_single_single, Eq.symm
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
inst : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₁.support

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
inst : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₂.support

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
inst : MulZeroClass β
inst_1 : DecidableEq α
g₁ g₂ : α →₀ β
⊢ (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support

Tactic:
subset_inter support_mul_subset_left support_mul_subset_right

Premises used: Finsupp.support_mul_subset_right, Finsupp.support_mul_subset_left, Finset.subset_inter
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
γ : Type u₃
inst : Zero γ
inst_1 : SMulZeroClass β γ
f : α → β
g : α →₀ γ
⊢ ∀ (x : α),
    ¬HSMul.hSMul (β := γ) (f x) ((g : (a : α) → γ) x : γ) = 0 → ¬Eq.{u₃ + 1} (α := γ) ((g : (a : α) → γ) x : γ) (0 : γ)

Tactic:
grind [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
inst : Semiring β
f : α → β
g : α →₀ β
⊢ (⇑(f • g) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) f (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst : Semiring β
r : β
f : α → β
m : α →₀ β
h : ∀ (a : α), Eq.{u₂ + 1} (α := β) (((r • f) • m : (a : α) → β) a : β) ((r • f • m : (a : α) → β) a : β)
⊢ (r • f) • m = r • f • m

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Pointwise
Goal:
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst : Semiring β
r : β
f : α → β
m : α →₀ β
a : α
⊢ Eq.{u₂ + 1} (α := β) (((r • f) • m : (a : α) → β) a : β) ((r • f • m : (a : α) → β) a : β)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : MonoidWithZero R
inst_2 : MulActionWithZero R M
a b : α
f : α → M
r : R
pos :
  ∀ (h : a = b),
    HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b
neg :
  ∀ (h : ¬a = b),
    HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b
⊢ HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b

Tactic:
by_cases h : a = b
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : MonoidWithZero R
inst_2 : MulActionWithZero R M
a b : α
f : α → M
r : R
h : a = b
⊢ HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : MonoidWithZero R
inst_2 : MulActionWithZero R M
a b : α
f : α → M
r : R
h : ¬a = b
⊢ HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
G : Type u_5
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f : α →₀ M
⊢ g • f = mapDomain (fun (x : α) ↦ g • x) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
G : Type u_5
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
a : α
b : M
⊢ HSMul.hSMul (β := α →₀ M) g (single a b) = single (g • a) b

Tactic:
mapDomain_single

Premises used: Finsupp.mapDomain_single
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g g' : G
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ (g * g') • x) f = g • g' • f
rw₁ : Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f) (mapDomain (fun (x : α) ↦ g • x) (g' • f))
rw₂ :
  Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f)
    (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
rw₃ :
  Eq (α := α →₀ M) (mapDomain ((fun (x : α) ↦ g • x) ∘ fun (x : α) ↦ g' • x) f)
    (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
rw₄ rw₅ :
  Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
    (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
⊢ (g * g') • f = g • g' • f

Tactic:
rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]

Premises used: Finsupp.comapSMul_def, comp_smul_left, Finsupp.mapDomain_comp
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ HSMul.hSMul.{u_5, u_1, u_1} (α := G) 1 x) f = f
rw₁ : mapDomain id f = f
rw₂ rw₃ : f = f
⊢ HSMul.hSMul (α := G) 1 f = f

Tactic:
rw [comapSMul_def, one_smul_eq_id, mapDomain_id]

Premises used: Finsupp.mapDomain_id, Finsupp.comapSMul_def, one_smul_eq_id
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
h : ∀ (a : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := α →₀ M) g 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ HSMul.hSMul (β := α →₀ M) g 0 = 0

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
a : α
h : Eq.{u_3 + 1} (α := M) ((mapDomain (fun (x : α) ↦ g • x) 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := α →₀ M) g 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
simp only [comapSMul_def]

Premises used: Finsupp.comapSMul_def
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
a : α
⊢ Eq.{u_3 + 1} (α := M) ((mapDomain (fun (x : α) ↦ g • x) 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f f' : α →₀ M
h : ∀ (a : α), Eq.{u_3 + 1} (α := M) ((g • (f + f') : (a : α) → M) a : M) ((g • f + g • f' : (a : α) → M) a : M)
⊢ g • (f + f') = g • f + g • f'

Tactic:
ext