awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) s
h :
  ∀ (a : List (ι →₀ M))
    (hs :
      Pairwise (Disjoint on Finsupp.support)
        (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)),
    (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).support =
      (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup
⊢ s.sum.support = (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn with | _ a
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a : List (ι →₀ M)
hs :
  Pairwise (Disjoint on Finsupp.support) (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)
h :
  ∀ (l : List (ι →₀ M))
    (hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M)))
    (hd : List.Pairwise (Disjoint on Finsupp.support) l),
    (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).support =
      (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup

Tactic:
obtain ⟨l, hl, hd⟩ := hs
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
⊢ a.sum.support = List.foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ a

Tactic:
List.support_sum_eq a this

Premises used: List.support_sum_eq
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
h :
  (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup =
    List.foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ a
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup

Tactic:
convert! List.support_sum_eq a this

Premises used: List.support_sum_eq
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
⊢ (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup =
    List.foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ a

Tactic:
simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]

Premises used: Finset.bot_eq_empty, Multiset.sup_coe, List.foldr_map, Multiset.map_coe, Finset.sup_eq_union, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
h : List.Pairwise (Disjoint on Finsupp.support) a
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).support =
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup

Tactic:
suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! List.support_sum_eq a this
    dsimp only [Function.comp_def]
    simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
⊢ a.Perm l

Tactic:
simp only [Multiset.quot_mk_to_coe'', Multiset.coe_eq_coe] at hl

Premises used: Multiset.coe_eq_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hd : List.Pairwise (Disjoint on Finsupp.support) l
hl : a.Perm l
⊢ List.Pairwise (Disjoint on Finsupp.support) a

Tactic:
hl.symm.pairwise hd fun h ↦ _root_.Disjoint.symm h

Premises used: Disjoint.symm, List.Perm.symm, List.Perm.pairwise
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hd : List.Pairwise (Disjoint on Finsupp.support) l
hl : a.Perm l
⊢ List.Pairwise (Disjoint on Finsupp.support) a

Tactic:
exact hl.symm.pairwise hd fun h ↦ _root_.Disjoint.symm h

Premises used: Disjoint.symm, List.Perm.symm, List.Perm.pairwise
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ s.val.sum.support = (Multiset.map Finsupp.support s.val).sup

Tactic:
Multiset.support_sum_eq s.1 this

Premises used: Finset.val, Multiset.support_sum_eq
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
h : s.sum id = s.val.sum
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
convert! Multiset.support_sum_eq s.1 this

Premises used: Finset.val, Multiset.support_sum_eq
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ s.sum id = s.val.sum

Tactic:
(Finset.sum_val _).symm

Premises used: Finset.sum_val, Eq.symm
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ s.sum id = s.val.sum

Tactic:
exact (Finset.sum_val _).symm

Premises used: Finset.sum_val, Eq.symm
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
suffices : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
⊢ ∃ (l : List (ι →₀ M)), l.toFinset = s ∧ l.Nodup

Tactic:
⟨s.toList, ?_, Finset.nodup_toList _⟩

Premises used: Finset.nodup_toList, Finset.toList, And.intro, Exists.intro
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
refine : s.toList.toFinset = s
⊢ ∃ (l : List (ι →₀ M)), l.toFinset = s ∧ l.Nodup

Tactic:
refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
⊢ s.toList.toFinset = s

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
obtain :
  ∀ (l : List (ι →₀ M)) (hl : l.toFinset = s) (hn : l.Nodup), Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val

Tactic:
obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
    refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
    simp

Premises used: List, Finsupp
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
l : List (ι →₀ M)
hl : l.toFinset = s
hn : l.Nodup
subst :
  ∀ (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
    Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val

Tactic:
subst hl
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
hr : Symmetric (α := ι →₀ M) (Disjoint on Finsupp.support)
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val

Tactic:
rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
    List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]

Premises used: Iff.mpr, List.dedup_eq_self, List.toFinset_val, List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint, Multiset.pairwise_coe_iff_pairwise
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
x y : ι →₀ M
hxy : (Disjoint on Finsupp.support) x y
⊢ (Disjoint on Finsupp.support) y x

Tactic:
symmetric_disjoint hxy

Premises used: symmetric_disjoint
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
x y : ι →₀ M
hxy : (Disjoint on Finsupp.support) x y
⊢ (Disjoint on Finsupp.support) y x

Tactic:
exact symmetric_disjoint hxy

Premises used: symmetric_disjoint
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
suffices suffices₁ suffices₂ : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
suffices₃ :
  ∀ (l : List (ι →₀ M)) (hl : l.toFinset = s) (hn : l.Nodup), Multiset.Pairwise (Disjoint on Finsupp.support) s.val
suffices₄ :
  ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
    Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val
hr :
  ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
    Symmetric (α := ι →₀ M) (Disjoint on Finsupp.support)
hr₁ :
  ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support)
    ⦃x y : ι →₀ M⦄ (hxy : (Disjoint on Finsupp.support) x y), (Disjoint on Finsupp.support) y x
⊢ (s.sum id).support = s.sup Finsupp.support

Tactic:
classical
  suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm
  obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
    refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
    simp
  subst hl
  rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
    List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
  intro x y hxy
  exact symmetric_disjoint hxy

