awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : (i : ι) → β i
s : Multiset ι
h : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
H :
  i ∈
    support (β := β)
      (mk' (β := β) f (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s h)))
⊢ i ∈ s.toFinset.val.toFinset

Tactic:
simpa using (Finset.mem_filter.1 H).1

Premises used: And.left, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
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
⊢ i ∈ f.support (β := β) ↔ (f : (a : ι) → β a) i ≠ 0

Tactic:
obtain ⟨f, s⟩ := f
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
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
⊢ i ∈ (mk' (β := fun (i : ι) ↦ β i) f s).support (β := β) ↔ (mk' (β := fun (i : ι) ↦ β i) f s : (a : ι) → β a) i ≠ 0

Tactic:
induction s using Trunc.induction_on with | _ s
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
h : i ∈ (↑s : Multiset ι) ∧ f i ≠ 0 ↔ 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

Tactic:
rw [Finset.mem_filter, Multiset.mem_toFinset, coe_mk']

Premises used: DFinsupp.coe_mk', Finset.mem_filter, Multiset.mem_toFinset
-- Module: Mathlib.Data.DFinsupp.Defs
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 ∈ (↑s : Multiset ι) ∧ f i ≠ 0 ↔ f i ≠ 0

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f =
    mk (β := β) (f.support (β := β)) fun (i : (↑(↑(f.support (β := β)) : Set ι) : Type u)) ↦
      (f : (a : ι) → β a) (↑i : ι)

Tactic:
aesop
-- Module: Mathlib.Data.DFinsupp.Defs
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 : ι))) ↔
    ∃ (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:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
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 : ι
⊢ (∃ (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 ∈ s), True

Tactic:
exists_congr fun h ↦ (iff_true _).mpr (f _).2

Premises used: Eq.mpr, iff_true, Ne, Subtype.mk, exists_congr, OfNat.ofNat, Subtype.val, Subtype.property
-- Module: Mathlib.Data.DFinsupp.Defs
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 ∈ s), True) ↔ i ∈ s

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
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₂ : (∃ (_ : i ∈ s), True) ↔ i ∈ s
⊢ i ∈ support (β := β) (mk (β := β) s fun (i : (↑(↑s : Set ι) : Type u)) ↦ (↑(f i) : β (↑i : ι))) ↔ 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

