awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℳ
ι' : Type u_5
s : Finset ι'
f : ι' → M
⊢ Eq (α := ⨁ (i : ι), ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) (∑ i ∈ s, f i))
    (∑ i ∈ s, (decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) (f i))

Tactic:
map_sum (decomposeAddEquiv ℳ) f s

Premises used: DirectSum.decomposeAddEquiv, map_sum
-- 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 ℳ
ι' : Type u_5
s : Finset ι'
f : ι' → ⨁ (i : ι), ↥(ℳ i)
⊢ Eq.{u_3 + 1} (α := M) ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) (∑ i ∈ s, f i) : M)
    (∑ i ∈ s, (Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) (f i) : M)

Tactic:
map_sum (decomposeAddEquiv ℳ).symm f s

Premises used: DirectSum.decomposeAddEquiv, map_sum, 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 ℳ
inst_5 : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
rw :
  ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
      (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
        ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
          ((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i)) :
    M)
| r

Tactic:
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]

Premises used: Equiv.symm_apply_apply, DFunLike.coe, DirectSum.sum_support_of, DirectSum.decompose
-- 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 ℳ
inst_5 : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
conv_rhs :
  Eq.{u_3 + 1} (α := M)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
        (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) :
      M)
    ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
        (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
          ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
            ((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i)) :
      M)
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) =
    r

Tactic:
conv_rhs =>
    rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]

Premises used: Equiv.symm_apply_apply, DFunLike.coe, DirectSum.sum_support_of, DirectSum.decompose
-- 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 ℳ
inst_5 : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
rw :
  Eq.{u_3 + 1} (α := M)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
      (Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
            ((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) :
          ⨁ (i : ι), ↥(ℳ i)))
⊢ Eq.{u_3 + 1} (α := M)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
        (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) :
      M)
    ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
        (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
          ((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
            ((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i)) :
      M)

Tactic:
rw [decompose_symm_sum]

Premises used: DirectSum.decompose_symm_sum
-- 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 ℳ
inst_5 : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
simp_rw simp_rw₁ :
  Eq.{u_3 + 1} (α := M)
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) x) : M))
    (∑ x ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
      (Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) x : ↥(ℳ x) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ x)) → ⨁ (i : ι), ↥(ℳ i))
            ((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) x) :
          ⨁ (i : ι), ↥(ℳ i)))
⊢ Eq.{u_3 + 1} (α := M)
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M))
    (∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r),
      (Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →+ ⨁ (i : ι), ↥(ℳ i)) : (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
            ((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) r : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) :
          ⨁ (i : ι), ↥(ℳ i)))

Tactic:
simp_rw [decompose_symm_of]

Premises used: 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
⊢ x ∈ p ↔
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p

Tactic:
⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩

