awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
⊢ 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
have h : p a → HAdd.hAdd (α := M) (β := M) ((f : (a : α) → M) a : M) (0 : M) = (f : (a : α) → M) a
Tactic: split
-- 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 : α
h : p a → HAdd.hAdd (α := M) (β := M) ((f : (a : α) → M) a : M) (0 : 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
have h₁ : ¬p a → HAdd.hAdd (α := M) (β := M) (0 : M) ((f : (a : α) → M) a : M) = (f : (a : α) → M) a
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
y : M
⊢ y ∈ f.frange ↔ y ≠ 0 ∧ Membership.mem (γ := Set M) (Set.range.{u_5, u_1 + 1} (ι := α) (⇑f : (a : α) → M)) y
have 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
Tactic: rw [frange, @Finset.mem_image _ _ (Classical.decEq _) _ f.support]
-- 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 p : α → Prop
f : α →₀ M
a : Subtype p
⊢ a ∈ Finset.subtype p f.support ↔ Ne.{u_5 + 1} (α := M) (((⇑f : (a : α) → M) ∘ Subtype.val (p := p)) a) 0
have 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
Tactic: simp only [@mem_subtype _ _ (Classical.decPred p), mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
have rw : (subtypeDomain p f).support = Finset.subtype p f.support
Tactic: rw [Subsingleton.elim D]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
p : α → Prop
f g : α →₀ 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)
have 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)
Tactic: simp_rw [DFunLike.ext_iff, subtypeDomain_apply, Subtype.forall]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ subtypeDomain p f = subtypeDomain p g ↔
    ∀ (x : α), p x → Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) x : M) ((g : (a : α) → M) x : M)
