awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)

Premises used: Set.Finite.subset, DFinsupp.support, Finset.finite_toSet, DirectSum.support_subset
-- 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:
classical
  exact (DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
inst_2 : DecidableEq ι
i : ι
x : α i
⊢ Eq (α := ⨁ (i : ι), β i)
    ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) ((of α i : (a : α i) → ⨁ (i : ι), α i) x) :
      ⨁ (i : ι), β i)
    ((of β i : (a : β i) → ⨁ (i : ι), β i) ((f i : (a : α i) → β i) x) : ⨁ (i : ι), β i)

Tactic:
DFinsupp.mapRange_single (hf := fun _ => map_zero _)

Premises used: DFinsupp.single, DFinsupp.mapRange_single, DFinsupp.mapRange, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
i : ι
x : ⨁ (i : ι), α i
⊢ (((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i) : (a : ι) → β a) i =
    (f i : (a : α i) → β i) ((x : (a : ι) → α a) i)

Tactic:
DFinsupp.mapRange_apply (hf := fun _ => map_zero _) _ _ _

Premises used: map_zero, DFinsupp.mapRange_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → AddCommMonoid (α i)
⊢ Eq (α := (⨁ (i : ι), α i) →+ ⨁ (i : ι), α i) (map (α := α) (β := α) fun (i : ι) ↦ AddMonoidHom.id (α i))
    (AddMonoidHom.id (⨁ (i : ι), α i))

Tactic:
DFinsupp.mapRange.addMonoidHom_id

Premises used: DirectSum.map, DirectSum, DFinsupp.mapRange.addMonoidHom_id
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
γ : ι → Type u_6
inst_2 : (i : ι) → AddCommMonoid (γ i)
g : (i : ι) → AddMonoidHom.{u_5, u_6} (β i) (γ i)
⊢ (map (α := α) (β := γ) fun (i : ι) ↦ (g i).comp (f i)) = (map (α := β) (β := γ) g).comp (map (α := α) (β := β) f)

Tactic:
DFinsupp.mapRange.addMonoidHom_comp _ _

Premises used: DFinsupp.mapRange.addMonoidHom_comp, DirectSum.map, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
⊢ Injective (α := ⨁ (i : ι), α i) (β := ⨁ (i : ι), β i)
      (⇑(map (α := α) (β := β) f) : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) ↔
    ∀ (i : ι), Injective.{u_4 + 1, u_5 + 1} (α := α i) (β := β i) (⇑(f i) : (a : α i) → β i)

Tactic:
DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange, DFinsupp.mapRange_injective, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
⊢ Injective (α := ⨁ (i : ι), α i) (β := ⨁ (i : ι), β i)
      (⇑(map (α := α) (β := β) f) : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) ↔
    ∀ (i : ι), Injective.{u_4 + 1, u_5 + 1} (α := α i) (β := β i) (⇑(f i) : (a : α i) → β i)

Tactic:
exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_injective
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
⊢ Injective (α := ⨁ (i : ι), α i) (β := ⨁ (i : ι), β i)
      (⇑(map (α := α) (β := β) f) : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) ↔
    ∀ (i : ι), Injective.{u_4 + 1, u_5 + 1} (α := α i) (β := β i) (⇑(f i) : (a : α i) → β i)

Tactic:
classical exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_injective
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
⊢ Surjective (α := ⨁ (i : ι), α i) (β := ⨁ (i : ι), β i)
      (⇑(map (α := α) (β := β) f) : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) ↔
    ∀ (i : ι), Surjective.{u_4 + 1, u_5 + 1} (α := α i) (β := β i) (⇑(f i) : (a : α i) → β i)

Tactic:
DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange, DFinsupp.mapRange_surjective, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
⊢ Surjective (α := ⨁ (i : ι), α i) (β := ⨁ (i : ι), β i)
      (⇑(map (α := α) (β := β) f) : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) ↔
    ∀ (i : ι), Surjective.{u_4 + 1, u_5 + 1} (α := α i) (β := β i) (⇑(f i) : (a : α i) → β i)

Tactic:
exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_surjective
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
⊢ Surjective (α := ⨁ (i : ι), α i) (β := ⨁ (i : ι), β i)
      (⇑(map (α := α) (β := β) f) : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) ↔
    ∀ (i : ι), Surjective.{u_4 + 1, u_5 + 1} (α := α i) (β := β i) (⇑(f i) : (a : α i) → β i)

Tactic:
classical exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_surjective
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → AddMonoidHom.{u_4, u_5} (α i) (β i)
x y : ⨁ (i : ι), α i
simp_rw simp_rw₁ :
  Eq (α := ⨁ (i : ι), β i) ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
      ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) ↔
    ∀ (i : ι),
      Eq.{u_5 + 1} (α := β i) ((f i : (a : α i) → β i) ((x : (a : ι) → α a) i) : β i)
        ((f i : (a : α i) → β i) ((y : (a : ι) → α a) i) : β i)
