awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
let let₁ let₂ :
  Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
    (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
let₃ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N'),
    Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
      (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
let₄ let₅ :
  let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
  ∀ (h : IsInternal N')
    (hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)),
    Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
      (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
⊢ Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
    (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)
have let₆ : let N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι));
∀ (h : IsInternal N')
  (hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p))
  (_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)),
  Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
    (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f sorry) : R)
Tactic: classical
  let N' : s → Submodule R p := fun i ↦ (N i).comap p.subtype
  replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h
  have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'
  let e : (i : s) → N' i ≃ₗ[R] N i := fun ⟨i, hi⟩ ↦ (N i).comapSubtypeEquivOfLe (hp ▸ le_biSup N hi)
  have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm
  have _i2 : ∀ i, Module.Free R (N' i) := fun i ↦ Module.Free.of_equiv (e i).symm
  rw [trace_eq_sum_trace_restrict h hf', ← s.sum_coe_sort]
  have : ∀ i : s, f.restrict (hf i) = (e i).conj ((f.restrict hp').restrict (hf' i)) := fun _ ↦ rfl
  simp [this]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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)
f g : ⨁ (i : ι), M i
h : f = g
x : ι
⊢ Eq.{w + 1} (α := M x) ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) f : M x)
    ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) g : M x)
have rw : Eq.{w + 1} (α := M x) ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) g : M x)
  ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) g : M x)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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 : ι ≃ κ
i : ι
k : κ
hik : i = (e.symm : (a : κ) → ι) k
x : M i
y : M ((e.symm : (a : κ) → ι) k)
hxy : cast ⋯ x = y
⊢ 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 i : (a : M i) → ⨁ (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))
        y :
      ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
have subst : ∀ (x : M ((e.symm : (a : κ) → ι) k)),
  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 sorry x) :
      ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
Tactic: subst hik hxy
Cleared hypotheses: i, hik, x, y, hxy
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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 (α := ⨁ (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))
have 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 sorry x) :
          ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
        (a : κ) → M ((e.symm : (a : κ) → ι) a))
      j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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 : κ
⊢ (((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
have 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 sorry
  else 0)
  (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast sorry x) sorry else 0)
Tactic: simp_rw [lequivCongrLeft_apply, lof_eq_of, of_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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.{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)
have 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 sorry
    else 0)
    (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast sorry x) sorry else 0)
Tactic: by_cases eq : k = j
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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)
⊢ 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)
have 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 sorry
    else 0)
    (if h : k = j then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast sorry x) sorry else 0)
Tactic: by_cases eq : k = j
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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.{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)
have 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 sorry
  else 0)
  (if h : k = k then Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast sorry x) sorry else 0)
Tactic: subst eq
Cleared hypotheses: j, eq
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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))
    (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)
have pos : Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) k))
  (Eq.rec (motive := fun (x : ι) (x_1 : (e.symm : (a : κ) → ι) k = x) ↦ M x) x sorry : M ((e.symm : (a : κ) → ι) k))
  (Eq.rec (motive := fun (x : κ) (x_1 : k = x) ↦ M ((e.symm : (a : κ) → ι) x)) (cast sorry x) sorry :
    M ((e.symm : (a : κ) → ι) k))
Tactic: rw [dif_pos rfl, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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.{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)
have 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 sorry x) sorry else 0)
Tactic: rw [dif_neg (by aesop), dif_neg eq]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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)
⊢ 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)
have neg₁ : Eq.{w + 1} (α := M ((e.symm : (a : κ) → ι) j)) 0 0
Tactic: rw [dif_neg (by aesop), dif_neg eq]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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 (α := ⨁ (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)
have 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))
Tactic: rw [LinearEquiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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))
    (((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))
have 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))
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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) ((coeLinearMap A : (a : ⨁ (i : ι), ↥(A i)) → M) x : M)
    (DFinsupp.sum (β := fun (i : ι) ↦ ↥(A i)) x fun (i : ι) (x : ↥(A i)) ↦ (↑x : M) : M)
have 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)
Tactic: simp only [coeLinearMap, toModule, DFinsupp.lsum, LinearEquiv.coe_mk, LinearMap.coe_mk,
    AddHom.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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.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)
have 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))
Tactic: rw [DFinsupp.sumAddHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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)
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      i =
    x
have 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
Tactic: rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      i =
    x
have 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
Tactic: rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      i =
    x
have rw₂ : x = x
Tactic: rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
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)
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0
have 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
Tactic: rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_of_ne i j _ hij.symm]