awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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 : i ∈ (↑s : Multiset ι) ∨ f.toFun (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i = 0
Tactic: cases s.prop i with
          | inl hi =>
            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]
          | inr hi => right; simp [toFun_eq_coe f ▸ hi]
-- 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
⊢ Eq (α := Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
    (sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)))
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x)
have h : ∀ (i' : ι) (j' : α i'),
  Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').snd (β := fun (x : ι) ↦ α x)))
    ((sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)) :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))
    ((single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))
Tactic: ext ⟨i', 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ Eq (α := δ i' j')
    ((sigmaUncurry (α := α) (δ := δ) (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x)) :
          (a : (x : ι) × α x) → δ a.fst a.snd)
        (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') :
      δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').fst (β := fun (x : ι) ↦ α x))
        ((Sigma.mk (β := fun (x : ι) ↦ α x) i' j').snd (β := fun (x : ι) ↦ α x)))
    ((single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j'))
have h : ((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 (x : ι) ↦ α x) i j) x :
      (a : (x : ι) × α x) → δ a.fst a.snd)
    (Sigma.mk (β := fun (x : ι) ↦ α x) i' j')
Tactic: rw [sigmaUncurry_apply]
-- 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
⊢ ((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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j')
have h : ∀ (j' : α i),
  ((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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
Tactic: obtain rfl | hi := eq_or_ne i i'
Cleared hypotheses: i', 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
i' : ι
j' : α i'
h :
  ∀ (j' : α i),
    ((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 (x : ι) ↦ α x) 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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j')
have h₁ : ∀ (hi : i ≠ i'),
  ((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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
⊢ ((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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
have h : (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 (x : ι) ↦ α x) i j) x :
      (a : (x : ι) × α x) → δ a.fst a.snd)
    (Sigma.mk (β := fun (x : ι) ↦ α x) i 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
⊢ (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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
have h : ∀ (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 (x : ι) ↦ α x) i j') x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
h :
  ∀ (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 (x : ι) ↦ α x) 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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
have h₁ : ∀ (hj : j' ≠ 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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j' : α i
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 (x : ι) ↦ α x) i j') x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
have h : x =
  (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
        (Sigma.mk (β := fun (x : ι) ↦ α x) i j') x :
      (a : (x : ι) × α x) → δ a.fst a.snd)
    (Sigma.mk (β := fun (x : ι) ↦ α x) i 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j' : α i
x : δ i j'
h :
  x =
    (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (x : ι) ↦ α x) 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 (x : ι) ↦ α x) i j') x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i 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 : ι) → (j : α i) → Zero (δ i j)
inst_2 : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ 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 (x : ι) ↦ α x) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j')
have h : Sigma.mk (β := fun (x : ι) ↦ α x) i j' ≠ Sigma.mk (β := fun (x : ι) ↦ α x) i j
Tactic: rw [single_eq_of_ne hj, single_eq_of_ne]
-- 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 : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
⊢ f.sigmaCurry (α := α) (δ := δ).sigmaUncurry (α := α) (δ := δ) = f
have h : ∀ (i : ι) (j : α i),
  Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x)))
    ((f.sigmaCurry (α := α) (δ := δ).sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
    ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
Tactic: ext ⟨i, j⟩
-- 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 : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
i : ι
j : α i
⊢ Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x)))
    ((f.sigmaCurry (α := α) (δ := δ).sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
    ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
have h : ((f.sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
  (f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j)
Tactic: rw [sigmaUncurry_apply, sigmaCurry_apply]
-- 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 : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
i : ι
j : α i
h :
  ((f.sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    (f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j)
⊢ Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x)))
    ((f.sigmaCurry (α := α) (δ := δ).sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
    ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
have h₁ : Eq (α :=
  δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
    ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x)))
  ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
  ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
Tactic: rw [sigmaUncurry_apply, sigmaCurry_apply]
-- 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
⊢ f.sigmaUncurry (α := α) (δ := δ).sigmaCurry (α := α) (δ := δ) = f
have h : ∀ (i : ι) (j : α i),
  ((f.sigmaUncurry (α := α) (δ := δ).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i :
        (a : α i) → δ i a)
      j =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
Tactic: ext i j
-- 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
i : ι
j : α i
⊢ ((f.sigmaUncurry (α := α) (δ := δ).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i :
        (a : α i) → δ i a)
      j =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
have h : (f.sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j) =
  ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
Tactic: rw [sigmaCurry_apply, sigmaUncurry_apply]
-- 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
i : ι
j : α i
h :
  (f.sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j) =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
⊢ ((f.sigmaUncurry (α := α) (δ := δ).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i :
        (a : α i) → δ i a)
      j =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
have h₁ : ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
  ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
Tactic: rw [sigmaCurry_apply, sigmaUncurry_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Small (goal)
Goal:
ι : Type u
π : ι → Type v
inst : (i : ι) → Zero (π i)
inst_1 : Small.{w, u} ι
inst_2 : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq :
  Eq (α := (j : ι) → π j) ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f)
    ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f')
⊢ f = f'
have h : ∀ (j : ι), (f : (a : ι) → π a) j = (f' : (a : ι) → π a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
S : Type u_1
inst_3 : SetLike S γ
inst_4 : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (c : ι),
    (f : (a : ι) → β a) c ≠ 0 → Membership.mem.{w, u_1} (α := γ) s ((g c : (a : β c) → γ) ((f : (a : ι) → β a) c) : γ)
⊢ Membership.mem.{w, u_1} (α := γ) s ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → γ) f : γ)
have rw : (f.sum (β := β) fun (x : ι) ↦ (⇑(g x) : (a : β x) → γ)) ∈ s
Tactic: rw [DFinsupp.sumAddHom_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
S : Type u_1
inst_3 : SetLike S γ
inst_4 : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (c : ι),
    (f : (a : ι) → β a) c ≠ 0 → Membership.mem.{w, u_1} (α := γ) s ((g c : (a : β c) → γ) ((f : (a : ι) → β a) c) : γ)
⊢ Membership.mem.{w, u_1} (α := γ) s ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → γ) f : γ)
have rw : (f.sum (β := β) fun (x : ι) ↦ (⇑(g x) : (a : β x) → γ)) ∈ s
Tactic: classical
    rw [DFinsupp.sumAddHom_apply]
    exact dfinsuppSum_mem s f (g ·) h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S =
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
have a : iSup S ≤
  AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
    (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
a :
  iSup S ≤
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
⊢ iSup S =
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
have a₁ : AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
    (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype) ≤
  iSup S
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S ≤
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
have apply : ∀ (i : ι),
  S i ≤
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
Tactic: apply iSup_le _
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ Eq (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
have a : LE.le (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
  (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
    (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
      (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
a :
  LE.le (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
⊢ Eq (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
have a₁ : LE.le (α := AddSubmonoid γ)
  (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
    (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
      (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
  (⨆ (i : ι), ⨆ (_ : p i), S i)
Tactic: apply le_antisymm