awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
a : Subtype P
m : M
a' : α
ha : a' ≠ (↑a : α)
⊢ Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) a' : M)
    ((single (↑a : α) m : (a : α) → M) a' : M)

Tactic:
simp [*, a.prop, single, Pi.single, Function.update, Subtype.ext_iff]

Premises used: Function.update, Pi.single, Subtype.ext_iff, Subtype.prop, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
s : Set α
M : Type u_12
inst : AddCommMonoid M
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f : Finsupp.{u_1, u_12} (↑s : Type u_1) M
⊢ f.extendDomain (P := fun (x : α) ↦ x ∈ s) = f.extendDomain (P := fun (x : α) ↦ x ∈ s)

Tactic:
congr
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
s : Set α
M : Type u_12
inst : AddCommMonoid M
a : (↑s : Type u_1)
x : M
⊢ Eq (α := α →₀ M)
    (↑((Equiv.symm (restrictSupportEquiv s M) : (a : (↑s : Type u_1) →₀ M) → { f : α →₀ M // (↑f.support : Set α) ⊆ s })
          (single a x)) :
      α →₀ M)
    (single (↑a : α) x)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
s : Set α
M : Type u_12
inst : AddCommMonoid M
a : (↑s : Type u_1)
x : M
⊢ Eq (α := α →₀ M)
    (↑((Equiv.symm (restrictSupportEquiv s M) : (a : (↑s : Type u_1) →₀ M) → { f : α →₀ M // (↑f.support : Set α) ⊆ s })
          (single a x)) :
      α →₀ M)
    (single (↑a : α) x)

Tactic:
classical 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 : AddCommMonoid M
e : α ≃ β
v : α →₀ M
simp_rw : equivMapDomain (Equiv.refl α) v = v
⊢ equivMapDomain e.symm (equivMapDomain e v) = v

Tactic:
simp_rw [← equivMapDomain_trans, Equiv.self_trans_symm]

Premises used: Equiv.self_trans_symm, Finsupp.equivMapDomain_trans
-- 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 : AddCommMonoid M
e : α ≃ β
v : α →₀ M
⊢ equivMapDomain (Equiv.refl α) v = v

Tactic:
equivMapDomain_refl _

Premises used: Finsupp.equivMapDomain_refl
-- 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 : AddCommMonoid M
e : α ≃ β
v : α →₀ M
⊢ equivMapDomain (Equiv.refl α) v = v

Tactic:
exact equivMapDomain_refl _

Premises used: Finsupp.equivMapDomain_refl
-- 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 : AddCommMonoid M
e : α ≃ β
v : β →₀ M
simp_rw : equivMapDomain (Equiv.refl β) v = v
⊢ equivMapDomain e (equivMapDomain e.symm v) = v

Tactic:
simp_rw [← equivMapDomain_trans, Equiv.symm_trans_self]

Premises used: Finsupp.equivMapDomain_trans, Equiv.symm_trans_self
-- 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 : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain (Equiv.refl β) v = v

Tactic:
equivMapDomain_refl _

Premises used: Finsupp.equivMapDomain_refl
-- 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 : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain (Equiv.refl β) v = v

Tactic:
exact equivMapDomain_refl _

Premises used: Finsupp.equivMapDomain_refl
-- 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 : AddCommMonoid M
e : α ≃ β
a b : α →₀ M
⊢ equivMapDomain e (a + b) = equivMapDomain e a + equivMapDomain e b

Tactic:
simp only [equivMapDomain_eq_mapDomain, mapDomain_add]

Premises used: Finsupp.equivMapDomain_eq_mapDomain, Finsupp.mapDomain_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
⊢ Eq (α := (α →₀ M) ≃+ (α →₀ M)) (Finsupp.domCongr (Equiv.refl α)) (AddEquiv.refl (α →₀ M))

Tactic:
AddEquiv.ext fun _ => equivMapDomain_refl _

Premises used: AddEquiv.ext, Finsupp.equivMapDomain_refl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
e : α ≃ β
⊢ Eq (α := (β →₀ M) ≃+ (α →₀ M)) (AddEquiv.symm (Finsupp.domCongr e)) (Finsupp.domCongr e.symm)

Tactic:
AddEquiv.ext fun _ => rfl

Premises used: AddEquiv.ext, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
e : α ≃ β
f : β ≃ γ
⊢ Eq (α := (α →₀ M) ≃+ (γ →₀ M)) (AddEquiv.trans (Finsupp.domCongr e) (Finsupp.domCongr f))
    (Finsupp.domCongr (e.trans f))

Tactic:
AddEquiv.ext fun _ => (equivMapDomain_trans _ _ _).symm

Premises used: AddEquiv.ext, Finsupp.equivMapDomain_trans, Eq.symm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
rw :
  Eq.{u_5 + 1} (α := M) ((comapDomain (Sigma.mk (β := αs) i) l ⋯ : (a : αs i) → M) x : M)
    ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := M) ((l : (a : Sigma αs) → M) (Sigma.mk (β := αs) i x) : M)
    ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)
⊢ Eq.{u_5 + 1} (α := M) ((l.split (αs := αs) i : (a : αs i) → M) x : M)
    ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)

Tactic:
rw [split, comapDomain_apply]

Premises used: Finsupp.comapDomain_apply, Finsupp.split
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
rw :
  (∃ a ∈ l.support, a.fst (β := fun (i : ι) ↦ αs i) = i) ↔
    ∃ (x : αs i),
      x ∈
        { support := l.support.preimage (Sigma.mk (β := αs) i) ⋯,
            toFun := fun (a : αs i) ↦ (l : (a : Sigma αs) → M) (Sigma.mk (β := αs) i a), mem_support_toFun := ⋯ :
            Finsupp.{u_12, u_5} (αs i) M }.support
⊢ i ∈ l.splitSupport (αs := αs) ↔ l.split (αs := αs) i ≠ 0

Tactic:
rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne,
    ← Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]

Premises used: Finset.mem_image, Ne, Finset.nonempty_iff_ne_empty, Finset.Nonempty, Finsupp.splitSupport, Finsupp.support_eq_empty, Finsupp.comapDomain, Finsupp.split
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
classical :
  (∃ a ∈ l.support, a.fst (β := fun (i : ι) ↦ αs i) = i) ↔
    ∃ (x : αs i),
      x ∈
        { support := l.support.preimage (Sigma.mk (β := αs) i) ⋯,
            toFun := fun (a : αs i) ↦ (l : (a : Sigma αs) → M) (Sigma.mk (β := αs) i a), mem_support_toFun := ⋯ :
            Finsupp.{u_12, u_5} (αs i) M }.support
⊢ i ∈ l.splitSupport (αs := αs) ↔ l.split (αs := αs) i ≠ 0

Tactic:
classical rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne,
    ← Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]