simp_rw₂ :
  (∀ (i : ι),
      (((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i) : (a : ι) → β a) i =
        (((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) : (a : ι) → β a) i) ↔
    ∀ (i : ι),
      Eq.{u_5 + 1} (α := β i) ((f i : (a : α i) → β i) ((x : (a : ι) → α a) i) : β i)
        ((f i : (a : α i) → β i) ((y : (a : ι) → α a) i) : β i)
⊢ Eq (α := ⨁ (i : ι), β i) ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i)
      ((map (α := α) (β := β) f : (a : ⨁ (i : ι), α i) → ⨁ (i : ι), β i) y : ⨁ (i : ι), β i) ↔
    ∀ (i : ι),
      Eq.{u_5 + 1} (α := β i) ((f i : (a : α i) → β i) ((x : (a : ι) → α a) i) : β i)
        ((f i : (a : α i) → β i) ((y : (a : ι) → α a) i) : β i)

Tactic:
simp_rw [DirectSum.ext_iff, map_apply]

Premises used: DirectSum.ext_iff, DirectSum.map_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι_1 : Type v
β : ι_1 → Type w
ι : Type u_1
inst : Fintype ι
G : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (G i)
g h : DirectSum ι G
x : ι
⊢ Equiv.toFun (DFinsupp.equivFunOnFintype (β := G)) (g + h) x =
    (Equiv.toFun (DFinsupp.equivFunOnFintype (β := G)) g + Equiv.toFun (DFinsupp.equivFunOnFintype (β := G)) h) x

Tactic:
simp only [DFinsupp.equivFunOnFintype, Equiv.toFun_as_coe, Equiv.coe_fn_mk, add_apply,
      Pi.add_apply]

Premises used: Equiv.toFun_as_coe, DFinsupp.equivFunOnFintype, Pi.add_apply, Equiv.coe_fn_mk, DirectSum.add_apply
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
x y : Decomposition ℳ
obtain :
  ∀ (decompose' : M → ⨁ (i : ι), ↥(ℳ i))
    (left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose')
    (xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'),
    { decompose' := decompose', left_inv := left_inv, right_inv := xr : Decomposition ℳ } = y
⊢ x = y

Tactic:
obtain ⟨_, _, xr⟩ := x
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
y : Decomposition ℳ
decompose' : M → ⨁ (i : ι), ↥(ℳ i)
left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
obtain :
  ∀ (decompose'_1 : M → ⨁ (i : ι), ↥(ℳ i))
    (yl : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1)
    (right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1),
    { decompose' := decompose', left_inv := left_inv, right_inv := xr : Decomposition ℳ } =
      { decompose' := decompose'_1, left_inv := yl, right_inv := right_inv }
⊢ { decompose' := decompose', left_inv := left_inv, right_inv := xr : Decomposition ℳ } = y

Tactic:
obtain ⟨_, yl, _⟩ := y
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
decompose' : M → ⨁ (i : ι), ↥(ℳ i)
left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
decompose'_1 : M → ⨁ (i : ι), ↥(ℳ i)
yl : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1
right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1
e_decompose' : decompose' = decompose'_1
⊢ { decompose' := decompose', left_inv := left_inv, right_inv := xr : Decomposition ℳ } =
    { decompose' := decompose'_1, left_inv := yl, right_inv := right_inv }

Tactic:
congr
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
decompose' : M → ⨁ (i : ι), ↥(ℳ i)
left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
decompose'_1 : M → ⨁ (i : ι), ↥(ℳ i)
yl : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1
right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1
⊢ decompose' = decompose'_1

Tactic:
Function.LeftInverse.eq_rightInverse xr yl

Premises used: Function.LeftInverse.eq_rightInverse
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
decompose' : M → ⨁ (i : ι), ↥(ℳ i)
left_inv : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'
decompose'_1 : M → ⨁ (i : ι), ↥(ℳ i)
yl : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1
right_inv : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) decompose'_1
⊢ decompose' = decompose'_1

Tactic:
exact Function.LeftInverse.eq_rightInverse xr yl

Premises used: Function.LeftInverse.eq_rightInverse
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
⊢ IsInternal ℳ

Tactic:
⟨Decomposition.right_inv.injective, Decomposition.left_inv.surjective⟩

Premises used: DirectSum.IsInternal, And.intro, Function.Bijective, Function.LeftInverse.surjective, DirectSum.Decomposition.left_inv, DirectSum.Decomposition.right_inv, Function.RightInverse.injective
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive (↑m : M)
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun (i : ι) ↦ { carrier := (↑(ℳ i) : Set M), add_mem' := ⋯, zero_mem' := ⋯ }
haveI : ∀ (t : Decomposition ℳ') (m : M), motive m
⊢ ∀ (m : M), motive m

Tactic:
haveI t : DirectSum.Decomposition ℳ' :=
    { decompose' := DirectSum.decompose ℳ
      left_inv := fun _ ↦ (decompose ℳ).left_inv _
      right_inv := fun _ ↦ (decompose ℳ).right_inv _ }
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive (↑m : M)
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun (i : ι) ↦ { carrier := (↑(ℳ i) : Set M), add_mem' := ⋯, zero_mem' := ⋯ }
t : Decomposition ℳ'
⊢ ∀ (m : M), m ∈ iSup ℳ'

Tactic:
have mem : ∀ m, m ∈ iSup ℳ' := fun _m ↦
    (DirectSum.IsInternal.addSubmonoid_iSup_eq_top ℳ' (Decomposition.isInternal ℳ')).symm ▸ trivial
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive (↑m : M)
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun (i : ι) ↦ { carrier := (↑(ℳ i) : Set M), add_mem' := ⋯, zero_mem' := ⋯ }
t : Decomposition ℳ'
mem : ∀ (m : M), m ∈ iSup ℳ'
⊢ ∀ (m : M), motive m

Tactic:
fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m)
    (fun i m h ↦ homogeneous ⟨m, h⟩) zero add

Premises used: Subtype.mk, AddSubmonoid.iSup_induction
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive (↑m : M)
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun (i : ι) ↦ { carrier := (↑(ℳ i) : Set M), add_mem' := ⋯, zero_mem' := ⋯ }
t : Decomposition ℳ'
mem : ∀ (m : M), m ∈ iSup ℳ'
⊢ ∀ (m : M), motive m

Tactic:
exact fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m)
    (fun i m h ↦ homogeneous ⟨m, h⟩) zero add

Premises used: Subtype.mk, AddSubmonoid.iSup_induction
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
⊢ Eq (α := M → ⨁ (i : ι), ↥(ℳ i)) (@decompose' _ _ _ inst _ _ _ _ _) (⇑(decompose ℳ) : (a : M) → ⨁ (i : ι), ↥(ℳ i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ (Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i)) x :
        ⨁ (i : ι), ↥(ℳ i)) =
    (↑x : M)

Tactic:
DirectSum.coeAddMonoidHom_of ℳ _ _

Premises used: Multiset.sum, Multiset.foldr, DirectSum.coeAddMonoidHom_of, List.foldr, Finset.sum, Trunc.lift
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
i : ι
x : ↥(ℳ i)
rw :
  Eq (α := ⨁ (i : ι), ↥(ℳ i))
    ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i))
        ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
          (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
              x :
            ⨁ (i : ι), ↥(ℳ i))) :
      ⨁ (i : ι), ↥(ℳ i))
    (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i)) x :
      ⨁ (i : ι), ↥(ℳ i))
