internlm/Lean-Github huggingface dataset:
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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⟩
Proof 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
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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⟩
Proof 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
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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
Proof 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
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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
Proof 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
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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
Proof 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
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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]
Proof 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, ⋯⟩)
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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]
Proof 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)
Theorem: Matrix.diag_inv_mul_diag_eq_one_of_lowerTriangular
Proof 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
Proof state after:
no goals
Theorem: LDL.lowerInv_diagonal
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
⊢ lowerInv hS i i = 1
Tactic:
simp only [lowerInv_eq_gramSchmidtBasis, gramSchmidtBasis]
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Theorem: LDL.lowerInv_diagonal
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Tactic:
letI := NormedAddCommGroup.ofMatrix hS.transpose
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
this : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Theorem: LDL.lowerInv_diagonal
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
this : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Tactic:
letI := InnerProductSpace.ofMatrix hS.transpose
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Theorem: LDL.lowerInv_diagonal
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(Basis.mk ⋯ ⋯)).transpose i i = 1
Tactic:
rw [Basis.coe_mk, ← @repr_gramSchmidt_diagonal 𝕜 (n → 𝕜) _ _ _ n _ _ _ i (Pi.basisFun 𝕜 n)]
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix (gramSchmidt 𝕜 ⇑(Pi.basisFun 𝕜 n))).transpose i i =
    ((Pi.basisFun 𝕜 n).repr (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n)) i)) i
Theorem: LDL.lowerInv_diagonal
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix ⋯
⊢ ((Pi.basisFun 𝕜 n).toMatrix (gramSchmidt 𝕜 ⇑(Pi.basisFun 𝕜 n))).transpose i i =
    ((Pi.basisFun 𝕜 n).repr (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n)) i)) i
Tactic:
simp [Basis.toMatrix]
Proof state after:
no goals
Theorem: LDL.lower_eq_to_matrix
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ lower hS = ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose
Tactic:
simp only [lower, lowerInv_eq_gramSchmidtBasis]
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose⁻¹ =
    ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose
Theorem: LDL.lower_eq_to_matrix
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose⁻¹ =
    ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose
Tactic:
apply Matrix.inv_eq_left_inv
Proof state after:
case h
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose *
      ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose =
    1
Theorem: LDL.lower_eq_to_matrix
Proof state before:
case h
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ ((gramSchmidtBasis (Pi.basisFun 𝕜 n)).toMatrix ⇑(Pi.basisFun 𝕜 n)).transpose *
      ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose =
    1
Tactic:
rw [← transpose_mul, Basis.toMatrix_mul_toMatrix_flip, transpose_one]
Proof state after:
no goals
Theorem: LDL.lowerTriangular_lowerInv
Proof state before:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
n : Type u_1
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ (lowerInv hS).lowerTriangular
Tactic:
apply lowerInv_triangular
Proof state after:
no goals
Theorem: LDL.lower_diagonal
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i : n
⊢ lower hS i i = 1
Tactic:
simpa using
  diag_inv_mul_diag_eq_one_of_lowerTriangular (lowerTriangular_lower hS) i
Proof state after:
no goals
Theorem: LDL.det_lowerInv
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ (lowerInv hS).det = 1
Tactic:
have h := det_of_lowerTriangular (lowerInv hS) (by apply lowerInv_triangular)
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ (lowerInv hS).det = 1
Theorem: LDL.det_lowerInv
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ (lowerInv hS).det = 1
Tactic:
rw [h, Finset.prod_eq_one]
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ ∀ x ∈ Finset.univ, lowerInv hS x x = 1
Theorem: LDL.det_lowerInv
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
⊢ ∀ x ∈ Finset.univ, lowerInv hS x x = 1
Tactic:
intros
Proof state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ lowerInv hS x✝ x✝ = 1
Theorem: LDL.det_lowerInv
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
h : (lowerInv hS).det = Finset.univ.prod fun i => lowerInv hS i i
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ lowerInv hS x✝ x✝ = 1
Tactic:
rw [lowerInv_diagonal]
Proof state after:
no goals
Theorem: LDL.det_lowerInv
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ (lowerInv hS).BlockTriangular ⇑OrderDual.toDual
Tactic:
apply lowerInv_triangular
Proof state after:
no goals
Theorem: LDL.det_lower
Proof state before:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ (lower hS).det = 1
Tactic:
simp [lower]
Proof state after:
no goals
Theorem: Matrix.vecCons_zero_zero
Proof state before:
m : ?m.1347
n✝ : ?m.1350
α : Type u_1
n : ℕ
inst✝ : Zero α
⊢ vecCons 0 0 = 0
Tactic:
ext i
Proof state after:
case h
m : ?m.1347
n✝ : ?m.1350
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i
Theorem: Matrix.vecCons_zero_zero
Proof state before:
case h
m : ?m.1347
n✝ : ?m.1350
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i
Tactic:
refine' Fin.cases _ _ i <;> simp [vecCons]
Proof state after:
no goals
Theorem: Matrix.smul_vecCons
Proof state before:
m : ?m.2988
n✝ : ?m.2991
α : Type u_1
n : ℕ
inst✝¹ : Zero α
inst✝ : SMulZeroClass ℝ α
x : ℝ
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)
Tactic:
ext i
Proof state after:
case h
m : ?m.2988
n✝ : ?m.2991
α : Type u_1
n : ℕ
inst✝¹ : Zero α
inst✝ : SMulZeroClass ℝ α
x : ℝ
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
Theorem: Matrix.smul_vecCons
Proof state before:
case h
m : ?m.2988
n✝ : ?m.2991
α : Type u_1
n : ℕ
inst✝¹ : Zero α
inst✝ : SMulZeroClass ℝ α
x : ℝ
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
Tactic:
refine' Fin.cases _ _ i <;> simp [vecCons]
Proof state after:
no goals
Theorem: Matrix.add_vecCons
Proof state before:
m : ?m.4819
n✝ : ?m.4822
α : Type u_1
n : ℕ
inst✝² : Zero α
inst✝¹ : SMulZeroClass ℝ α
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v + vecCons y w = vecCons (x + y) (v + w)
Tactic:
ext i
Proof state after:
case h
m : ?m.4819
n✝ : ?m.4822
α : Type u_1
n : ℕ
inst✝² : Zero α
inst✝¹ : SMulZeroClass ℝ α
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (vecCons x v + vecCons y w) i = vecCons (x + y) (v + w) i
Theorem: Matrix.add_vecCons
Proof state before:
case h
m : ?m.4819
n✝ : ?m.4822
α : Type u_1
n : ℕ
inst✝² : Zero α
inst✝¹ : SMulZeroClass ℝ α
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (vecCons x v + vecCons y w) i = vecCons (x + y) (v + w) i
Tactic:
refine' Fin.cases _ _ i <;> simp [vecCons]
Proof state after:
no goals
Theorem: Real.exp_iff_expCone
Proof state before:
t x : ℝ
⊢ x.exp ≤ t ↔ x.expCone 1 t
Tactic:
unfold expCone
Proof state after:
t x : ℝ
⊢ x.exp ≤ t ↔ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Theorem: Real.exp_iff_expCone
Proof state before:
t x : ℝ
⊢ x.exp ≤ t ↔ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Tactic:
rw [iff_def]
Proof state after:
t x : ℝ
⊢ (x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0) ∧
    (0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t)
