awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m
have hif₁ : Set.InjOn f (f ⁻¹' {f a})
Tactic: rw [support_single _ hm, coe_singleton] at hif
Cleared hypotheses: hif, hm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hf : Injective f
l' : α →₀ M
⊢ ∃ (a : β →₀ M), (fun (l : β →₀ M) ↦ comapDomain f l ⋯) a = l'
have h : (fun (l : β →₀ M) ↦ comapDomain f l sorry) (embDomain { toFun := f, inj' := hf : α ↪ β } l') = l'
Tactic: use l'.embDomain ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' (↑v₁.support : Set β))
hv₂ : Set.InjOn f (f ⁻¹' (↑v₂.support : Set β))
hv₁₂ : Set.InjOn f (f ⁻¹' (↑(v₁ + v₂).support : Set β))
⊢ comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂
have h : ∀ (a : α),
  Eq.{u_5 + 1} (α := M) ((comapDomain f (v₁ + v₂) hv₁₂ : (a : α) → M) a : M)
    ((comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂ : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : (↑l.support : Set β) ⊆ Set.range f
| l
have rw : mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β)
  (comapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) l sorry)
Tactic: rw [← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M), embDomain_eq_mapDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : (↑l.support : Set β) ⊆ Set.range f
⊢ mapDomain f (comapDomain f l ⋯) = l
have conv_rhs : mapDomain f (comapDomain f l sorry) =
  mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β)
    (comapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) l sorry)
Tactic: conv_rhs => rw [← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M), embDomain_eq_mapDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
⊢ mapDomain (fun (x : ℕ) ↦ x + 1) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l) =
    erase 0 l
have refine_1 : Eq (α := ℕ →₀ M)
  (mapDomain (fun (x : ℕ) ↦ x + 1) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ M) → ℕ →₀ M) l))
  (mapDomain (fun (x : ℕ) ↦ x + 1) (comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) sorry))
Tactic: refine .trans ?_ (mapDomain_comapDomain _ (add_left_injective 1) _ fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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) ⋯))
⊢ mapDomain (fun (x : ℕ) ↦ x + 1) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l) =
    erase 0 l
have refine_2 : ∀ x ∈ (↑(erase 0 l).support : Set ℕ), Membership.mem (γ := Set ℕ) (Set.range fun (x : ℕ) ↦ x + 1) x
Tactic: refine .trans ?_ (mapDomain_comapDomain _ (add_left_injective 1) _ fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
⊢ 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) ⋯))
have refine_1 : (comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ M) → ℕ →₀ M) l =
  comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
⊢ (comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l =
    comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) ⋯
