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

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

State before:
α : Type ?u.15206
m : Type u_1
n : Type ?u.15212
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.lowerTriangular
k : m
this : Unique { a // OrderDual.toDual 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.15206
m : Type u_1
n : Type ?u.15212
R : Type u_2
inst✝³ : CommRing R
M N : Matrix m m R
inst✝² : Fintype m
inst✝¹ : LinearOrder m
inst✝ : Invertible M
hM : M.lowerTriangular
k : m
this : Unique { a // OrderDual.toDual a = k } := { default := ⟨k, ⋯⟩, uniq := ⋯ }
h : (M⁻¹.toSquareBlock (⇑OrderDual.toDual) k * M.toSquareBlock (⇑OrderDual.toDual) k) ⟨k, ⋯⟩ ⟨k, ⋯⟩ = 1 ⟨k, ⋯⟩ ⟨k, ⋯⟩
⊢ M⁻¹ k k * M k k = 1

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

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

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

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

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

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