awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
p_1 p : α → Prop
f : α →₀ M
a : Subtype p
simp :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) (↑a : α) : M) (0 : M) ↔
    Ne.{u_5 + 1} (α := M) (((⇑f : (a : α) → M) ∘ Subtype.val (p := p)) a) 0
⊢ a ∈ Finset.subtype p f.support ↔ Ne.{u_5 + 1} (α := M) (((⇑f : (a : α) → M) ∘ Subtype.val (p := p)) a) 0

Tactic:
simp only [@mem_subtype _ _ (Classical.decPred p), mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finset.mem_subtype
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
p_1 p : α → Prop
f : α →₀ M
a : Subtype p
⊢ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) (↑a : α) : M) (0 : M) ↔
    Ne.{u_5 + 1} (α := M) (((⇑f : (a : α) → M) ∘ Subtype.val (p := p)) a) 0

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
rw : (subtypeDomain p f).support = Finset.subtype p f.support
rw₁ : DecidablePred p
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
rw [Subsingleton.elim D]

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
a : Subtype p
v : α →₀ M
⊢ Eq.{u_5 + 1} (α := M) ((subtypeDomain p v : (a : Subtype p) → M) a : M) ((v : (a : α) → M) (↑a : α) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
⊢ Eq (α := Finsupp.{u_1, u_5} (Subtype p) M) (subtypeDomain p 0) 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, Multiset.ofList, Finsupp.subtypeDomain, Finset.subtype, rfl, Multiset.filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
f g : α →₀ M
simp_rw :
  (∀ (x : Subtype p),
      Eq.{u_5 + 1} (α := M) ((subtypeDomain p f : (a : Subtype p) → M) x : M)
        ((subtypeDomain p g : (a : Subtype p) → M) x : M)) ↔
    ∀ (x : α), p x → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
simp_rw₁ :
  (∀ (x : Subtype p), Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) (↑x : α) : M) ((g : (a : α) → M) (↑x : α) : M)) ↔
    ∀ (x : α), p x → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
⊢ subtypeDomain p f = subtypeDomain p g ↔
    ∀ (x : α), p x → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)

Tactic:
simp_rw [DFunLike.ext_iff, subtypeDomain_apply, Subtype.forall]

Premises used: Subtype.forall, DFunLike.ext_iff, Finsupp.subtypeDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
f g : α →₀ M
hf : ∀ x ∈ f.support, p x
hg : ∀ x ∈ g.support, p x
⊢ subtypeDomain p f = subtypeDomain p g ↔ f = g

Tactic:
subtypeDomain_eq_iff_forall.trans
    ⟨fun H ↦ Finsupp.ext fun _a ↦ (em _).elim (H _ <| hf _ ·) fun haf ↦ (em _).elim (H _ <| hg _ ·)
        fun hag ↦ (notMem_support_iff.mp haf).trans (notMem_support_iff.mp hag).symm,
      fun H _ _ ↦ congr($H _)⟩

Premises used: Finsupp.ext, congrArg, Finsupp.notMem_support_iff, Finsupp.support, Membership.mem, em, id, Finsupp.subtypeDomain_eq_iff_forall, Iff.intro, Iff.mp, Iff.trans, Or.elim, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
f : α →₀ M
⊢ subtypeDomain p f = 0 ↔ ∀ (x : α), p x → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)

Tactic:
subtypeDomain_eq_iff_forall (g := 0)

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, Multiset.ofList, Finsupp.subtypeDomain_eq_iff_forall, Finsupp.subtypeDomain, Finset.subtype, Multiset.filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
f : α →₀ M
hf : ∀ x ∈ f.support, p x
⊢ ∀ (x : α), Membership.mem (γ := Finset α) (support.{u_1, u_5} (M := M) 0) x → p x

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ((subtypeDomain p v).prod fun (a : Subtype p) (b : M) ↦ h (↑a : α) b) = v.prod h

Tactic:
Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_

