awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
k : κ
h₁ :
  ((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 : ι) → β a)
      ((h.symm : (a : κ) → ι) k) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₂ :
  (Equiv.cast ⋯ :
        (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k)))) → β ((h.symm : (a : κ) → ι) k))
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯ f :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        ((h.symm : (a : κ) → ι) k)) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₃ :
  (Equiv.cast ⋯ :
        (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k)))) → β ((h.symm : (a : κ) → ι) k))
      ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι))) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₄ :
  HEq (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι) : κ)))
    ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι)))
    ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k)
h₅ h₆ : (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) :
        (a : κ) → β ((h.symm : (a : κ) → ι) a))
      k =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k

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

Premises used: Equiv.apply_symm_apply, Equiv.cast_eq_iff_heq, DFinsupp.comapDomain'_apply, DFinsupp.mapRange_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : ι), α (some i)
a : α none
⊢ (extendWith (α := α) a f : (a : Option ι) → α a) none = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : ι), α (some i)
a : α none
i : ι
⊢ (extendWith (α := α) a f : (a : Option ι) → α a) (some i) = (f : (a : ι) → α (some a)) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
h :
  Eq (α := α none) ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) none)
    ((single (β := α) (some i) x : (a : Option ι) → α a) none)
h₁ :
  ∀ (j : ι),
    Eq (α := α (some j))
      ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) (some j))
      ((single (β := α) (some i) x : (a : Option ι) → α a) (some j))
⊢ Eq (α := Π₀ (i : Option ι), α i) (extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x))
    (single (β := α) (some i) x)

Tactic:
ext (_ | j)
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
h : Eq (α := α none) 0 ((single (β := α) (some i) x : (a : Option ι) → α a) none)
h₁ h₂ : Eq.{v + 1} (α := α none) 0 0
⊢ Eq (α := α none) ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) none)
    ((single (β := α) (some i) x : (a : Option ι) → α a) none)

Tactic:
rw [extendWith_none, single_eq_of_ne (Option.some_ne_none _).symm]

Premises used: DFinsupp.single_eq_of_ne, Ne.symm, Option.some_ne_none, DFinsupp.extendWith_none
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
h :
  (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
⊢ Eq (α := α (some j))
    ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) (some j))
    ((single (β := α) (some i) x : (a : Option ι) → α a) (some j))

Tactic:
rw [extendWith_some]

