awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C((↑(spectrum ℝ a) : Type), ℝ)
⊢ Eq (α := n → 𝕜)
    (star
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) ⋯))
    (RCLike.ofReal ∘
      Function.comp (β := (↑(spectrum ℝ a) : Type)) (⇑f : (a : (↑(spectrum ℝ a) : Type)) → ℝ) fun (i : n) ↦
        Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ a) (ha.eigenvalues i) ⋯)

Tactic:
simp [Pi.star_def, Function.comp_def]

Premises used: Function.comp_def, Pi.star_def
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) ⋯) hA.cfcAux

Tactic:
cfcHom_eq_of_continuous_of_map_id hA hA.cfcAux
    hA.isClosedEmbedding_cfcAux.continuous hA.cfcAux_id

Premises used: Matrix.IsHermitian.isClosedEmbedding_cfcAux, IsSelfAdjoint, cfcHom_eq_of_continuous_of_map_id, Topology.IsClosedEmbedding.continuous, Matrix.IsHermitian.cfcAux_id, Matrix.IsHermitian, Matrix.IsHermitian.cfcAux
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ IsSelfAdjoint A

Tactic:
have hA' : IsSelfAdjoint A := hA
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
⊢ Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux

Tactic:
have := cfcHom_eq_of_continuous_of_map_id hA' hA.cfcAux hA.isClosedEmbedding_cfcAux.continuous
    hA.cfcAux_id
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux
rw : Continuous ((spectrum ℝ A).restrict (π := fun (a : ℝ) ↦ ℝ) f)
⊢ ContinuousOn f (spectrum ℝ A)

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux
⊢ Continuous ((spectrum ℝ A).restrict (π := fun (a : ℝ) ↦ ℝ) f)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux
rw :
  (hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
      { toFun := (spectrum ℝ A).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ } =
    hA.cfc f
⊢ cfc (p := IsSelfAdjoint) f A = hA.cfc f

Tactic:
rw [cfc_apply f A hA' (by rw [continuousOn_iff_continuous_restrict]; fun_prop), this]

Premises used: cfc_apply
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux
⊢ (hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
      { toFun := (spectrum ℝ A).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ } =
    hA.cfc f

Tactic:
simp only [cfcAux_apply, ContinuousMap.coe_mk, Function.comp_def, Set.restrict_apply,
    IsHermitian.cfc]

Premises used: Set.restrict_apply, Matrix.IsHermitian.cfcAux_apply, Function.comp_def, Matrix.IsHermitian.cfc, ContinuousMap.coe_mk
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
rw :
  Eq (α := 𝕜[X])
    (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
        diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues)).charpoly
    (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(f (hA.eigenvalues i)) : 𝕜)))
⊢ Eq (α := 𝕜[X]) (cfc (p := IsSelfAdjoint) f A).charpoly
    (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(f (hA.eigenvalues i)) : 𝕜)))

Tactic:
rw [cfc_eq hA f, IsHermitian.cfc, conjStarAlgAut_apply, charpoly_mul_comm, ← mul_assoc]

Premises used: Matrix.IsHermitian.cfc_eq, mul_assoc, Unitary.conjStarAlgAut_apply, Matrix.IsHermitian.cfc, Matrix.charpoly_mul_comm
-- Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ Eq (α := 𝕜[X])
    (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
        diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues)).charpoly
    (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(f (hA.eigenvalues i)) : 𝕜)))

Tactic:
simp [charpoly_diagonal]

Premises used: Matrix.charpoly_diagonal
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
this_1 : NormedAddCommGroup (n → 𝕜) := Sᵀ.toNormedAddCommGroup ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := Sᵀ.toInnerProductSpace ⋯
a :
  ∀ (i j : n),
    lowerInv hS i j = (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ i j
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ

Tactic:
ext i j
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
this_1 : NormedAddCommGroup (n → 𝕜) := Sᵀ.toNormedAddCommGroup ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := Sᵀ.toInnerProductSpace ⋯
i j : n
a :
  Eq.{u_1 + 1} (α := 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j)
    ((gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜))ᵀᵀ i j)