Premises used: Iff.intro
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
refine :
  ∀
    (hx :
      ∀ (i : ι),
        (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p),
    x ∈ p
⊢ x ∈ p ↔
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p

Tactic:
refine ⟨fun hx i ↦ hp i hx, fun 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p
rw :
  ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈
    p
⊢ x ∈ p

Tactic:
rw [← DirectSum.sum_support_decompose ℳ x]

Premises used: DirectSum.sum_support_decompose
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈
    p

Tactic:
sum_mem (fun i _ ↦ hx i)

Premises used: sum_mem
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x),
      (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈
    p

Tactic:
exact sum_mem (fun i _ ↦ hx i)

Premises used: sum_mem
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
refine :
  ∀
    (hx :
      ∀ (i : ι),
        (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p),
    x ∈ p
refine₁ :
  ∀
    (hx :
      ∀ (i : ι),
        (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p),
    ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x),
        (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈
      p
⊢ x ∈ p ↔
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p

Tactic:
classical
  refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩
  rw [← DirectSum.sum_support_decompose ℳ x]
  exact sum_mem (fun i _ ↦ hx i)
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
⊢ p = q

Tactic:
SetLike.ext fun m ↦ ?_

Premises used: SetLike.ext
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
refine : ∀ (m : M), m ∈ p ↔ m ∈ q
⊢ p = q

Tactic:
refine SetLike.ext fun m ↦ ?_

Premises used: SetLike.ext
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
m : M
rw :
  (∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p) ↔
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ q
⊢ m ∈ p ↔ m ∈ q

Tactic:
rw [AddSubmonoidClass.IsHomogeneous.mem_iff ℳ p hp,
    AddSubmonoidClass.IsHomogeneous.mem_iff ℳ q hq]

Premises used: DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
m : M
⊢ (∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p) ↔
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ q

Tactic:
forall_congr' fun i ↦ hpq i _ (decompose ℳ _ i).2

Premises used: forall_congr', Subtype.val, DFunLike.coe, Subtype.property, DirectSum.decompose
-- 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 ℳ
P : Type u_5
inst_5 : SetLike P M
inst_6 : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
m : M
⊢ (∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p) ↔
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ q

Tactic:
exact forall_congr' fun i ↦ hpq i _ (decompose ℳ _ i).2

Premises used: forall_congr', Subtype.val, DFunLike.coe, Subtype.property, DirectSum.decompose
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddCommGroup M
inst_2 : SetLike σ M
inst_3 : AddSubgroupClass σ M
ℳ : ι → σ
inst_4 : Decomposition ℳ
x : M
⊢ Eq (α := ⨁ (i : ι), ↥(ℳ i)) ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) (-x) : ⨁ (i : ι), ↥(ℳ i))
    (-(decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i))

Tactic:
map_neg (decomposeAddEquiv ℳ) x

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

Tactic:
map_neg (decomposeAddEquiv ℳ).symm x

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

Tactic:
map_sub (decomposeAddEquiv ℳ) x y

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

Tactic:
map_sub (decomposeAddEquiv ℳ).symm x y

Premises used: map_sub, DirectSum.decomposeAddEquiv, AddEquiv.symm
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : Decomposition ℳ
m : M
⊢ Eq (α := ⨁ (i : ι), ↥(ℳ i)) ((decomposeLinearEquiv ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i))
    ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) m : ⨁ (i : ι), ↥(ℳ i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : Decomposition ℳ
m : ⨁ (i : ι), ↥(ℳ i)
⊢ Eq.{u_3 + 1} (α := M) (((decomposeLinearEquiv ℳ).symm : (a : ⨁ (i : ι), ↥(ℳ i)) → M) m : M)
    ((Equiv.symm (decompose ℳ) : (a : ⨁ (i : ι), ↥(ℳ i)) → M) m : M)

Tactic:
rfl

Premises used: rfl, Trunc.lift
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : Decomposition ℳ
r : R
x : M
⊢ (decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) (r • x) =
    HSMul.hSMul (β := ⨁ (i : ι), ↥(ℳ i)) r ((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i))

Tactic:
map_smul (decomposeLinearEquiv ℳ) r x

Premises used: DirectSum.decomposeLinearEquiv, map_smul
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : Decomposition ℳ
i : ι
⊢ (↑(decomposeLinearEquiv ℳ).symm : (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] M) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (x : ι) ↦ ↥(ℳ x)) i =
    (ℳ i).subtype

Tactic:
LinearMap.ext <| decompose_symm_of _

