awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst_4 : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support (β := β), p x
refine_1 :
  ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
          (↑p_1 : ι))
        a ha ∈
      v.support (β := β)
refine_2 :
  ∀ (a₁ : Subtype p) (ha₁ : a₁ ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι)))
    (a₂ : Subtype p) (ha₂ : a₂ ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
    Eq.{u + 1} (α := ι)
        ((fun (p_1 : Subtype p)
              (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a₁ ha₁)
        ((fun (p_1 : Subtype p)
              (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a₂ ha₂) →
      a₁ = a₂
refine_3 :
  ∀ b ∈ v.support (β := β),
    ∃ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
      (fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a ha =
        b
⊢ ((subtypeDomain (β := β) p v).prod (β := fun (i : Subtype p) ↦ β (↑i : ι)) fun (i : Subtype p) (b : β (↑i : ι)) ↦
      h (↑i : ι) b) =
    v.prod (β := β) h
have refine_4 : ∀ (a : Subtype p) (ha : a ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))),
  (fun (i : Subtype p) (b : β (↑i : ι)) ↦ h (↑i : ι) b) a
      ((subtypeDomain (β := β) p v : (a : Subtype p) → β (↑a : ι)) a) =
    h
      ((fun (p_1 : Subtype p) (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
          (↑p_1 : ι))
        a ha)
      ((v : (a : ι) → β a)
        ((fun (p_1 : Subtype p)
              (x : p_1 ∈ (subtypeDomain (β := β) p v).support (β := fun (i : Subtype p) ↦ β (↑i : ι))) ↦
            (↑p_1 : ι))
          a ha))
Tactic: refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
x x_1 : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁_1 : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
f₂ : (i : ι) → β i
s₁ : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }
h : f₁ = f₂
⊢ mk' (β := fun (i : ι) ↦ β i) f₁ s₁_1 = mk' (β := fun (i : ι) ↦ β i) f₂ s₁
have subst : ∀ (s₁ : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }),
  mk' (β := fun (i : ι) ↦ β i) f₁ s₁_1 = mk' (β := fun (i : ι) ↦ β i) f₁ s₁
Tactic: subst h
Cleared hypotheses: f₂, s₁, h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
x x_1 : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁_1 s₁ : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
⊢ mk' (β := fun (i : ι) ↦ β i) f₁ s₁_1 = mk' (β := fun (i : ι) ↦ β i) f₁ s₁
have e_support' : s₁_1 = s₁
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
i : ι
h : (x : (a : ι) → β₁ a) i = 0
⊢ Eq.{v₂ + 1} (α := β₂ i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i) 0
have rw : (fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i = f i 0
Tactic: rw [← hf i, ← h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
i : ι
h : (x : (a : ι) → β₁ a) i = 0
rw : (fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i = f i 0
⊢ Eq.{v₂ + 1} (α := β₂ i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i) 0
have rw₁ : (fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i)) i = f i ((x : (a : ι) → β₁ a) i)
Tactic: rw [← hf i, ← h]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
inst : (i : ι) → Zero (β₁ i)
h : ∀ (i : ι), Eq.{v₁ + 1} (α := β₁ i) (id 0) 0
g : Π₀ (i : ι), β₁ i
⊢ mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) h g = g
have h₁ : ∀ (i : ι), (mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) h g : (a : ι) → β₁ a) i = (g : (a : ι) → β₁ a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
f₂ : (i : ι) → β i → β₁ i
hf : ∀ (i : ι), f i 0 = 0
hf₂ : ∀ (i : ι), f₂ i 0 = 0
h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
g : Π₀ (i : ι), β i
⊢ mapRange (β₁ := β) (β₂ := β₂) (fun (i : ι) ↦ f i ∘ f₂ i) h g =
    mapRange (β₁ := β₁) (β₂ := β₂) f hf (mapRange (β₁ := β) (β₂ := β₁) f₂ hf₂ g)
have h₁ : ∀ (i : ι),
  (mapRange (β₁ := β) (β₂ := β₂) (fun (i : ι) ↦ f i ∘ f₂ i) h g : (a : ι) → β₂ a) i =
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (mapRange (β₁ := β) (β₂ := β₁) f₂ hf₂ g) : (a : ι) → β₂ a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
f₂ : (i : ι) → β i → β₁ i
hf : ∀ (i : ι), f i 0 = 0
hf₂ : ∀ (i : ι), f₂ i 0 = 0
h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
g : Π₀ (i : ι), β i
i : ι
⊢ (mapRange (β₁ := β) (β₂ := β₂) (fun (i : ι) ↦ f i ∘ f₂ i) h g : (a : ι) → β₂ a) i =
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (mapRange (β₁ := β) (β₂ := β₁) f₂ hf₂ g) : (a : ι) → β₂ a) i
have h₁ : (f i ∘ f₂ i) ((g : (a : ι) → β a) i) = f i (f₂ i ((g : (a : ι) → β a) i))
Tactic: simp only [mapRange_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf 0 = 0
have h : ∀ (i : ι), (mapRange (β₁ := β₁) (β₂ := β₂) f hf 0 : (a : ι) → β₂ a) i = (0 : (a : ι) → β₂ a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
⊢ Trunc
    { s : Multiset ι //
      ∀ (i : ι),
        i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }
have refine : (xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }) →
  Trunc
    { s : Multiset ι //
      ∀ (i : ι),
        i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }
Tactic: refine x.support'.bind fun xs => ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
⊢ Trunc
    { s : Multiset ι //
      ∀ (i : ι),
        i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }
have refine : (ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }) →
  { s : Multiset ι //
    ∀ (i : ι),
      i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }
Tactic: refine y.support'.map fun ys => ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
⊢ { s : Multiset ι //
    ∀ (i : ι),
      i ∈ s ∨ Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0 }
have refine : ∀ (i : ι),
  i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
Tactic: refine ⟨xs + ys, fun i => ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
have inl : ∀ (h1 : i ∈ (↑xs : Multiset ι)),
  i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
Tactic: obtain h1 | (h1 : x i = 0) := xs.prop i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
inl :
  ∀ (h1 : i ∈ (↑xs : Multiset ι)),
    i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
      Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
have inr : ∀ (h1 : (x : (a : ι) → β₁ a) i = 0),
  i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
Tactic: obtain h1 | (h1 : x i = 0) := xs.prop i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
h1 : (x : (a : ι) → β₁ a) i = 0
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
have inr : ∀ (h2 : i ∈ (↑ys : Multiset ι)),
  i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
Tactic: obtain h2 | (h2 : y i = 0) := ys.prop i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x.toFun (β := fun (i : ι) ↦ β₁ i) i = 0 }
ys : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ y.toFun (β := fun (i : ι) ↦ β₂ i) i = 0 }
i : ι
h1 : (x : (a : ι) → β₁ a) i = 0
inr :
  ∀ (h2 : i ∈ (↑ys : Multiset ι)),
    i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
      Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
⊢ i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
have inr₁ : ∀ (h2 : (y : (a : ι) → β₂ a) i = 0),
  i ∈ (↑xs : Multiset ι) + (↑ys : Multiset ι) ∨
    Eq.{v + 1} (α := β i) ((fun (i : ι) ↦ f i ((x : (a : ι) → β₁ a) i) ((y : (a : ι) → β₂ a) i)) i) 0
Tactic: obtain h2 | (h2 : y i = 0) := ys.prop i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
i : ι
⊢ (filter (β := β) p f + filter (β := β) (fun (i : ι) ↦ ¬p i) f : (a : ι) → β a) i = (f : (a : ι) → β a) i
have simp : ((if p i then (f : (a : ι) → β a) i else 0) + if ¬p i then (f : (a : ι) → β a) i else 0) = (f : (a : ι) → β a) i
Tactic: simp only [add_apply, filter_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
i : ι
⊢ ((if p i then (f : (a : ι) → β a) i else 0) + if ¬p i then (f : (a : ι) → β a) i else 0) = (f : (a : ι) → β a) i
have pos : p i → (f : (a : ι) → β a) i + 0 = (f : (a : ι) → β a) i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst_1 : DecidablePred p
i : ι
pos : p i → (f : (a : ι) → β a) i + 0 = (f : (a : ι) → β a) i
⊢ ((if p i then (f : (a : ι) → β a) i else 0) + if ¬p i then (f : (a : ι) → β a) i else 0) = (f : (a : ι) → β a) i
have neg : ¬p i → 0 + (f : (a : ι) → β a) i = (f : (a : ι) → β a) i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
p : ι → Prop
inst_1 : DecidablePred p
⊢ Eq (α := Π₀ (i : ι), β i) (filter (β := β) p 0) 0
have h : ∀ (i : ι), (filter (β := β) p 0 : (a : ι) → β a) i = (0 : (a : ι) → β a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst_1 : DecidablePred p
f g : Π₀ (i : ι), β i
⊢ filter (β := β) p (f + g) = filter (β := β) p f + filter (β := β) p g
have h : ∀ (i : ι), (filter (β := β) p (f + g) : (a : ι) → β a) i = (filter (β := β) p f + filter (β := β) p g : (a : ι) → β a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
H : Eq (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y)
⊢ x = y
have h : ∀ (i : (↑(↑s : Set ι) : Type u)), x i = y i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
s : Finset ι
x y : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
H : Eq (α := Π₀ (i : ι), β i) (mk (β := β) s x) (mk (β := β) s y)
i : (↑(↑s : Set ι) : Type u)
⊢ x i = y i
have h1 : Eq (α := β (↑i : ι)) ((mk (β := β) s x : (a : ι) → β a) (↑i : ι)) ((mk (β := β) s y : (a : ι) → β a) (↑i : ι))
Tactic: have h1 : (mk s x : ∀ i, β i) i = (mk s y : ∀ i, β i) i := by grind
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i i' : ι
b : β i
⊢ (single (β := β) i b : (a : ι) → β a) i' =
    if h : i = i' then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h b else 0
have rw : Eq.{v + 1} (α := β i') (if h : i' = i then Eq.ndrec (motive := β) b sorry else 0 i')
  (if h : i = i' then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h b else 0)
Tactic: rw [single_eq_pi_single, Pi.single, Function.update]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj) ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have mp : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj) → i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
mp : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj) → i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj) ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have mpr : i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0 → Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have pos : ∀ (hij : i = j), i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
pos : ∀ (hij : i = j), i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have neg : ∀ (hij : ¬i = j), i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : i = j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have pos : ∀ (xj : β i) (h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xj)),
  i = i ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Tactic: subst hij
Cleared hypotheses: j, xj, h, hij
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
Tactic: have h_coe : ⇑(DFinsupp.single i xi) = DFinsupp.single j xj := congr_arg (⇑) h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have hci : (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i
Tactic: have hci := congr_fun h_coe i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have hcj : (single (β := β) i xi : (a : ι) → β a) j = (single (β := β) j xj : (a : ι) → β a) j
Tactic: have hcj := congr_fun h_coe j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i
hcj : (single (β := β) i xi : (a : ι) → β a) j = (single (β := β) j xj : (a : ι) → β a) j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have hci₁ : xi = (single (β := β) j xj : (a : ι) → β a) i
Tactic: rw [DFinsupp.single_eq_same] at hci hcj
Cleared hypotheses: hci, hcj
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : (single (β := β) i xi : (a : ι) → β a) i = (single (β := β) j xj : (a : ι) → β a) i
hcj : (single (β := β) i xi : (a : ι) → β a) j = (single (β := β) j xj : (a : ι) → β a) j
hci₁ : xi = (single (β := β) j xj : (a : ι) → β a) i
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have hcj₁ : (single (β := β) i xi : (a : ι) → β a) j = xj
Tactic: rw [DFinsupp.single_eq_same] at hci hcj
Cleared hypotheses: hci, hcj
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : xi = (single (β := β) j xj : (a : ι) → β a) i
hcj : (single (β := β) i xi : (a : ι) → β a) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have hci₁ : xi = 0
Tactic: rw [DFinsupp.single_eq_of_ne hij] at hci
Cleared hypotheses: hci, hcj
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
hij : ¬i = j
h_coe : (⇑(single (β := β) i xi) : (a : ι) → β a) = (⇑(single (β := β) j xj) : (a : ι) → β a)
hci : xi = 0
hcj : (single (β := β) i xi : (a : ι) → β a) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
have hcj₁ : 0 = xj
Tactic: rw [DFinsupp.single_eq_of_ne (Ne.symm hij)] at hcj
Cleared hypotheses: hcj
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i : ι
xi xj : β i
hxi : xi ≍ xj
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) i xj)
have mpr : Eq (α := Π₀ (i : ι), β i) (single (β := β) i xj) (single (β := β) i xj)
Tactic: rw [eq_of_heq hxi]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ Eq (α := Π₀ (i : ι), β i) (single (β := β) i xi) (single (β := β) j xj)
have mpr : Eq (α := Π₀ (i : ι), β i) (single (β := β) i 0) (single (β := β) j xj)
Tactic: rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]