awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α × β →₀ M
a : α
⊢ ∀ (a_1 : β),
    a_1 ∈ filterMap (fun (x : α × β) ↦ if x.1 = a then some x.2 else none) f.support ⋯ ↔
      Ne.{u_5 + 1} (α := M) ((f : (a : α × β) → M) (a, a_1) : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α × β →₀ M
⊢ ∀ (a : α),
    a ∈ image Prod.fst f.support ↔
      { support := filterMap (fun (x : α × β) ↦ if x.1 = a then some x.2 else none) f.support ⋯,
          toFun := fun (b : β) ↦ (f : (a : α × β) → M) (a, b), mem_support_toFun := ⋯ : β →₀ M } ≠
        0

Tactic:
simp [DFunLike.ext_iff]

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α × β →₀ M
⊢ { support := image Prod.fst f.support,
        toFun := fun (a : α) ↦
          { support := filterMap (fun (x : α × β) ↦ if x.1 = a then some x.2 else none) f.support ⋯,
            toFun := fun (b : β) ↦ (f : (a : α × β) → M) (a, b), mem_support_toFun := ⋯ : β →₀ M },
        mem_support_toFun := ⋯ : α →₀ β →₀ M }.support =
    image Prod.fst f.support

Tactic:
congr!
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α →₀ β →₀ M
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)
⊢ f.uncurry.curry = f

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

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

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

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
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))))
rw₁ rw₂ : Eq (α := α →₀ β →₀ M) (Finsupp.curry (single a m)) (Finsupp.curry (single (a.1, a.2) m))
⊢ Eq (α := α →₀ β →₀ M) (Finsupp.curry (single a m)) (single a.1 (single a.2 m))

Tactic:
rw [← curry_uncurry (single _ _), uncurry_single]

Premises used: Finsupp.uncurry_single, Finsupp.curry_uncurry, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : Zero M
inst_1 : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← sum_uncurry_index', uncurry_curry]

Premises used: Finsupp.uncurry_curry, Finsupp.sum_uncurry_index'
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α × β →₀ M
p : α → Prop
inst_1 : DecidablePred p
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)
⊢ (filter (fun (a : α × β) ↦ p a.1) f).curry = filter p f.curry

Tactic:
ext a b
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α × β →₀ M
p : α → Prop
inst_1 : DecidablePred p
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:
simp [filter_apply, apply_ite (DFunLike.coe · b)]

Premises used: apply_ite, Finsupp.filter_apply, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : AddZeroClass M
x x_1 : α × β →₀ M
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)
⊢ Equiv.toFun curryEquiv (x + x_1) = Equiv.toFun curryEquiv x + Equiv.toFun curryEquiv x_1

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : AddZeroClass M
x x_1 : α × β →₀ M
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:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
⊢ Eq (α := (a : α × β →₀ M) → α →₀ β →₀ M) (⇑curryAddEquiv : (a : α × β →₀ M) → α →₀ β →₀ M) Finsupp.curry

Tactic:
rfl

Premises used: Finsupp.curry, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ ∀ (a : α ⊕ β),
    a ∈ f.support.disjSum g.support ↔ Ne.{u_3 + 1} (α := γ) (Sum.elim (⇑f : (a : α) → γ) (⇑g : (a : β) → γ) a) 0

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ Eq (α := (a : α ⊕ β) → γ) (⇑(f.sumElim g) : (a : α ⊕ β) → γ) (Sum.elim (⇑f : (a : α) → γ) (⇑g : (a : β) → γ))

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
x : α ⊕ β
⊢ Eq.{u_3 + 1} (α := γ) ((f.sumElim g : (a : α ⊕ β) → γ) x : γ) (Sum.elim (⇑f : (a : α) → γ) (⇑g : (a : β) → γ) x : γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
x : α
⊢ Eq.{u_3 + 1} (α := γ) ((f.sumElim g : (a : α ⊕ β) → γ) (Sum.inl x) : γ) ((f : (a : α) → γ) x : γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
x : β
⊢ Eq.{u_3 + 1} (α := γ) ((f.sumElim g : (a : α ⊕ β) → γ) (Sum.inr x) : γ) ((g : (a : β) → γ) x : γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
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) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ) ((0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 0) 0

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
val : α
⊢ Eq.{u_3 + 1} (α := γ) ((sumElim 0 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ) ((0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
val : β
⊢ Eq.{u_3 + 1} (α := γ) ((sumElim 0 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ) ((0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
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) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim (single a c) 0) (single (Sum.inl a) c)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α
c : γ
val : α
⊢ Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)

Tactic:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α
c : γ
val : β
⊢ Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)

Tactic:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
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) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
h₂ :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₃ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
h₄ :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₅ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
h₆ :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₇ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim (single a c) 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inl a) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim (single a c) 0) (single (Sum.inl a) c)

Tactic:
classical ext (_ | _) <;> simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
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) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 (single b c)) (single (Sum.inr b) c)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β
c : γ
val : α
⊢ Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)

Tactic:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β
c : γ
val : β
⊢ Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)