Premises used: Subtype.val, Finset.prod_bij, Finsupp.prod
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
refine_1 :
  ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain p v).support),
    (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha ∈ v.support
refine_2 :
  ∀ (a₁ : Subtype p) (ha₁ : a₁ ∈ (subtypeDomain p v).support) (a₂ : Subtype p) (ha₂ : a₂ ∈ (subtypeDomain p v).support),
    Eq.{u_1 + 1} (α := α) ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a₁ ha₁)
        ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a₂ ha₂) →
      a₁ = a₂
refine_3 :
  ∀ b ∈ v.support,
    ∃ (a : Subtype p) (ha : a ∈ (subtypeDomain p v).support),
      (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha = b
refine_4 :
  ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain p v).support),
    (fun (a : Subtype p) (b : M) ↦ h (↑a : α) b) a ((subtypeDomain p v : (a : Subtype p) → M) a) =
      h ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha)
        ((v : (a : α) → M) ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha))
⊢ ((subtypeDomain p v).prod fun (a : Subtype p) (b : M) ↦ h (↑a : α) b) = v.prod h

Tactic:
refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_

Premises used: Finset.prod_bij
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain p v).support),
    (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha ∈ v.support

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ (a₁ : Subtype p) (ha₁ : a₁ ∈ (subtypeDomain p v).support) (a₂ : Subtype p) (ha₂ : a₂ ∈ (subtypeDomain p v).support),
    Eq.{u_1 + 1} (α := α) ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a₁ ha₁)
        ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a₂ ha₂) →
      a₁ = a₂

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ b ∈ v.support,
    ∃ (a : Subtype p) (ha : a ∈ (subtypeDomain p v).support),
      (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha = b

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain p v).support),
    (fun (a : Subtype p) (b : M) ↦ h (↑a : α) b) a ((subtypeDomain p v : (a : Subtype p) → M) a) =
      h ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha)
        ((v : (a : α) → M) ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain p v).support) ↦ (↑p_1 : α)) a ha))

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddZeroClass M
p : α → Prop
v v' : α →₀ M
⊢ subtypeDomain p (v + v') = subtypeDomain p v + subtypeDomain p v'

Tactic:
ext fun _ => rfl

Premises used: Finsupp.ext, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : AddZeroClass M
p_1 : α → Prop
v v' : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
f g : α →₀ M
simp_rw :
  Set.indicator {x : α | p x} (⇑(f + g) : (a : α) → M) =
    HAdd.hAdd (α := (a : α) → M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M))
      (Set.indicator {x : α | p x} (⇑g : (a : α) → M))
⊢ Eq (α := (a : α) → M) ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (filter p (f + g)))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (filter p f + filter p g))

Tactic:
simp_rw [coe_add, filter_eq_indicator]

Premises used: Finsupp.filter_eq_indicator, Finsupp.coe_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : AddZeroClass M
p_1 : α → Prop
v v' : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
f g : α →₀ M
⊢ Set.indicator {x : α | p x} (⇑(f + g) : (a : α) → M) =
    HAdd.hAdd (α := (a : α) → M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M))
      (Set.indicator {x : α | p x} (⇑g : (a : α) → M))

Tactic:
Set.indicator_add { x | p x } f g

Premises used: setOf, Set.indicator_add, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : AddZeroClass M
p_1 : α → Prop
v v' : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
f g : α →₀ M
⊢ Set.indicator {x : α | p x} (⇑(f + g) : (a : α) → M) =
    HAdd.hAdd (α := (a : α) → M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M))
      (Set.indicator {x : α | p x} (⇑g : (a : α) → M))

Tactic:
exact Set.indicator_add { x | p x } f g