rw₁ rw₂ :
  Eq (α := ⨁ (i : ι), ↥(ℳ i))
    (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i)) x :
      ⨁ (i : ι), ↥(ℳ i))
    (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i)) x :
      ⨁ (i : ι), ↥(ℳ i))
⊢ Eq (α := ⨁ (i : ι), ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) (↑x : M) : ⨁ (i : ι), ↥(ℳ i))
    (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i)) x :
      ⨁ (i : ι), ↥(ℳ i))

Tactic:
rw [← decompose_symm_of _, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, DirectSum.decompose_symm_of
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ Eq (α := ⨁ (i : ι), ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i))
    (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
        (Subtype.mk (p := fun (x : M) ↦ x ∈ ℳ i) x hx) :
      ⨁ (i : ι), ↥(ℳ i))

Tactic:
decompose_coe _ ⟨x, hx⟩

Premises used: Subtype.mk, DirectSum.decompose_coe
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
rw :
  (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
                (Subtype.mk (p := fun (x : M) ↦ x ∈ ℳ i) x hx) :
              ⨁ (i : ι), ↥(ℳ i)) :
            (a : ι) → ↥(ℳ a))
          i) :
      M) =
    x
rw₁ : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ ℳ i) x hx) : M) = x
rw₂ rw₃ : x = x
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) = x

