awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
rw :
  card.{u_1} (α := α) ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s)) =
    s.card
rw₁ rw₂ : s.card = s.card
⊢ (Finsupp.sum (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s) fun (x : α) ↦ id) = s.card

Tactic:
rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]

Premises used: Finsupp.card_toMultiset, Multiset.toFinsupp_toMultiset
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
⊢ (Multiset.toFinsupp : (a : Multiset α) → α →₀ ℕ) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) = f

Tactic:
Multiset.toFinsupp.apply_symm_apply _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, AddEquiv.apply_symm_apply, Multiset.toFinsupp, Finset.sum
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
s : Multiset α
⊢ (toMultiset : (a : α →₀ ℕ) → Multiset α) f = s ↔ f = (Multiset.toFinsupp : (a : Multiset α) → α →₀ ℕ) s

Tactic:
Multiset.toFinsupp.symm_apply_eq

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Multiset.toFinsupp, AddEquiv.symm_apply_eq, Finset.sum
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq ι
f g : ι →₀ ℕ
⊢ LE.le (α := Multiset ι)
      ((AddEquiv.toEquiv (AddEquiv.symm Multiset.toFinsupp) : (a : ι →₀ ℕ) → Multiset ι) f : Multiset ι)
      ((AddEquiv.toEquiv (AddEquiv.symm Multiset.toFinsupp) : (a : ι →₀ ℕ) → Multiset ι) g : Multiset ι) ↔
    f ≤ g

Tactic:
simp [le_def, Multiset.le_iff_count]

Premises used: Multiset.le_iff_count, Finsupp.le_def
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
inst : DecidableEq ι
⊢ Eq.{u_3 + 1} (α := (a : ι →₀ ℕ) → Multiset ι) (⇑orderIsoMultiset : (a : ι →₀ ℕ) → Multiset ι)
    (⇑toMultiset : (a : ι →₀ ℕ) → Multiset ι)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
inst : DecidableEq ι
⊢ Eq.{u_3 + 1} (α := (a : Multiset ι) → ι →₀ ℕ) (⇑(OrderIso.symm orderIsoMultiset) : (a : Multiset ι) → ι →₀ ℕ)
    (⇑Multiset.toFinsupp : (a : Multiset ι) → ι →₀ ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
⊢ StrictMono.{u_3, u_3} (α := ι →₀ ℕ) (β := Multiset ι) (⇑toMultiset : (a : ι →₀ ℕ) → Multiset ι)

Tactic:
(@orderIsoMultiset ι _).strictMono

Premises used: Multiset.sum, Multiset.foldr, OrderIso.strictMono, Finsupp.sum, Finsupp.orderIsoMultiset, Finset.sum
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
⊢ StrictMono.{u_3, u_3} (α := ι →₀ ℕ) (β := Multiset ι) (⇑toMultiset : (a : ι →₀ ℕ) → Multiset ι)

Tactic:
exact (@orderIsoMultiset ι _).strictMono

Premises used: OrderIso.strictMono, Finsupp.orderIsoMultiset
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
⊢ StrictMono.{u_3, u_3} (α := ι →₀ ℕ) (β := Multiset ι) (⇑toMultiset : (a : ι →₀ ℕ) → Multiset ι)

Tactic:
classical exact (@orderIsoMultiset ι _).strictMono
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
rw :
  Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m) <
    Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n)
⊢ LT.lt (α := ℕ) (m.sum fun (x : ι) ↦ id) (n.sum fun (x : ι) ↦ id)

Tactic:
rw [← card_toMultiset, ← card_toMultiset]

Premises used: Finsupp.card_toMultiset
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
h₁ :
  LT.lt (α := Multiset ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m : Multiset ι)
    ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n : Multiset ι)
⊢ Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m) <
    Multiset.card.{u_3} (α := ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n)

Tactic:
apply Multiset.card_lt_card

