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)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : Ne (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0
pos pos₁ :
  (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:
try simp at h2; simp [h2]
-- 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 : ¬Ne (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0
⊢ Eq (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0

Tactic:
simp at h2
-- 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]
-- 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 : ¬Ne (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0
neg neg₁ :
  ∀ (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
⊢ (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:
try simp at h2; simp [h2]
-- 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 :
  ∀ (a : Subtype p),
    a ∈ (subtypeDomain (β := β) p f).support (β := fun (i : Subtype p) ↦ β (↑i : ι)) ↔
      a ∈ Finset.subtype p (f.support (β := β))
⊢ (subtypeDomain (β := β) p f).support (β := fun (i : Subtype p) ↦ β (↑i : ι)) = Finset.subtype p (f.support (β := β))

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

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
g₁ g₂ : Π₀ (i : ι), β i
⊢ (g₁ + g₂).support (β := β) ⊆ g₁.support (β := β) ∪ g₂.support (β := β)

Tactic:
support_zipWith

Premises used: DFinsupp.support_zipWith, Set.Mem, setOf
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
h : ∀ (a : ι), a ∈ (-f).support (β := β) ↔ a ∈ f.support (β := β)
⊢ (-f).support (β := β) = f.support (β := β)

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
a : ι
⊢ a ∈ (-f).support (β := β) ↔ a ∈ f.support (β := β)

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 : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
h_1 : f.support (β := β) = g.support (β := β) ∧ ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
h₁ : f.support (β := β) = g.support (β := β)
h₂ : ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
i : ι
h : i ∉ f.support (β := β)
rwa : ∀ (h : ¬(f : (a : ι) → β a) i ≠ 0), (f : (a : ι) → β a) i = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : (f : (a : ι) → β a) i = 0), (f : (a : ι) → β a) i = 0
⊢ (f : (a : ι) → β a) i = 0

Tactic:
rwa [mem_support_iff, not_not] at h

Premises used: Classical.not_not, DFinsupp.mem_support_iff
-- 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 : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
h_1 : f.support (β := β) = g.support (β := β) ∧ ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
h₁ : f.support (β := β) = g.support (β := β)
h₂ : ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
i : ι
h : i ∉ f.support (β := β)
⊢ (f : (a : ι) → β a) i = 0

Tactic:
have hf : f i = 0 := by rwa [mem_support_iff, not_not] at h
-- 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 : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
h_1 : f.support (β := β) = g.support (β := β) ∧ ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
h₁ : f.support (β := β) = g.support (β := β)
h₂ : ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
i : ι
h : i ∉ f.support (β := β)
hf : (f : (a : ι) → β a) i = 0
rwa : ∀ (h : i ∉ g.support (β := β)) (hf : (f : (a : ι) → β a) i = 0), (g : (a : ι) → β a) i = 0
rwa₁ : ∀ (h : ¬(g : (a : ι) → β a) i ≠ 0) (hf : (f : (a : ι) → β a) i = 0), (g : (a : ι) → β a) i = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : (g : (a : ι) → β a) i = 0) (hf : (f : (a : ι) → β a) i = 0), (g : (a : ι) → β a) i = 0
⊢ (g : (a : ι) → β a) i = 0

Tactic:
rwa [h₁, mem_support_iff, not_not] at h

Premises used: Classical.not_not, DFinsupp.mem_support_iff
-- 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 : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
h_1 : f.support (β := β) = g.support (β := β) ∧ ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
h₁ : f.support (β := β) = g.support (β := β)
h₂ : ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
i : ι
h : i ∉ f.support (β := β)
hf : (f : (a : ι) → β a) i = 0
⊢ (g : (a : ι) → β a) i = 0

Tactic:
have hg : g i = 0 := by rwa [h₁, mem_support_iff, not_not] at h
-- 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 : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
h_1 : f.support (β := β) = g.support (β := β) ∧ ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
h₁ : f.support (β := β) = g.support (β := β)
h₂ : ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
i : ι
h : i ∉ f.support (β := β)
hf : (f : (a : ι) → β a) i = 0
hg : (g : (a : ι) → β a) i = 0
rw : 0 = (g : (a : ι) → β a) i
rw₁ rw₂ : Eq.{v + 1} (α := β i) 0 0
⊢ (f : (a : ι) → β a) i = (g : (a : ι) → β a) i

Tactic:
rw [hf, hg]
-- 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 : ι) → DecidableEq (β i)
f : Π₀ (i : ι), β i
⊢ f.support (β := β) = f.support (β := β) ∧ ∀ i ∈ f.support (β := β), (f : (a : ι) → β a) i = (f : (a : ι) → β a) i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
f : Π₀ (i : ι), β i
k : κ
⊢ (comapDomain (β := β) h hh f : (a : κ) → β (h a)) k = (f : (a : ι) → β a) (h k)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
h₁ : ∀ (i : κ), (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
⊢ Eq (α := Π₀ (k : κ), β (h k)) (comapDomain (β := β) h hh 0) 0

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
h₁ : (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = 0
h₂ : Eq (α := β (h i)) ((0 : (a : ι) → β a) (h i)) 0
h₃ h₄ : Eq.{v + 1} (α := β (h i)) 0 0
⊢ (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i

Tactic:
rw [zero_apply, comapDomain_apply, zero_apply]

Premises used: DFinsupp.zero_apply, DFinsupp.comapDomain_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
h₁ :
  ∀ (i : κ),
    (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
      (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
⊢ comapDomain (β := β) h hh (f + g) = comapDomain (β := β) h hh f + comapDomain (β := β) h hh g

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i + (comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
h₂ :
  (f + g : (a : ι) → β a) (h i) =
    (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i + (comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
h₃ : (f + g : (a : ι) → β a) (h i) = (f : (a : ι) → β a) (h i) + (comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
h₄ : (f + g : (a : ι) → β a) (h i) = HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
h₅ h₆ :
  HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i)) =
    HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
⊢ (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i

Tactic:
rw [add_apply, comapDomain_apply, comapDomain_apply, comapDomain_apply, add_apply]

Premises used: DFinsupp.comapDomain_apply, DFinsupp.add_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
h₁ :
  ∀ (i : κ),
    ((comapDomain (β := β) h hh (single (β := β) (h k) x) : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i =
      (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
⊢ Eq (α := Π₀ (k : κ), β (h k)) (comapDomain (β := β) h hh (single (β := β) (h k) x))
    (single (β := fun (i : κ) ↦ β (h i)) k x)

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
h₁ : (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
⊢ ((comapDomain (β := β) h hh (single (β := β) (h k) x) : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i =
    (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i

Tactic:
rw [comapDomain_apply]

Premises used: DFinsupp.comapDomain_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
h₁ :
  ∀ (x : β (h i)),
    (single (β := β) (h i) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) i x : (a : κ) → β (h a)) i
h₂ :
  ∀ (hik : i ≠ k),
    (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
⊢ (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i

Tactic:
obtain rfl | hik := Decidable.eq_or_ne i k

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
x : β (h i)
h₁ : x = (single (β := fun (i : κ) ↦ β (h i)) i x : (a : κ) → β (h a)) i
h₂ h₃ : x = x
⊢ (single (β := β) (h i) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) i x : (a : κ) → β (h a)) i

Tactic:
rw [single_eq_same, single_eq_same]

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
h₁ : Eq (α := β (h i)) ((single (β := β) (h k) x : (a : ι) → β a) (h i)) 0
h₂ h₃ : Eq.{v + 1} (α := β (h i)) 0 0
⊢ (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i

Tactic:
rw [single_eq_of_ne hik, single_eq_of_ne (hh.ne hik)]

Premises used: Function.Injective.ne, DFinsupp.single_eq_of_ne
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f : Π₀ (i : ι), β i
k : κ
⊢ (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) k = (f : (a : ι) → β a) (h k)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
h₁ :
  ∀ (i : κ), (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
⊢ Eq (α := Π₀ (k : κ), β (h k)) (comapDomain' (β := β) h hh' 0) 0

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i : κ
h₁ : (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = 0
h₂ : Eq (α := β (h i)) ((0 : (a : ι) → β a) (h i)) 0
h₃ h₄ : Eq.{v + 1} (α := β (h i)) 0 0
⊢ (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i

Tactic:
rw [zero_apply, comapDomain'_apply, zero_apply]

Premises used: DFinsupp.zero_apply, DFinsupp.comapDomain'_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
h₁ :
  ∀ (i : κ),
    (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
      (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
⊢ comapDomain' (β := β) h hh' (f + g) = comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₂ :
  (f + g : (a : ι) → β a) (h i) =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₃ : (f + g : (a : ι) → β a) (h i) = (f : (a : ι) → β a) (h i) + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₄ : (f + g : (a : ι) → β a) (h i) = HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
h₅ h₆ :
  HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i)) =
    HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
⊢ (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i

Tactic:
rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]

Premises used: DFinsupp.comapDomain'_apply, DFinsupp.add_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
⊢ Eq (α := Π₀ (k : κ), β (h k)) (comapDomain' (β := β) h hh' (single (β := β) (h k) x))
    (single (β := fun (i : κ) ↦ β (h i)) k x)

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)
i : ι
rw rw₁ : HEq.{v + 1} (α := β i) 0 (β := β i) 0
⊢ HEq.{v + 1} (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) 0 (β := β i) 0

Tactic:
rw [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
h₁ :
  ∀ (i : ι),
    ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
              (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                  (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
                  (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
                    f) :
                Π₀ (i : ι), β i))
            (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
          (a : ι) → β a)
        i =
      (f : (a : ι) → β a) i
⊢ (fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
        (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
            (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
            (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯ f) :
          Π₀ (i : ι), β i))
      (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) =
    f

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
h₁ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
            (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        i) =
    (f : (a : ι) → β a) i
h₂ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f : (a : κ) → β ((h.symm : (a : κ) → ι) a))
        ((h : (a : ι) → κ) i)) =
    (f : (a : ι) → β a) i
h₃ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((f : (a : ι) → β a) ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) =
    (f : (a : ι) → β a) i
h₄ :
  HEq (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ)))
    ((f : (a : ι) → β a) ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) ((f : (a : ι) → β a) i)
h₅ h₆ : (f : (a : ι) → β a) i ≍ (f : (a : ι) → β a) i
⊢ ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
            (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
                (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
                  f) :
              Π₀ (i : ι), β i))
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
        (a : ι) → β a)
      i =
    (f : (a : ι) → β a) i

Tactic:
rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Equiv.cast_eq_iff_heq, DFinsupp.comapDomain'_apply, DFinsupp.mapRange_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)
h₁ :
  ∀ (k : κ),
    (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯
            ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
                (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                    (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
                    (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun)
                      ⋯ f) :
                  Π₀ (i : ι), β i))
              f) :
          (a : κ) → β ((h.symm : (a : κ) → ι) a))
        k =
      (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
⊢ comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯
      ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
          (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
              (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
              (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯ f) :
            Π₀ (i : ι), β i))
        f) =
    f

Tactic:
ext k