Premises used: Finset.mem_image, Ne, Finset.nonempty_iff_ne_empty, Finset.Nonempty, Finsupp.splitSupport, Finsupp.support_eq_empty, Finsupp.comapDomain, Finsupp.split
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst (β := fun (i : ι) ↦ αs i) = i) ↔
    ∃ (x : αs i),
      x ∈
        { support := l.support.preimage (Sigma.mk (β := αs) i) ⋯,
            toFun := fun (a : αs i) ↦ (l : (a : Sigma αs) → M) (Sigma.mk (β := αs) i a), mem_support_toFun := ⋯ :
            Finsupp.{u_12, u_5} (αs i) M }.support

Tactic:
simp only [Finset.mem_preimage, exists_and_right, exists_eq_right, mem_support_iff,
    Sigma.exists, Ne]

Premises used: Finsupp.mem_support_iff, Sigma.exists, exists_eq_right, Ne, exists_and_right, Finset.mem_preimage
-- 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
inst_1 : Zero N
g : (i : ι) → Finsupp.{u_12, u_5} (αs i) M → N
hg : ∀ (i : ι) (x : Finsupp.{u_12, u_5} (αs i) M), x = 0 ↔ g i x = 0
i : ι
rw : l.split (αs := αs) i ≠ 0 ↔ g i (l.split (αs := αs) i) ≠ 0
rw₁ : l.split (αs := αs) i = 0 ↔ g i (l.split (αs := αs) i) = 0
rw₂ rw₃ : g i (l.split (αs := αs) i) = 0 ↔ g i (l.split (αs := αs) i) = 0
⊢ i ∈ l.splitSupport (αs := αs) ↔ g i (l.split (αs := αs) i) ≠ 0

Tactic:
rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]

Premises used: not_iff_not, Finsupp.mem_splitSupport_iff_nonzero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
simp_rw :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
⊢ l.support = l.splitSupport (αs := αs).sigma (α := αs) fun (i : ι) ↦ (l.split (αs := αs) i).support

Tactic:
simp_rw [Finset.ext_iff, splitSupport, split, comapDomain, Sigma.forall, mem_sigma, mem_image,
    mem_preimage]