Premises used: Multiset.card_lt_card
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ LT.lt (α := Multiset ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m : Multiset ι)
    ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n : Multiset ι)

Tactic:
toMultiset_strictMono h

Premises used: Finsupp.toMultiset_strictMono
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ LT.lt (α := Multiset ι) ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) m : Multiset ι)
    ((toMultiset : (a : ι →₀ ℕ) → Multiset ι) n : Multiset ι)

Tactic:
exact toMultiset_strictMono h

Premises used: Finsupp.toMultiset_strictMono
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
⊢ WellFounded.{u_3 + 1} (α := ι →₀ ℕ) LT.lt

Tactic:
Subrelation.wf (sum_id_lt_of_lt _ _) <| InvImage.wf _ Nat.lt_wfRel.2

Premises used: Finsupp.sum_id_lt_of_lt, Subrelation.wf, WellFoundedRelation.wf, InvImage.wf
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
ι : Type u_3
inst : DecidableEq ι
⊢ StrictMono.{u_3, u_3} (α := Multiset ι) (β := ι →₀ ℕ) (⇑toFinsupp : (a : Multiset ι) → ι →₀ ℕ)

Tactic:
(@Finsupp.orderIsoMultiset ι).symm.strictMono

Premises used: OrderIso.strictMono, OrderIso.symm, Finsupp.orderIsoMultiset
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
n : ℕ
⊢ ∀ (a : Multiset α),
    a.card = n ↔
      (Finsupp.sum (M := ℕ) ((AddEquiv.toEquiv Multiset.toFinsupp : (a : Multiset α) → α →₀ ℕ) a) fun (x : α) ↦ id) = n

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
s : Sym α n
a : α
⊢ ((↑((equivNatSum α n : (a : Sym α n) → { P : α →₀ ℕ // (P.sum fun (x : α) ↦ id) = n }) s) : α →₀ ℕ) : (a : α) → ℕ) a =
    Multiset.count a (↑s : Multiset α)

Tactic:
rfl

Premises used: Multiset.count, Sym.toMultiset, Multiset.countP, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
P : { P : α →₀ ℕ // (P.sum fun (x : α) ↦ id) = n }
⊢ Eq.{u_1 + 1} (α := Multiset α)
    (↑(((equivNatSum α n).symm : (a : { P : α →₀ ℕ // (P.sum fun (x : α) ↦ id) = n }) → Sym α n) P) : Multiset α)
    ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) (↑P : α →₀ ℕ))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Sym.toMultiset, Finset.sum, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
⊢ ∀ (a : α →₀ ℕ), (a.sum fun (x : α) ↦ id) = n ↔ ∑ i : α, (Finsupp.equivFunOnFinite : (a : α →₀ ℕ) → α → ℕ) a i = n

Tactic:
simp [Finsupp.sum_fintype]

Premises used: Finsupp.sum_fintype
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
s : Sym α n
a : α
⊢ (↑((equivNatSumOfFintype α n : (a : Sym α n) → { P : α → ℕ // ∑ i : α, P i = n }) s) : α → ℕ) a =
    Multiset.count a (↑s : Multiset α)

Tactic:
rfl

Premises used: Multiset.count, Sym.toMultiset, Multiset.countP, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : { P : α → ℕ // ∑ i : α, P i = n }
obtain :
  ∀ (P : α → ℕ) (hP : ∑ i : α, P i = n),
    Eq.{u_1 + 1} (α := Multiset α)
      (↑((Equiv.symm (equivNatSumOfFintype α n) : (a : { P : α → ℕ // ∑ i : α, P i = n }) → Sym α n)
            (Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP)) :
        Multiset α)
      (∑ a : α,
        HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a) {a})
⊢ Eq.{u_1 + 1} (α := Multiset α)
    (↑((Equiv.symm (equivNatSumOfFintype α n) : (a : { P : α → ℕ // ∑ i : α, P i = n }) → Sym α n) P) : Multiset α)
    (∑ a : α, HSMul.hSMul (β := Multiset α) ((↑P : α → ℕ) a) {a})

Tactic:
obtain ⟨P, hP⟩ := P
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
change :
  Eq (α := Multiset α)
    ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P) :
      Multiset α)
    (Multiset.sum
        (Multiset.map
          (fun (a : α) ↦
            HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a)
              {a})
          (val univ)) :
      Multiset α)
⊢ Eq.{u_1 + 1} (α := Multiset α)
    (↑((Equiv.symm (equivNatSumOfFintype α n) : (a : { P : α → ℕ // ∑ i : α, P i = n }) → Sym α n)
          (Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP)) :
      Multiset α)
    (∑ a : α,
      HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a) {a})

Tactic:
change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _

Premises used: Multiset.sum, Finsupp.toMultiset, Finsupp.equivFunOnFinite, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a :
  ∀ (a : α),
    Multiset.count a
        ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α)
          ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P)) =
      Multiset.count a
        (Multiset.sum
          (Multiset.map
            (fun (a : α) ↦
              HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a)
                {a})
            (val univ)))
⊢ Eq (α := Multiset α)
    ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P) :
      Multiset α)
    (Multiset.sum
        (Multiset.map
          (fun (a : α) ↦
            HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a)
              {a})
          (val univ)) :
      Multiset α)

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a : α
a₁ :
  Multiset.count a
      ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P)) =
    Multiset.sum
      (Multiset.map
        (fun (b : α) ↦
          Multiset.count a
            (HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) b)
              {b}))
        (val univ))
⊢ Multiset.count a
      ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P)) =
    Multiset.count a
      (Multiset.sum
        (Multiset.map
          (fun (a : α) ↦
            HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) a)
              {a})
          (val univ)))

Tactic:
rw [Multiset.count_sum]

Premises used: Multiset.count_sum
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
inst_1 : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a : α
⊢ Multiset.count a
      ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α)
        ((Equiv.symm Finsupp.equivFunOnFinite : (a : α → ℕ) → α →₀ ℕ) P)) =
    Multiset.sum
      (Multiset.map
        (fun (b : α) ↦
          Multiset.count a
            (HSMul.hSMul (β := Multiset α) ((↑(Subtype.mk (p := fun (P : α → ℕ) ↦ ∑ i : α, P i = n) P hP) : α → ℕ) b)
              {b}))
        (val univ))

Tactic:
simp [Multiset.count_singleton]

Premises used: Multiset.count_singleton
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
x : α
⊢ x ∈ Option.some ⁻¹' (↑f.support : Set (Option α)) →
    ∀ ⦃x₂ : α⦄, x₂ ∈ Option.some ⁻¹' (↑f.support : Set (Option α)) → Option.some x = Option.some x₂ → x = x₂

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((f.some : (a : α) → M) a : M) ((f : (a : Option α) → M) (Option.some a) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((some 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ Eq (α := α →₀ M) (some 0) 0

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((some 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
f g : Finsupp.{u_1, u_2} (Option α) M
h : ∀ (a : α), Eq.{u_2 + 1} (α := M) (((f + g).some : (a : α) → M) a : M) ((f.some + g.some : (a : α) → M) a : M)
⊢ (f + g).some = f.some + g.some

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
f g : Finsupp.{u_1, u_2} (Option α) M
a : α
⊢ Eq.{u_2 + 1} (α := M) (((f + g).some : (a : α) → M) a : M) ((f.some + g.some : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
m : M
h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((some (single none m) : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ Eq (α := α →₀ M) (some (single none m)) 0

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
m : M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((some (single none m) : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
m : M
h :
  ∀ (b : α),
    Eq.{u_2 + 1} (α := M) ((some (single (Option.some a) m) : (a : α) → M) b : M) ((single a m : (a : α) → M) b : M)
⊢ Eq (α := α →₀ M) (some (single (Option.some a) m)) (single a m)

Tactic:
ext b
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
m : M
b : α
⊢ Eq.{u_2 + 1} (α := M) ((some (single (Option.some a) m) : (a : α) → M) b : M) ((single a m : (a : α) → M) b : M)

Tactic:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
m : M
h :
  ∀ (b : α),
    Eq.{u_2 + 1} (α := M) ((some (single (Option.some a) m) : (a : α) → M) b : M) ((single a m : (a : α) → M) b : M)
⊢ Eq (α := α →₀ M) (some (single (Option.some a) m)) (single a m)

Tactic:
classical
    ext b
    simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
h : ∀ (a : α), Eq.{u_2 + 1} (α := M) (((embDomain Embedding.some f).some : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ (embDomain Embedding.some f).some = f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h :
  Eq.{u_2 + 1} (α := M) ((embDomain Embedding.some f : (a : Option α) → M) (Option.some a) : M)
    ((f : (a : α) → M) a : M)
⊢ Eq.{u_2 + 1} (α := M) (((embDomain Embedding.some f).some : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
rw [some_apply]

Premises used: Finsupp.some_apply
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((embDomain Embedding.some f : (a : Option α) → M) (Option.some a) : M)
    ((f : (a : α) → M) a : M)

Tactic:
embDomain_apply_self _ _ _

Premises used: Set.Mem, setOf, Finsupp.embDomain_apply_self
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((embDomain Embedding.some f : (a : Option α) → M) (Option.some a) : M)
    ((f : (a : α) → M) a : M)

Tactic:
exact embDomain_apply_self _ _ _

Premises used: Finsupp.embDomain_apply_self
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
⊢ none ∉ Set.range (ι := α) (⇑Embedding.some : (a : α) → Option α)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
⊢ Eq.{u_2 + 1} (α := M) ((embDomain Embedding.some f : (a : Option α) → M) (Option.some x) : M)
    ((f : (a : α) → M) x : M)

Tactic:
simp [← Function.Embedding.some_apply]

Premises used: Function.Embedding.some_apply
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
a : M
h : ∀ (a_1 : α), Eq.{u_2 + 1} (α := M) (((f.update none a).some : (a : α) → M) a_1 : M) ((f.some : (a : α) → M) a_1 : M)
⊢ (f.update none a).some = f.some

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
a : M
a_1 : α
⊢ Eq.{u_2 + 1} (α := M) (((f.update none a).some : (a : α) → M) a_1 : M) ((f.some : (a : α) → M) a_1 : M)

Tactic:
simp [Finsupp.update]

Premises used: Finsupp.update
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : Finsupp.{u_1, u_2} (Option α) M
h :
  Eq.{u_2 + 1} (α := M)
    (((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
            ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) :
          (a : Option α) → M)
        none :
      M)
    ((P : (a : Option α) → M) none : M)
h₁ :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := M)
      (((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
              ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
                P) :
            (a : Option α) → M)
          (Option.some a) :
        M)
      ((P : (a : Option α) → M) (Option.some a) : M)
⊢ (fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
      ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) =
    P

Tactic:
ext (_ | a)
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : Finsupp.{u_1, u_2} (Option α) M
⊢ Eq.{u_2 + 1} (α := M)
    (((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
            ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) :
          (a : Option α) → M)
        none :
      M)
    ((P : (a : Option α) → M) none : M)

Tactic:
simp [Finsupp.update]

Premises used: Finsupp.update
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : Finsupp.{u_1, u_2} (Option α) M
a : α
⊢ Eq.{u_2 + 1} (α := M)
    (((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1)
            ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M))) P) :
          (a : Option α) → M)
        (Option.some a) :
      M)
    ((P : (a : Option α) → M) (Option.some a) : M)

Tactic:
simp [Finsupp.update]

Premises used: Finsupp.update
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : M × (α →₀ M)
fst :
  ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
        ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 =
    P.1
snd :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := M)
      ((((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
                ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P)).2 :
            (a : α) → M)
          a :
        M)
      ((P.2 : (a : α) → M) a : M)
⊢ (fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
      ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P) =
    P

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : M × (α →₀ M)
⊢ ((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
        ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 =
    P.1

Tactic:
simp [Finsupp.update]

Premises used: Finsupp.update
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst : Zero M
P : M × (α →₀ M)
a : α
⊢ Eq.{u_2 + 1} (α := M)
    ((((fun (P : Finsupp.{u_1, u_2} (Option α) M) ↦ (((P : (a : Option α) → M) none, P.some) : M × (α →₀ M)))
              ((fun (P : M × (α →₀ M)) ↦ (embDomain Embedding.some P.2).update none P.1) P)).2 :
          (a : α) → M)
        a :
      M)
    ((P.2 : (a : α) → M) a : M)

Tactic:
simp [Finsupp.update]

Premises used: Finsupp.update
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f : (a : Option α) → M) none = y

Tactic:
simp [optionElim]

Premises used: Finsupp.optionElim
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f : (a : Option α) → M) none = y

Tactic:
classical
  simp [optionElim]

Premises used: Finsupp.optionElim
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
x : α
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) (Option.some x) : M) ((f : (a : α) → M) x : M)

Tactic:
simp [optionElim]

Premises used: Finsupp.optionElim
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
x : α
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) (Option.some x) : M) ((f : (a : α) → M) x : M)

Tactic:
classical
  simp [optionElim]

Premises used: Finsupp.optionElim
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f : (a : Option α) → M) none = Option.elim.{u_1, u_2 + 1} (α := α) none y (⇑f : (a : α) → M)

Tactic:
optionElim_apply_none y f

Premises used: Finsupp.optionElim_apply_none
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f : (a : Option α) → M) none = Option.elim.{u_1, u_2 + 1} (α := α) none y (⇑f : (a : α) → M)

Tactic:
exact optionElim_apply_none y f

Premises used: Finsupp.optionElim_apply_none
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
x : α
⊢ (optionElim y f : (a : Option α) → M) (Option.some x) = (Option.some x).elim y (⇑f : (a : α) → M)

Tactic:
simp only [optionElim_apply_some, Option.elim_some]

Premises used: Option.elim_some, Finsupp.optionElim_apply_some
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
a : Option α
none :
  (optionElim y f : (a : Option α) → M) Option.none =
    Option.elim.{u_1, u_2 + 1} (α := α) Option.none y (⇑f : (a : α) → M)
some : ∀ (x : α), (optionElim y f : (a : Option α) → M) (Option.some x) = (Option.some x).elim y (⇑f : (a : α) → M)
⊢ (optionElim y f : (a : Option α) → M) a = a.elim y (⇑f : (a : α) → M)

Tactic:
cases a with
  | none => exact optionElim_apply_none y f
  | some x => simp only [optionElim_apply_some, Option.elim_some]

Premises used: Finsupp.some, Option.elim_some, Option.none, Finsupp.optionElim_apply_some, Finsupp.optionElim_apply_none
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
a : Option α
rw : a.elim y (⇑f : (a : α) → M) = Option.elim' y (⇑f : (a : α) → M) a
rw₁ rw₂ : a.elim y (⇑f : (a : α) → M) = a.elim y (⇑f : (a : α) → M)
⊢ (optionElim y f : (a : Option α) → M) a = Option.elim' y (⇑f : (a : α) → M) a

Tactic:
rw [optionElim_apply_eq_elim, Option.elim'_eq_elim]

Premises used: Option.elim'_eq_elim, Finsupp.optionElim_apply_eq_elim
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : ∀ (a : α), Eq.{u_2 + 1} (α := M) (((optionElim y f).some : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ (optionElim y f).some = f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) (((optionElim y f).some : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
simp