awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Internal
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
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
⊢ (l.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

Premises used: List.length_cons, forall_eq_or_imp, add_comm, add_smul, List.mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.DirectSum.Internal
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
⊢ ∀ xn ∈ s.toList, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0

Tactic:
simpa using hs
-- Module: Mathlib.Algebra.DirectSum.Internal
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
⊢ n < (List.map Prod.snd s.toList).sum

Tactic:
simpa [← Multiset.sum_coe, ← Multiset.map_coe]

Premises used: Multiset.sum_coe, Multiset.map_coe
-- Module: Mathlib.Algebra.DirectSum.Internal
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
⊢ ((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])
-- Module: Mathlib.Algebra.DirectSum.Internal
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
this : ((List.map Prod.fst s.toList).prod : (a : ι) → ↥(A a)) n = 0
⊢ ((Multiset.map Prod.fst s).prod : (a : ι) → ↥(A a)) n = 0

Tactic:
simpa [← Multiset.prod_coe, ← Multiset.map_coe]

Premises used: Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.DirectSum.Internal
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
⊢ ∀ x ∈ s.toList, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0

Tactic:
simpa using hs
-- Module: Mathlib.Algebra.DirectSum.Internal
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
⊢ n < s.toList.length • m

Tactic:
simpa [← Multiset.sum_coe, ← Multiset.map_coe]

Premises used: Multiset.sum_coe, Multiset.map_coe
-- Module: Mathlib.Algebra.DirectSum.Internal
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.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])
-- Module: Mathlib.Algebra.DirectSum.Internal
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
this : (s.toList.prod : (a : ι) → ↥(A a)) n = 0
⊢ (s.prod : (a : ι) → ↥(A a)) n = 0

Tactic:
simpa [← Multiset.prod_coe, ← Multiset.map_coe]

Premises used: Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.DirectSum.Internal
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 : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ ∀ xn ∈ s.toList, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0

Tactic:
simpa using hs
-- Module: Mathlib.Algebra.DirectSum.Internal
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 : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ n < (List.map Prod.snd s.toList).sum

Tactic:
simpa
-- Module: Mathlib.Algebra.DirectSum.Internal
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 : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, (xn.1 : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ ((∏ xn ∈ s, xn.1 : ⨁ (i : ι), ↥(A i)) : (a : ι) → ↥(A a)) n = 0

Tactic:
simpa using listProd_apply_eq_zero' (l := s.toList) (by simpa using hs) (by simpa)

Premises used: listProd_apply_eq_zero'
-- Module: Mathlib.Algebra.DirectSum.Internal
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 : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < s.card • m
⊢ ∀ x ∈ s.toList, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0

Tactic:
simpa using hs
-- Module: Mathlib.Algebra.DirectSum.Internal
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 : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < s.card • m
⊢ n < s.toList.length • m

Tactic:
simpa
-- Module: Mathlib.Algebra.DirectSum.Internal
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 : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, (x : (a : ι) → ↥(A a)) k = 0
n : ι
hn : n < s.card • m
⊢ ((∏ x ∈ s, x : ⨁ (i : ι), ↥(A i)) : (a : ι) → ↥(A a)) n = 0

Tactic:
simpa using listProd_apply_eq_zero (l := s.toList) (by simpa using hs) (by simpa)

Premises used: listProd_apply_eq_zero
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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₂)
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 ⋯))
          (Sigma.mk (β := fun (i : ι) ↦ κ₂ i) i snd) (Sigma.mk (β := fun (i : ι) ↦ κ₁ i) j snd_1) :
        R)
⊢ 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)

Tactic:
ext ⟨i, _⟩ ⟨j, _⟩
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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
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 ⋯ : 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)
⊢ 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)

Tactic:
simp only [toMatrix_apply, Matrix.blockDiagonal'_apply]

Premises used: Matrix.blockDiagonal'_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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
snd_1 : κ₁ 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_1) :
                  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 ⋯ : 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)

Tactic:
simp [h₂.collectedBasis_repr_of_mem _ (hf _ (Subtype.mem _)), restrict_apply]

Premises used: Subtype.mem, DirectSum.IsInternal.collectedBasis_repr_of_mem, LinearMap.restrict_apply
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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
hij : i ≠ 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)

Tactic:
simp [hij, h₂.collectedBasis_repr_of_mem_ne _ hij.symm (hf _ (Subtype.mem _))]

Premises used: Ne.symm, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, Subtype.mem
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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 = ⊥
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))
⊢ 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

Tactic:
ext ⟨i, k⟩
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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 : ι)
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)
⊢ 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:
simp only [Matrix.diag_apply, Pi.zero_apply, toMatrix_apply, IsInternal.collectedBasis_coe]

Premises used: DirectSum.IsInternal.collectedBasis_coe, Pi.zero_apply, Matrix.diag_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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)
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)
⊢ 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

Premises used: Subtype.val
-- Module: Mathlib.Algebra.DirectSum.LinearMap
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
⊢ j ≠ i

Tactic:
replace hσ : j ≠ i := fun hij ↦ hσ i <| Subtype.ext_iff.mp hij