Tactic:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
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) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
h₂ :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₃ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
h₄ :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₅ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
h₆ :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₇ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((sumElim 0 (single b c) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((single (Sum.inr b) c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (sumElim 0 (single b c)) (single (Sum.inr b) c)

Tactic:
classical ext (_ | _) <;> simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : 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)
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)
⊢ sumElim (single a m₁) (single b m₂) = HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddMonoid M
a : α
b : β
m₁ m₂ : M
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:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddMonoid M
a : α
b : β
m₁ m₂ : M
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:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : 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)
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)
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)
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)
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)
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)
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)
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)
⊢ sumElim (single a m₁) (single b m₂) = HAdd.hAdd (α := α ⊕ β →₀ M) (single (Sum.inl a) m₁) (single (Sum.inr b) m₂)

Tactic:
classical ext (_ | _) <;> simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
g : β →₀ M
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)
h₁ :
  ∀ (val : β),
    Eq.{u_5 + 1} (α := M) ((f.sumElim g : (a : α ⊕ β) → M) (Sum.inr val) : M)
      ((mapDomain Sum.inl f + mapDomain Sum.inr g : (a : α ⊕ β) → M) (Sum.inr val) : M)
⊢ f.sumElim g = mapDomain Sum.inl f + mapDomain Sum.inr g

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
g : β →₀ M
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:
simp [mapDomain_notin_range, Sum.inl_injective, Sum.inr_injective]

Premises used: Sum.inr_injective, Sum.inl_injective, Finsupp.mapDomain_notin_range
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
g : β →₀ M
val : β
⊢ Eq.{u_5 + 1} (α := M) ((f.sumElim g : (a : α ⊕ β) → M) (Sum.inr val) : M)
    ((mapDomain Sum.inl f + mapDomain Sum.inr g : (a : α ⊕ β) → M) (Sum.inr val) : M)

Tactic:
simp [mapDomain_notin_range, Sum.inl_injective, Sum.inr_injective]

Premises used: Sum.inr_injective, Sum.inl_injective, Finsupp.mapDomain_notin_range
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
g : β →₀ M
⊢ mapDomain Sum.swap (f.sumElim g) = g.sumElim f

Tactic:
simp [sumElim_eq_add, mapDomain_add, ← mapDomain_comp, Function.comp_def, add_comm]

Premises used: add_comm, Function.comp_def, Finsupp.mapDomain_comp, Finsupp.mapDomain_add, Finsupp.sumElim_eq_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι₁ : Type u_12
ι₂ : Type u_13
α : Type u_14
M : Type u_15
inst : Zero α
inst_1 : CommMonoid M
f₁ : ι₁ →₀ α
f₂ : ι₂ →₀ α
g : ι₁ ⊕ ι₂ → α → M
⊢ (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)

Tactic:
simp [Finsupp.prod, Finset.prod_disjSum]

Premises used: Finset.prod_disjSum, Finsupp.prod
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
h :
  ∀ (a : α), Eq.{u_3 + 1} (α := γ) ((comapDomain Sum.inl (f.sumElim g) ⋯ : (a : α) → γ) a : γ) ((f : (a : α) → γ) a : γ)
⊢ comapDomain Sum.inl (f.sumElim g) ⋯ = f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
a : α
⊢ Eq.{u_3 + 1} (α := γ) ((comapDomain Sum.inl (f.sumElim g) ⋯ : (a : α) → γ) a : γ) ((f : (a : α) → γ) a : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
h :
  ∀ (a : β), Eq.{u_3 + 1} (α := γ) ((comapDomain Sum.inr (f.sumElim g) ⋯ : (a : β) → γ) a : γ) ((g : (a : β) → γ) a : γ)
⊢ comapDomain Sum.inr (f.sumElim g) ⋯ = g

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
a : β
⊢ Eq.{u_3 + 1} (α := γ) ((comapDomain Sum.inr (f.sumElim g) ⋯ : (a : β) → γ) a : γ) ((g : (a : β) → γ) a : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α →₀ γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inl a : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((a.sumElim 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inl a : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((a.sumElim 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (embDomain Embedding.inl a) (a.sumElim 0)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α →₀ γ
val : α
⊢ Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inl a : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((a.sumElim 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)

Tactic:
simp [embDomain_apply]

Premises used: Finsupp.embDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α →₀ γ
val : β
⊢ Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inl a : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((a.sumElim 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)

Tactic:
simp [embDomain_apply]

Premises used: Finsupp.embDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β →₀ γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inr b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((sumElim 0 b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inr b : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((sumElim 0 b : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (embDomain Embedding.inr b) (sumElim 0 b)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β →₀ γ
val : α
⊢ Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inr b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((sumElim 0 b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)

Tactic:
simp [embDomain_apply]

Premises used: Finsupp.embDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β →₀ γ
val : β
⊢ Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inr b : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((sumElim 0 b : (a : α ⊕ β) → γ) (Sum.inr val) : γ)

Tactic:
simp [embDomain_apply]

Premises used: Finsupp.embDomain_apply