awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
refine_1 :
  Eq (α := ℕ →₀ M)
    (mapDomain (fun (x : ℕ) ↦ x + 1)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l))
    (mapDomain (fun (x : ℕ) ↦ x + 1) (comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) ⋯))
refine_2 : ∀ x ∈ (↑(erase 0 l).support : Set ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (x : ℕ) ↦ x + 1) x
⊢ mapDomain (fun (x : ℕ) ↦ x + 1) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l) =
    erase 0 l

Tactic:
refine .trans ?_ (mapDomain_comapDomain _ (add_left_injective 1) _ fun _ ↦ ?_)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
refine_1 :
  (comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l =
    comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) ⋯
⊢ Eq (α := ℕ →₀ M)
    (mapDomain (fun (x : ℕ) ↦ x + 1)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l))
    (mapDomain (fun (x : ℕ) ↦ x + 1) (comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) ⋯))

Tactic:
congr
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
refine_1 :
  ∀ (a : ℕ),
    Eq (α := M)
      ((((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l : ℕ →₀ M) : (a : ℕ) → M) a :
        M)
      ((comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) ⋯ : (a : ℕ) → M) a : M)
⊢ (comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l =
    comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) ⋯

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
a : ℕ
⊢ Eq (α := M)
    ((((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l : ℕ →₀ M) : (a : ℕ) → M) a : M)
    ((comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) ⋯ : (a : ℕ) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
x : ℕ
⊢ x ∈ (↑(erase 0 l).support : Set ℕ) → Membership.mem (γ := Set ℕ) (Set.range fun (x : ℕ) ↦ x + 1) x

Tactic:
simp_all [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (mapDomain f l) ⋯ : (a : α) → M) a : M) ((l : (a : α) → M) a : M)
⊢ comapDomain f (mapDomain f l) ⋯ = l

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a : α
h : Eq.{u_5 + 1} (α := M) ((mapDomain f l : (a : β) → M) (f a) : M) ((l : (a : α) → M) a : M)
h₁ h₂ : Eq.{u_5 + 1} (α := M) ((l : (a : α) → M) a : M) ((l : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f (mapDomain f l) ⋯ : (a : α) → M) a : M) ((l : (a : α) → M) a : M)

Tactic:
rw [comapDomain_apply, mapDomain_apply hf]

Premises used: Finsupp.comapDomain_apply, Finsupp.mapDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
⊢ Membership.mem (γ := Set (β →₀ M)) (Set.range (mapDomain f)) x ↔
    ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)

Tactic:
⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_notin_range y x hx, fun h ↦ ?_⟩

Premises used: Eq.rec, Iff.intro, OfNat.ofNat, Eq, DFunLike.coe, Finsupp.mapDomain_notin_range, _private.0.Finsupp.mem_range_mapDomain_iff.match_1
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
refine :
  ∀ (h : ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)),
    Membership.mem (γ := Set (β →₀ M)) (Set.range (mapDomain f)) x
⊢ Membership.mem (γ := Set (β →₀ M)) (Set.range (mapDomain f)) x ↔
    ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)

Tactic:
refine ⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_notin_range y x hx, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
⊢ Membership.mem (γ := Set (β →₀ M)) (Set.range (mapDomain f)) x

Tactic:
⟨Finsupp.comapDomain f x hf.injOn, Finsupp.mapDomain_comapDomain f hf _ fun i hi ↦ ?_⟩

Premises used: Set.Mem, Function.Injective.injOn, setOf, Finsupp.mapDomain_comapDomain, Exists.intro, Set.range, Finsupp.comapDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
refine : ∀ (i : β) (hi : i ∈ (↑x.support : Set β)), i ∈ Set.range f
⊢ Membership.mem (γ := Set (β →₀ M)) (Set.range (mapDomain f)) x

Tactic:
refine ⟨Finsupp.comapDomain f x hf.injOn, Finsupp.mapDomain_comapDomain f hf _ fun i hi ↦ ?_⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
i : β
hi : i ∈ (↑x.support : Set β)
by_contra : ∀ (hc : i ∉ Set.range f), False
⊢ i ∈ Set.range f

Tactic:
by_contra hc
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
i : β
hi : i ∈ (↑x.support : Set β)
hc : i ∉ Set.range f
⊢ ¬Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) i : M) (0 : M)

Tactic:
simp only [Finset.mem_coe, Finsupp.mem_support_iff, ne_eq] at hi

Premises used: Finsupp.mem_support_iff, ne_eq, Finset.mem_coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
i : β
hc : i ∉ Set.range f
hi : ¬Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) i : M) (0 : M)
⊢ False

