awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih :
  ∀ (hl : ∀ x ∈ tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < tail.length • m),
    (tail.prod : (a : ι) → ↥(A a)) n = 0
hl : ∀ x ∈ head :: tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < (head :: tail).length • m
⊢ ((head :: tail).prod : (a : ι) → ↥(A a)) n = 0
have cons : ∀ (hl : (∀ k < m, (head : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < m, (a : (a : ι) → ↥(A a)) k = 0),
  (head * tail.prod : (a : ι) → ↥(A a)) n = 0
Tactic: simp only [List.mem_cons, forall_eq_or_imp, List.length_cons, List.prod_cons] at hl hn ⊢
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih :
  ∀ (hl : ∀ x ∈ tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < tail.length • m),
    (tail.prod : (a : ι) → ↥(A a)) n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, (head : (a : ι) → ↥(A a)) k = 0) ∧ ∀ a ∈ tail, ∀ k < m, (a : (a : ι) → ↥(A a)) k = 0
⊢ (head * tail.prod : (a : ι) → ↥(A a)) n = 0
have cons : n < m + tail.length • m
Tactic: refine mul_apply_eq_zero hl.1 (ih hl.2) ?_
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
l : List (⨁ (i : ι), ↥(A i))
m : ι
hl : ∀ x ∈ l, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < l.length • m
⊢ (l.prod : (a : ι) → ↥(A a)) n = 0
have nil : ∀
  (hl :
    ∀ (x : ⨁ (i : ι), ↥(A i)),
      Membership.mem (γ := List (⨁ (i : ι), ↥(A i))) [] x → ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0)
  ⦃n : ι⦄ (hn : n < List.length (α := ⨁ (i : ι), ↥(A i)) [] • m),
  ((List.prod [] : ⨁ (i : ι), ↥(A i)) : (a : ι) → ↥(A a)) n = 0
Tactic: induction l generalizing n with
  | nil => simp at hn
  | cons head tail ih =>
    simp only [List.mem_cons, forall_eq_or_imp, List.length_cons, List.prod_cons] at hl hn ⊢
    refine mul_apply_eq_zero hl.1 (ih hl.2) ?_
    simpa [add_smul, add_comm m] using hn
Cleared hypotheses: l, hl, n, hn
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (goal)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : Semiring R
inst_5 : SetLike σ R
inst_6 : AddSubmonoidClass σ R
A : ι → σ
inst_7 : SetLike.GradedMonoid A
inst_8 : CanonicallyOrderedAdd ι
l : List (⨁ (i : ι), ↥(A i))
m : ι
hl : ∀ x ∈ l, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < l.length • m
nil :
  ∀
    (hl :
      ∀ (x : ⨁ (i : ι), ↥(A i)),
        Membership.mem (γ := List (⨁ (i : ι), ↥(A i))) [] x → ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0)
    ⦃n : ι⦄ (hn : n < List.length (α := ⨁ (i : ι), ↥(A i)) [] • m),
    ((List.prod [] : ⨁ (i : ι), ↥(A i)) : (a : ι) → ↥(A a)) n = 0
⊢ (l.prod : (a : ι) → ↥(A a)) n = 0
have cons : ∀ (head : ⨁ (i : ι), ↥(A i)) (tail : List (⨁ (i : ι), ↥(A i)))
  (ih :
    ∀ (hl : ∀ x ∈ tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < tail.length • m),
      (tail.prod : (a : ι) → ↥(A a)) n = 0)
  (hl : ∀ x ∈ head :: tail, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0) ⦃n : ι⦄ (hn : n < (head :: tail).length • m),
  ((head :: tail).prod : (a : ι) → ↥(A a)) n = 0
Tactic: induction l generalizing n with
  | nil => simp at hn
  | cons head tail ih =>
    simp only [List.mem_cons, forall_eq_or_imp, List.length_cons, List.prod_cons] at hl hn ⊢
    refine mul_apply_eq_zero hl.1 (ih hl.2) ?_
    simpa [add_smul, add_comm m] using hn
Cleared hypotheses: l, hl, n, hn
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (hypothesis)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : CommSemiring R
inst_6 : SetLike σ R
inst_7 : AddSubmonoidClass σ R
A : ι → σ
inst_8 : SetLike.GradedMonoid A
s : Multiset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < (Multiset.map Prod.snd s).sum
⊢ ((Multiset.map Prod.fst s).prod : (a : ι) → ↥(A a)) n = 0
have this : ((List.map Prod.fst s.toList).prod : (a : ι) → ↥(A a)) n = 0
Tactic: have := listProd_apply_eq_zero' (l := s.toList) (by simpa using hs)
    (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Internal (hypothesis)
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst : AddCommMonoid ι
inst_1 : LinearOrder ι
inst_2 : IsOrderedAddMonoid ι
inst_3 : DecidableEq ι
inst_4 : CanonicallyOrderedAdd ι
inst_5 : CommSemiring R
inst_6 : SetLike σ R
inst_7 : AddSubmonoidClass σ R
A : ι → σ
inst_8 : SetLike.GradedMonoid A
s : Multiset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < s.card • m
⊢ (s.prod : (a : ι) → ↥(A a)) n = 0
have this : (s.toList.prod : (a : ι) → ↥(A a)) n = 0
Tactic: have := listProd_apply_eq_zero (l := s.toList) (by simpa using hs)
    (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst_6 : (i : ι) → Fintype (κ₁ i)
inst_7 : ∀ (i : ι), Finite.{u_8 + 1} (κ₂ i)
inst_8 : (i : ι) → DecidableEq (κ₁ i)
inst_9 : Fintype ι
b₁ : (i : ι) → Basis.{u_7, u_4, u_5} (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis.{u_8, u_4, u_6} (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo (⇑f : (a : M₁) → M₂) (↑(N₁ i) : Set M₁) (↑(N₂ i) : Set M₂)
⊢ Eq (α := Matrix ((i : ι) × κ₂ i) ((i : ι) × κ₁ i) R)
    ((toMatrix (h₁.collectedBasis (α := κ₁) b₁) (h₂.collectedBasis (α := κ₂) b₂) :
          (a : M₁ →ₗ[R] M₂) → Matrix ((i : ι) × κ₂ i) ((i : ι) × κ₁ i) R)
        f :
      Matrix ((i : ι) × κ₂ i) ((i : ι) × κ₁ i) R)
    (Matrix.blockDiagonal' (m' := κ₂) (n' := κ₁) fun (i : ι) ↦
        (toMatrix (b₁ i) (b₂ i) : (a : ↥(N₁ i) →ₗ[R] ↥(N₂ i)) → Matrix (κ₂ i) (κ₁ i) R) (f.restrict ⋯) :
      Matrix ((i : ι) × κ₂ i) ((i : ι) × κ₁ i) R)
have a : ∀ (i : ι) (snd : κ₂ i) (j : ι) (snd_1 : κ₁ j),
  Eq.{u_4 + 1} (α := R)
    ((toMatrix (h₁.collectedBasis (α := κ₁) b₁) (h₂.collectedBasis (α := κ₂) b₂) :
          (a : M₁ →ₗ[R] M₂) → Matrix ((i : ι) × κ₂ i) ((i : ι) × κ₁ i) R)
        f (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
      R)
    (Matrix.blockDiagonal' (m' := κ₂) (n' := κ₁)
        (fun (i : ι) ↦ (toMatrix (b₁ i) (b₂ i) : (a : ↥(N₁ i) →ₗ[R] ↥(N₂ i)) → Matrix (κ₂ i) (κ₁ i) R) (f.restrict sorry))
        (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
      R)
Tactic: ext ⟨i, _⟩ ⟨j, _⟩
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst_6 : (i : ι) → Fintype (κ₁ i)
inst_7 : ∀ (i : ι), Finite.{u_8 + 1} (κ₂ i)
inst_8 : (i : ι) → DecidableEq (κ₁ i)
inst_9 : Fintype ι
b₁ : (i : ι) → Basis.{u_7, u_4, u_5} (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis.{u_8, u_4, u_6} (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo (⇑f : (a : M₁) → M₂) (↑(N₁ i) : Set M₁) (↑(N₂ i) : Set M₂)
i : ι
snd : κ₂ i
j : ι
snd_1 : κ₁ j
⊢ Eq.{u_4 + 1} (α := R)
    ((toMatrix (h₁.collectedBasis (α := κ₁) b₁) (h₂.collectedBasis (α := κ₂) b₂) :
          (a : M₁ →ₗ[R] M₂) → Matrix ((i : ι) × κ₂ i) ((i : ι) × κ₁ i) R)
        f (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
      R)
    (Matrix.blockDiagonal' (m' := κ₂) (n' := κ₁)
        (fun (i : ι) ↦ (toMatrix (b₁ i) (b₂ i) : (a : ↥(N₁ i) →ₗ[R] ↥(N₂ i)) → Matrix (κ₂ i) (κ₁ i) R) (f.restrict ⋯))
        (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
      R)
have a : Eq.{u_4 + 1} (α := R)
  (((((h₂.collectedBasis (α := κ₂) b₂).repr : (a : M₂) → (i : ι) × κ₂ i →₀ R)
            ((f : (a : M₁) → M₂)
              ((h₁.collectedBasis (α := κ₁) b₁ : (a : (i : ι) × κ₁ i) → M₁)
                  (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
                M₁)) :
          (i : ι) × κ₂ i →₀ R) :
        (a : (i : ι) × κ₂ i) → R)
      (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) :
    R)
  (if h : i = j then
      ((((b₂ i).repr : (a : ↥(N₂ i)) → κ₂ i →₀ R)
              (((f.restrict sorry : LinearMap.{u_4, u_4, u_5, u_6} (RingHom.id R) ↥(N₁ i) ↥(N₂ i)) :
                  (a : ↥(N₁ i)) → ↥(N₂ i))
                ((b₁ i : (a : κ₁ i) → ↥(N₁ i)) (cast sorry snd_1))) :
            Finsupp.{u_8, u_4} (κ₂ i) R) :
          (a : κ₂ i) → R)
        snd
    else 0 :
    R)
Tactic: simp only [toMatrix_apply, Matrix.blockDiagonal'_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst_6 : (i : ι) → Fintype (κ₁ i)
inst_7 : ∀ (i : ι), Finite.{u_8 + 1} (κ₂ i)
inst_8 : (i : ι) → DecidableEq (κ₁ i)
inst_9 : Fintype ι
b₁ : (i : ι) → Basis.{u_7, u_4, u_5} (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis.{u_8, u_4, u_6} (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo (⇑f : (a : M₁) → M₂) (↑(N₁ i) : Set M₁) (↑(N₂ i) : Set M₂)
i : ι
snd : κ₂ i
j : ι
snd_1 : κ₁ j
⊢ Eq.{u_4 + 1} (α := R)
    (((((h₂.collectedBasis (α := κ₂) b₂).repr : (a : M₂) → (i : ι) × κ₂ i →₀ R)
              ((f : (a : M₁) → M₂)
                ((h₁.collectedBasis (α := κ₁) b₁ : (a : (i : ι) × κ₁ i) → M₁)
                    (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
                  M₁)) :
            (i : ι) × κ₂ i →₀ R) :
          (a : (i : ι) × κ₂ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) :
      R)
    (if h : i = j then
        ((((b₂ i).repr : (a : ↥(N₂ i)) → κ₂ i →₀ R)
                (((f.restrict ⋯ : LinearMap.{u_4, u_4, u_5, u_6} (RingHom.id R) ↥(N₁ i) ↥(N₂ i)) :
                    (a : ↥(N₁ i)) → ↥(N₂ i))
                  ((b₁ i : (a : κ₁ i) → ↥(N₁ i)) (cast ⋯ snd_1))) :
              Finsupp.{u_8, u_4} (κ₂ i) R) :
            (a : κ₂ i) → R)
          snd
      else 0 :
      R)
have a : ∀ (snd_2 : κ₁ i),
  Eq.{u_4 + 1} (α := R)
    (((((h₂.collectedBasis (α := κ₂) b₂).repr : (a : M₂) → (i : ι) × κ₂ i →₀ R)
              ((f : (a : M₁) → M₂)
                ((h₁.collectedBasis (α := κ₁) b₁ : (a : (i : ι) × κ₁ i) → M₁)
                    (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) i snd_2) :
                  M₁)) :
            (i : ι) × κ₂ i →₀ R) :
          (a : (i : ι) × κ₂ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) :
      R)
    (if h : i = i then
        ((((b₂ i).repr : (a : ↥(N₂ i)) → κ₂ i →₀ R)
                (((f.restrict sorry : LinearMap.{u_4, u_4, u_5, u_6} (RingHom.id R) ↥(N₁ i) ↥(N₂ i)) :
                    (a : ↥(N₁ i)) → ↥(N₂ i))
                  ((b₁ i : (a : κ₁ i) → ↥(N₁ i)) (cast sorry snd_2))) :
              Finsupp.{u_8, u_4} (κ₂ i) R) :
            (a : κ₂ i) → R)
          snd
      else 0 :
      R)
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: j, snd_1
-- 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 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
⊢ Eq (α := (i : (i : ↥s) × κ (↑i : ι)) → R)
    (Matrix.diag
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f))
    0
have h₁ : ∀ (i : ↥s) (k : κ (↑i : ι)),
  Eq.{u_2 + 1} (α := R)
    (Matrix.diag (n := (i : ↥s) × κ (↑i : ι))
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f)
      (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k))
    (0 (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k))
Tactic: ext ⟨i, k⟩
-- 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 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
⊢ Eq.{u_2 + 1} (α := R)
    (Matrix.diag (n := (i : ↥s) × κ (↑i : ι))
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f)
      (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k))
    (0 (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k))
have h₁ : Eq.{u_2 + 1} (α := R)
  (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
            ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
          (i : ↥s) × κ (↑i : ι) →₀ R) :
        (a : (i : ↥s) × κ (↑i : ι)) → R)
      (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
    R)
  (0 : R)
Tactic: simp only [Matrix.diag_apply, Pi.zero_apply, toMatrix_apply, IsInternal.collectedBasis_coe]
-- 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 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)
have pos : ∀ (hi : σ (↑i : ι) ∈ s),
  Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)
Tactic: by_cases hi : σ i ∈ s
-- 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 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
pos :
  ∀ (hi : σ (↑i : ι) ∈ s),
    Eq.{u_2 + 1} (α := R)
      (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
                ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
              (i : ↥s) × κ (↑i : ι) →₀ R) :
            (a : (i : ↥s) × κ (↑i : ι)) → R)
          (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
        R)
      (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)
have neg : ∀ (hi : σ (↑i : ι) ∉ s),
  Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)
Tactic: by_cases hi : σ i ∈ s
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.LinearMap (hypothesis)
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 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
hi : σ (↑i : ι) ∈ s
j : ↥s := Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (σ (↑i : ι)) hi
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)
have hσ₁ : j ≠ i
Tactic: replace hσ : j ≠ i := fun hij ↦ hσ i <| Subtype.ext_iff.mp hij
Cleared hypotheses: hσ
-- 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 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
hi : σ (↑i : ι) ∉ s
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)
have neg : Eq (α := M) ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M) : M) (0 : M)
Tactic: suffices f (b i k) = 0 by simp [this]
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
b : (i : ι) → Basis.{u_3, u_2, u_3} (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun (i : ι) ↦ Free.chooseBasis R ↥(N i)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯) : R)
have simp_rw : Eq.{u_2 + 1} (α := R)
  (Matrix.trace (n := (i : ι) × Free.ChooseBasisIndex R ↥(N i))
    ((toMatrix (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b)
          (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b) :
        (a : M →ₗ[R] M) →
          Matrix ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) R)
      f))
  (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict sorry))
Tactic: simp_rw [trace_eq_matrix_trace R (h.collectedBasis b),
    toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf, Matrix.trace_blockDiagonal',
    ← trace_eq_matrix_trace]
-- 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 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
b : (i : ι) → Basis.{u_3, u_2, u_3} (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun (i : ι) ↦ Free.chooseBasis R ↥(N i)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ι) × Free.ChooseBasisIndex R ↥(N i))
      ((toMatrix (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b)
            (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b) :
          (a : M →ₗ[R] M) →
            Matrix ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) R)
        f))
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯))
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯) : R)
have simp_rw₁ : Eq.{u_2 + 1} (α := R)
  (Matrix.trace (n := (i : ι) × Free.ChooseBasisIndex R ↥(N i))
    (Matrix.blockDiagonal' (m' := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) (n' := fun (i : ι) ↦
      Free.ChooseBasisIndex R ↥(N i)) fun (i : ι) ↦
      (toMatrix (b i) (b i) :
          (a : ↥(N i) →ₗ[R] ↥(N i)) → Matrix (Free.ChooseBasisIndex R ↥(N i)) (Free.ChooseBasisIndex R ↥(N i)) R)
        (f.restrict sorry)))
  (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict sorry))
Tactic: simp_rw [trace_eq_matrix_trace R (h.collectedBasis b),
    toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf, Matrix.trace_blockDiagonal',
    ← trace_eq_matrix_trace]