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 : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
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
have 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
Tactic: by_cases h2 : f i ≠ 0
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (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
have 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
Tactic: by_cases h2 : f i ≠ 0
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
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
⊢ (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
have h2₁ : Eq (α := β (↑i : ι)) ((f : (a : ι) → β a) (↑i : ι)) 0
Tactic: simp at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (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
have 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
Tactic: try simp at h2; simp [h2]
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (subtypeDomain (β := β) p f).support (β := fun (i : Subtype p) ↦ β (↑i : ι)) = Finset.subtype p (f.support (β := β))
have h : ∀ (a : Subtype p),
  a ∈ (subtypeDomain (β := β) p f).support (β := fun (i : Subtype p) ↦ β (↑i : ι)) ↔
    a ∈ Finset.subtype p (f.support (β := β))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddGroup (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ (-f).support (β := β) = f.support (β := β)
have h : ∀ (a : ι), a ∈ (-f).support (β := β) ↔ a ∈ f.support (β := β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
have rwa : ∀ (h : ¬(f : (a : ι) → β a) i ≠ 0), (f : (a : ι) → β a) i = 0
Tactic: rwa [mem_support_iff, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (f : (a : ι) → β a) i = 0
have rwa₁ : ∀ (h : (f : (a : ι) → β a) i = 0), (f : (a : ι) → β a) i = 0
Tactic: rwa [mem_support_iff, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
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 = (g : (a : ι) → β a) i
have hf : (f : (a : ι) → β a) i = 0
Tactic: have hf : f i = 0 := by rwa [mem_support_iff, not_not] at h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
have rwa : ∀ (h : i ∉ g.support (β := β)) (hf : (f : (a : ι) → β a) i = 0), (g : (a : ι) → β a) i = 0
Tactic: rwa [h₁, mem_support_iff, not_not] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (g : (a : ι) → β a) i = 0
have rwa₁ : ∀ (h : ¬(g : (a : ι) → β a) i ≠ 0) (hf : (f : (a : ι) → β a) i = 0), (g : (a : ι) → β a) i = 0
Tactic: rwa [h₁, mem_support_iff, not_not] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (g : (a : ι) → β a) i = 0
have rwa₂ : ∀ (h : (g : (a : ι) → β a) i = 0) (hf : (f : (a : ι) → β a) i = 0), (g : (a : ι) → β a) i = 0
Tactic: rwa [h₁, mem_support_iff, not_not] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
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
⊢ (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
have hg : (g : (a : ι) → β a) i = 0
Tactic: have hg : g i = 0 := by rwa [h₁, mem_support_iff, not_not] at h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
have rw : 0 = (g : (a : ι) → β a) i
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (f : (a : ι) → β a) i = (g : (a : ι) → β a) i
have rw₁ : Eq.{v + 1} (α := β i) 0 0
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
⊢ Eq (α := Π₀ (k : κ), β (h k)) (comapDomain (β := β) h hh 0) 0
have h₁ : ∀ (i : κ), (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
⊢ (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
have h₁ : (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = 0
Tactic: rw [zero_apply, comapDomain_apply, zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
have h₂ : Eq (α := β (h i)) ((0 : (a : ι) → β a) (h i)) 0
Tactic: rw [zero_apply, comapDomain_apply, zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (comapDomain (β := β) h hh 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
have h₃ : Eq.{v + 1} (α := β (h i)) 0 0
Tactic: rw [zero_apply, comapDomain_apply, zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
⊢ comapDomain (β := β) h hh (f + g) = comapDomain (β := β) h hh f + comapDomain (β := β) h hh g
have h₁ : ∀ (i : κ),
  (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
i : κ
⊢ (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
have 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
Tactic: rw [add_apply, comapDomain_apply, comapDomain_apply, comapDomain_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
have h₂ : (f + g : (a : ι) → β a) (h i) =
  (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i + (comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
Tactic: rw [add_apply, comapDomain_apply, comapDomain_apply, comapDomain_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
have h₃ : (f + g : (a : ι) → β a) (h i) = (f : (a : ι) → β a) (h i) + (comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
Tactic: rw [add_apply, comapDomain_apply, comapDomain_apply, comapDomain_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
have h₄ : (f + g : (a : ι) → β a) (h i) = HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
Tactic: rw [add_apply, comapDomain_apply, comapDomain_apply, comapDomain_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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))
⊢ (comapDomain (β := β) h hh (f + g) : (a : κ) → β (h a)) i =
    (comapDomain (β := β) h hh f + comapDomain (β := β) h hh g : (a : κ) → β (h a)) i
have 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))
Tactic: rw [add_apply, comapDomain_apply, comapDomain_apply, comapDomain_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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)
⊢ Eq (α := Π₀ (k : κ), β (h k)) (comapDomain (β := β) h hh (single (β := β) (h k) x))
    (single (β := fun (i : κ) ↦ β (h i)) k x)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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 : κ
⊢ ((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
have h₁ : (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
Tactic: rw [comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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 : κ
⊢ (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
have h₁ : ∀ (x : β (h i)),
  (single (β := β) (h i) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) i x : (a : κ) → β (h a)) i
Tactic: obtain rfl | hik := Decidable.eq_or_ne i k
Cleared hypotheses: k, x
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
have h₂ : ∀ (hik : i ≠ k),
  (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
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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)
⊢ (single (β := β) (h i) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) i x : (a : κ) → β (h a)) i
have h₁ : x = (single (β := fun (i : κ) ↦ β (h i)) i x : (a : κ) → β (h a)) i
Tactic: rw [single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (single (β := β) (h i) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) i x : (a : κ) → β (h a)) i
have h₂ : x = x
Tactic: rw [single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
have h₁ : Eq (α := β (h i)) ((single (β := β) (h k) x : (a : ι) → β a) (h i)) 0
Tactic: rw [single_eq_of_ne hik, single_eq_of_ne (hh.ne hik)]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
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
⊢ (single (β := β) (h k) x : (a : ι) → β a) (h i) = (single (β := fun (i : κ) ↦ β (h i)) k x : (a : κ) → β (h a)) i
have h₂ : Eq.{v + 1} (α := β (h i)) 0 0
Tactic: rw [single_eq_of_ne hik, single_eq_of_ne (hh.ne hik)]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
⊢ Eq (α := Π₀ (k : κ), β (h k)) (comapDomain' (β := β) h hh' 0) 0
have h₁ : ∀ (i : κ), (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i : κ
⊢ (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
have h₁ : (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = 0
Tactic: rw [zero_apply, comapDomain'_apply, zero_apply]