Tactic:
rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

Premises used: Subtype.coe_mk, DirectSum.decompose_of_mem, DirectSum.of_eq_same
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x : M
i j : ι
hx : x ∈ ℳ i
hij : i ≠ j
rw :
  (↑(((((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
                (Subtype.mk (p := fun (x : M) ↦ x ∈ ℳ i) x hx) :
              ⨁ (i : ι), ↥(ℳ i)) :
            (a : ι) → ↥(ℳ a))
          j) :
      M) =
    0
rw₁ : Eq.{u_3 + 1} (α := M) (↑0 : M) 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) j) : M) = 0

Tactic:
rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij.symm, ZeroMemClass.coe_zero]

Premises used: DirectSum.decompose_of_mem, Ne.symm, ZeroMemClass.coe_zero, DirectSum.of_eq_of_ne
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : x ≠ 0
contrapose! : ∀ (hx : i ≠ j), x = 0
⊢ i = j

Tactic:
contrapose! hx
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : i ≠ j
rw : (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) j) : M) = 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) 0 0
⊢ x = 0

Tactic:
rw [← decompose_of_mem_same ℳ hxj, decompose_of_mem_ne ℳ hxi hx]

Premises used: DirectSum.decompose_of_mem_same, DirectSum.decompose_of_mem_ne
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
⊢ Eq (α := ⨁ (i : ι), ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) 0) 0

Tactic:
map_zero (decomposeAddEquiv ℳ)

Premises used: DirectSum.decomposeAddEquiv, map_zero
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
⊢ Eq.{u_3 + 1} (α := M) ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) 0 : M) (0 : M)

Tactic:
map_zero (decomposeAddEquiv ℳ).symm

Premises used: DirectSum.decomposeAddEquiv, map_zero, AddEquiv.symm
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x y : M
⊢ (decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) (x + y) =
    HAdd.hAdd (α := ⨁ (i : ι), ↥(ℳ i)) (β := ⨁ (i : ι), ↥(ℳ i))
      ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i))
      ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) y : ⨁ (i : ι), ↥(ℳ i))

Tactic:
map_add (decomposeAddEquiv ℳ) x y

Premises used: DirectSum.decomposeAddEquiv, map_add
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : SetLike σ M
inst_3 : AddSubmonoidClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x y : ⨁ (i : ι), ↥(ℳ i)
⊢ (Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) (x + y) =
    HAdd.hAdd (α := M) (β := M) ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) x : M)
      ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) y : M)

Tactic:
map_add (decomposeAddEquiv ℳ).symm x y

Premises used: DirectSum.decomposeAddEquiv, map_add, AddEquiv.symm