Theorem: Real.exp_iff_expCone
Proof state before:
t x : ℝ
⊢ (x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0) ∧
    (0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t)
Tactic:
split_ands
Proof state after:
case refine_1
t x : ℝ
⊢ x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0

case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1
t x : ℝ
⊢ x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0

case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Tactic:
{ intro hexp
  apply Or.intro_left
  split_ands
  { apply Real.zero_lt_one }
  { rwa [div_one, one_mul] } }
Proof state after:
case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Tactic:
{ intro h
  cases h with
  | inl h =>
      have h : 1 * exp (x / 1) ≤ t := h.2
      rwa [div_one, one_mul] at h
  | inr h =>
      exfalso
      exact zero_ne_one h.1.symm }
Proof state after:
no goals
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1
t x : ℝ
⊢ x.exp ≤ t → 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Tactic:
intro hexp
Proof state after:
case refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
Tactic:
apply Or.intro_left
Proof state after:
case refine_1.h
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1.h
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t
Tactic:
split_ands
Proof state after:
case refine_1.h.refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1

case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1.h.refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1

case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Tactic:
{ apply Real.zero_lt_one }
Proof state after:
case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Tactic:
{ rwa [div_one, one_mul] }
Proof state after:
no goals
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1.h.refine_1
t x : ℝ
hexp : x.exp ≤ t
⊢ 0 < 1
Tactic:
apply Real.zero_lt_one
Proof state after:
no goals
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_1.h.refine_2
t x : ℝ
hexp : x.exp ≤ t
⊢ 1 * (x / 1).exp ≤ t
Tactic:
rwa [div_one, one_mul]
Proof state after:
no goals
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_2
t x : ℝ
⊢ 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0 → x.exp ≤ t
Tactic:
intro h
Proof state after:
case refine_2
t x : ℝ
h : 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ x.exp ≤ t
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_2
t x : ℝ
h : 0 < 1 ∧ 1 * (x / 1).exp ≤ t ∨ 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ x.exp ≤ t
Tactic:
cases h with
| inl h =>
    have h : 1 * exp (x / 1) ≤ t := h.2
    rwa [div_one, one_mul] at h
| inr h =>
    exfalso
    exact zero_ne_one h.1.symm
Proof state after:
no goals
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_2.inl
t x : ℝ
h : 0 < 1 ∧ 1 * (x / 1).exp ≤ t
⊢ x.exp ≤ t
Tactic:
have h : 1 * exp (x / 1) ≤ t := h.2
Proof state after:
case refine_2.inl
t x : ℝ
h✝ : 0 < 1 ∧ 1 * (x / 1).exp ≤ t
h : 1 * (x / 1).exp ≤ t
⊢ x.exp ≤ t
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_2.inl
t x : ℝ
h✝ : 0 < 1 ∧ 1 * (x / 1).exp ≤ t
h : 1 * (x / 1).exp ≤ t
⊢ x.exp ≤ t
Tactic:
rwa [div_one, one_mul] at h
Proof state after:
no goals
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_2.inr
t x : ℝ
h : 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ x.exp ≤ t
Tactic:
exfalso
Proof state after:
case refine_2.inr
t x : ℝ
h : 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ False
Theorem: Real.exp_iff_expCone
Proof state before:
case refine_2.inr
t x : ℝ
h : 1 = 0 ∧ 0 ≤ t ∧ x ≤ 0
⊢ False
Tactic:
exact zero_ne_one h.1.symm
Proof state after:
no goals