awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u_1
inst_2 : AddZeroClass γ
f g : (⨁ (i : ι), β i) →+ γ
H :
  ∀ (i : ι) (y : β i),
    Eq.{u_1 + 1} (α := γ)
      ((f : (a : ⨁ (i : ι), β i) → γ) ((of β i : (a : β i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) : γ)
      ((g : (a : ⨁ (i : ι), β i) → γ) ((of β i : (a : β i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) : γ)
⊢ f = g

Tactic:
DFinsupp.addHom_ext H

Premises used: DFinsupp.addHom_ext, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u_1
inst_2 : AddZeroClass γ
f g : (⨁ (i : ι), β i) →+ γ
H : ∀ (i : ι), f.comp (of β i) = g.comp (of β i)
⊢ f = g

Tactic:
addHom_ext fun i => DFunLike.congr_fun <| H i

Premises used: DFunLike.congr_fun, DirectSum.addHom_ext
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
φ : (i : ι) → AddMonoidHom.{w, u₁} (β i) γ
i : ι
x : β i
⊢ Eq.{u₁ + 1} (α := γ)
    ((toAddMonoid (β := β) φ : (a : ⨁ (i : ι), β i) → γ) ((of β i : (a : β i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i) : γ)
    ((φ i : (a : β i) → γ) x : γ)

Tactic:
DFinsupp.liftAddHom_apply_single φ i x

Premises used: DFinsupp.liftAddHom_apply_single
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
e_a : ψ = toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i)
⊢ Eq.{u₁ + 1} (α := γ) ((ψ : (a : ⨁ (i : ι), β i) → γ) f : γ)
    ((toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i) : (a : ⨁ (i : ι), β i) → γ) f : γ)

Tactic:
congr
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
e_a :
  ∀ (x : ι),
    ψ.comp (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x) =
      AddMonoidHom.comp (toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i))
        (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x)
⊢ ψ = toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i)

Tactic:
apply DFinsupp.addHom_ext'

Premises used: DFinsupp.addHom_ext'
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
x : ι
e_a : ψ.comp (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x) = ψ.comp (of β x)
⊢ ψ.comp (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x) =
    AddMonoidHom.comp (toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i)) (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x)

Tactic:
simp [toAddMonoid]

Premises used: DirectSum.toAddMonoid
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
x : ι
⊢ ψ.comp (DFinsupp.singleAddHom (fun (i : ι) ↦ β i) x) = ψ.comp (of β x)

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
⊢ Injective (α := (i : ι) → AddMonoidHom.{w, u₁} (β i) γ) (toAddMonoid (β := β))

Tactic:
DFinsupp.liftAddHom.injective

Premises used: DFinsupp.liftAddHom, AddEquiv.injective, DirectSum, DirectSum.toAddMonoid
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
f g : (i : ι) → AddMonoidHom.{w, u₁} (β i) γ
⊢ toAddMonoid (β := β) f = toAddMonoid (β := β) g ↔ f = g

Tactic:
toAddMonoid_injective.eq_iff

Premises used: Function.Injective.eq_iff, DirectSum.toAddMonoid_injective
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
i : ι
f : AddMonoidHom.{u₁, w} γ (β i)
rw :
  (((AddMonoidHom.compHom : (a : β i →+ ⨁ (i : ι), β i) → (γ →+ β i) →+ γ →+ ⨁ (i : ι), β i) (of β i) :
          AddMonoidHom.{u₁, w} γ (β i) →+ γ →+ ⨁ (i : ι), β i) :
        (a : γ →+ β i) → γ →+ ⨁ (i : ι), β i)
      f =
    AddMonoidHom.comp (of β i) f
⊢ (fromAddMonoid (β := β) : (a : ⨁ (i : ι), γ →+ β i) → γ →+ ⨁ (i : ι), β i)
      (((of (fun (i : ι) ↦ AddMonoidHom.{u₁, w} γ (β i)) i :
            AddMonoidHom.{u₁, w} γ (β i) →+ ⨁ (i : ι), AddMonoidHom.{u₁, w} γ (β i)) :
          (a : γ →+ β i) → ⨁ (i : ι), γ →+ β i)
        f) =
    AddMonoidHom.comp (of β i) f

Tactic:
rw [fromAddMonoid, toAddMonoid_of]

Premises used: DirectSum.fromAddMonoid, DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
i : ι
f : AddMonoidHom.{u₁, w} γ (β i)
⊢ (((AddMonoidHom.compHom : (a : β i →+ ⨁ (i : ι), β i) → (γ →+ β i) →+ γ →+ ⨁ (i : ι), β i) (of β i) :
          AddMonoidHom.{u₁, w} γ (β i) →+ γ →+ ⨁ (i : ι), β i) :
        (a : γ →+ β i) → γ →+ ⨁ (i : ι), β i)
      f =
    AddMonoidHom.comp (of β i) f

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
i : ι
f : AddMonoidHom.{u₁, w} γ (β i)
x : γ
rw :
  Eq (α := ⨁ (i : ι), β i) ((AddMonoidHom.comp (of β i) f : (a : γ) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
rw₁ :
  Eq (α := ⨁ (i : ι), β i)
    (comp (β := β i) (⇑(of β i) : (a : β i) → ⨁ (i : ι), β i) (⇑f : (a : γ) → β i) x : ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
rw₂ rw₃ :
  Eq (α := ⨁ (i : ι), β i) ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)
⊢ Eq (α := ⨁ (i : ι), β i)
    ((((fromAddMonoid (β := β) : (a : ⨁ (i : ι), γ →+ β i) → γ →+ ⨁ (i : ι), β i)
              (((of (fun (i : ι) ↦ AddMonoidHom.{u₁, w} γ (β i)) i :
                    AddMonoidHom.{u₁, w} γ (β i) →+ ⨁ (i : ι), AddMonoidHom.{u₁, w} γ (β i)) :
                  (a : γ →+ β i) → ⨁ (i : ι), γ →+ β i)
                f) :
            γ →+ ⨁ (i : ι), β i) :
          (a : γ) → ⨁ (i : ι), β i)
        x :
      ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f : (a : γ) → β i) x) : ⨁ (i : ι), β i)

Tactic:
rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]