Tactic:
hi (h _ hc)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
i : β
hc : i ∉ Set.range f
hi : ¬Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) i : M) (0 : M)
⊢ False

Tactic:
exact hi (h _ hc)
-- 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 : α → Prop
inst_1 : DecidablePred p_1
f_1 : α →₀ M
p : α → Prop
inst_2 : DecidablePred p
f : α →₀ M
a : α
pos : ∀ (h : p a), a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
neg : ∀ (h : ¬p a), a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) 0 0
⊢ a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) (if p a then (f : (a : α) → M) a else 0 : M) (0 : M)

Tactic:
split_ifs with h
-- 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 : α → Prop
inst_1 : DecidablePred p_1
f_1 : α →₀ M
p : α → Prop
inst_2 : DecidablePred p
f : α →₀ M
a : α
h : p a
pos :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ True ↔
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
simp only [h, mem_filter, mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finset.mem_filter
-- 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 : α → Prop
inst_1 : DecidablePred p_1
f_1 : α →₀ M
p : α → Prop
inst_2 : DecidablePred p
f : α →₀ M
a : α
h : p a
pos :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ True →
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
pos₁ :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) →
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ True
pos₂ pos₃ :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) →
    True → Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
pos₄ :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) →
    True → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → False
pos₅ pos₆ :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) →
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ True
pos₇ : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
pos₈ :
  Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) →
    True → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → False
⊢ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ True ↔
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
tauto
-- 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 : α → Prop
inst_1 : DecidablePred p_1
f_1 : α →₀ M
p : α → Prop
inst_2 : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
neg : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False ↔ Ne.{u_5 + 1} (α := M) 0 0
⊢ a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) 0 0

Tactic:
simp only [h, mem_filter, mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finset.mem_filter
-- 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 : α → Prop
inst_1 : DecidablePred p_1
f_1 : α →₀ M
p : α → Prop
inst_2 : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
neg : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False → Ne.{u_5 + 1} (α := M) 0 0
neg₁ neg₂ : Ne.{u_5 + 1} (α := M) 0 0 → Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False
⊢ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False ↔ Ne.{u_5 + 1} (α := M) 0 0

Tactic:
tauto
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) ((filter p f : (a : α) → M) a : M) (if p a then (f : (a : α) → M) a else 0 : M)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a : α
h :
  ∀ (a_1 : α),
    Eq.{u_5 + 1} (α := M) ((filter (fun (x : α) ↦ a = x) f : (a : α) → M) a_1 : M)
      (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) a_1 : M)
⊢ filter (fun (x : α) ↦ a = x) f = single a ((f : (a : α) → M) a)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a a_1 : α
h :
  Eq.{u_5 + 1} (α := M) (if a = a_1 then (f : (a : α) → M) a_1 else 0 : M)
    (if a = a_1 then (f : (a : α) → M) a else 0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((filter (fun (x : α) ↦ a = x) f : (a : α) → M) a_1 : M)
    (((single a ((f : (a : α) → M) a) : α →₀ M) : (a : α) → M) a_1 : M)

Tactic:
rw [filter_apply, single_apply]

Premises used: Finsupp.filter_apply, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a a_1 : α
h : a = a_1 → a_1 = a
⊢ Eq.{u_5 + 1} (α := M) (if a = a_1 then (f : (a : α) → M) a_1 else 0 : M)
    (if a = a_1 then (f : (a : α) → M) a else 0 : M)

Tactic:
congr!
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a a_1 : α
h : a = a_1
⊢ a_1 = a

Tactic:
simp_all
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a : α
⊢ filter (fun (x : α) ↦ x = a) f = single a ((f : (a : α) → M) a)

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
h :
  ∀ (x : α),
    Eq.{u_5 + 1} (α := M) ((filter p f : (a : α) → M) x : M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M) x : M)
⊢ Eq (α := (a : α) → M) (⇑(filter p f) : (a : α) → M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M))

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
x : α
⊢ Eq.{u_5 + 1} (α := M) ((filter p f : (a : α) → M) x : M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M) x : M)

Tactic:
simp [filter_apply, Set.indicator_apply]

Premises used: Set.indicator_apply, Finsupp.filter_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
⊢ filter p f = 0 ↔ ∀ (x : α), p x → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)

Tactic:
simp [DFunLike.ext_iff, filter_eq_indicator]

Premises used: Finsupp.filter_eq_indicator, DFunLike.ext_iff
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
⊢ filter p f = f ↔ ∀ (x : α), Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M) → p x

Tactic:
simp only [DFunLike.ext_iff, filter_eq_indicator, Set.indicator_apply_eq_self, Set.mem_setOf_eq,
    not_imp_comm]

