Theorem: Matrix.diag_inv_mul_diag_eq_one_of_upperTriangular (CvxLean/Lib/Math/LinearAlgebra/Matrix/Triangular.lean)

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
⊢ M⁻¹ k k * M k k = 1
Tactic:
letI : Unique {a // id a = k} := ⟨⟨⟨k, rfl⟩⟩, fun j => Subtype.ext j.property⟩
State after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
⊢ M⁻¹ k k * M k k = 1

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
⊢ M⁻¹ k k * M k k = 1
Tactic:
have h := congr_fun (congr_fun
  (toSquareBlock_inv_mul_toSquareBlock_eq_one hM k) ⟨k, rfl⟩) ⟨k, rfl⟩
State after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : (M⁻¹.toSquareBlock id k * M.toSquareBlock id k) ⟨k, ⋯⟩ ⟨k, ⋯⟩ = 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : (M⁻¹.toSquareBlock id k * M.toSquareBlock id k) ⟨k, ⋯⟩ ⟨k, ⋯⟩ = 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Tactic:
dsimp only [HMul.hMul, dotProduct] at h
State after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h :
  ∑ i : { a // id a = k }, Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ i) (M.toSquareBlock id k i ⟨k, ⋯⟩) =
    OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h :
  ∑ i : { a // id a = k }, Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ i) (M.toSquareBlock id k i ⟨k, ⋯⟩) =
    OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Tactic:
rw [@Fintype.sum_unique _ _ _ _] at h
State after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ default) (M.toSquareBlock id k default ⟨k, ⋯⟩) = OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ default) (M.toSquareBlock id k default ⟨k, ⋯⟩) = OfNat.ofNat 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1
Tactic:
simp at h
State after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = 1

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = 1
Tactic:
rw [← h]
State after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩)

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩)
Tactic:
simp [toSquareBlock, toSquareBlockProp]
State after:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹ k k) (M k k)

State before:
α : Type ?u.10355
m : Type u_1
n : Type ?u.10361
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.upperTriangular
k : m
this : Unique { a // id a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : Mul.mul (M⁻¹.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) (M.toSquareBlock id k ⟨k, ⋯⟩ ⟨k, ⋯⟩) = 1
⊢ M⁻¹ k k * M k k = Mul.mul (M⁻¹ k k) (M k k)
Tactic:
rfl
State after:
no goals