Premises used: Finset.mem_image, Sigma.forall, Finset.mem_sigma, Finset.ext_iff, Finset.mem_preimage, Finsupp.splitSupport, Finsupp.comapDomain, Finsupp.split
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mpr :
  ∀ (a : ι) (b : αs a),
    (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₁ mp₂ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
mp₄ : ∀ (a : ι) (b : αs a), Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → Sigma.mk (β := αs) a b ∈ l.support
mpr₁ mpr₂ mpr₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := αs) a b ∈ l.support →
      ∀ w ∈ l.support, w.fst (β := fun (i : ι) ↦ αs i) = a → Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₅ mp₆ mp₇ mp₈ mp₉ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
mp₁₀ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ∧
        (Sigma.mk (β := fun (a : ι) ↦ αs a) a b).fst (β := fun (i : ι) ↦ αs i) = a
mp₁₁ : (a : ι) → (b : αs a) → Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → (i : ι) × αs i
mp₁₂ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ∧
        (Sigma.mk (β := fun (a : ι) ↦ αs a) a b).fst (β := fun (i : ι) ↦ αs i) = a
mp₁₃ : (a : ι) → (b : αs a) → Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → (i : ι) × αs i
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support

Tactic:
tauto
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
ι : Type u_4
M : Type u_5
N : Type u_6
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
inst_1 : AddCommMonoid N
f : (i : ι) × αs i → M → N
⊢ l.sum f =
    ∑ i ∈ l.splitSupport (αs := αs),
      (l.split (αs := αs) i).sum fun (a : αs i) (b : M) ↦ f (Sigma.mk (β := fun (i : ι) ↦ αs i) i a) b

Tactic:
simp only [sum, sigma_support, sum_sigma, split_apply]

