-- Mathlib/Data/Matrix/Basis.lean
theorem mem_range_scalar_of_commute_stdBasisMatrix {M : Matrix n n α}
    (hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M) :
    M ∈ Set.range (Matrix.scalar n)

Proof state:
case inr.intro.inl.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Tactic:
exact diag_eq_of_commute_stdBasisMatrix (hM hij)

Result:
no goals

Proof state:
case inr.intro.inr.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
hij : i ≠ j
⊢ 0 = M j k

Tactic:
rw [row_eq_zero_of_commute_stdBasisMatrix (hM hij) hkl.symm]

Result:
no goals

Proof state:
case inr.intro.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
⊢ diagonal (fun x => M i i) j k = M j k

Tactic:
rw [diagonal_apply_ne _ hkl]

Result:
case inr.intro.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
⊢ 0 = M j k

Proof state:
case inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : IsEmpty n
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
exact ⟨0, Subsingleton.elim _ _⟩

Result:
no goals

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
cases isEmpty_or_nonempty n

Result:
case inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : IsEmpty n
⊢ M ∈ Set.range ⇑(scalar n)

case inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
⊢ M ∈ Set.range ⇑(scalar n)

Proof state:
case inr.intro
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
⊢ (scalar n) (M i i) j k = M j k

Tactic:
simp only [scalar_apply]

Result:
case inr.intro
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
⊢ diagonal (fun x => M i i) j k = M j k

Proof state:
case inr.intro.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j : n
⊢ M i i = M j j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case inr.intro.inl.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i : n
⊢ M i i = M i i

case inr.intro.inl.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Proof state:
case inr.intro.inr.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i k : n
hkl : i ≠ k
⊢ 0 = M i k

Tactic:
rw [col_eq_zero_of_commute_stdBasisMatrix (hM hkl.symm) hkl]

Result:
no goals

Proof state:
case inr.intro.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
⊢ 0 = M j k

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case inr.intro.inr.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i k : n
hkl : i ≠ k
⊢ 0 = M i k

case inr.intro.inr.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
hij : i ≠ j
⊢ 0 = M j k

Proof state:
case inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
obtain ⟨i⟩ := ‹Nonempty n›

Result:
case inr.intro
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i : n
⊢ M ∈ Set.range ⇑(scalar n)

Proof state:
case inr.intro.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j : n
⊢ diagonal (fun x => M i i) j j = M j j

Tactic:
rw [diagonal_apply_eq]

Result:
case inr.intro.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j : n
⊢ M i i = M j j

Proof state:
case inr.intro.inl.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i : n
⊢ M i i = M i i

Tactic:
rfl

Result:
no goals

Proof state:
case inr.intro
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
⊢ diagonal (fun x => M i i) j k = M j k

Tactic:
obtain rfl | hkl := Decidable.eq_or_ne j k

Result:
case inr.intro.inl
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j : n
⊢ diagonal (fun x => M i i) j j = M j j

case inr.intro.inr
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
⊢ diagonal (fun x => M i i) j k = M j k

Proof state:
case inr.intro
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i : n
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
refine ⟨M i i, Matrix.ext fun j k => ?_⟩

Result:
case inr.intro
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
h✝ : Nonempty n
i j k : n
⊢ (scalar n) (M i i) j k = M j k