awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Surjective (f i)

Tactic:
⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)) (i : ι) (u : β₂ i), ∃ (a : β₁ i), f i a = u
refine_2 :
  ∀ (h : ∀ (i : ι), Function.Surjective (f i)) (x : Π₀ (i : ι), β₂ i),
    ∃ (a : Π₀ (i : ι), β₁ i), mapRange (β₁ := β₁) (β₂ := β₂) f hf a = x
⊢ Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Surjective (f i)

Tactic:
refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
-- 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.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)
i : ι
u : β₂ i
refine_1 :
  ∀ (x : Π₀ (i : ι), β₁ i) (hx : mapRange (β₁ := β₁) (β₂ := β₂) f hf x = single (β := β₂) i u), ∃ (a : β₁ i), f i a = u
⊢ ∃ (a : β₁ i), f i a = u

Tactic:
obtain ⟨x, hx⟩ := h (single i u)

Premises used: DFinsupp.single
-- 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.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)
i : ι
u : β₂ i
x : Π₀ (i : ι), β₁ i
hx : mapRange (β₁ := β₁) (β₂ := β₂) f hf x = single (β := β₂) i u
⊢ f i ((x : (a : ι) → β₁ a) i) = u

Tactic:
simpa using congr($hx 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
h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)
i : ι
u : β₂ i
x : Π₀ (i : ι), β₁ i
hx : mapRange (β₁ := β₁) (β₂ := β₂) f hf x = single (β := β₂) i u
⊢ ∃ (a : β₁ i), f i a = u

Tactic:
exact ⟨x i, by simpa using congr($hx 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
h : ∀ (i : ι), Function.Surjective (f i)
x : Π₀ (i : ι), β₂ i
refine_2 :
  ∀ (x : (i : ι) → β₂ i) (support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }) (s : Multiset ι)
    (hs : ∀ (i : ι), i ∈ s ∨ x i = 0),
    ∃ (a : Π₀ (i : ι), β₁ i),
      mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
        mk' (β := fun (i : ι) ↦ β₂ i) x
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } →
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
⊢ ∃ (a : Π₀ (i : ι), β₁ i), mapRange (β₁ := β₁) (β₂ := β₂) f hf a = x

Tactic:
obtain ⟨x, s, hs⟩ := x
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
i : ι
h' : x i ≠ 0
obtain : ∀ (u : β₁ i) (hu : f i u = x i), ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)
⊢ ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)

Tactic:
obtain ⟨u, hu⟩ := h i (x 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
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
i : ι
h' : x i ≠ 0
u : β₁ i
hu : f i u = x i
⊢ ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)

Tactic:
⟨u, hu, fun h'' ↦ (h' h'').elim⟩

Premises used: False.elim, And.intro, Exists.intro
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
i : ι
h' : x i ≠ 0
u : β₁ i
hu : f i u = x i
⊢ ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)

Tactic:
exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
⊢ ∀ (i : ι), ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)

Tactic:
have (i : ι) : ∃ u : β₁ i, f i u = x i ∧ (x i = 0 → u = 0) :=
      (eq_or_ne (x i) 0).elim
        (fun h ↦ ⟨0, (hf i).trans h.symm, fun _ ↦ rfl⟩)
        (fun h' ↦ by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩)
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
this : ∀ (i : ι), ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)
refine_2 :
  ∀ (y : (i : ι) → β₁ i) (hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)),
    ∃ (a : Π₀ (i : ι), β₁ i),
      mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
        mk' (β := fun (i : ι) ↦ β₂ i) x
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } →
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
⊢ ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))

Tactic:
choose y hy using this
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
⊢ ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))

Tactic:
⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩

Premises used: DFinsupp.ext, Subtype.mk, Trunc.mk, DFinsupp.mk', Exists.intro
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
refine_2 : ∀ (i : ι), i ∈ s ∨ y i = 0
refine_2₁ :
  ∀ (i : ι),
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf
            (mk' (β := fun (i : ι) ↦ β₁ i) y
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ y i = 0) s ⋯))) :
          (a : ι) → β₂ a)
        i =
      (mk' (β := fun (i : ι) ↦ β₂ i) x
            (Quot.mk
              (⇑trueSetoid :
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } →
                  { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
              (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs)) :
          (a : ι) → β₂ a)
        i
⊢ ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))

Tactic:
refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun 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
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ i ∈ s ∨ y i = 0

Tactic:
(hs i).imp_right (hy i).2

Premises used: And.right, Or.imp_right
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ i ∈ s ∨ y i = 0

Tactic:
exact (hs i).imp_right (hy i).2

Premises used: And.right, Or.imp_right
-- 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf
          (mk' (β := fun (i : ι) ↦ β₁ i) y
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ y i = 0) s ⋯))) :
        (a : ι) → β₂ a)
      i =
    (mk' (β := fun (i : ι) ↦ β₂ i) x
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } →
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs)) :
        (a : ι) → β₂ a)
      i

Tactic:
simp [(hy i).1]

Premises used: And.left
-- 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
refine_1 : ∀ (h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)) (i : ι) (u : β₂ i), ∃ (a : β₁ i), f i a = u
refine_2 refine_2₁ :
  ∀ (h : ∀ (i : ι), Function.Surjective (f i)) (x : Π₀ (i : ι), β₂ i),
    ∃ (a : Π₀ (i : ι), β₁ i), mapRange (β₁ := β₁) (β₂ := β₂) f hf a = x
⊢ Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Surjective (f i)

Tactic:
classical
  refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨x, hx⟩ := h (single i u)
    exact ⟨x i, by simpa using congr($hx i)⟩
  · obtain ⟨x, s, hs⟩ := x
    have (i : ι) : ∃ u : β₁ i, f i u = x i ∧ (x i = 0 → u = 0) :=
      (eq_or_ne (x i) 0).elim
        (fun h ↦ ⟨0, (hf i).trans h.symm, fun _ ↦ rfl⟩)
        (fun h' ↦ by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩)
    choose y hy using this
    refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩
    · exact (hs i).imp_right (hy i).2
    · simp [(hy i).1]
-- 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)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf g).support (β := β₂) ⊆ g.support (β := β₁)

Tactic:
simp [mapRange_def]

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

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → Zero (β₁ i)
inst_4 : (i : ι) → Zero (β₂ i)
inst_5 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_6 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
⊢ (zipWith (β := β) (β₁ := β₁) (β₂ := β₂) f hf g₁ g₂).support (β := β) ⊆ g₁.support (β := β₁) ∪ g₂.support (β := β₂)

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 : ι
f : Π₀ (i : ι), β i
⊢ erase (β := β) i f =
    mk (β := β) (f.support (β := β).erase i) fun (j : (↑(↑(f.support (β := β).erase i) : Set ι) : Type u)) ↦
      (f : (a : ι) → β a) (↑j : ι)

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 : ι
f : Π₀ (i : ι), β i
h : ∀ (a : ι), a ∈ (erase (β := β) i f).support (β := β) ↔ a ∈ f.support (β := β).erase i
⊢ (erase (β := β) i f).support (β := β) = f.support (β := β).erase i

Tactic:
ext
-- 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
a : ι
⊢ a ∈ (erase (β := β) i f).support (β := β) ↔ a ∈ f.support (β := β).erase i

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)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
h₁ : ∀ (j : ι), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
⊢ (f.update (β := β) i b).support (β := β) = insert i (f.support (β := β))

Tactic:
ext j
-- 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 : ι
b : β i
h : b ≠ 0
j : ι
h₁ : i ∈ (f.update (β := β) i b).support (β := β) ↔ i ∈ insert i (f.support (β := β))
h₂ : ∀ (hi : i ≠ j), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Premises used: eq_or_ne, rfl
-- 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 : ι
b : β i
h : b ≠ 0
⊢ i ∈ (f.update (β := β) i b).support (β := β) ↔ i ∈ insert i (f.support (β := β))