Premises used: List, List.toFinset_val, Multiset.pairwise_coe_iff_pairwise, Finsupp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
e_support : s = t
⊢ { support := s, toFun := f, mem_support_toFun := hf : α →₀ M } = { support := t, toFun := f, mem_support_toFun := hg }

Tactic:
congr
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
e_support : ∀ (a : α), a ∈ s ↔ a ∈ t
⊢ s = t

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
a : α
⊢ a ∈ s ↔ a ∈ t

Tactic:
(hf _).trans (hg _).symm

Premises used: Iff.trans, Iff.symm
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
a : α
⊢ a ∈ s ↔ a ∈ t

Tactic:
exact (hf _).trans (hg _).symm

Premises used: Iff.trans, Iff.symm
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h : ∀ (a : α), Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : IsEmpty α
f g : α →₀ M
h : ∀ (x : α), Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : IsEmpty α
f g : α →₀ M
x : α
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)

Tactic:
isEmptyElim x

Premises used: isEmptyElim
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : IsEmpty α
f g : α →₀ M
x : α
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)

Tactic:
exact isEmptyElim x
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Subsingleton M
f g : α →₀ M
h : ∀ (x : α), Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Subsingleton M
f g : α →₀ M
x : α
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)

Tactic:
Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Subsingleton M
f g : α →₀ M
x : α
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)

Tactic:
exact Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
h : Nontrivial (α →₀ M)
contrapose! : ∀ (h : Subsingleton M), Subsingleton (α →₀ M)
⊢ Nontrivial M

Tactic:
contrapose! h
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
h : Subsingleton M
⊢ Subsingleton (α →₀ M)

Tactic:
infer_instance
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
⊢ f ≠ g ↔ ∃ (a : α), Ne.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)

Tactic:
DFunLike.ne_iff

Premises used: DFunLike.ne_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α → M
s : Finset α
h : ∀ (a : α), a ∈ s ↔ f a ≠ 0
⊢ (⇑{ support := s, toFun := f, mem_support_toFun := h : α →₀ M } : (a : α) → M) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
⊢ Eq (α := (a : α) → M) (⇑0 : (a : α) → M) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
a : α
⊢ Eq.{u_4 + 1} (α := M) ((0 : (a : α) → M) a : M) (0 : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
⊢ Eq.{u_1 + 1} (α := Finset α) (support.{u_1, u_4} (M := M) 0) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
⊢ Eq (α := α →₀ M) default 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ ∀ {a : α}, a ∈ f.support ↔ Ne.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
@(f.mem_support_toFun)

Premises used: Finsupp.mem_support_toFun
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ Function.support.{u_1, u_4} (M := M) (⇑f : (a : α) → M) = (↑f.support : Set α)

Tactic:
Set.ext fun _x => mem_support_iff.symm

Premises used: Finsupp.mem_support_iff, Set.ext, Iff.symm
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
a : α
⊢ a ∉ f.support ↔ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
not_iff_comm.1 mem_support_iff.symm

Premises used: Finsupp.mem_support_iff, Iff.mp, Iff.symm, not_iff_comm
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
rw : Eq (α := (a : α) → M) (⇑f : (a : α) → M) (⇑0 : (a : α) → M) ↔ f = 0
rw₁ rw₂ : f = 0 ↔ f = 0
⊢ Eq (α := (a : α) → M) (⇑f : (a : α) → M) 0 ↔ f = 0

Tactic:
rw [← coe_zero, DFunLike.coe_fn_eq]

Premises used: DFunLike.coe_fn_eq, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
have hf : f a = 0 := notMem_support_iff.1 h
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
rwa :
  ∀ (h : a ∉ g.support) (hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M))
    (hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)

Tactic:
rwa [h₁, notMem_support_iff] at h

Premises used: Finsupp.notMem_support_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)

Tactic:
have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h_1 : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
h : a ∉ f.support
hf : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
hg : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
rw : Eq.{u_4 + 1} (α := M) (0 : M) ((g : (a : α) → M) a : M)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)

Tactic:
rw [hf, hg]
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)

Tactic:
exact if h : a ∈ f.support then h₂ a h else by
        have hf : f a = 0 := notMem_support_iff.1 h
        have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
        rw [hf, hg]

Premises used: Finsupp.support
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f g : α →₀ M
h : f.support = g.support ∧ ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
a : α
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)

Tactic:
classical
      exact if h : a ∈ f.support then h₂ a h else by
        have hf : f a = 0 := notMem_support_iff.1 h
        have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
        rw [hf, hg]

Premises used: Finsupp.support
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ f.support = ∅ ↔ f = 0

Tactic:
mod_cast @Function.support_eq_empty_iff _ _ _ f

Premises used: congrArg, Finsupp.fun_support_eq, cast, Function.support_eq_empty_iff, Iff, congr, Finsupp.coe_eq_zero._simp_1, Finset.coe_eq_empty._simp_1, congrFun', EmptyCollection.emptyCollection, Eq, Eq.trans
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
contrapose! : f.support = ∅ ↔ f = 0
⊢ f.support.Nonempty ↔ f ≠ 0

Tactic:
contrapose!
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ f.support = ∅ ↔ f = 0

Tactic:
support_eq_empty

Premises used: Finsupp.support_eq_empty
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ f.support = ∅ ↔ f = 0

Tactic:
exact support_eq_empty

Premises used: Finsupp.support_eq_empty
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ #f.support = 0 ↔ f = 0

Tactic:
simp