awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
w :
  ∀ (j : κ),
    (((lequivCongrLeft R (M := M) e : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
              ((lof R ι M ((e.symm : (a : κ) → ι) k) : (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
            ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k)) :
          (a : κ) → M ((e.symm : (a : κ) → ι) a))
        j =
      ((((lof.{u, u_1, w} R κ (fun (i : κ) ↦ M ((e.symm : (a : κ) → ι) i)) k :
                  M ((e.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
                (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
              (cast ⋯ x) :
            ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
          (a : κ) → M ((e.symm : (a : κ) → ι) a))
        j
⊢ Eq (α := ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
    ((lequivCongrLeft R (M := M) e : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
        ((lof R ι M ((e.symm : (a : κ) → ι) k) : (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
      ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
    (((lof.{u, u_1, w} R κ (fun (i : κ) ↦ M ((e.symm : (a : κ) → ι) i)) k :
            M ((e.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
          (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
        (cast ⋯ x) :
      ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))

Tactic:
ext j
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
j : κ
w :
  Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j))
    (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) j : ι) then
      Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
    else 0)
    (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ else 0)
⊢ (((lequivCongrLeft R (M := M) e : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
            ((lof R ι M ((e.symm : (a : κ) → ι) k) : (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
          ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k)) :
        (a : κ) → M ((e.symm : (a : κ) → ι) a))
      j =
    ((((lof.{u, u_1, w} R κ (fun (i : κ) ↦ M ((e.symm : (a : κ) → ι) i)) k :
                M ((e.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
              (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
            (cast ⋯ x) :
          ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
        (a : κ) → M ((e.symm : (a : κ) → ι) a))
      j

Tactic:
simp_rw [lequivCongrLeft_apply, lof_eq_of, of_apply]

Premises used: DirectSum.lequivCongrLeft_apply, DirectSum.lof_eq_of, DirectSum.of_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
j : κ
pos :
  ∀ (eq : k = j),
    Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j))
      (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) j : ι) then
        Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
      else 0)
      (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯
      else 0)
neg :
  ∀ (eq : ¬k = j),
    Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j))
      (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) j : ι) then
        Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
      else 0)
      (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯
      else 0)
⊢ Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j))
    (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) j : ι) then
      Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
    else 0)
    (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ else 0)

Tactic:
by_cases eq : k = j
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
j : κ
eq : k = j
pos :
  Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) k))
    (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) k : ι) then
      Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
    else 0)
    (if h : k = k then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ else 0)
⊢ Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j))
    (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) j : ι) then
      Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
    else 0)
    (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ else 0)

Tactic:
subst eq
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
pos :
  Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) k))
    (Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯ : M ((e.symm : (a : κ) → ι) k))
    (Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ :
      M ((e.symm : (a : κ) → ι) k))
⊢ Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) k))
    (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) k : ι) then
      Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
    else 0)
    (if h : k = k then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ else 0)

Tactic:
rw [dif_pos rfl, dif_pos rfl]

Premises used: dif_pos, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
⊢ Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) k))
    (Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯ : M ((e.symm : (a : κ) → ι) k))
    (Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ :
      M ((e.symm : (a : κ) → ι) k))

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
j : κ
eq : ¬k = j
⊢ ¬Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) j : ι)

Tactic:
aesop
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
k : κ
x : M ((e.symm : (a : κ) → ι) k)
j : κ
eq : ¬k = j
neg :
  Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j)) 0
    (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ else 0)
neg₁ neg₂ : Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j)) 0 0
⊢ Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j))
    (if h : Eq.{v + 1} (α := ι) ((e.symm : (a : κ) → ι) k : ι) ((e.symm : (a : κ) → ι) j : ι) then
      Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x ⋯
    else 0)
    (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast ⋯ x) ⋯ else 0)

Tactic:
rw [dif_neg (by aesop), dif_neg eq]