⊢ lowerInv hS i j = (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ i j

Tactic:
rw [LDL.lowerInv, Basis.coePiBasisFun.toMatrix_eq_transpose, coe_gramSchmidtBasis]

Premises used: LDL.lowerInv, InnerProductSpace.coe_gramSchmidtBasis, Module.Basis.coePiBasisFun.toMatrix_eq_transpose
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
this_1 : NormedAddCommGroup (n → 𝕜) := Sᵀ.toNormedAddCommGroup ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := Sᵀ.toInnerProductSpace ⋯
i j : n
⊢ Eq.{u_1 + 1} (α := 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j)
    ((gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜))ᵀᵀ i j)

Tactic:
rfl
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
rw :
  Invertible (α := Matrix n n 𝕜)
    (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ
⊢ Invertible (lowerInv hS)

Tactic:
rw [LDL.lowerInv_eq_gramSchmidtBasis]

Premises used: LDL.lowerInv_eq_gramSchmidtBasis
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
haveI :
  (this :
      Invertible (α := Matrix n n 𝕜)
        (Basis.toMatrix (Pi.basisFun 𝕜 n)
          (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n) : Basis n 𝕜 (n → 𝕜)) : (a : n) → n → 𝕜))) →
    Invertible (α := Matrix n n 𝕜)
      (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ
⊢ Invertible (α := Matrix n n 𝕜)
    (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ

Tactic:
haveI :=
    Basis.invertibleToMatrix (Pi.basisFun 𝕜 n)
      (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
        (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ (Pi.basisFun 𝕜 n))
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
this :
  Invertible (α := Matrix n n 𝕜)
    (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n) : Basis n 𝕜 (n → 𝕜)) : (a : n) → n → 𝕜))
⊢ Invertible (α := Matrix n n 𝕜)
    (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
h₀ : i ≠ j
⊢ inner 𝕜 (E := WithLp 2 (n → 𝕜)) (WithLp.toLp 2 (lowerInv hS i)) (WithLp.toLp 2 (Sᵀ *ᵥ lowerInv hS j)) = 0

Tactic:
@gramSchmidt_orthogonal 𝕜 _ _ (Sᵀ.toNormedAddCommGroup hS.transpose)
    (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) _ _ _ _ _ _ _ h₀

Premises used: Multiset.sum, LDL.lowerInv, Multiset.foldr, dotProduct, InnerProductSpace.gramSchmidt_orthogonal, WellFounded.fixF, Matrix.mulVec, Finset.sum, WellFounded.fix
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : i < j
rw :
  lowerInv hS i j =
    ((Basis.repr (Pi.basisFun 𝕜 n) : (a : n → 𝕜) → n →₀ 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i) :
        (a : n) → 𝕜)
      j
rw₁ : lowerInv hS i j = gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j)
    (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j)
⊢ lowerInv hS i j = 0