Premises used: Finsupp.filter_eq_indicator, not_imp_comm, Set.mem_setOf_eq, DFunLike.ext_iff, Set.indicator_apply_eq_self
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
a : α
h : p a
⊢ Eq.{u_5 + 1} (α := M) ((filter p f : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
if_pos h

Premises used: if_pos, ite
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
a : α
h : ¬p a
⊢ Eq.{u_5 + 1} (α := M) ((filter p f : (a : α) → M) a : M) (0 : M)

Tactic:
if_neg h

Premises used: if_neg, ite
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
⊢ (filter p f).support = {x ∈ f.support | p x}

Tactic:
rfl

Premises used: Finset.filter, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
rw : support.{u_1, u_5} (M := M) (filter p 0) = ∅
rw₁ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ support.{u_1, u_5} (M := M) 0 | p x}) ∅
rw₂ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ ∅ | p x}) ∅
rw₃ rw₄ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0

Tactic:
rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]

Premises used: Finsupp.support_zero, Finset.filter_empty, Finsupp.support_eq_empty, Finsupp.support_filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
classical : support.{u_1, u_5} (M := M) (filter p 0) = ∅
classical₁ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ support.{u_1, u_5} (M := M) 0 | p x}) ∅
classical₂ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ ∅ | p x}) ∅
classical₃ classical₄ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0

Tactic:
classical rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]

Premises used: Finsupp.support_zero, Finset.filter_empty, Finsupp.support_eq_empty, Finsupp.support_filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
a : α
b : M
h : p a
⊢ Eq (α := α →₀ M) (filter p (single a b)) (single a b)

Tactic:
(filter_eq_self_iff _ _).2 fun _ hx => (single_apply_ne_zero.1 hx).1.symm ▸ h

Premises used: Iff.mpr, Eq.rec, Finsupp.single_apply_ne_zero, And.left, Iff.mp, Eq.symm, Finsupp.filter_eq_self_iff
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
a : α
b : M
h : ¬p a
⊢ Eq (α := α →₀ M) (filter p (single a b)) 0

Tactic:
(filter_eq_zero_iff _ _).2 fun _ hpx =>
    single_apply_eq_zero.2 fun hxa => absurd hpx (hxa.symm ▸ h)

Premises used: Iff.mpr, Eq.rec, Finsupp.filter_eq_zero_iff, Finsupp.single_apply_eq_zero, absurd, Eq.symm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
inst_2 : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g = ∏ x ∈ (filter p f).support, g x ((f : (a : α) → M) x)

Tactic:
Finset.prod_congr rfl fun x hx => ?_