Premises used: dif_neg
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
h : ι ≃ κ
k : κ
x : M ((h.symm : (a : κ) → ι) k)
rw :
  Eq (α := ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    (((lof.{u, u_1, w} R κ (fun (k : κ) ↦ M ((h.symm : (a : κ) → ι) k)) k :
            M ((h.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i)) :
          (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
        x :
      ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
    ((lequivCongrLeft R (M := M) h : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
        ((lof R ι M ((h.symm : (a : κ) → ι) k) : (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
      ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
⊢ Eq (α := ⨁ (i : ι), M i)
    ((LinearEquiv.symm (lequivCongrLeft R (M := M) h) : (a : ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i)
        (((lof.{u, u_1, w} R κ (fun (k : κ) ↦ M ((h.symm : (a : κ) → ι) k)) k :
              M ((h.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i)) :
            (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
          x) :
      ⨁ (i : ι), M i)
    ((lof R ι M ((h.symm : (a : κ) → ι) k) : (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x : ⨁ (i : ι), M i)

Tactic:
rw [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
h : ι ≃ κ
k : κ
x : M ((h.symm : (a : κ) → ι) k)
symm :
  Eq (α := ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    ((lequivCongrLeft R (M := M) h : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
        ((lof R ι M ((h.symm : (a : κ) → ι) k) : (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
      ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    (((lof.{u, u_1, w} R κ (fun (k : κ) ↦ M ((h.symm : (a : κ) → ι) k)) k :
            M ((h.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i)) :
          (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
        x :
      ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
⊢ Eq (α := ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    (((lof.{u, u_1, w} R κ (fun (k : κ) ↦ M ((h.symm : (a : κ) → ι) k)) k :
            M ((h.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i)) :
          (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
        x :
      ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
    ((lequivCongrLeft R (M := M) h : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
        ((lof R ι M ((h.symm : (a : κ) → ι) k) : (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
      ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))

Tactic:
symm
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
h : ι ≃ κ
k : κ
x : M ((h.symm : (a : κ) → ι) k)
⊢ Eq (α := ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    ((lequivCongrLeft R (M := M) h : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
        ((lof R ι M ((h.symm : (a : κ) → ι) k) : (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
      ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    (((lof.{u, u_1, w} R κ (fun (k : κ) ↦ M ((h.symm : (a : κ) → ι) k)) k :
            M ((h.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i)) :
          (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
        x :
      ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))

Tactic:
lequivCongrLeft_lof _ rfl _ _ rfl

Premises used: DirectSum.lequivCongrLeft_lof, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
h : ι ≃ κ
k : κ
x : M ((h.symm : (a : κ) → ι) k)
⊢ Eq (α := ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    ((lequivCongrLeft R (M := M) h : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
        ((lof R ι M ((h.symm : (a : κ) → ι) k) : (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
      ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k))
    (((lof.{u, u_1, w} R κ (fun (k : κ) ↦ M ((h.symm : (a : κ) → ι) k)) k :
            M ((h.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i)) :
          (a : M ((h.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))
        x :
      ⨁ (i : κ), M ((h.symm : (a : κ) → ι) i))

Tactic:
exact lequivCongrLeft_lof _ rfl _ _ rfl

Premises used: DirectSum.lequivCongrLeft_lof, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst_5 : (i : ι) → (j : α i) → Module.{u, w} R (δ i j)
r : R
⊢ ∀ (f : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))),
    (r • f).sigmaCurry (α := α) (δ := δ) =
      HSMul.hSMul (β := Π₀ (i : ι) (j : α i), δ i j) r (f.sigmaCurry (α := α) (δ := δ))

Tactic:
DFinsupp.sigmaCurry_smul (δ := δ) r

Premises used: DFinsupp.sigmaCurry_smul
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst_5 : (i : ι) → (j : α i) → Module.{u, w} R (δ i j)
r : R
⊢ ∀ (x : ⨁ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))),
    ZeroHom.toFun
        (↑(sigmaCurry (α := α) (δ := δ)) :
          ZeroHom (⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) (⨁ (i : ι) (j : α i), δ i j))
        (r • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        (ZeroHom.toFun
          (↑(sigmaCurry (α := α) (δ := δ)) :
            ZeroHom (⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) (⨁ (i : ι) (j : α i), δ i j))
          x)

Tactic:
convert! DFinsupp.sigmaCurry_smul (δ := δ) r

Premises used: DFinsupp.sigmaCurry_smul
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst_3 : (i : ι) → (j : α i) → Module.{u, w} R (δ i j)
f : ⨁ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
i : ι
j : α i
⊢ ((((sigmaLcurry R (α := α) (δ := δ) : (a : ⨁ (i : (x : ι) × α x), δ 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 : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j)

Tactic:
sigmaCurry_apply f i j

Premises used: DirectSum.sigmaCurry_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst_3 : (i : ι) → (j : α i) → Module.{u, w} R (δ i j)
f : ⨁ (i : ι) (j : α i), δ i j
i : ι
j : α i
⊢ (((sigmaLuncurry R (α := α) (δ := δ) : (a : ⨁ (i : ι) (j : α i), δ i j) → ⨁ (i : (x : ι) × α x), δ i.fst i.snd) f :
          ⨁ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))) :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j) =
    ((f : (a : ι) → ⨁ (j : α a), δ a j) i : (a : α i) → δ i a) j

Tactic:
sigmaUncurry_apply f i j

Premises used: DirectSum.sigmaUncurry_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
inst_3 : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
simp :
  Eq (α := M)
    ((DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtype.toAddMonoidHom :
          (a : Π₀ (i : ι), ↥(A i)) → M)
        x :
      M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)
⊢ Eq (α := M) ((coeLinearMap 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 [coeLinearMap, toModule, DFinsupp.lsum, LinearEquiv.coe_mk, LinearMap.coe_mk,
    AddHom.coe_mk]

Premises used: LinearMap.coe_mk, LinearEquiv.coe_mk, DFinsupp.lsum, DirectSum.toModule, DirectSum.coeLinearMap, AddHom.coe_mk
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
inst_3 : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
rw :
  Eq (α := M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (x : ι) ↦ (⇑(A x).subtype.toAddMonoidHom : (a : ↥(A x)) → M))
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M))
⊢ Eq (α := M)
    ((DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(A i)) fun (i : ι) ↦ (A i).subtype.toAddMonoidHom :
          (a : Π₀ (i : ι), ↥(A i)) → M)
        x :
      M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)

Tactic:
rw [DFinsupp.sumAddHom_apply]

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
inst_3 : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ Eq (α := M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (x : ι) ↦ (⇑(A x).subtype.toAddMonoidHom : (a : ↥(A x)) → M))
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M))

Tactic:
simp only [LinearMap.toAddMonoidHom_coe, Submodule.coe_subtype]

Premises used: LinearMap.toAddMonoidHom_coe, Submodule.coe_subtype
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i : ι
x : ↥(A i)
⊢ (coeLinearMap 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 (β := fun i => A i) (fun i ↦ ((A i).subtype : A i →+ M)) i x

Premises used: Multiset.sum, Multiset.foldr, AddMonoidHomClass.toAddMonoidHom, Submodule.subtype, List.foldr, DirectSum.toAddMonoid_of, Finset.sum, Trunc.lift
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i : ι
x : ↥(A i)
⊢ (coeLinearMap A : (a : ⨁ (i : ι), ↥(A i)) → M)
      (((lof.{u, v, u_1} R ι (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →ₗ[R] ⨁ (i : ι), ↥(A i)) :
            (a : ↥(A i)) → ⨁ (i : ι), ↥(A i))
          x :
        ⨁ (i : ι), ↥(A i)) =
    (↑x : M)

Tactic:
coeLinearMap_of A i x

Premises used: DirectSum.coeLinearMap_of
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
⊢ (coeLinearMap A).range = ⨆ (i : ι), A i

Tactic:
(Submodule.iSup_eq_range_dfinsupp_lsum _).symm

Premises used: Submodule.iSup_eq_range_dfinsupp_lsum, DirectSum.toModule, DirectSum.coeLinearMap, Eq.symm, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
i : ι
x : ↥(A i)
rw :
  (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i))
            ((coeLinearMap 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))) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      i =
    x
rw₁ :
  ((((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))
      i =
    x
rw₂ rw₃ : x = x
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      i =
    x

Tactic:
rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_same]

Premises used: LinearEquiv.ofBijective_symm_apply_apply, DirectSum.coeLinearMap_of, DirectSum.of_eq_same
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
i j : ι
hij : i ≠ j
x : ↥(A i)
rw :
  (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i))
            ((coeLinearMap 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))) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0
rw₁ :
  ((((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 =
    0
rw₂ rw₃ : Eq.{u_1 + 1} (α := ↥(A j)) 0 0
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0

Tactic:
rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_of_ne i j _ hij.symm]

Premises used: LinearEquiv.ofBijective_symm_apply_apply, DirectSum.coeLinearMap_of, Ne.symm, DirectSum.of_eq_of_ne
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
i : ι
x : M
hx : x ∈ A i
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) x :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      i =
    Subtype.mk (p := fun (x : M) ↦ x ∈ A i) x hx

Tactic:
h.ofBijective_coeLinearMap_same ⟨x, hx⟩

Premises used: DirectSum.IsInternal.ofBijective_coeLinearMap_same, Subtype.mk