awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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'
⊢ { decompose' := decompose', left_inv := left_inv, right_inv := xr : Decomposition ℳ } = y
have 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 }
Tactic: obtain ⟨_, yl, _⟩ := y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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', left_inv := left_inv, right_inv := xr : Decomposition ℳ } =
    { decompose' := decompose'_1, left_inv := yl, right_inv := right_inv }
have e_decompose' : decompose' = decompose'_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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' := ⋯ }
⊢ ∀ (m : M), motive m
have haveI : ∀ (t : Decomposition ℳ') (m : M), motive m
Tactic: haveI t : DirectSum.Decomposition ℳ' :=
    { decompose' := DirectSum.decompose ℳ
      left_inv := fun _ ↦ (decompose ℳ).left_inv _
      right_inv := fun _ ↦ (decompose ℳ).right_inv _ }
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (hypothesis)
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), motive m
have mem : ∀ (m : M), m ∈ iSup ℳ'
Tactic: have mem : ∀ m, m ∈ iSup ℳ' := fun _m ↦
    (DirectSum.IsInternal.addSubmonoid_iSup_eq_top ℳ' (Decomposition.isInternal ℳ')).symm ▸ trivial
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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)
⊢ 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))
have 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))
Tactic: rw [← decompose_symm_of _, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← decompose_symm_of _, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) = x
have 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
Tactic: rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) = x
have rw₁ : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ ℳ i) x hx) : M) = x
Tactic: rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) = x
have rw₂ : x = x
Tactic: rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) j) : M) = 0
have 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
Tactic: rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij.symm, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) j) : M) = 0
have rw₁ : Eq.{u_3 + 1} (α := M) (↑0 : M) 0
Tactic: rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij.symm, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) j) : M) = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij.symm, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ i = j
have contrapose! : ∀ (hx : i ≠ j), x = 0
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ x = 0
have rw : (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) j) : M) = 0
Tactic: rw [← decompose_of_mem_same ℳ hxj, decompose_of_mem_ne ℳ hxi hx]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ x = 0
have rw₁ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [← decompose_of_mem_same ℳ hxj, decompose_of_mem_ne ℳ hxi hx]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
| r
have 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)
Tactic: rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ ∑ 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
have 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)
Tactic: conv_rhs =>
    rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ 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)
have 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)))
Tactic: rw [decompose_symm_sum]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
have refine : ∀
  (hx :
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p),
  x ∈ p
Tactic: refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ x ∈ p
have 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
Tactic: rw [← DirectSum.sum_support_decompose ℳ x]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
have refine : ∀
  (hx :
    ∀ (i : ι), (↑((((decompose ℳ : (a : M) → ⨁ (i : ι), ↥(ℳ i)) x : ⨁ (i : ι), ↥(ℳ i)) : (a : ι) → ↥(ℳ a)) i) : M) ∈ p),
  x ∈ 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)
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
have 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
Tactic: classical
  refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩
  rw [← DirectSum.sum_support_decompose ℳ x]
  exact sum_mem (fun i _ ↦ hx i)
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
have refine : ∀ (m : M), m ∈ p ↔ m ∈ q
Tactic: refine SetLike.ext fun m ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ m ∈ p ↔ m ∈ q
have 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
Tactic: rw [AddSubmonoidClass.IsHomogeneous.mem_iff ℳ p hp,
    AddSubmonoidClass.IsHomogeneous.mem_iff ℳ q hq]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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 : ι
⊢ (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
have 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
Tactic: simp_rw [LinearMap.comp_assoc, decomposeLinearEquiv_symm_comp_lof ℳ i, h]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Decomposition (goal)
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
⊢ (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
have simp_rw₁ : f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
Tactic: simp_rw [LinearMap.comp_assoc, decomposeLinearEquiv_symm_comp_lof ℳ i, h]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Finsupp (goal)
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
⊢ 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)
have 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) sorry m) :
          ⨁ (x : ι), N) :
        (a : ι) → N)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Idempotents (goal)
Goal:
R : Type u_1
I : Type u_2
inst : Semiring R
inst_1 : DecidableEq I
V : I → Ideal R
inst_2 : Decomposition V
x : R
i : I
⊢ (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) =
    x * idempotent V i
have rw : (↑((((decompose V : (a : R) → ⨁ (i : I), ↥(V i)) x : ⨁ (i : I), ↥(V i)) : (a : I) → ↥(V a)) i) : R) = x • idempotent V i
Tactic: rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]