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)
p : (Π₀ (i : ι), β i) → Prop
f : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
⊢ p f
have obtain : ∀ (f : (i : ι) → β i) (s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }), p (mk' (β := fun (i : ι) ↦ β i) f s)
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 : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
f : (i : ι) → β i
s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ p (mk' (β := fun (i : ι) ↦ β i) f s)
have h : ∀ (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }), p (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s))
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 : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
f : (i : ι) → β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ p (mk' (β := fun (i : ι) ↦ β i) f (Trunc.mk s))
have h : ∀ (s : Multiset ι) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
  p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
Tactic: obtain ⟨s, H⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
f : (i : ι) → β i
H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ f i = 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) 0 H)))
have h : ∀ (this : f = 0),
  p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) 0 H)))
Tactic: have : f = 0 := funext fun i => (H i).resolve_left (Multiset.notMem_zero _)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
f : (i : ι) → β i
H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ f i = 0
this : f = 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) 0 H)))
have h : ∀ (H : ∀ (i : ι), Membership.mem (γ := Multiset ι) 0 i ∨ Eq.{v + 1} (α := β i) (0 i) 0),
  p
    (mk' (β := fun (i : ι) ↦ β i) 0
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (0 i) 0) 0 H)))
Tactic: subst this
Cleared hypotheses: f, H, this
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
f : (i : ι) → β i
s : Multiset ι
H : ∀ (i : ι), i ∈ s ∨ f i = 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
have h : ∀ (i : ι) (s : Multiset ι)
  (ih :
    ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
      p
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H))))
  (f : (i : ι) → β i) (H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0),
  p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))
Tactic: induction s using Multiset.induction_on generalizing f with
  | empty =>
    have : f = 0 := funext fun i => (H i).resolve_left (Multiset.notMem_zero _)
    subst this
    exact h0
  | cons i s ih => ?_
Cleared hypotheses: f, s, H
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
⊢ p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
have dsimp : p
  (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
    (Trunc.mk
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s) sorry)))
Tactic: dsimp only [erase, Trunc.map, Trunc.bind, Trunc.liftOn, Trunc.lift_mk,
      Function.comp, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
          ⋯)))
have have : ∀ (H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0),
  p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
          sorry)))
Tactic: have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0 := by grind
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
          ⋯)))
have H3 : ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0),
  Eq (α := Π₀ (i : ι), β i)
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦
          ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) (i ::ₘ s)
          aux)))
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦
          ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))
Tactic: have H3 : ∀ aux, (⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨i ::ₘ s, aux⟩⟩ : Π₀ i, β i) =
        ⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨s, H2⟩⟩ :=
      fun _ ↦ ext fun _ => rfl
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
H3 :
  ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0),
    Eq (α := Π₀ (i : ι), β i)
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) (i ::ₘ s)
            aux)))
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
          ⋯)))
have rw : p
  (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
    (Trunc.mk
      (Subtype.mk (p := fun (s : Multiset ι) ↦
        ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))
Tactic: rw [H3]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))
have h : ∀
  (H2 :
    p
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))),
  p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))
Tactic: have H2 : p (erase i ⟨f, Trunc.mk ⟨i ::ₘ s, H⟩⟩) := by
    dsimp only [erase, Trunc.map, Trunc.bind, Trunc.liftOn, Trunc.lift_mk,
      Function.comp, Subtype.coe_mk]
    have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0 := by grind
    have H3 : ∀ aux, (⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨i ::ₘ s, aux⟩⟩ : Π₀ i, β i) =
        ⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨s, H2⟩⟩ :=
      fun _ ↦ ext fun _ => rfl
    rw [H3]
    apply ih
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))
have H3 : HAdd.hAdd (α := Π₀ (i : ι), β i)
    (single (β := β) i
      ((mk' (β := fun (i : ι) ↦ β i) f
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
          (a : ι) → β a)
        i))
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
  mk' (β := fun (i : ι) ↦ β i) f
    (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
Tactic: have H3 : single i _ + _ = (⟨f, Trunc.mk ⟨i ::ₘ s, H⟩⟩ : Π₀ i, β i) := single_add_erase _ _
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))
have h : p
  (HAdd.hAdd (α := Π₀ (i : ι), β i)
    (single (β := β) i
      ((mk' (β := fun (i : ι) ↦ β i) f
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
          (a : ι) → β a)
        i))
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
Tactic: rw [← H3]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
⊢ p
    (HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
have h : p
  (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
Tactic: change p (single i (f i) + _)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
⊢ p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
have h : ∀ (h : f i = 0),
  p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
Tactic: rcases Classical.em (f i = 0) with h | h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h :
  ∀ (h : f i = 0),
    p
      (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
        (erase (β := β) i
          (mk' (β := fun (i : ι) ↦ β i) f
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
⊢ p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
have h₁ : ∀ (h : ¬f i = 0),
  p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
Tactic: rcases Classical.em (f i = 0) with h | h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
⊢ f + single (β := β) i b = single (β := β) i b + f
have h : ∀ (j : ι), (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
j : ι
⊢ (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
have pos : ∀ (H : i = j), (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
Tactic: by_cases H : i = j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
j : ι
pos : ∀ (H : i = j), (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
⊢ (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
have neg : ∀ (H : ¬i = j), (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
Tactic: by_cases H : i = j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f_1 : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (f + single (β := β) i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : i = j
⊢ (f + single (β := β) i b : (a : ι) → β a) j = (single (β := β) i b + f : (a : ι) → β a) j
have pos : (f + single (β := β) i b : (a : ι) → β a) i = (single (β := β) i b + f : (a : ι) → β a) i
Tactic: subst H
Cleared hypotheses: j, H