Premises used: setOf, Set.indicator_add, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddZeroClass M
p : α → Prop
inst_1 : DecidablePred p
v v' : α →₀ M
⊢ filter p (v + v') = filter p v + filter p v'

Tactic:
(filterAddHom p).map_add v v'

Premises used: Finsupp.filterAddHom, AddMonoidHom.map_add, Finsupp.filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_4
M : Type u_5
inst : AddCommMonoid M
p : α → Prop
s : Finset ι
h : ι → α →₀ M
⊢ Eq (α := Finsupp.{u_1, u_5} (Subtype p) M) (subtypeDomain p (∑ c ∈ s, h c)) (∑ c ∈ s, subtypeDomain p (h c))

Tactic:
map_sum subtypeDomainAddMonoidHom _ s

Premises used: map_sum, Finsupp.subtypeDomainAddMonoidHom, Finsupp.subtypeDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
p : α → Prop
inst_1 : Zero N
s : β →₀ N
h : β → N → α →₀ M
⊢ subtypeDomain p (s.sum h) = s.sum fun (c : β) (d : N) ↦ subtypeDomain p (h c d)

Tactic:
subtypeDomain_sum

Premises used: Finsupp.sum, Finsupp.subtypeDomain_sum
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_4
M : Type u_5
inst : AddCommMonoid M
p : α → Prop
inst_1 : DecidablePred p
s : Finset ι
f : ι → α →₀ M
⊢ Eq (α := α →₀ M) (filter p (∑ a ∈ s, f a)) (∑ a ∈ s, filter p (f a))

Tactic:
map_sum (filterAddHom p) f s

Premises used: Finsupp.filterAddHom, map_sum, Finsupp.filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
x : α
hx : x ∈ Finset.filter p f.support
rw rw₁ : Eq (α := α →₀ M) (single x ((f : (a : α) → M) x) : α →₀ M) (single x ((f : (a : α) → M) x) : α →₀ M)
⊢ Eq (α := α →₀ M) (single x ((filter p f : (a : α) → M) x) : α →₀ M) (single x ((f : (a : α) → M) x) : α →₀ M)

Tactic:
rw [filter_apply_pos _ _ (mem_filter.1 hx).2]

Premises used: Finsupp.filter_apply_pos, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
G : Type u_8
inst : AddGroup G
p : α → Prop
v : α →₀ G
⊢ subtypeDomain p (-v) = -subtypeDomain p v

Tactic:
ext fun _ => rfl

Premises used: Finsupp.ext, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
G : Type u_8
inst : AddGroup G
p : α → Prop
v v' : α →₀ G
⊢ subtypeDomain p (v - v') = subtypeDomain p v - subtypeDomain p v'

Tactic:
ext fun _ => rfl

Premises used: Finsupp.ext, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
G : Type u_8
inst : AddGroup G
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ G
⊢ filter p (-f) = -filter p f

Tactic:
(filterAddHom p : (_ →₀ G) →+ _).map_neg f

Premises used: Finsupp.filterAddHom, AddMonoidHom.map_neg, Finsupp.filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
G : Type u_8
inst : AddGroup G
p : α → Prop
inst_1 : DecidablePred p
f₁ f₂ : α →₀ G
⊢ filter p (f₁ - f₂) = filter p f₁ - filter p f₂

Tactic:
(filterAddHom p : (_ →₀ G) →+ _).map_sub f₁ f₂

Premises used: Finsupp.filterAddHom, AddMonoidHom.map_sub, Finsupp.filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s : Multiset (α →₀ M)
a : α
h : Membership.mem (γ := Finset α) (support.{u_1, u_5} (M := M) (Multiset.sum 0)) a
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s_1 : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
pos : ∀ (h : a ∈ f.support), ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
neg : ∀ (h : a ∉ f.support), ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
by_cases h : a ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s_1 : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∈ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
⟨f, Multiset.mem_cons_self _ _, h⟩

Premises used: And.intro, Exists.intro, Multiset.mem_cons_self
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s_1 : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∈ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
exact ⟨f, Multiset.mem_cons_self _ _, h⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s_1 : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∉ f.support
⊢ Ne.{u_5 + 1} (α := M) ((s.sum : (a : α) → M) a : M) (0 : M)

Tactic:
simp_rw [Multiset.sum_cons, mem_support_iff, add_apply, notMem_support_iff.1 h,
          zero_add] at ha

Premises used: Finsupp.mem_support_iff, Finsupp.notMem_support_iff, Finsupp.add_apply, zero_add, Iff.mp, Multiset.sum_cons
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s_1 : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
h : a ∉ f.support
ha : Ne.{u_5 + 1} (α := M) ((s.sum : (a : α) → M) a : M) (0 : M)
neg : ∀ (f' : α →₀ M) (h₀ : f' ∈ s) (h₁ : a ∈ f'.support), ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩

Premises used: Iff.mpr, Finsupp.mem_support_iff
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s_1 : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
h : a ∉ f.support
ha : Ne.{u_5 + 1} (α := M) ((s.sum : (a : α) → M) a : M) (0 : M)
f' : α →₀ M
h₀ : f' ∈ s
h₁ : a ∈ f'.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
⟨f', Multiset.mem_cons_of_mem h₀, h₁⟩

Premises used: Multiset.mem_cons_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
s_1 : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
h : a ∉ f.support
ha : Ne.{u_5 + 1} (α := M) ((s.sum : (a : α) → M) a : M) (0 : M)
f' : α →₀ M
h₀ : f' ∈ s
h₁ : a ∈ f'.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
exact ⟨f', Multiset.mem_cons_of_mem h₀, h₁⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_4
M : Type u_5
inst : AddCommMonoid M
s : Finset ι
h : ι → α →₀ M
a : α
ha : Membership.mem (γ := Finset α) (support.{u_1, u_5} (M := M) (∑ c ∈ s, h c)) a
⊢ ∃ c ∈ s, a ∈ (h c).support

Tactic:
let ⟨_, hf, hfa⟩ := mem_support_multiset_sum a ha
  let ⟨c, hc, Eq⟩ := Multiset.mem_map.1 hf
  ⟨c, hc, Eq.symm ▸ hfa⟩

Premises used: _private.0.Finsupp.mem_support_finsetSum.match_2, Multiset.mem_map, Finsupp.support, Membership.mem, Exists, Eq.rec, _private.0.Finsupp.mem_support_finsetSum.match_1, Finsupp.mem_support_multiset_sum, And, And.intro, Exists.intro, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α →₀ β →₀ M
a₁ : α
_ :
  a₁ ∈ (↑f.support : Set α) →
    ∀ ⦃y : α⦄,
      y ∈ (↑f.support : Set α) →
        a₁ ≠ y →
          onFun (β := Finset (α × β)) Disjoint
            (fun (a : α) ↦ map (Embedding.sectR a β) (support.{u_2, u_5} (M := M) ((f : (a : α) → β →₀ M) a))) a₁ y
⊢ a₁ ∈ (↑f.support : Set α) →
    ∀ ⦃y : α⦄,
      y ∈ (↑f.support : Set α) →
        a₁ ≠ y →
          onFun (β := Finset (α × β)) Disjoint
            (fun (a : α) ↦ map (Embedding.sectR a β) (support.{u_2, u_5} (M := M) ((f : (a : α) → β →₀ M) a))) a₁ y

Tactic:
_
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α →₀ β →₀ M
a₁ : α
h : a₁ ∈ (↑f.support : Set α)
a₂ : α
_ :
  a₂ ∈ (↑f.support : Set α) →
    a₁ ≠ a₂ →
      onFun (β := Finset (α × β)) Disjoint
        (fun (a : α) ↦ map (Embedding.sectR a β) (support.{u_2, u_5} (M := M) ((f : (a : α) → β →₀ M) a))) a₁ a₂
⊢ a₂ ∈ (↑f.support : Set α) →
    a₁ ≠ a₂ →
      onFun (β := Finset (α × β)) Disjoint
        (fun (a : α) ↦ map (Embedding.sectR a β) (support.{u_2, u_5} (M := M) ((f : (a : α) → β →₀ M) a))) a₁ a₂

Tactic:
_
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α →₀ β →₀ M
a₁ : α
h : a₁ ∈ (↑f.support : Set α)
a₂ : α
h_1 : a₂ ∈ (↑f.support : Set α)
hne : a₁ ≠ a₂
⊢ onFun (β := Finset (α × β)) Disjoint
    (fun (a : α) ↦ map (Embedding.sectR a β) (support.{u_2, u_5} (M := M) ((f : (a : α) → β →₀ M) a))) a₁ a₂

Tactic:
simp [Finset.disjoint_iff_ne, hne]

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α →₀ β →₀ M
⊢ ∀ (a : α × β),
    a ∈
        f.support.disjiUnion
          (fun (a : α) ↦ map (Embedding.sectR a β) (support.{u_2, u_5} (M := M) ((f : (a : α) → β →₀ M) a))) ⋯ ↔
      Ne.{u_5 + 1} (α := M) ((((f : (a : α) → β →₀ M) a.1 : β →₀ M) : (a : β) → M) a.2 : M) (0 : M)

Tactic:
aesop
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α →₀ β →₀ M
x : α × β
⊢ Eq.{u_5 + 1} (α := M) ((f.uncurry : (a : α × β) → M) x : M)
    ((((f : (a : α) → β →₀ M) x.1 : β →₀ M) : (a : β) → M) x.2 : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α →₀ β →₀ M
a : α
b : β
⊢ Eq.{u_5 + 1} (α := M) ((f.uncurry : (a : α × β) → M) (a, b) : M)
    ((((f : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) b : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
h :
  ∀ (x : α) (y : β),
    Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (x, y) : M)
      ((single (a, b) m : (a : α × β) → M) (x, y) : M)
⊢ Eq (α := α × β →₀ M) (Finsupp.uncurry (single a (single b m))) (single (a, b) m)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
x : α
y : β
h :
  Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (a, y) : M)
    ((single (a, b) m : (a : α × β) → M) (a, y) : M)
h₁ :
  ∀ (hne : a ≠ x),
    Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (x, y) : M)
      ((single (a, b) m : (a : α × β) → M) (x, y) : M)
⊢ Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (x, y) : M)
    ((single (a, b) m : (a : α × β) → M) (x, y) : M)

Tactic:
rcases eq_or_ne a x with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
y : β
⊢ Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (a, y) : M)
    ((single (a, b) m : (a : α × β) → M) (a, y) : M)

Tactic:
simp [single_apply, *]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
y : β
⊢ Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (a, y) : M)
    ((single (a, b) m : (a : α × β) → M) (a, y) : M)

Tactic:
classical simp [single_apply, *]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
x : α
y : β
hne : a ≠ x
⊢ Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (x, y) : M)
    ((single (a, b) m : (a : α × β) → M) (x, y) : M)