have 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)
Tactic: simp_rw [DFunLike.ext_iff, subtypeDomain_apply, Subtype.forall]
-- 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 : 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
have 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
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_
-- 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 : 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
⊢ ((subtypeDomain p v).prod fun (a : Subtype p) (b : M) ↦ h (↑a : α) b) = v.prod h
have 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₂
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_
-- 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 : 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₂
⊢ ((subtypeDomain p v).prod fun (a : Subtype p) (b : M) ↦ h (↑a : α) b) = v.prod h
have 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
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_
-- 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 : 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
⊢ ((subtypeDomain p v).prod fun (a : Subtype p) (b : M) ↦ h (↑a : α) b) = v.prod h
have 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))
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_
-- 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 : AddZeroClass M
p_1 : α → Prop
v v' : α →₀ M
p : α → Prop
inst_1 : DecidablePred p
f g : α →₀ 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))
have 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))
Tactic: simp_rw [coe_add, filter_eq_indicator]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ Eq (α := α →₀ M) (single x ((filter p f : (a : α) → M) x) : α →₀ M) (single x ((f : (a : α) → M) x) : α →₀ M)
have rw : Eq (α := α →₀ M) (single x ((f : (a : α) → M) x) : α →₀ M) (single x ((f : (a : α) → M) x) : α →₀ M)
Tactic: rw [filter_apply_pos _ _ (mem_filter.1 hx).2]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
have pos : ∀ (h : a ∈ f.support), ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Tactic: by_cases h : a ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
have neg : ∀ (h : a ∉ f.support), ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Tactic: by_cases h : a ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
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
have ha₁ : 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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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_1 ∈ f ::ₘ s, a ∈ f_1.support
have neg : ∀ (f' : α →₀ M) (h₀ : f' ∈ s) (h₁ : a ∈ f'.support), ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Tactic: rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
⊢ Eq (α := α × β →₀ M) (Finsupp.uncurry (single a (single b m))) (single (a, b) m)
have 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)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α
b : β
m : M
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)
have 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)
Tactic: rcases eq_or_ne a x with rfl | hne
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne a x with rfl | hne
-- 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 : α →₀ β →₀ M
⊢ f.uncurry.curry = f
have h : ∀ (a : α) (b : β),
  Eq.{u_5 + 1} (α := M) ((((f.uncurry.curry : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) b : M)
    ((((f : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) b : M)
Tactic: ext a b
-- 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 : α × β →₀ M
⊢ f.curry.uncurry = f
have h : ∀ (a : α) (b : β),
  Eq.{u_5 + 1} (α := M) ((f.curry.uncurry : (a : α × β) → M) (a, b) : M) ((f : (a : α × β) → M) (a, b) : M)
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α × β
m : M
⊢ Eq (α := α →₀ β →₀ M) (Finsupp.curry (single a m)) (single a.1 (single a.2 m))
have rw : Eq (α := α →₀ β →₀ M) (Finsupp.curry (single a m)) (Finsupp.curry (Finsupp.uncurry (single a.1 (single a.2 m))))
Tactic: rw [← curry_uncurry (single _ _), uncurry_single]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
a : α × β
m : M
rw : Eq (α := α →₀ β →₀ M) (Finsupp.curry (single a m)) (Finsupp.curry (Finsupp.uncurry (single a.1 (single a.2 m))))
⊢ Eq (α := α →₀ β →₀ M) (Finsupp.curry (single a m)) (single a.1 (single a.2 m))
have rw₁ : Eq (α := α →₀ β →₀ M) (Finsupp.curry (single a m)) (Finsupp.curry (single (a.1, a.2) m))
Tactic: rw [← curry_uncurry (single _ _), uncurry_single]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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.curry.sum fun (a : α) (f : β →₀ M) ↦ f.sum (g a))
    (f.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
have rw : Eq.{u_6 + 1} (α := N) (f.curry.uncurry.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
  (f.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
Tactic: rw [← sum_uncurry_index', uncurry_curry]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
rw :
  Eq.{u_6 + 1} (α := N) (f.curry.uncurry.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
    (f.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
⊢ Eq.{u_6 + 1} (α := N) (f.curry.sum fun (a : α) (f : β →₀ M) ↦ f.sum (g a))
    (f.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
have rw₁ : Eq.{u_6 + 1} (α := N) (f.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c) (f.sum fun (p : α × β) (c : M) ↦ g p.1 p.2 c)
Tactic: rw [← sum_uncurry_index', uncurry_curry]
-- 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 : α × β →₀ M
p : α → Prop
inst_1 : DecidablePred p
⊢ (filter (fun (a : α × β) ↦ p a.1) f).curry = filter p f.curry
have h : ∀ (a : α) (b : β),
  Eq.{u_5 + 1} (α := M)
    (((((filter (fun (a : α × β) ↦ p a.1) f).curry : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) b : M)
    ((((filter p f.curry : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) b : M)
Tactic: ext a b
-- 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 : AddZeroClass M
x x_1 : α × β →₀ M
⊢ Equiv.toFun curryEquiv (x + x_1) = Equiv.toFun curryEquiv x + Equiv.toFun curryEquiv x_1
have h : ∀ (a : α) (a_1 : β),
  Eq.{u_5 + 1} (α := M) ((((Equiv.toFun curryEquiv (x + x_1) : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) a_1 : M)
    ((((Equiv.toFun curryEquiv x + Equiv.toFun curryEquiv x_1 : (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
β : Type u_2
γ : Type u_3
inst : Zero γ
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 0) 0
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ) ((sumElim 0 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ) ((0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ) ((0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 0) 0
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ) ((sumElim 0 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ) ((0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α
c : γ
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim (single a c) 0) (single (Sum.inl a) c)
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α
c : γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim (single a c) 0) (single (Sum.inl a) c)
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α
c : γ
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim (single a c) 0) (single (Sum.inl a) c)
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: classical ext (_ | _) <;> simp [single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α
c : γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim (single a c) 0) (single (Sum.inl a) c)
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: classical ext (_ | _) <;> simp [single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β
c : γ
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 (single b c)) (single (Sum.inr b) c)
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β
c : γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 (single b c)) (single (Sum.inr b) c)
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β
c : γ
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 (single b c)) (single (Sum.inr b) c)
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: classical ext (_ | _) <;> simp [single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β
c : γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 (single b c)) (single (Sum.inr b) c)
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: classical ext (_ | _) <;> simp [single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddMonoid M
a : α
b : β
m₁ m₂ : M
⊢ sumElim (single a m₁) (single b m₂) = HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂)
have h : ∀ (val : α),
  Eq.{u_5 + 1} (α := M) ((sumElim (single a m₁) (single b m₂) : (a : α ⊕ β) → M) (Sum.inl val) : M)
    ((HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂) : (a : α ⊕ β) → M) (Sum.inl val) : 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 : AddMonoid M
a : α
b : β
m₁ m₂ : M
h :
  ∀ (val : α),
    Eq.{u_5 + 1} (α := M) ((sumElim (single a m₁) (single b m₂) : (a : α ⊕ β) → M) (Sum.inl val) : M)
      ((HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂) : (a : α ⊕ β) → M) (Sum.inl val) :
        M)
⊢ sumElim (single a m₁) (single b m₂) = HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂)
have h₁ : ∀ (val : β),
  Eq.{u_5 + 1} (α := M) ((sumElim (single a m₁) (single b m₂) : (a : α ⊕ β) → M) (Sum.inr val) : M)
    ((HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂) : (a : α ⊕ β) → M) (Sum.inr val) : 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 : AddMonoid M
a : α
b : β
m₁ m₂ : M
⊢ sumElim (single a m₁) (single b m₂) = HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂)
have h : ∀ (val : α),
  Eq.{u_5 + 1} (α := M) ((sumElim (single a m₁) (single b m₂) : (a : α ⊕ β) → M) (Sum.inl val) : M)
    ((HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂) : (a : α ⊕ β) → M) (Sum.inl val) : M)
Tactic: classical ext (_ | _) <;> simp [single_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddMonoid M
a : α
b : β
m₁ m₂ : M
h :
  ∀ (val : α),
    Eq.{u_5 + 1} (α := M) ((sumElim (single a m₁) (single b m₂) : (a : α ⊕ β) → M) (Sum.inl val) : M)
      ((HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂) : (a : α ⊕ β) → M) (Sum.inl val) :
        M)
⊢ sumElim (single a m₁) (single b m₂) = HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂)
have h₁ : ∀ (val : β),
  Eq.{u_5 + 1} (α := M) ((sumElim (single a m₁) (single b m₂) : (a : α ⊕ β) → M) (Sum.inr val) : M)
    ((HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂) : (a : α ⊕ β) → M) (Sum.inr val) : M)
Tactic: classical ext (_ | _) <;> simp [single_apply]
-- 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 : α →₀ M
g : β →₀ M
⊢ f.sumElim g = mapDomain Sum.inl f + mapDomain Sum.inr g
have h : ∀ (val : α),
  Eq.{u_5 + 1} (α := M) ((f.sumElim g : (a : α ⊕ β) → M) (Sum.inl val) : M)
    ((mapDomain Sum.inl f + mapDomain Sum.inr g : (a : α ⊕ β) → M) (Sum.inl val) : M)
Tactic: ext (_ | _)