awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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'
⊢ (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'
have 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'
Tactic: obtain rfl | hi := eq_or_ne i i'
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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
⊢ (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'
have 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'
Tactic: rw [single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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
⊢ (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'
have 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'
Tactic: obtain rfl | hj := eq_or_ne j' j
Cleared hypotheses: j, x
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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'
⊢ (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'
have 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'
Tactic: obtain rfl | hj := eq_or_ne j' j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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))
⊢ (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'
have h : x = (single (β := δ i) j' x : (a : α i) → δ i a) j'
Tactic: rw [single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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'
⊢ (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'
have h₁ : x = x
Tactic: rw [single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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
⊢ (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'
have h : Sigma.mk (β := fun (x : ι) ↦ α x) i j' ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i j
Tactic: rw [single_eq_of_ne, single_eq_of_ne hj]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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
⊢ 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
have 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)
Tactic: left
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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
⊢ 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)
have 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 : ι)))
Tactic: rw [Multiset.mem_bind]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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
⊢ ∃ 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 : ι)))
have h : Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry ∈ (↑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 sorry) : ι))
      (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry)) : Multiset (α (↑⟨i, sorry⟩ : ι)))
Tactic: use ⟨i, Multiset.mem_toFinset.mpr hi⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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 ∧
    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, ⋯⟩ : ι)))
have constructor : Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry ∈ (↑s : Multiset ι).toFinset.attach.val
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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
⊢ 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, ⋯⟩ : ι)))
have 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 sorry) : ι))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry)) : Multiset (α (↑⟨i, sorry⟩ : ι)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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 :
  toFun (β := fun (j : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι)) ↦
      δ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι) j)
      ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i ⋯) : ι))
      a =
    0
⊢ 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
have inl : 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: right
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (hypothesis)
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 ι)
⊢ 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
have x : Membership.mem (γ := Multiset (α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry) : ι)))
    (↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry)) : Multiset (α (↑⟨i, sorry⟩ : ι))) a ∨
  toFun (β := fun (j : α (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry) : ι)) ↦
      δ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry) : ι) j)
      ((f : (a : ι) → Π₀ (j : α a), δ a j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Multiset ι).toFinset) i sorry) : ι))
      a =
    0
Tactic: cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
            | inl ha =>
              left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach
            | inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
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 : f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0
⊢ 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
have inr : 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: right