Tactic:
simp [h]
-- 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 : ι
b : β i
h : b ≠ 0
j : ι
hi : i ≠ j
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))

Tactic:
simp [hi.symm]

Premises used: Ne.symm
-- 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 : ι
b : β i
inst_3 : Decidable (b = 0)
h :
  ∀ (j : ι),
    j ∈ (f.update (β := β) i b).support (β := β) ↔
      j ∈ if b = 0 then (erase (β := β) i f).support (β := β) else insert i (f.support (β := β))
⊢ (f.update (β := β) i b).support (β := β) =
    if b = 0 then (erase (β := β) i f).support (β := β) else insert i (f.support (β := β))

Tactic:
ext j
-- 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 : ι
b : β i
inst_3 : Decidable (b = 0)
j : ι
pos : ∀ (hb : b = 0), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)
neg : ∀ (hb : ¬b = 0), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔
    j ∈ if b = 0 then (erase (β := β) i f).support (β := β) else insert i (f.support (β := β))

Tactic:
split_ifs with hb
-- 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 : ι
b : β i
inst_3 : Decidable (b = 0)
j : ι
hb : b = 0
pos :
  ∀ [Decidable (Eq.{v + 1} (α := β i) 0 0)],
    j ∈ (f.update (β := β) i 0).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)

Tactic:
subst hb
-- 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 j : ι
inst_3 : Decidable (Eq.{v + 1} (α := β i) 0 0)
⊢ j ∈ (f.update (β := β) i 0).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)

Tactic:
simp [update_eq_erase, support_erase]

Premises used: DFinsupp.support_erase, DFinsupp.update_eq_erase
-- 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 : ι
b : β i
inst_3 : Decidable (b = 0)
j : ι
hb : ¬b = 0
neg neg₁ : j ∈ insert i (f.support (β := β)) ↔ j ∈ insert i (f.support (β := β))
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))

Tactic:
rw [support_update_ne_zero f _ hb]

Premises used: DFinsupp.support_update_ne_zero
-- 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)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
⊢ filter (β := β) p f =
    mk (β := β) (Finset.filter p (f.support (β := β)))
      fun (i : (↑(↑(Finset.filter p (f.support (β := β))) : Set ι) : Type u)) ↦ (f : (a : ι) → β a) (↑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)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
⊢ (filter (β := β) p f).support (β := β) = {x ∈ f.support (β := β) | p x}

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)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
h :
  ∀ (i : Subtype p),
    (subtypeDomain (β := β) p f : (a : Subtype p) → β (↑a : ι)) i =
      (mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
            fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
            (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι) :
          (a : Subtype p) → β (↑a : ι))
        i
⊢ subtypeDomain (β := β) p f =
    mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
      fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
      (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι)

Tactic:
ext i
-- 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)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
pos :
  ∀ (h2 : Ne (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0),
    (subtypeDomain (β := β) p f : (a : Subtype p) → β (↑a : ι)) i =
      (mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
            fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
            (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι) :
          (a : Subtype p) → β (↑a : ι))
        i
neg :
  ∀ (h2 : ¬Ne (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0),
    (subtypeDomain (β := β) p f : (a : Subtype p) → β (↑a : ι)) i =
      (mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
            fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
            (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι) :
          (a : Subtype p) → β (↑a : ι))
        i
⊢ (subtypeDomain (β := β) p f : (a : Subtype p) → β (↑a : ι)) i =
    (mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
          fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
          (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι) :
        (a : Subtype p) → β (↑a : ι))
      i

Tactic:
by_cases h2 : f i ≠ 0

Premises used: Subtype.val, DFunLike.coe
-- 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)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : ¬Eq (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0
⊢ (subtypeDomain (β := β) p f : (a : Subtype p) → β (↑a : ι)) i =
    (mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
          fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
          (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι) :
        (a : Subtype p) → β (↑a : ι))
      i

Tactic:
simp [h2]