Premises used: Finset.sum_sigma, Finsupp.sum, Finsupp.split_apply, Finsupp.sigma_support
-- 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs : η → Type u_14
inst_2 : Zero α
f : (j : η) × ιs j →₀ α
h :
  ∀ (a : (j : η) × ιs j),
    Eq.{u_1 + 1} (α := α)
      (((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
                (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
                    (fun (ji : (j : η) × ιs j) ↦
                      (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
                    ⋯ :
                  (j : η) × ιs j →₀ α))
              (f.split (αs := ιs)) :
            (a : (j : η) × ιs j) → α)
          a :
        α)
      ((f : (a : (j : η) × ιs j) → α) a : α)
⊢ (fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
        (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
            (fun (ji : (j : η) × ιs j) ↦
              (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
            ⋯ :
          (j : η) × ιs j →₀ α))
      (f.split (αs := ιs)) =
    f

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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs : η → Type u_14
inst_2 : Zero α
f : (j : η) × ιs j →₀ α
a : (j : η) × ιs j
⊢ Eq.{u_1 + 1} (α := α)
    (((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
              (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
                  (fun (ji : (j : η) × ιs j) ↦
                    (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
                  ⋯ :
                (j : η) × ιs j →₀ α))
            (f.split (αs := ιs)) :
          (a : (j : η) × ιs j) → α)
        a :
      α)
    ((f : (a : (j : η) × ιs j) → α) a : α)

Tactic:
simp [split]

Premises used: Finsupp.split
-- 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs : η → Type u_14
inst_2 : Zero α
f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α
h :
  ∀ (x : η) (a : ιs x),
    Eq.{u_1 + 1} (α := α)
      ((split (αs := ιs)
              ((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
                  (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
                      (fun (ji : (j : η) × ιs j) ↦
                        (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
                      ⋯ :
                    (j : η) × ιs j →₀ α))
                f)
              x :
            (a : ιs x) → α)
          a :
        α)
      ((f x : (a : ιs x) → α) a : α)
⊢ split (αs := ιs)
      ((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
          (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
              (fun (ji : (j : η) × ιs j) ↦
                (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
              ⋯ :
            (j : η) × ιs j →₀ α))
        f) =
    f

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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs : η → Type u_14
inst_2 : Zero α
f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α
x : η
a : ιs x
⊢ Eq.{u_1 + 1} (α := α)
    ((split (αs := ιs)
            ((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
                (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
                    (fun (ji : (j : η) × ιs j) ↦
                      (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
                    ⋯ :
                  (j : η) × ιs j →₀ α))
              f)
            x :
          (a : ιs x) → α)
        a :
      α)
    ((f x : (a : ιs x) → α) a : α)

Tactic:
simp [split]

Premises used: Finsupp.split
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
η : Type u_13
inst : Fintype η
ιs : η → Type u_14
inst_1 : Zero α
f : (j : η) × ιs j →₀ α
j : η
i : ιs j
⊢ Eq.{u_1 + 1} (α := α)
    ((((sigmaFinsuppEquivPiFinsupp (ιs := ιs) : (a : (j : η) × ιs j →₀ α) → (j : η) → ιs j →₀ α) f j :
            Finsupp.{u_14, u_1} (ιs j) α) :
          (a : ιs j) → α)
        i :
      α)
    ((f : (a : (j : η) × ιs j) → α) (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs_1 : η → Type u_14
inst_2 : Zero α_1
α : Type u_15
ιs : η → Type u_16
inst_3 : AddMonoid α
f g : (j : η) × ιs j →₀ α
h :
  ∀ (x : η) (a : ιs x),
    Eq.{u_15 + 1} (α := α) ((Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) (f + g) x : (a : ιs x) → α) a : α)
      (((Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) f + Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) g)
              x :
            (a : ιs x) → α)
          a :
        α)
⊢ Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) (f + g) =
    Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) f + Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) g

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs_1 : η → Type u_14
inst_2 : Zero α_1
α : Type u_15
ιs : η → Type u_16
inst_3 : AddMonoid α
f g : (j : η) × ιs j →₀ α
x : η
a : ιs x
⊢ Eq.{u_15 + 1} (α := α) ((Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) (f + g) x : (a : ιs x) → α) a : α)
    (((Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) f + Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) g)
            x :
          (a : ιs x) → α)
        a :
      α)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
η : Type u_13
inst : Fintype η
α : Type u_15
ιs : η → Type u_16
inst_1 : AddMonoid α
f : (j : η) × ιs j →₀ α
j : η
i : ιs j
⊢ Eq.{u_15 + 1} (α := α)
    ((((sigmaFinsuppAddEquivPiFinsupp (ιs := ιs) : (a : (j : η) × ιs j →₀ α) → (j : η) → ιs j →₀ α) f j :
            Finsupp.{u_16, u_15} (ιs j) α) :
          (a : ιs j) → α)
        i :
      α)
    ((f : (a : (j : η) × ιs j) → α) (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) : α)

Tactic:
rfl

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

Tactic:
mem_range_mapDomain_iff _ f.injective _

Premises used: Finsupp.mem_range_mapDomain_iff, Function.Embedding.injective
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
x : β →₀ M
h : Eq (α := (α →₀ M) → β →₀ M) (embDomain f) (mapDomain (⇑f : (a : α) → β))
h₁ :
  (↑x.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ↔
    ∀ b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β), Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
⊢ Membership.mem (γ := Set (β →₀ M)) (Set.range (embDomain f)) x ↔
    (↑x.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
convert! mem_range_mapDomain_iff _ f.injective _

Premises used: Finsupp.mem_range_mapDomain_iff, Function.Embedding.injective
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
x : β →₀ M
h :
  ∀ (x : α →₀ M) (a : β),
    Eq.{u_5 + 1} (α := M) ((embDomain f x : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) a : M)
⊢ Eq (α := (α →₀ M) → β →₀ M) (embDomain f) (mapDomain (⇑f : (a : α) → β))

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
x : β →₀ M
x_1 : α →₀ M
a : β
h h₁ :
  Eq.{u_5 + 1} (α := M) ((mapDomain (⇑f : (a : α) → β) x_1 : (a : β) → M) a : M)
    ((mapDomain (⇑f : (a : α) → β) x_1 : (a : β) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f x_1 : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) x_1 : (a : β) → M) a : M)

Tactic:
rw [embDomain_eq_mapDomain]

Premises used: Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
x : β →₀ M
⊢ (↑x.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ↔
    ∀ b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β), Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α ↪ β
g : β ↪ γ
⊢ embDomain (f.trans g) v = embDomain g (embDomain f v)

Tactic:
simp only [embDomain_eq_mapDomain, ← mapDomain_comp, Embedding.coe_trans]

Premises used: Function.Embedding.coe_trans, Finsupp.embDomain_eq_mapDomain, Finsupp.mapDomain_comp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
h : ∀ (t : β), t ∈ (mapDomain f x).support ↔ t ∈ image f x.support
⊢ (mapDomain f x).support = image f x.support

Tactic:
ext t
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
h : ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) ↔ ∃ a ∈ x.support, f a = t
⊢ t ∈ (mapDomain f x).support ↔ t ∈ image f x.support

Tactic:
rw [mem_support_iff, ne_eq, Finset.mem_image]

Premises used: Finsupp.mem_support_iff, Finset.mem_image, ne_eq
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) ↔ ∃ a ∈ x.support, f a = t

Tactic:
⟨?_, fun ⟨i, i_in, hi⟩ ↦ ?_⟩

Premises used: Finsupp.mapDomain, _private.0.Finsupp.mapDomain_support_of_subsingletonAddUnits.match_1, Iff.intro, OfNat.ofNat, Eq, DFunLike.coe, Not