Premises used: DFinsupp.extendWith_some
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
h :
  ∀ (x : α (some j)),
    (single (β := fun (i : ι) ↦ α (some i)) j x : (a : ι) → α (some a)) j =
      (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
h₁ :
  ∀ (hij : j ≠ i),
    (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
      (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
⊢ (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)

Tactic:
obtain rfl | hij := Decidable.eq_or_ne j i

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
j : ι
x : α (some j)
h : x = (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
h₁ h₂ : x = x
⊢ (single (β := fun (i : ι) ↦ α (some i)) j x : (a : ι) → α (some a)) j =
    (single (β := α) (some j) x : (a : Option ι) → α a) (some j)

Tactic:
rw [single_eq_same, single_eq_same]

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
h : Eq (α := α (some j)) 0 ((single (β := α) (some i) x : (a : Option ι) → α a) (some j))
h₁ h₂ : Eq.{v + 1} (α := α (some j)) 0 0
⊢ (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)

Tactic:
rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]

Premises used: Function.Injective.ne, DFinsupp.single_eq_of_ne, Option.some_injective
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
h :
  Eq (α := α none) ((extendWith (α := α) x 0 : (a : Option ι) → α a) none)
    ((single (β := α) none x : (a : Option ι) → α a) none)
h₁ :
  ∀ (j : ι),
    Eq (α := α (some j)) ((extendWith (α := α) x 0 : (a : Option ι) → α a) (some j))
      ((single (β := α) none x : (a : Option ι) → α a) (some j))
⊢ Eq (α := Π₀ (i : Option ι), α i) (extendWith (α := α) x 0) (single (β := α) none x)

Tactic:
ext (_ | j)
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
h : x = (single (β := α) none x : (a : Option ι) → α a) none
h₁ h₂ : x = x
⊢ Eq (α := α none) ((extendWith (α := α) x 0 : (a : Option ι) → α a) none)
    ((single (β := α) none x : (a : Option ι) → α a) none)

Tactic:
rw [extendWith_none, single_eq_same]

Premises used: DFinsupp.single_eq_same, DFinsupp.extendWith_none
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
j : ι
h : (0 : (a : ι) → α (some a)) j = (single (β := α) none x : (a : Option ι) → α a) (some j)
h₁ : (0 : (a : ι) → α (some a)) j = 0
h₂ h₃ : Eq.{v + 1} (α := α (some j)) 0 0
⊢ Eq (α := α (some j)) ((extendWith (α := α) x 0 : (a : Option ι) → α a) (some j))
    ((single (β := α) none x : (a : Option ι) → α a) (some j))

Tactic:
rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]

Premises used: DFinsupp.zero_apply, DFinsupp.extendWith_some, DFinsupp.single_eq_of_ne, Option.some_ne_none
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
h :
  ∀ (i : Option ι),
    ((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
            ((fun (f : Π₀ (i : Option ι), α i) ↦
                (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
              f) :
          (a : Option ι) → α a)
        i =
      (f : (a : Option ι) → α a) i
⊢ (fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
      ((fun (f : Π₀ (i : Option ι), α i) ↦
          (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
        f) =
    f

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : Option ι
h :
  Eq (α := α none)
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      none)
    ((f : (a : Option ι) → α a) none)
h₁ :
  ∀ (i : ι),
    Eq (α := α (some i))
      (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
            ((fun (f : Π₀ (i : Option ι), α i) ↦
                (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
              f) :
          (a : Option ι) → α a)
        (some i))
      ((f : (a : Option ι) → α a) (some i))
⊢ ((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      i =
    (f : (a : Option ι) → α a) i

Tactic:
obtain - | i := i
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
h h₁ :
  Eq (α := α none)
    ((fun (f : Π₀ (i : Option ι), α i) ↦
          (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
        f).1
    ((f : (a : Option ι) → α a) none)
⊢ Eq (α := α none)
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      none)
    ((f : (a : Option ι) → α a) none)

Tactic:
rw [extendWith_none]

Premises used: DFinsupp.extendWith_none
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
h :
  (((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f).2 :
        (a : ι) → α (some a))
      i =
    (f : (a : Option ι) → α a) (some i)
h₁ h₂ : Eq (α := α (some i)) ((f : (a : Option ι) → α a) (some i)) ((f : (a : Option ι) → α a) (some i))
⊢ Eq (α := α (some i))
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      (some i))
    ((f : (a : Option ι) → α a) (some i))

Tactic:
rw [extendWith_some, comapDomain_apply]

Premises used: DFinsupp.extendWith_some, DFinsupp.comapDomain_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
dsimp :
  ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
      comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)) =
    x
⊢ (fun (f : Π₀ (i : Option ι), α i) ↦
        (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
      ((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2) x) =
    x

Tactic:
dsimp only
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
fst :
  ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
        comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).1 =
    x.1
snd :
  ∀ (i : ι),
    (((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
              comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).2 :
          (a : ι) → α (some a))
        i =
      (x.2 : (a : ι) → α (some a)) i
⊢ ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
      comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)) =
    x

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
⊢ ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
        comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).1 =
    x.1

Tactic:
extendWith_none x.snd _

Premises used: Prod.snd, DFinsupp.extendWith_none
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
⊢ ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
        comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).1 =
    x.1

Tactic:
exact extendWith_none x.snd _

Premises used: Prod.snd, DFinsupp.extendWith_none
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
i : ι
snd : (extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) (some i) = (x.2 : (a : ι) → α (some a)) i
snd₁ snd₂ : (x.2 : (a : ι) → α (some a)) i = (x.2 : (a : ι) → α (some a)) i
⊢ (((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
            comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).2 :
        (a : ι) → α (some a))
      i =
    (x.2 : (a : ι) → α (some a)) i

Tactic:
rw [comapDomain_apply, extendWith_some]

Premises used: DFinsupp.extendWith_some, DFinsupp.comapDomain_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
α : Option ι → Type v
inst : (i : Option ι) → AddZeroClass (α i)
f g : Π₀ (i : Option ι), α i
⊢ (equivProdDFinsupp (α := α) : (a : Π₀ (i : Option ι), α i) → α none × Π₀ (i : ι), α (some i)) (f + g) =
    HAdd.hAdd (α := α none × Π₀ (i : ι), α (some i)) (β := α none × Π₀ (i : ι), α (some i))
      ((equivProdDFinsupp (α := α) : (a : Π₀ (i : Option ι), α i) → α none × Π₀ (i : ι), α (some i)) f :
        α none × Π₀ (i : ι), α (some i))
      ((equivProdDFinsupp (α := α) : (a : Π₀ (i : Option ι), α i) → α none × Π₀ (i : ι), α (some i)) g :
        α none × Π₀ (i : ι), α (some i))

Tactic:
Prod.ext (add_apply _ _ _) (comapDomain_add _ (Option.some_injective _) _ _)

Premises used: DFinsupp.comapDomain_add, DFinsupp.add_apply, Prod.ext, Option.some_injective
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β₁ i)
inst_1 : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
h :
  ∀ (i : ι),
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (g₁ + g₂) : (a : ι) → β₂ a) i =
      (mapRange (β₁ := β₁) (β₂ := β₂) f hf g₁ + mapRange (β₁ := β₁) (β₂ := β₂) f hf g₂ : (a : ι) → β₂ a) i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf (g₁ + g₂) =
    mapRange (β₁ := β₁) (β₂ := β₂) f hf g₁ + mapRange (β₁ := β₁) (β₂ := β₂) f hf g₂

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β₁ i)
inst_1 : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
i : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (g₁ + g₂) : (a : ι) → β₂ a) i =
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf g₁ + mapRange (β₁ := β₁) (β₂ := β₂) f hf g₂ : (a : ι) → β₂ a) i

Tactic:
simp only [mapRange_apply f, coe_add, Pi.add_apply, hf']

Premises used: DFinsupp.coe_add, DFinsupp.mapRange_apply, Pi.add_apply
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β₂ i)
⊢ Eq (α := (Π₀ (i : ι), β₂ i) →+ Π₀ (i : ι), β₂ i)
    (addMonoidHom (β₁ := β₂) (β₂ := β₂) fun (i : ι) ↦ AddMonoidHom.id (β₂ i)) (AddMonoidHom.id (Π₀ (i : ι), β₂ i))

Tactic:
AddMonoidHom.ext mapRange_id

Premises used: DFinsupp.mapRange_id, AddMonoidHom.ext, rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → AddMonoidHom.{v₁, v₂} (β₁ i) (β₂ i)
f₂ : (i : ι) → AddMonoidHom.{v, v₁} (β i) (β₁ i)
h :
  ∀ (x : Π₀ (i : ι), β i) (i : ι),
    (((addMonoidHom (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).comp (f₂ i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i) x :
            Π₀ (i : ι), β₂ i) :
          (a : ι) → β₂ a)
        i =
      ((((addMonoidHom (β₁ := β₁) (β₂ := β₂) f).comp (addMonoidHom (β₁ := β) (β₂ := β₁) f₂) :
                (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i)
              x :
            Π₀ (i : ι), β₂ i) :
          (a : ι) → β₂ a)
        i
⊢ (addMonoidHom (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).comp (f₂ i)) =
    (addMonoidHom (β₁ := β₁) (β₂ := β₂) f).comp (addMonoidHom (β₁ := β) (β₂ := β₁) f₂)

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → AddMonoidHom.{v₁, v₂} (β₁ i) (β₂ i)
f₂ : (i : ι) → AddMonoidHom.{v, v₁} (β i) (β₁ i)
x : Π₀ (i : ι), β i
i : ι
⊢ (((addMonoidHom (β₁ := β) (β₂ := β₂) fun (i : ι) ↦ (f i).comp (f₂ i) : (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i) x :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i =
    ((((addMonoidHom (β₁ := β₁) (β₂ := β₂) f).comp (addMonoidHom (β₁ := β) (β₂ := β₁) f₂) :
              (a : Π₀ (i : ι), β i) → Π₀ (i : ι), β₂ i)
            x :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
rw :
  mapRange (β₁ := β₁) (β₂ := β₁)
      (fun (i : ι) ↦
        (fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x)
      ⋯ x =
    x
h :
  ∀ (i : ι),
    Eq.{v₁ + 1} (α := β₁ i)
      (((fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) 0) 0
⊢ mapRange (β₁ := β₂) (β₂ := β₁) (fun (i : ι) (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ⋯
      (mapRange (β₁ := β₁) (β₂ := β₂) (fun (i : ι) (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ⋯ x) =
    x

Tactic:
rw [← mapRange_comp]

Premises used: DFinsupp.mapRange_comp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
simp_rw : mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) ⋯ x = x
⊢ mapRange (β₁ := β₁) (β₂ := β₁)
      (fun (i : ι) ↦
        (fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x)
      ⋯ x =
    x

Tactic:
simp_rw [AddEquiv.symm_comp_self]

Premises used: AddEquiv.symm_comp_self
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
⊢ mapRange (β₁ := β₁) (β₂ := β₁) (fun (i : ι) ↦ id) ⋯ x = x

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
h : ∀ (i : ι), Eq.{v₁ + 1} (α := β₁ i) (id 0) 0
⊢ ∀ (i : ι),
    Eq.{v₁ + 1} (α := β₁ i)
      (((fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ∘ fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) 0) 0

Tactic:
simp_rw [AddEquiv.symm_comp_self]

Premises used: AddEquiv.symm_comp_self
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₁ i
⊢ ∀ (i : ι), Eq.{v₁ + 1} (α := β₁ i) (id 0) 0

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
rw :
  mapRange (β₁ := β₂) (β₂ := β₂)
      (fun (i : ι) ↦
        (fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x)
      ⋯ x =
    x
h :
  ∀ (i : ι),
    Eq.{v₂ + 1} (α := β₂ i)
      (((fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) 0) 0
⊢ mapRange (β₁ := β₁) (β₂ := β₂) (fun (i : ι) (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ⋯
      (mapRange (β₁ := β₂) (β₂ := β₁) (fun (i : ι) (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x) ⋯ x) =
    x

Tactic:
rw [← mapRange_comp]

Premises used: DFinsupp.mapRange_comp
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β i)
inst_1 : (i : ι) → AddZeroClass (β₁ i)
inst_2 : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → AddEquiv.{v₁, v₂} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
simp_rw : mapRange (β₁ := β₂) (β₂ := β₂) (fun (i : ι) ↦ id) ⋯ x = x
⊢ mapRange (β₁ := β₂) (β₂ := β₂)
      (fun (i : ι) ↦
        (fun (x : β₁ i) ↦ (e i : (a : β₁ i) → β₂ i) x) ∘ fun (x : β₂ i) ↦ ((e i).symm : (a : β₂ i) → β₁ i) x)
      ⋯ x =
    x

Tactic:
simp_rw [AddEquiv.self_comp_symm]

Premises used: AddEquiv.self_comp_symm