Tactic:
simp [single_apply, *]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
x : α
y : β
hne : a ≠ x
⊢ Eq.{u_5 + 1} (α := M) ((Finsupp.uncurry (single a (single b m)) : (a : α × β) → M) (x, y) : M)
    ((single (a, b) m : (a : α × β) → M) (x, y) : M)

Tactic:
classical simp [single_apply, *]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : Zero M
inst_1 : AddCommMonoid N
f : α →₀ β →₀ M
g : α × β → M → N
⊢ Eq.{u_6 + 1} (α := N) (f.uncurry.sum fun (p : α × β) (c : M) ↦ g p c)
    (f.sum fun (a : α) (f : β →₀ M) ↦ f.sum fun (b : β) ↦ g (a, b))

Tactic:
simp [Finsupp.sum, Finsupp.uncurry, Finset.sum_disjiUnion]

Premises used: Finsupp.sum, Finsupp.uncurry, Finset.sum_disjiUnion
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : Zero M
inst_1 : AddCommMonoid N
f : α →₀ β →₀ M
g : α → β → M → N
⊢ Eq.{u_6 + 1} (α := N) (f.uncurry.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
    (f.sum fun (a : α) (f : β →₀ M) ↦ f.sum (g a))

Tactic:
sum_uncurry_index ..

Premises used: Finsupp.sum_uncurry_index
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α × β →₀ M
a : α
⊢ ∀ (a_1 a' : α × β) (b : β),
    Membership.mem (γ := Option β) ((fun (x : α × β) ↦ if x.1 = a then some x.2 else none) a_1) b →
      Membership.mem (γ := Option β) ((fun (x : α × β) ↦ if x.1 = a then some x.2 else none) a') b → a_1 = a'

Tactic:
simp +contextual