Premises used: Eq.mpr, DFinsupp.mk, iff_true, Ne, DFinsupp.support, exists_congr, True, OfNat.ofNat, Subtype.val, Subtype.property
-- Module: Mathlib.Data.DFinsupp.Defs
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
i : ι
⊢ ((↑((fun (f_1 : (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 }) ↦
                (Subtype.mk (p := fun (f_2 : Π₀ (i : ι), β i) ↦ f_2.support (β := β) = f.support (β := β))
                    (mk (β := β) (f.support (β := β)) fun (i : (↑(↑(f.support (β := β)) : Set ι) : Type u)) ↦
                      (↑(f_1 i) : β (↑i : ι)))
                    ⋯ :
                  { f_2 : Π₀ (i : ι), β i // f_2.support (β := β) = f.support (β := β) }))
              ((fun (x : { f_1 : Π₀ (i : ι), β i // f_1.support (β := β) = f.support (β := β) }) ↦
                  (match (motive :=
                      { f_1 : Π₀ (i : ι), β i // f_1.support (β := β) = f.support (β := β) } →
                        (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 })
                      x with
                    | ⟨f_1, hf⟩ => fun (x : ↥(f.support (β := β))) ↦
                      match (motive := (x : ↥(f.support (β := β))) → { x_1 : β (↑x : ι) // x_1 ≠ 0 }) x with
                      | ⟨i, hi⟩ =>
                        Subtype.mk (p :=
                          fun (x : β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ f.support (β := β)) i hi) : ι)) ↦ x ≠ 0)
                          ((f_1 : (a : ι) → β a) i) ⋯ :
                    (i : ↥(f.support (β := β))) → { x : β (↑i : ι) // x ≠ 0 }))
                (Subtype.mk (p := fun (f_1 : Π₀ (i : ι), β i) ↦ f_1.support (β := β) = f.support (β := β)) f ⋯))) :
          Π₀ (i : ι), β i) :
        (a : ι) → β a)
      i =
    ((↑(Subtype.mk (p := fun (f_1 : Π₀ (i : ι), β i) ↦ f_1.support (β := β) = f.support (β := β)) f ⋯) :
          Π₀ (i : ι), β i) :
        (a : ι) → β a)
      i

Tactic:
simpa using Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
⊢ (fun (x : { f : Π₀ (i : ι), β i // f.support (β := β) = s }) ↦
        (match (motive := { f : Π₀ (i : ι), β i // f.support (β := β) = s } → (i : ↥s) → { x : β (↑i : ι) // x ≠ 0 })
            x with
          | ⟨f, hf⟩ => fun (x : ↥s) ↦
            match (motive := (x : ↥s) → { x_1 : β (↑x : ι) // x_1 ≠ 0 }) x with
            | ⟨i, hi⟩ =>
              Subtype.mk (p := fun (x : β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι)) ↦ x ≠ 0)
                ((f : (a : ι) → β a) i) ⋯ :
          (i : ↥s) → { x : β (↑i : ι) // x ≠ 0 }))
      ((fun (f : (i : ↥s) → { x : β (↑i : ι) // x ≠ 0 }) ↦
          (Subtype.mk (p := fun (f : Π₀ (i : ι), β i) ↦ f.support (β := β) = s)
              (mk (β := β) s fun (i : (↑(↑s : Set ι) : Type u)) ↦ (↑(f i) : β (↑i : ι))) ⋯ :
            { f : Π₀ (i : ι), β i // f.support (β := β) = s }))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
⊢ Eq.{u + 1} (α := Finset ι) (support (β := β) 0) ∅

Tactic:
rfl

Premises used: Multiset.zero, DFinsupp.support, Finset.empty, Multiset.ofList, List.filter, Finset.filter, rfl, Multiset.filter, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.Defs
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

Tactic:
f.mem_support_toFun _

Premises used: DFinsupp.mem_support_toFun
-- Module: Mathlib.Data.DFinsupp.Defs
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

Tactic:
not_iff_comm.1 mem_support_iff.symm

Premises used: DFinsupp.mem_support_iff, Iff.mp, Iff.symm, not_iff_comm
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
H : f.support (β := β) = ∅
⊢ ∀ (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
simpa [Finset.ext_iff] using H

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f = 0 → f.support (β := β) = ∅

Tactic:
simp +contextual
-- Module: Mathlib.Data.DFinsupp.Defs
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
constructor₁ : f = 0 → ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
⊢ (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) ↔ f = 0

Tactic:
constructor
-- Module: Mathlib.Data.DFinsupp.Defs
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)
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }
i : ι
h : i ∈ (↑s : Multiset ι)
⊢ (0 : (a : ι) → β a) i = 0

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
⊢ f = 0 → ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0

Tactic:
case mpr => rintro rfl _ _; rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
h : ∀ (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
⊢ f = 0

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
by_cases : ∀ (hs₂ : i ∈ (↑s : Multiset ι)), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
by_cases₁ : ∀ (hs₂ : i ∉ (↑s : Multiset ι)), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
by_cases hs₂ : i ∈ s.val

Premises used: Subtype.val
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∈ (↑s : Multiset ι)
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
hs₁ _ hs₂
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∈ (↑s : Multiset ι)
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
exact hs₁ _ hs₂
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∈ (↑s : Multiset ι)
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
case pos => exact hs₁ _ hs₂
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∉ (↑s : Multiset ι)
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
(s.prop i).resolve_left hs₂

Premises used: Or.resolve_left, Subtype.prop
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∉ (↑s : Multiset ι)
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
exact (s.prop i).resolve_left hs₂

Premises used: Or.resolve_left, Subtype.prop
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
hs₂ : i ∉ (↑s : Multiset ι)
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
case neg => exact (s.prop i).resolve_left hs₂

Premises used: Or.resolve_left, Subtype.prop
-- Module: Mathlib.Data.DFinsupp.Defs
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 }
case case₁ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0), f = 0
h : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
h₁ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
case₂ :
  ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι) (hs₂ : i ∈ (↑s : Multiset ι)),
    (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
case₃ case₄ :
  ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι) (hs₂ : i ∉ (↑s : Multiset ι)),
    (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
⊢ (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) → f = 0

Tactic:
case mp =>
        intro hs₁; ext i
        -- This instance prevent consuming `DecidableEq ι` in the next `by_cases`.
        letI := Classical.propDecidable
        by_cases hs₂ : i ∈ s.val
        case pos => exact hs₁ _ hs₂
        case neg => exact (s.prop i).resolve_left hs₂

Premises used: Subtype.val
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Set ι
f : Π₀ (i : ι), β i
⊢ (↑(f.support (β := β)) : Set ι) ⊆ s ↔ ∀ i ∉ s, (f : (a : ι) → β a) i = 0

Tactic:
simpa [Set.subset_def] using forall_congr' fun i => not_imp_comm

Premises used: Set.subset_def, not_imp_comm, forall_congr'
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
⊢ support (β := β) (single (β := β) i b) = {i}

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
⊢ support (β := β) (single (β := β) i b) ⊆ {i}

Tactic:
support_mk'_subset

Premises used: Set.Mem, DFinsupp.single, Multiset.dedup, setOf, List.dedup, Multiset.cons, DFinsupp.support_mk'_subset, Multiset.ofList, List.pwFilter, List.foldr, ite
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h :
  ∀ (i : ι),
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf g : (a : ι) → β₂ a) i =
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf g =
    mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
      f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι))

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
i : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf g : (a : ι) → β₂ a) i =
    (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
          f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
        (a : ι) → β₂ a)
      i

Tactic:
simp_all
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
pos :
  ∀ (h : i = i'),
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
      (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
neg :
  ∀ (h : ¬i = i'),
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
      (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'

Tactic:
by_cases h : i = i'
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
h : i = i'
pos :
  (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'

Tactic:
subst i'
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
h : ¬i = i'
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'

Tactic:
simp [h, hf]
-- Module: Mathlib.Data.DFinsupp.Defs
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
h : Function.Injective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)
i : ι
x y : β₁ i
eq : f i x = f i y
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i x) =
    mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i y)

Tactic:
simpa using congr_arg _ eq

Premises used: congr_arg
-- Module: Mathlib.Data.DFinsupp.Defs
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
⊢ Function.Injective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Injective (f i)

Tactic:
exact ⟨fun h i x y eq ↦ single_injective (@h (single i x) (single i y) <| by
    simpa using congr_arg _ eq), fun h _ _ eq ↦ DFinsupp.ext fun i ↦ h i congr($eq i)⟩
-- Module: Mathlib.Data.DFinsupp.Defs
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
⊢ Function.Injective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Injective (f i)

Tactic:
classical exact ⟨fun h i x y eq ↦ single_injective (@h (single i x) (single i y) <| by
    simpa using congr_arg _ eq), fun h _ _ eq ↦ DFinsupp.ext fun i ↦ h i congr($eq i)⟩