Tactic:
rw [← @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
      (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ i j hij (Pi.basisFun 𝕜 n),
    Pi.basisFun_repr, LDL.lowerInv]

Premises used: LDL.lowerInv, InnerProductSpace.gramSchmidt_triangular, Pi.basisFun, Pi.basisFun_repr
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
a : ∀ (i j : n), diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ

Tactic:
ext i j
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
pos : ∀ (hij : i = j), diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
neg : ∀ (hij : ¬i = j), diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j

Tactic:
by_cases hij : i = j
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : i = j
pos : lowerInv hS j ⬝ᵥ S *ᵥ star (lowerInv hS j) = (lowerInv hS * (S * (lowerInv hS)ᴴ)) j j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j

Tactic:
simp only [diag, diagEntries, EuclideanSpace.inner_toLp_toLp, star_star, hij,
      diagonal_apply_eq, Matrix.mul_assoc, dotProduct_comm]

Premises used: star_star, Matrix.mul_assoc, Matrix.diagonal_apply_eq, LDL.diagEntries, LDL.diag, EuclideanSpace.inner_toLp_toLp, dotProduct_comm
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : i = j
⊢ lowerInv hS j ⬝ᵥ S *ᵥ star (lowerInv hS j) = (lowerInv hS * (S * (lowerInv hS)ᴴ)) j j

Tactic:
rfl
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : ¬i = j
neg : 0 = lowerInv hS i ⬝ᵥ S *ᵥ (lowerInv hS)ᴴᵀ j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j

Tactic:
simp only [LDL.diag, hij, diagonal_apply_ne, Ne, not_false_iff, mul_mul_apply]

Premises used: Ne, LDL.diag, not_false_iff, Matrix.diagonal_apply_ne, Matrix.mul_mul_apply
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : ¬i = j
neg : lowerInv hS i ᵥ* S ⬝ᵥ star (lowerInv hS j) = lowerInv hS i ᵥ* S ⬝ᵥ (lowerInv hS).map star j
⊢ 0 = lowerInv hS i ⬝ᵥ S *ᵥ (lowerInv hS)ᴴᵀ j

Tactic:
rw [conjTranspose, transpose_map, transpose_transpose, dotProduct_mulVec,
      (LDL.lowerInv_orthogonal hS fun h : j = i => hij h.symm).symm, ← inner_conj_symm,
      mulVec_transpose, EuclideanSpace.inner_toLp_toLp, ← RCLike.star_def, ←
      star_dotProduct_star, star_star]

Premises used: Matrix.mulVec_transpose, RCLike.star_def, Matrix.transpose_transpose, star_star, LDL.lowerInv_orthogonal, Matrix.star_dotProduct_star, Matrix.transpose_map, EuclideanSpace.inner_toLp_toLp, Eq.symm, Matrix.conjTranspose, inner_conj_symm, Matrix.dotProduct_mulVec
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : ¬i = j
⊢ lowerInv hS i ᵥ* S ⬝ᵥ star (lowerInv hS j) = lowerInv hS i ᵥ* S ⬝ᵥ (lowerInv hS).map star j

Tactic:
rfl
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
rw : diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
⊢ lower hS * diag hS * (lower hS)ᴴ = S

Tactic:
rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
    Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS),
    Matrix.mul_inv_eq_iff_eq_mul_of_invertible]

Premises used: LDL.lowerInv, Matrix.inv_mul_eq_iff_eq_mul_of_invertible, Matrix.mul_inv_eq_iff_eq_mul_of_invertible, Matrix.mul_assoc, Matrix.conjTranspose_nonsing_inv, LDL.lower
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ

Tactic:
LDL.diag_eq_lowerInv_conj hS

Premises used: LDL.diag_eq_lowerInv_conj
-- Module: Mathlib.Analysis.Matrix.LDL
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ

Tactic:
exact LDL.diag_eq_lowerInv_conj hS

Premises used: LDL.diag_eq_lowerInv_conj
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
simp_rw :
  (norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) =
    (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)
simp_rw₁ :
  (↑(Finset.sup Finset.univ fun (b : m) ↦ nnnorm (E := (j : n) → α) fun (j : n) ↦ A b j) : ℝ) =
    (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)
⊢ ‖A‖ = (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)

Tactic:
simp_rw [Matrix.norm_def, Pi.norm_def, Pi.nnnorm_def]

