awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
h :
  ∀ (i' : ι) (j' : α i'),
    ((sigmaCurry (α := α) (δ := δ)
                (single (β := fun (i : (x : ι) × α x) ↦
                  δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
                  (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
              (a : ι) → Π₀ (j : α a), δ a j)
            i' :
          (a : α i') → δ i' a)
        j' =
      ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
                ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
                (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
                  ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x) :
              (a : ι) → Π₀ (j : α a), δ a j)
            i' :
          (a : α i') → δ i' a)
        j'
⊢ Eq (α := Π₀ (i : ι) (j : α i), δ i j)
    (sigmaCurry (α := α) (δ := δ)
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x))
    (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
      ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
      (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
        ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x))

Tactic:
ext i' j'
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
i' : ι
j' : α i'
h :
  ((sigmaCurry (α := α) (δ := δ)
              (single (β := fun (i : (x : ι) × α x) ↦
                δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
                (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j' =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j'
⊢ ((sigmaCurry (α := α) (δ := δ)
              (single (β := fun (i : (x : ι) × α x) ↦
                δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
                (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j' =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
              ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
              (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
                ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j'

Tactic:
dsimp only
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
i' : ι
j' : α i'
h :
  (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j'
⊢ ((sigmaCurry (α := α) (δ := δ)
              (single (β := fun (i : (x : ι) × α x) ↦
                δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
                (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j' =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j'

Tactic:
rw [sigmaCurry_apply]

Premises used: DFinsupp.sigmaCurry_apply
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
i' : ι
j' : α i'
h :
  ∀ (j' : α i),
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
      ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i :
          (a : α i) → δ i a)
        j'
h₁ :
  ∀ (hi : i ≠ i'),
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') =
      ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
          (a : α i') → δ i' a)
        j'
⊢ (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j'

Tactic:
obtain rfl | hi := eq_or_ne i i'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
j' : α i
h :
  (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
    (single (β := δ i) j x : (a : α i) → δ i a) j'
⊢ (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i :
        (a : α i) → δ i a)
      j'

Tactic:
rw [single_eq_same]

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
j' : α i
h :
  ∀
    (x :
      δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j').fst (β := fun (i : ι) ↦ α i))
        ((Sigma.mk (β := fun (i : ι) ↦ α i) i j').snd (β := fun (i : ι) ↦ α i))),
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (i : ι) ↦ α i) i j') x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
      (single (β := δ i) j' x : (a : α i) → δ i a) j'
h₁ :
  ∀ (hj : j' ≠ j),
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
            (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
      (single (β := δ i) j x : (a : α i) → δ i a) j'
⊢ (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
    (single (β := δ i) j x : (a : α i) → δ i a) j'

Tactic:
obtain rfl | hj := eq_or_ne j' j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j' : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j').fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j').snd (β := fun (i : ι) ↦ α i))
h : x = (single (β := δ i) j' x : (a : α i) → δ i a) j'
h₁ h₂ : x = x
⊢ (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j') x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
    (single (β := δ i) j' x : (a : α i) → δ i a) j'

Tactic:
rw [single_eq_same, single_eq_same]

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
j' : α i
hj : j' ≠ j
h : Sigma.mk (β := fun (x : ι) ↦ α x) i j' ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i j
⊢ (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
    (single (β := δ i) j x : (a : α i) → δ i a) j'

Tactic:
rw [single_eq_of_ne, single_eq_of_ne hj]

Premises used: DFinsupp.single_eq_of_ne
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
j' : α i
hj : j' ≠ j
⊢ Sigma.mk (β := fun (x : ι) ↦ α x) i j' ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i j

Tactic:
simpa using hj
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
i' : ι
j' : α i'
hi : i ≠ i'
⊢ (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j'

Tactic:
simp [hi]
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
inl :
  Membership.mem (γ := Multiset ((x : ι) × α x))
    ((↑s : Multiset ι).toFinset.attach.val.bind fun (i : ↥(↑s : Multiset ι).toFinset) ↦
      Multiset.map (Sigma.mk (β := fun (x : ι) ↦ α x) (↑i : ι)) (↑(fs i) : Multiset (α (↑i : ι))))
    (Sigma.mk (β := fun (x : ι) ↦ α x) i a)
⊢ Membership.mem (γ := Multiset ((x : ι) × α x))
      ((↑s : Multiset ι).toFinset.attach.val.bind fun (i : ↥(↑s : Multiset ι).toFinset) ↦
        Multiset.map (Sigma.mk (β := fun (x : ι) ↦ α x) (↑i : ι)) (↑(fs i) : Multiset (α (↑i : ι))))
      (Sigma.mk (β := fun (x : ι) ↦ α x) i a) ∨
    Eq (α :=
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
      (((f : (a : ι) → Π₀ (j : α a), δ a j) ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).fst (β := fun (x : ι) ↦ α x)) :
          (a_1 : α ⟨i, a⟩.fst) → δ ⟨i, a⟩.fst a_1)
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i a).snd (β := fun (x : ι) ↦ α x)))
      0

Tactic:
left
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
inl :
  ∃ a_1 ∈ (↑s : Multiset ι).toFinset.attach.val,
    Sigma.mk (β := fun (x : ι) ↦ α x) i a ∈
      Multiset.map (Sigma.mk (β := fun (x : ι) ↦ α x) (↑a_1 : ι)) (↑(fs a_1) : Multiset (α (↑a_1 : ι)))
⊢ Membership.mem (γ := Multiset ((x : ι) × α x))
    ((↑s : Multiset ι).toFinset.attach.val.bind fun (i : ↥(↑s : Multiset ι).toFinset) ↦
      Multiset.map (Sigma.mk (β := fun (x : ι) ↦ α x) (↑i : ι)) (↑(fs i) : Multiset (α (↑i : ι))))
    (Sigma.mk (β := fun (x : ι) ↦ α x) i a)

Tactic:
rw [Multiset.mem_bind]

Premises used: Multiset.mem_bind
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
h :
  Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯ ∈ (↑s : Multiset ι).toFinset.attach.val ∧
    Sigma.mk (β := fun (x : ι) ↦ α x) i a ∈
      Multiset.map
        (Sigma.mk (β := fun (x : ι) ↦ α x) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
        (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι)))
⊢ ∃ a_1 ∈ (↑s : Multiset ι).toFinset.attach.val,
    Sigma.mk (β := fun (x : ι) ↦ α x) i a ∈
      Multiset.map (Sigma.mk (β := fun (x : ι) ↦ α x) (↑a_1 : ι)) (↑(fs a_1) : Multiset (α (↑a_1 : ι)))

Tactic:
use ⟨i, Multiset.mem_toFinset.mpr hi⟩
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
constructor : Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯ ∈ (↑s : Multiset ι).toFinset.attach.val
constructor₁ :
  Sigma.mk (β := fun (x : ι) ↦ α x) i a ∈
    Multiset.map
      (Sigma.mk (β := fun (x : ι) ↦ α x) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
      (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι)))
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯ ∈ (↑s : Multiset ι).toFinset.attach.val ∧
    Sigma.mk (β := fun (x : ι) ↦ α x) i a ∈
      Multiset.map
        (Sigma.mk (β := fun (x : ι) ↦ α x) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
        (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι)))

Tactic:
constructor
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
⊢ Sigma.mk (β := fun (x : ι) ↦ α x) i a ∈
    Multiset.map
      (Sigma.mk (β := fun (x : ι) ↦ α x) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
      (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι)))

Tactic:
simp [ha]
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
⊢ Sigma.mk (β := fun (x : ι) ↦ α x) i a ∈
    Multiset.map
      (Sigma.mk (β := fun (x : ι) ↦ α x) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
      (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι)))

Tactic:
case right => simp [ha]
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯ ∈ (↑s : Multiset ι).toFinset.attach.val

Tactic:
apply Multiset.mem_attach

Premises used: Multiset.mem_attach
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0 }
fs :
  (i : ↥(↑s : Multiset ι).toFinset) →
    { s_1 : Multiset (α (↑i : ι)) //
      ∀ (i_1 : α (↑i : ι)),
        i_1 ∈ s_1 ∨
          toFun (β := fun (j : α (↑i : ι)) ↦ δ (↑i : ι) j) ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑i : ι)) i_1 = 0 }
i : ι
a : α i
hi : i ∈ (↑s : Multiset ι)
ha :
  Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯)) : Multiset (α (↑⟨i, ⋯⟩ : ι))) a
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯ ∈ (↑s : Multiset ι).toFinset.attach.val

Tactic:
case left => apply Multiset.mem_attach

Premises used: Multiset.mem_attach