Premises used: DirectSum.fromAddMonoid_of, Function.comp, AddMonoidHom.coe_comp
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x : ⨁ (x : ι), M
rw : Eq (α := ⨁ (x : ι), M) (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) 0) 0
rw₁ rw₂ : Eq (α := ⨁ (x : ι), M) 0 0
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M) 0) :
      ⨁ (i : ι), M)
    (0 : ⨁ (i : ι), M)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x_1 : ⨁ (x : ι), M
p : ι
x : M
rw :
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
          (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
rw₁ :
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((AddMonoidHom.id M : (a : M) → M) x) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
rw₂ rw₃ :
  Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M)
          (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) p : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)

Tactic:
rw [Unique.default_eq p, toAddMonoid_of, AddMonoidHom.id_apply]

Premises used: AddMonoidHom.id_apply, Unique.default_eq, DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι_1 : Type v
β : ι_1 → Type w
inst : (i : ι_1) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Unique ι
x_1 x y : ⨁ (i : ι), M
ihx :
  ((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M) x) =
    x
ihy :
  ((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M) y) =
    y
⊢ ((of.{u_1, v} (fun (x : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((toAddMonoid (β := fun (x : ι) ↦ M) fun (x : ι) ↦ AddMonoidHom.id M : (a : ⨁ (i : ι), M) → M) (x + y)) =
    x + y

Tactic:
grind
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x : M
⊢ Eq (α := ⨁ (x : ι), M) ((AddEquiv.symm (DirectSum.id M ι) : (a : M) → ⨁ (x : ι), M) x : ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)

Tactic:
rfl

Premises used: DFinsupp.single, rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x : ⨁ (x : ι), M
rw :
  ((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) ((x : (a : ι) → M) default) = x
⊢ (DirectSum.id M ι : (a : ⨁ (x : ι), M) → M) x = (x : (a : ι) → M) default

Tactic:
rw [← AddEquiv.eq_symm_apply, id_symm_apply, eq_comm]

Premises used: DirectSum.id_symm_apply, eq_comm, AddEquiv.eq_symm_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x : ⨁ (x : ι), M
zero :
  Eq (α := ⨁ (x : ι), M)
    (((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((0 : (a : ι) → M) default) :
      ⨁ (i : ι), M)
    (0 : ⨁ (i : ι), M)
of :
  ∀ (i : ι) (x : M),
    Eq (α := ⨁ (x : ι), M)
      (((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
          (((((DirectSum.of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x :
                ⨁ (i : ι), M) :
              (a : ι) → M)
            default) :
        ⨁ (i : ι), M)
      (((DirectSum.of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)
add :
  ∀ (x y : ⨁ (i : ι), M),
    ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
          ((x : (a : ι) → M) default) =
        x →
      ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
            ((y : (a : ι) → M) default) =
          y →
        ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
            ((x + y : (a : ι) → M) default) =
          x + y
⊢ ((DirectSum.of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((x : (a : ι) → M) default) =
    x

Tactic:
induction x using DirectSum.induction_on
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        ((0 : (a : ι) → M) default) :
      ⨁ (i : ι), M)
    (0 : ⨁ (i : ι), M)

Tactic:
simp [Unique.eq_default, *]

Premises used: Unique.eq_default
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
i : ι
x : M
⊢ Eq (α := ⨁ (x : ι), M)
    (((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
        (((((of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M) :
            (a : ι) → M)
          default) :
      ⨁ (i : ι), M)
    (((of.{u_1, v} (fun (x : ι) ↦ M) i : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)

Tactic:
simp [Unique.eq_default, *]

Premises used: Unique.eq_default
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
M : Type v
ι : Type u_1
inst : AddCommMonoid M
inst_1 : Unique ι
x y : ⨁ (i : ι), M
h :
  ((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) ((x : (a : ι) → M) default) = x
h_1 :
  ((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) ((y : (a : ι) → M) default) = y
⊢ ((of.{u_1, v} (fun (i : ι) ↦ M) default : M →+ ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M)
      ((x + y : (a : ι) → M) default) =
    x + y

Tactic:
simp [Unique.eq_default, *]

Premises used: Unique.eq_default
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
κ : Type u_1
h : ι ≃ κ
f : ⨁ (i : ι), β i
k : κ
⊢ (((equivCongrLeft (β := β) h : (a : ⨁ (i : ι), β i) → ⨁ (k : κ), β ((h.symm : (a : κ) → ι) k)) f :
          ⨁ (k : κ), β ((h.symm : (a : κ) → ι) k)) :
        (a : κ) → β ((h.symm : (a : κ) → ι) a))
      k =
    (f : (a : ι) → β a) ((h.symm : (a : κ) → ι) k)

Tactic:
DFinsupp.comapDomain'_apply _ h.right_inv _ _

Premises used: Equiv.right_inv, DFinsupp.comapDomain'_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
κ : Type u_1
h : ι ≃ κ
f : ⨁ (i : ι), β i
k : κ
⊢ (((equivCongrLeft (β := β) h : (a : ⨁ (i : ι), β i) → ⨁ (k : κ), β ((h.symm : (a : κ) → ι) k)) f :
          ⨁ (k : κ), β ((h.symm : (a : κ) → ι) k)) :
        (a : κ) → β ((h.symm : (a : κ) → ι) a))
      k =
    (f : (a : ι) → β a) ((h.symm : (a : κ) → ι) k)

Tactic:
exact DFinsupp.comapDomain'_apply _ h.right_inv _ _

Premises used: Equiv.right_inv, DFinsupp.comapDomain'_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
inst : DecidableEq ι
α : ι → Type u
δ : (i : ι) → α i → Type w
inst_1 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
f : ⨁ (i : (_i : ι) × α _i), δ (i.fst (β := fun (_i : ι) ↦ α _i)) (i.snd (β := fun (_i : ι) ↦ α _i))
i : ι
j : α i
⊢ ((((sigmaCurry (α := α) (δ := δ) : (a : ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) → ⨁ (i : ι) (j : α i), δ i j) f :
              ⨁ (i : ι) (j : α i), δ i j) :
            (a : ι) → ⨁ (j : α a), δ a j)
          i :
        (a : α i) → δ i a)
      j =
    (f : (a : (_i : ι) × α _i) → δ a.fst a.snd) (Sigma.mk (β := fun (_i : ι) ↦ α _i) i j)

Tactic:
DFinsupp.sigmaCurry_apply (δ := δ) _ i j

Premises used: DFinsupp.sigmaCurry_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
inst : DecidableEq ι
α : ι → Type u
δ : (i : ι) → α i → Type w
inst_1 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
f : ⨁ (i : ι) (j : α i), δ i j
i : ι
j : α i
⊢ (((sigmaUncurry (α := α) (δ := δ) : (a : ⨁ (i : ι) (j : α i), δ i j) → ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) f :
          ⨁ (i : (_i : ι) × α _i), δ (i.fst (β := fun (_i : ι) ↦ α _i)) (i.snd (β := fun (_i : ι) ↦ α _i))) :
        (a : (_i : ι) × α _i) → δ a.fst a.snd)
      (Sigma.mk (β := fun (_i : ι) ↦ α _i) i j) =
    ((f : (a : ι) → ⨁ (j : α a), δ a j) i : (a : α i) → δ i a) j

Tactic:
DFinsupp.sigmaUncurry_apply f i j

Premises used: DFinsupp.sigmaUncurry_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
inst : DecidableEq ι
M : Type u_1
S : Type u_2
inst_1 : DecidableEq M
inst_2 : AddCommMonoid M
inst_3 : SetLike S M
inst_4 : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
simp :
  Eq (α := M)
    ((DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (A i) :
          (a : ⨁ (i : ι), ↥(A i)) → M)
        x :
      M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)
⊢ Eq (α := M) ((DirectSum.coeAddMonoidHom A : (a : ⨁ (i : ι), ↥(A i)) → M) x : M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)

Tactic:
simp only [DirectSum.coeAddMonoidHom, toAddMonoid, DFinsupp.liftAddHom, AddEquiv.coe_mk,
    Equiv.coe_fn_mk]

Premises used: DirectSum.coeAddMonoidHom, DFinsupp.liftAddHom, Equiv.coe_fn_mk, AddEquiv.coe_mk, DirectSum.toAddMonoid
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
inst : DecidableEq ι
M : Type u_1
S : Type u_2
inst_1 : DecidableEq M
inst_2 : AddCommMonoid M
inst_3 : SetLike S M
inst_4 : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ Eq (α := M)
    ((DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (A i) :
          (a : ⨁ (i : ι), ↥(A i)) → M)
        x :
      M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)

Tactic:
DFinsupp.sumAddHom_apply _ x

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
inst : DecidableEq ι
M : Type u_1
S : Type u_2
inst_1 : DecidableEq M
inst_2 : AddCommMonoid M
inst_3 : SetLike S M
inst_4 : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ Eq (α := M)
    ((DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (A i) :
          (a : ⨁ (i : ι), ↥(A i)) → M)
        x :
      M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)

Tactic:
exact DFinsupp.sumAddHom_apply _ x

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i : ι
x : ↥(A i)
⊢ (DirectSum.coeAddMonoidHom A : (a : ⨁ (i : ι), ↥(A i)) → M)
      (((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
        ⨁ (i : ι), ↥(A i)) =
    (↑x : M)

Tactic:
toAddMonoid_of _ _ _

Premises used: DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
inl :
  ∀ (x : ↥(A j)),
    (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) j : ↥(A j) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A j)) → ⨁ (i : ι), ↥(A i)) x :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            j) :
        M) =
      (↑(if j = j then x else 0) : M)
inr :
  ∀ (h : j ≠ i),
    (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
                ⨁ (i : ι), ↥(A i)) :
              (a : ι) → ↥(A a))
            j) :
        M) =
      (↑(if i = j then x else 0) : M)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)

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

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
j : ι
x : ↥(A j)
inl : (↑x : M) = (↑(if j = j then x else 0) : M)
inl₁ inl₂ : (↑x : M) = (↑x : M)
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) j : ↥(A j) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A j)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if j = j then x else 0) : M)

Tactic:
rw [DirectSum.of_eq_same, if_pos rfl]

Premises used: if_pos, DirectSum.of_eq_same, rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike S M
inst_3 : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
inr : (↑0 : M) = (↑(if i = j then x else 0) : M)
inr₁ : Eq.{u_1 + 1} (α := M) (↑0 : M) (↑0 : M)
inr₂ : Eq.{u_1 + 1} (α := M) 0 (↑0 : M)
inr₃ inr₄ : Eq.{u_1 + 1} (α := M) 0 0
⊢ (↑(((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
              ⨁ (i : ι), ↥(A i)) :
            (a : ι) → ↥(A a))
          j) :
      M) =
    (↑(if i = j then x else 0) : M)

Tactic:
rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]

Premises used: Ne.symm, ZeroMemClass.coe_zero, if_neg, DirectSum.of_eq_of_ne
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
inst : DecidableEq ι
inst_1 : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
rw :
  Surjective (α := Π₀ (i : ι), ↥(A i)) (β := M)
    (⇑(DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtype) : (a : Π₀ (i : ι), ↥(A i)) → M)
⊢ iSup A = ⊤

Tactic:
rw [AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, AddMonoidHom.mrange_eq_top]

Premises used: AddMonoidHom.mrange_eq_top, AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
inst : DecidableEq ι
inst_1 : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ Surjective (α := Π₀ (i : ι), ↥(A i)) (β := M)
    (⇑(DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtype) : (a : Π₀ (i : ι), ↥(A i)) → M)

Tactic:
Function.Bijective.surjective h

Premises used: Function.Bijective.surjective
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
inst : DecidableEq ι
inst_1 : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ Surjective (α := Π₀ (i : ι), ↥(A i)) (β := M)
    (⇑(DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtype) : (a : Π₀ (i : ι), ↥(A i)) → M)

Tactic:
exact Function.Bijective.surjective h

Premises used: Function.Bijective.surjective
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : AddCommMonoid M
inst_1 : SetLike S M
inst_2 : AddSubmonoidClass S M
inst_3 : DecidableEq ι
inst_4 : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ Membership.mem (γ := Set ι) (support.{v, u_1} (M := M) fun (i : ι) ↦ (↑((x : (a : ι) → ↥(A a)) i) : M)) m →
    m ∈ (↑(DFinsupp.support (β := fun (i : ι) ↦ ↥(A i)) x) : Set ι)

Tactic:
simp only [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not,
    ZeroMemClass.coe_eq_zero, imp_self]

Premises used: ZeroMemClass.coe_eq_zero, DFinsupp.mem_support_toFun, imp_self, Function.mem_support, Finset.mem_coe, not_imp_not
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
M : Type u_1
S : Type u_2
inst : AddCommMonoid M
inst_1 : SetLike S M
inst_2 : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ HasFiniteSupport.{v, u_1} (M := M) fun (i : ι) ↦ (↑((x : (a : ι) → ↥(A a)) i) : M)

Tactic:
(DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)

Premises used: Function.HasFiniteSupport, Set.Finite.subset, DFinsupp.support, Finset.finite_toSet, DirectSum.support_subset