Premises used: LinearMap.ext, DirectSum.decompose_symm_of
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ ((decomposeLinearEquiv ℳ).symm : (a : ⨁ (i : ι), ↥(ℳ i)) → M)
      (((lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(ℳ i)) :
            (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
          x :
        ⨁ (i : ι), ↥(ℳ i)) =
    (↑x : M)

Tactic:
congr($(decomposeLinearEquiv_symm_comp_lof ℳ i) x)

Premises used: congrArg, id, DirectSum.decomposeLinearEquiv_symm_comp_lof, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ Eq (α := ⨁ (i : ι), ↥(ℳ i)) ((decomposeLinearEquiv ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) (↑x : M) : ⨁ (i : ι), ↥(ℳ i))
    (((lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i : ↥(ℳ i) →ₗ[R] ⨁ (i : ι), ↥(ℳ i)) :
          (a : ↥(ℳ i)) → ⨁ (i : ι), ↥(ℳ i))
        x :
      ⨁ (i : ι), ↥(ℳ i))

Tactic:
(LinearEquiv.eq_symm_apply _).mp (decomposeLinearEquiv_symm_lof ..).symm

Premises used: LinearEquiv.eq_symm_apply, Iff.mp, DirectSum.decomposeLinearEquiv_symm_lof, Eq.symm
-- Module: Mathlib.Algebra.DirectSum.Decomposition
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ℳ : ι → Submodule R M
inst_4 : Decomposition ℳ
N : Type u_5
inst_5 : AddCommMonoid N
inst_6 : Module R N
f g : M →ₗ[R] N
h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
i : ι
simp_rw :
  f ∘ₗ
      (↑(decomposeLinearEquiv ℳ).symm : (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] M) ∘ₗ
        lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i =
    g ∘ₗ
      (↑(decomposeLinearEquiv ℳ).symm : (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] M) ∘ₗ lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i
simp_rw₁ : f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
⊢ (f ∘ₗ (↑(decomposeLinearEquiv ℳ).symm : (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] M)) ∘ₗ
      lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i =
    (g ∘ₗ (↑(decomposeLinearEquiv ℳ).symm : (⨁ (i : ι), ↥(ℳ i)) →ₗ[R] M)) ∘ₗ
      lof.{u_2, u_1, u_3} R ι (fun (i : ι) ↦ ↥(ℳ i)) i

Tactic:
simp_rw [LinearMap.comp_assoc, decomposeLinearEquiv_symm_comp_lof ℳ i, h]

Premises used: LinearMap.comp_assoc, DirectSum.decomposeLinearEquiv_symm_comp_lof
-- Module: Mathlib.Algebra.DirectSum.Finsupp
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : DecidableEq ι
i : ι
m : M
⊢ Eq (α := ⨁ (x : ι), M)
    ((finsuppLEquivDirectSum R M ι : (a : ι →₀ M) → ⨁ (x : ι), M) (Finsupp.single i m) : ⨁ (x : ι), M)
    (((lof.{u, u_1, v} R ι (fun (i : ι) ↦ M) i : M →ₗ[R] ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) m : ⨁ (i : ι), M)

Tactic:
Finsupp.toDFinsupp_single i m

Premises used: DFinsupp.single, Finsupp.toDFinsupp, Finsupp.toDFinsupp_single, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Finsupp
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : DecidableEq ι
m : ι →₀ M
i : ι
⊢ (((finsuppLEquivDirectSum R M ι : (a : ι →₀ M) → ⨁ (x : ι), M) m : ⨁ (x : ι), M) : (a : ι) → M) i =
    (m : (a : ι) → M) i

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Finsupp
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : DecidableEq ι
i : ι
m : M
⊢ Eq (α := ι →₀ M)
    ((LinearEquiv.symm (finsuppLEquivDirectSum R M ι) : (a : ⨁ (x : ι), M) → ι →₀ M)
        (((lof.{u, u_1, v} R ι (fun (x : ι) ↦ M) i : M →ₗ[R] ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) m) :
      ι →₀ M)
    (Finsupp.single i m : ι →₀ M)

Tactic:
letI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
  DFinsupp.toFinsupp_single i m

Premises used: DFinsupp.single, DFinsupp.toFinsupp_single, DFinsupp.toFinsupp
-- Module: Mathlib.Algebra.DirectSum.Finsupp
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : DecidableEq ι
N : Type u_2
inst_4 : AddCommMonoid N
inst_5 : Module R N
ε : M →ₗ[R] N
m : ι →₀ M
w :
  ∀ (i : ι),
    (((lmap (M := fun (x : ι) ↦ M) (N := fun (x : ι) ↦ N) fun (x : ι) ↦ ε : (a : ⨁ (i : ι), M) → ⨁ (i : ι), N)
              ((finsuppLEquivDirectSum R M ι : (a : ι →₀ M) → ⨁ (x : ι), M) m) :
            ⨁ (i : ι), N) :
          (a : ι) → N)
        i =
      (((finsuppLEquivDirectSum R N ι : (a : ι →₀ N) → ⨁ (x : ι), N) (Finsupp.mapRange (⇑ε : (a : M) → N) ⋯ m) :
            ⨁ (x : ι), N) :
          (a : ι) → N)
        i
⊢ Eq (α := ⨁ (i : ι), N)
    ((lmap (M := fun (x : ι) ↦ M) (N := fun (x : ι) ↦ N) fun (x : ι) ↦ ε : (a : ⨁ (i : ι), M) → ⨁ (i : ι), N)
        ((finsuppLEquivDirectSum R M ι : (a : ι →₀ M) → ⨁ (x : ι), M) m) :
      ⨁ (i : ι), N)
    ((finsuppLEquivDirectSum R N ι : (a : ι →₀ N) → ⨁ (x : ι), N) (Finsupp.mapRange (⇑ε : (a : M) → N) ⋯ m) :
      ⨁ (x : ι), N)

Tactic:
ext i