awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (mk (β := β) s (x + y) : (a : ι) → β a) i =
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y) : (a : ι) → β a) i
have simp : (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
  HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
Tactic: simp only [add_apply, mk_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HAdd.hAdd (α := β i) (β := β i)
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HAdd.hAdd (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
⊢ (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → 0 = HAdd.hAdd (α := β i) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
⊢ 0 = HAdd.hAdd (α := β i) 0 0
have neg : Eq.{v + 1} (α := β i) 0 0
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HAdd.hAdd (α := β i) (β := β i)
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
Tactic: split_ifs <;> [rfl; rw [zero_add]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HAdd.hAdd (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
⊢ (if H : i ∈ s then (x + y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HAdd.hAdd (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → 0 = HAdd.hAdd (α := β i) 0 0
Tactic: split_ifs <;> [rfl; rw [zero_add]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (mk (β := β) s 0 : (a : ι) → β a) i = (0 : (a : ι) → β a) i
have simp : (if H : i ∈ s then 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) = (0 : (a : ι) → β a) i
Tactic: simp only [mk_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (if H : i ∈ s then 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) = (0 : (a : ι) → β a) i
have pos : ∀ (h : i ∈ s), 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) = (0 : (a : ι) → β a) i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
s : Finset ι
i : ι
pos : ∀ (h : i ∈ s), 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) = (0 : (a : ι) → β a) i
⊢ (if H : i ∈ s then 0 (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) = (0 : (a : ι) → β a) i
have neg : i ∉ s → 0 = (0 : (a : ι) → β a) i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (mk (β := β) s (-x) : (a : ι) → β a) i = (-mk (β := β) s x : (a : ι) → β a) i
have simp : Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
  (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
Tactic: simp only [neg_apply, mk_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)
⊢ Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → Eq.{v + 1} (α := β i) 0 (-0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
⊢ Eq.{v + 1} (α := β i) 0 (-0)
have neg : Eq.{v + 1} (α := β i) 0 0
Tactic: rw [neg_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)
Tactic: split_ifs <;> [rfl; rw [neg_zero]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      -x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h)
⊢ Eq.{v + 1} (α := β i) (if H : i ∈ s then (-x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (-if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → Eq.{v + 1} (α := β i) 0 (-0)
Tactic: split_ifs <;> [rfl; rw [neg_zero]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (mk (β := β) s (x - y) : (a : ι) → β a) i =
    (HSub.hSub (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y) : (a : ι) → β a) i
have simp : (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
  HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
    (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
Tactic: simp only [sub_apply, mk_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HSub.hSub (α := β i) (β := β i)
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSub.hSub (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
⊢ (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → 0 = HSub.hSub (α := β i) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
⊢ 0 = HSub.hSub (α := β i) 0 0
have neg : Eq.{v + 1} (α := β i) 0 0
Tactic: rw [sub_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
⊢ (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have pos : ∀ (h : i ∈ s),
  (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HSub.hSub (α := β i) (β := β i)
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
Tactic: split_ifs <;> [rfl; rw [sub_zero]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSub.hSub (α := β i) (β := β i)
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
        (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h))
⊢ (if H : i ∈ s then (x - y) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSub.hSub (α := β i) (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
      (if H : i ∈ s then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
have neg : i ∉ s → 0 = HSub.hSub (α := β i) 0 0
Tactic: split_ifs <;> [rfl; rw [sub_zero]]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
⊢ Eq.{u + 1} (α := Finset ι)
    ((fun (xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        {i ∈ (↑xs : Multiset ι).toFinset | (f : (a : ι) → β a) i ≠ 0})
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sx hx))
    ((fun (xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        {i ∈ (↑xs : Multiset ι).toFinset | (f : (a : ι) → β a) i ≠ 0})
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sy hy))
have dsimp : {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} = {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
Tactic: dsimp only [Subtype.coe_mk, toFun_eq_coe] at *
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
⊢ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} = {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
have h : ∀ (i : ι), i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} ↔ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
⊢ i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} ↔ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
have h : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} → i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
h : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} → i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0} ↔ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
have h₁ : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0} → i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
have left : i ∈ sx.toFinset
Tactic: rcases Finset.mem_filter.1 H with ⟨_, h⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sx.toFinset
⊢ i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
have h : (f : (a : ι) → β a) i ≠ 0
Tactic: rcases Finset.mem_filter.1 H with ⟨_, h⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
⊢ i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
have left : i ∈ sy.toFinset
Tactic: rcases Finset.mem_filter.1 H with ⟨_, h⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | (f : (a : ι) → β a) i ≠ 0}
left : i ∈ sy.toFinset
⊢ i ∈ {i ∈ sx.toFinset | (f : (a : ι) → β a) i ≠ 0}
have h : (f : (a : ι) → β a) i ≠ 0
Tactic: rcases Finset.mem_filter.1 H with ⟨_, h⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ i ∈ f.support (β := β) ↔ (f : (a : ι) → β a) i ≠ 0
have obtain : ∀ (f : (i : ι) → β i) (s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }),
  i ∈ (mk' (β := fun (i : ι) ↦ β i) f s).support (β := β) ↔ (mk' (β := fun (i : ι) ↦ β i) f s : (a : ι) → β a) i ≠ 0
Tactic: obtain ⟨f, s⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ (mk' (β := fun (i : ι) ↦ β i) f s).support (β := β) ↔ (mk' (β := fun (i : ι) ↦ β i) f s : (a : ι) → β a) i ≠ 0
have h : ∀ (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }),
  i ∈ (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s)).support (β := β) ↔
    (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s) : (a : ι) → β a) i ≠ 0
Tactic: induction s using Trunc.induction_on with | _ s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ {i ∈ (↑s : Multiset ι).toFinset | (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s) : (a : ι) → β a) i ≠ 0} ↔
    (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s) : (a : ι) → β a) i ≠ 0
have h : i ∈ (↑s : Multiset ι) ∧ f i ≠ 0 ↔ f i ≠ 0
Tactic: rw [Finset.mem_filter, Multiset.mem_toFinset, coe_mk']
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
f : (i : ↥s) → { x : β (↑i : ι) // x ≠ 0 }
i : ι
⊢ i ∈ support (β := β) (mk (β := β) s fun (i : (↑(↑s : Set ι) : Type u)) ↦ (↑(f i) : β (↑i : ι))) ↔ i ∈ s
have i₁ : i ∈ support (β := β) (mk (β := β) s fun (i : (↑(↑s : Set ι) : Type u)) ↦ (↑(f i) : β (↑i : ι))) ↔
  ∃ (h : i ∈ s),
    Ne (α := β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι))
      (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h)) : β (↑⟨i, h⟩ : ι)) 0
Tactic: calc
      i ∈ support (mk s fun i ↦ (f i).1) ↔ ∃ h : i ∈ s, (f ⟨i, h⟩).1 ≠ 0 := by simp
      _ ↔ ∃ _ : i ∈ s, True := exists_congr fun h ↦ (iff_true _).mpr (f _).2
      _ ↔ i ∈ s := by simp
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
f : (i : ↥s) → { x : β (↑i : ι) // x ≠ 0 }
i : ι
i₁ :
  i ∈ support (β := β) (mk (β := β) s fun (i : (↑(↑s : Set ι) : Type u)) ↦ (↑(f i) : β (↑i : ι))) ↔
    ∃ (h : i ∈ s),
      Ne (α := β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι))
        (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h)) : β (↑⟨i, h⟩ : ι)) 0
⊢ i ∈ support (β := β) (mk (β := β) s fun (i : (↑(↑s : Set ι) : Type u)) ↦ (↑(f i) : β (↑i : ι))) ↔ i ∈ s
have i₂ : (∃ (_ : i ∈ s), True) ↔ i ∈ s
Tactic: calc
      i ∈ support (mk s fun i ↦ (f i).1) ↔ ∃ h : i ∈ s, (f ⟨i, h⟩).1 ≠ 0 := by simp
      _ ↔ ∃ _ : i ∈ s, True := exists_congr fun h ↦ (iff_true _).mpr (f _).2
      _ ↔ i ∈ s := by simp
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
⊢ (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) ↔ f = 0
have constructor : (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) → f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
constructor : (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) → f = 0
⊢ (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) ↔ f = 0
have constructor₁ : f = 0 → ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
Tactic: constructor