Premises used: Matrix.norm_def, Pi.norm_def, Pi.nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖₊ = nnnorm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
r : ℝ
hr : 0 ≤ r
A : Matrix m n α
simp_rw : (norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
⊢ ‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r

Tactic:
simp_rw [norm_def, pi_norm_le_iff_of_nonneg hr]

Premises used: Matrix.norm_def, pi_norm_le_iff_of_nonneg
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
r : ℝ≥0
A : Matrix m n α
simp_rw : (nnnorm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
⊢ ‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r

Tactic:
simp_rw [nnnorm_def, pi_nnnorm_le_iff]

Premises used: pi_nnnorm_le_iff, Matrix.nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
r : ℝ
hr : 0 < r
A : Matrix m n α
simp_rw : (norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
⊢ ‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r

Tactic:
simp_rw [norm_def, pi_norm_lt_iff hr]

Premises used: Matrix.norm_def, pi_norm_lt_iff
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
r : ℝ≥0
hr : 0 < r
A : Matrix m n α
simp_rw : (nnnorm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r
⊢ ‖A‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r

Tactic:
simp_rw [nnnorm_def, pi_nnnorm_lt_iff hr]

Premises used: pi_nnnorm_lt_iff, Matrix.nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
i : m
j : n
⊢ ‖A i j‖ ≤ ‖A‖

Tactic:
(norm_le_pi_norm (A i) j).trans (norm_le_pi_norm A i)

Premises used: norm_le_pi_norm, LE.le.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
i : m
j : n
⊢ ‖A i j‖₊ ≤ ‖A‖₊

Tactic:
(nnnorm_le_pi_nnnorm (A i) j).trans (nnnorm_le_pi_nnnorm A i)

Premises used: nnnorm_le_pi_nnnorm, LE.le.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖A.map f‖₊ = ‖A‖₊

Tactic:
simp only [nnnorm_def, Pi.nnnorm_def, Matrix.map_apply, hf]

Premises used: Matrix.map_apply, Pi.nnnorm_def, Matrix.nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖ = ‖a‖
⊢ ‖A.map f‖ = ‖A‖

Tactic:
(congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_map_eq A f fun a => Subtype.ext <| hf a :)

Premises used: Multiset.foldr, Finset.fold, NNReal.mk, NNReal, congr_arg, Finset.sup, NNReal.toReal, Matrix.nnnorm_map_eq, Multiset.fold, Subtype.ext
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖Aᵀ‖₊ = ‖A‖₊

Tactic:
Finset.sup_comm _ _ _

Premises used: Multiset.foldr, Finset.fold, NNReal.mk, NNReal, Finset.sup_comm, Matrix.transpose, Finset.sup, NNReal.toReal, Multiset.fold
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖Aᵀ‖ = ‖A‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_transpose A

Premises used: congr_arg, Matrix.nnnorm_transpose, NNReal.toReal
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : StarAddMonoid α
inst_4 : NormedStarGroup α
A : Matrix m n α
⊢ ‖Aᴴ‖₊ = ‖A‖₊

Tactic:
(nnnorm_map_eq _ _ nnnorm_star).trans A.nnnorm_transpose

Premises used: nnnorm_star, Matrix.nnnorm_transpose, Matrix.conjTranspose, Matrix.nnnorm_map_eq, Eq.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : StarAddMonoid α
inst_4 : NormedStarGroup α
A : Matrix m n α
⊢ ‖Aᴴ‖ = ‖A‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_conjTranspose A

Premises used: congr_arg, Matrix.nnnorm_conjTranspose, NNReal.toReal
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
ι : Type u_7
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : Unique ι
inst_4 : SeminormedAddCommGroup α
inst_5 : SeminormedAddCommGroup β
inst_6 : StarAddMonoid α
inst_7 : NormedStarGroup α
⊢ NormedStarGroup (Matrix m m α)

Tactic:
⟨(le_of_eq <| norm_conjTranspose ·)⟩

Premises used: NormedStarGroup.mk, Matrix.norm_conjTranspose, le_of_eq
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
⊢ ‖replicateCol ι v‖₊ = ‖v‖₊

Tactic:
simp [nnnorm_def, Pi.nnnorm_def]

Premises used: Pi.nnnorm_def, Matrix.nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
⊢ ‖replicateCol ι v‖ = ‖v‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_replicateCol v

Premises used: congr_arg, NNReal.toReal, Matrix.nnnorm_replicateCol
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
ι : Type u_7
inst : Fintype n
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : n → α
⊢ ‖replicateRow ι v‖₊ = ‖v‖₊

Tactic:
simp [nnnorm_def, Pi.nnnorm_def]

Premises used: Pi.nnnorm_def, Matrix.nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
ι : Type u_7
inst : Fintype n
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : n → α
⊢ ‖replicateRow ι v‖ = ‖v‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_replicateRow v

Premises used: Matrix.nnnorm_replicateRow, congr_arg, NNReal.toReal