Premises used: Finset.prod_congr, Finsupp.prod, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
inst_2 : CommMonoid N
g : α → M → N
refine : ∀ (x : α) (hx : x ∈ (filter p f).support), g x ((filter p f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
⊢ (filter p f).prod g = ∏ x ∈ (filter p f).support, g x ((f : (a : α) → M) x)

Tactic:
refine Finset.prod_congr rfl fun x hx => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
inst_2 : CommMonoid N
g : α → M → N
x : α
hx : x ∈ (filter p f).support
⊢ x ∈ f.support ∧ p x

Tactic:
rw [support_filter, Finset.mem_filter] at hx

Premises used: Finset.mem_filter, Finsupp.support_filter
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
inst_2 : CommMonoid N
g : α → M → N
x : α
hx : x ∈ f.support ∧ p x
rw rw₁ : g x ((f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
⊢ g x ((filter p f : (a : α) → M) x) = g x ((f : (a : α) → M) x)

Tactic:
rw [filter_apply_pos _ _ hx.2]

Premises used: Finsupp.filter_apply_pos, And.right
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
inst_2 : CommMonoid N
g : α → M → N
simp_rw :
  HMul.hMul (α := N) (∏ x ∈ (filter p f).support, g x ((f : (a : α) → M) x))
      (∏ x ∈ (filter (fun (a : α) ↦ ¬p a) f).support, g x ((f : (a : α) → M) x)) =
    f.prod g
simp_rw₁ :
  HMul.hMul (α := N) (∏ x ∈ f.support with p x, g x ((f : (a : α) → M) x))
      (∏ x ∈ f.support with ¬p x, g x ((f : (a : α) → M) x)) =
    f.prod g
simp_rw₂ : ∏ x ∈ f.support, g x ((f : (a : α) → M) x) = f.prod g
⊢ (filter p f).prod g * (filter (fun (a : α) ↦ ¬p a) f).prod g = f.prod g

Tactic:
simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not, Finsupp.prod]

Premises used: Finsupp.prod_filter_index, Finset.prod_filter_mul_prod_filter_not, Finsupp.support_filter, Finsupp.prod
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
G : Type u_8
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
inst_2 : CommGroup G
g : α → M → G
⊢ f.prod g / (filter p f).prod g = (filter (fun (a : α) ↦ ¬p a) f).prod g

Tactic:
div_eq_of_eq_mul' (prod_filter_mul_prod_filter_not _ _ _).symm

Premises used: div_eq_of_eq_mul', Finsupp.prod_filter_mul_prod_filter_not, Eq.symm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
h :
  ∀ (a : α),
    Eq.{u_5 + 1} (α := M) ((filter p f + filter (fun (x : α) ↦ ¬p x) f : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ filter p f + filter (fun (x : α) ↦ ¬p x) f = f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
a : α
h :
  HAdd.hAdd (α := M) (β := M) (if p a then (f : (a : α) → M) a else 0 : M)
      (if p a then 0 else (f : (a : α) → M) a : M) =
    (f : (a : α) → M) a
⊢ Eq.{u_5 + 1} (α := M) ((filter p f + filter (fun (x : α) ↦ ¬p x) f : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
simp [filter_apply]

Premises used: Finsupp.filter_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
a : α
h : p a → HAdd.hAdd (α := M) (β := M) ((f : (a : α) → M) a : M) (0 : M) = (f : (a : α) → M) a
h₁ : ¬p a → HAdd.hAdd (α := M) (β := M) (0 : M) ((f : (a : α) → M) a : M) = (f : (a : α) → M) a
⊢ HAdd.hAdd (α := M) (β := M) (if p a then (f : (a : α) → M) a else 0 : M)
      (if p a then 0 else (f : (a : α) → M) a : M) =
    (f : (a : α) → M) a

Tactic:
split
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
a : α
h : p a
⊢ HAdd.hAdd (α := M) (β := M) ((f : (a : α) → M) a : M) (0 : M) = (f : (a : α) → M) a

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
a : α
h : ¬p a
⊢ HAdd.hAdd (α := M) (β := M) (0 : M) ((f : (a : α) → M) a : M) = (f : (a : α) → M) a

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
y : M
rw :
  (∃ a ∈ f.support, (f : (a : α) → M) a = y) ↔
    y ≠ 0 ∧ Membership.mem (γ := Set M) (Set.range.{u_5, u_1 + 1} (ι := α) (⇑f : (a : α) → M)) y
⊢ y ∈ f.frange ↔ y ≠ 0 ∧ Membership.mem (γ := Set M) (Set.range.{u_5, u_1 + 1} (ι := α) (⇑f : (a : α) → M)) y

Tactic:
rw [frange, @Finset.mem_image _ _ (Classical.decEq _) _ f.support]

Premises used: Finset.mem_image, Finsupp.frange
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, (f : (a : α) → M) a = y) ↔
    y ≠ 0 ∧ Membership.mem (γ := Set M) (Set.range.{u_5, u_1 + 1} (ι := α) (⇑f : (a : α) → M)) y

Tactic:
⟨fun ⟨x, hx1, hx2⟩ => ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩, fun ⟨hy, x, hx⟩ =>
    ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩

Premises used: Iff.mpr, Finsupp.mem_support_iff, _private.0.Finsupp.mem_frange.match_3, _private.0.Finsupp.mem_frange.match_2, Finsupp.support, Membership.mem, Exists, Eq.rec, Ne, And, And.intro, Iff.intro, Exists.intro, Iff.mp, Set.range, OfNat.ofNat, Eq.symm, Eq, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
y : M
⊢ (∃ a ∈ f.support, (f : (a : α) → M) a = y) ↔
    y ≠ 0 ∧ Membership.mem (γ := Set M) (Set.range.{u_5, u_1 + 1} (ι := α) (⇑f : (a : α) → M)) y

Tactic:
exact ⟨fun ⟨x, hx1, hx2⟩ => ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩, fun ⟨hy, x, hx⟩ =>
    ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
⊢ 0 ∉ f.frange

Tactic:
fun H => (mem_frange.1 H).1 rfl

Premises used: And.left, Iff.mp, Finsupp.mem_frange, Not, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
x : α
y : M
⊢ frange (single x y) ⊆ {y}

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
x : α
y : M
⊢ frange (single x y) ⊆ {y}

Tactic:
classical grind
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
x : α
f : α →₀ M
h : x ∈ f.support
⊢ Membership.mem (α := M) f.frange ((f : (a : α) → M) x : M)

Tactic:
simp_all
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
⊢ Set.range.{u_5, u_1 + 1} (ι := α) (⇑f : (a : α) → M) ⊆ insert 0 (↑f.frange : Set M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
⊢ (insert 0 (↑f.frange : Set M)).Finite

Tactic:
simp