have refine_1 : ∀ (a : ℕ),
  Eq (α := M)
    ((((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ M) → ℕ →₀ M) l : ℕ →₀ M) : (a : ℕ) → M) a : M)
    ((comapDomain (fun (x : ℕ) ↦ x + 1) (erase 0 l) sorry : (a : ℕ) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
⊢ comapDomain f (mapDomain f l) ⋯ = l
have h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (mapDomain f l) sorry : (a : α) → M) a : M) ((l : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f (mapDomain f l) ⋯ : (a : α) → M) a : M) ((l : (a : α) → M) a : M)
have h : Eq.{u_5 + 1} (α := M) ((mapDomain f l : (a : β) → M) (f a) : M) ((l : (a : α) → M) a : M)
Tactic: rw [comapDomain_apply, mapDomain_apply hf]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f (mapDomain f l) ⋯ : (a : α) → M) a : M) ((l : (a : α) → M) a : M)
have h₁ : Eq.{u_5 + 1} (α := M) ((l : (a : α) → M) a : M) ((l : (a : α) → M) a : M)
Tactic: rw [comapDomain_apply, mapDomain_apply hf]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
have 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
Tactic: refine ⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_notin_range y x hx, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
have refine : ∀ (i : β) (hi : i ∈ (↑x.support : Set β)), i ∈ Set.range f
Tactic: refine ⟨Finsupp.comapDomain f x hf.injOn, Finsupp.mapDomain_comapDomain f hf _ fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 β)
⊢ i ∈ Set.range f
have by_contra : ∀ (hc : i ∉ Set.range f), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
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
⊢ False
have hi₁ : ¬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
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : α
⊢ a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) (if p a then (f : (a : α) → M) a else 0 : M) (0 : M)
have pos : ∀ (h : p a), a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) (if p a then (f : (a : α) → M) a else 0 : M) (0 : M)
have neg : ∀ (h : ¬p a), a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
have 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)
Tactic: simp only [h, mem_filter, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ 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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ 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)
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ 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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ 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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ a ∈ Finset.filter p f.support ↔ Ne.{u_5 + 1} (α := M) 0 0
have neg : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False ↔ Ne.{u_5 + 1} (α := M) 0 0
Tactic: simp only [h, mem_filter, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False ↔ Ne.{u_5 + 1} (α := M) 0 0
have neg : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False → Ne.{u_5 + 1} (α := M) 0 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False ↔ Ne.{u_5 + 1} (α := M) 0 0
have neg₁ : Ne.{u_5 + 1} (α := M) 0 0 → Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧ False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a : α
⊢ filter (fun (x : α) ↦ a = x) f = single a ((f : (a : α) → M) a)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a 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)
have 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)
Tactic: rw [filter_apply, single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a a_1 : α
⊢ 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)
have h : a = a_1 → a_1 = a
Tactic: congr!
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
f : α →₀ M
⊢ Eq (α := (a : α) → M) (⇑(filter p f) : (a : α) → M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M))
have h : ∀ (x : α),
  Eq.{u_5 + 1} (α := M) ((filter p f : (a : α) → M) x : M) (Set.indicator {x : α | p x} (⇑f : (a : α) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
⊢ Eq (α := α →₀ M) (filter p 0) 0
have rw : support.{u_1, u_5} (M := M) (filter p 0) = ∅
Tactic: rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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) = ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0
have rw₁ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ support.{u_1, u_5} (M := M) 0 | p x}) ∅
Tactic: rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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}) ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0
have rw₂ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ ∅ | p x}) ∅
Tactic: rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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}) ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0
have rw₃ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
Tactic: rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
inst_1 : DecidablePred p
⊢ Eq (α := α →₀ M) (filter p 0) 0
have classical : support.{u_1, u_5} (M := M) (filter p 0) = ∅
Tactic: classical rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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) = ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0
have classical₁ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ support.{u_1, u_5} (M := M) 0 | p x}) ∅
Tactic: classical rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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}) ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0
have classical₂ : Eq.{u_1 + 1} (α := Finset α) ({x ∈ ∅ | p x}) ∅
Tactic: classical rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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}) ∅
⊢ Eq (α := α →₀ M) (filter p 0) 0
have classical₃ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
Tactic: classical rw [← support_eq_empty, support_filter, support_zero, Finset.filter_empty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
have refine : ∀ (x : α) (hx : x ∈ (filter p f).support), g x ((filter p f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
Tactic: refine Finset.prod_congr rfl fun x hx => ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
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
⊢ g x ((filter p f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
have hx₁ : x ∈ f.support ∧ p x
Tactic: rw [support_filter, Finset.mem_filter] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ g x ((filter p f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
have rw : g x ((f : (a : α) → M) x) = g x ((f : (a : α) → M) x)
Tactic: rw [filter_apply_pos _ _ hx.2]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 * (filter (fun (a : α) ↦ ¬p a) f).prod g = f.prod g
have 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
Tactic: simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not, Finsupp.prod]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ (filter p f).prod g * (filter (fun (a : α) ↦ ¬p a) f).prod g = f.prod g
have 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
Tactic: simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not, Finsupp.prod]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ (filter p f).prod g * (filter (fun (a : α) ↦ ¬p a) f).prod g = f.prod g
have simp_rw₂ : ∏ x ∈ f.support, g x ((f : (a : α) → M) x) = f.prod g
Tactic: simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not, Finsupp.prod]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
⊢ filter p f + filter (fun (x : α) ↦ ¬p x) f = f
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
a : α
⊢ Eq.{u_5 + 1} (α := M) ((filter p f + filter (fun (x : α) ↦ ¬p x) f : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have 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
Tactic: simp [filter_apply]