awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
X : Matrix n n 𝕜
hX : IsSelfAdjoint X
hA : 0 ≤ X * X
⊢ ∃ (s : Matrix n n 𝕜), X * X = star s * s

Tactic:
exact ⟨X, hX.star_eq.symm ▸ rfl⟩
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
obtain : ∀ (X : Matrix n n 𝕜) (hX : IsSelfAdjoint X) (hA : 0 ≤ X * X), ∃ (s : Matrix n n 𝕜), X * X = star s * s
⊢ ∃ (s : Matrix n n 𝕜), A = star s * s

Tactic:
classical
      obtain ⟨X, hX, -, rfl⟩ :=
        sub_zero A ▸ CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hA.isHermitian
          (QuasispectrumRestricts.nnreal_of_nonneg hA.nonneg)
      exact ⟨X, hX.star_eq.symm ▸ rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
rw : CFC.sqrt A⁻¹ = (CFC.sqrt A)⁻¹
rw₁ : (CFC.sqrt A)⁻¹ * (CFC.sqrt A)⁻¹ = A⁻¹
rw₂ : HPow.hPow (β := ℕ) (CFC.sqrt A)⁻¹ 2 = A⁻¹
rw₃ : (HPow.hPow (β := ℕ) (CFC.sqrt A) 2)⁻¹ = A⁻¹
rw₄ rw₅ : A⁻¹ = A⁻¹
⊢ (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹

Tactic:
rw [eq_comm, CFC.sqrt_eq_iff _ _ hA.inv.nonneg (CFC.sqrt_nonneg A).posSemidef.inv.nonneg, ← sq,
    inv_pow', CFC.sq_sqrt A]

Premises used: CFC.sq_sqrt, Matrix.LE.le.posSemidef, CFC.sqrt_eq_iff, Matrix.PosSemidef.nonneg, sq, eq_comm, Matrix.inv_pow', CFC.sqrt_nonneg, Matrix.PosSemidef.inv
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩

Premises used: Eq.rec, Iff.intro, dotProduct_zero, Eq.symm, Star.star
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
refine : ∀ (h : star x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
h : star x ⬝ᵥ A *ᵥ x = 0
obtain :
  ∀ (B : Matrix n n 𝕜) (hA : (star B * B).PosSemidef) (h : star x ⬝ᵥ (star B * B) *ᵥ x = 0), (star B * B) *ᵥ x = 0
⊢ A *ᵥ x = 0

Tactic:
obtain ⟨B, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hA.nonneg

Premises used: Matrix.PosSemidef.nonneg, CStarAlgebra.nonneg_iff_eq_star_mul_self, Iff.mp, rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
x : n → 𝕜
B : Matrix n n 𝕜
hA : (star B * B).PosSemidef
h : star x ⬝ᵥ (star B * B) *ᵥ x = 0
simp_rw : ∀ (h : B *ᵥ x = 0), Bᴴ *ᵥ B *ᵥ x = 0
⊢ (star B * B) *ᵥ x = 0

Tactic:
simp_rw [← Matrix.mulVec_mulVec, dotProduct_mulVec _ _ (B *ᵥ x), star_eq_conjTranspose,
    vecMul_conjTranspose, star_star, dotProduct_star_self_eq_zero] at h ⊢

Premises used: Matrix.star_eq_conjTranspose, dotProduct_star_self_eq_zero, star_star, Matrix.vecMul_conjTranspose, Matrix.mulVec, Matrix.dotProduct_mulVec, Matrix.mulVec_mulVec
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
x : n → 𝕜
B : Matrix n n 𝕜
hA : (star B * B).PosSemidef
h : B *ᵥ x = 0
rw : Bᴴ *ᵥ 0 = 0
rw₁ rw₂ : Eq (α := n → 𝕜) 0 0
⊢ Bᴴ *ᵥ B *ᵥ x = 0

Tactic:
rw [h, mulVec_zero]

Premises used: Matrix.mulVec_zero
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
refine : ∀ (h : star x ⬝ᵥ A *ᵥ x = 0), A *ᵥ x = 0
refine₁ :
  ∀ (B : Matrix n n 𝕜) (hA : (star B * B).PosSemidef) (h : star x ⬝ᵥ (star B * B) *ᵥ x = 0), (star B * B) *ᵥ x = 0
refine₂ : ∀ (B : Matrix n n 𝕜) (hA : (star B * B).PosSemidef) (h : B *ᵥ x = 0), Bᴴ *ᵥ B *ᵥ x = 0
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Tactic:
classical
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩
  obtain ⟨B, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hA.nonneg
  simp_rw [← Matrix.mulVec_mulVec, dotProduct_mulVec _ _ (B *ᵥ x), star_eq_conjTranspose,
    vecMul_conjTranspose, star_star, dotProduct_star_self_eq_zero] at h ⊢
  rw [h, mulVec_zero]

Premises used: Matrix.star_eq_conjTranspose, dotProduct_star_self_eq_zero, star_star, Matrix.PosSemidef.nonneg, Matrix.mulVec_zero, Matrix.vecMul_conjTranspose, CStarAlgebra.nonneg_iff_eq_star_mul_self, Iff.mp, rfl, Matrix.mulVec_mulVec
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜)
      (((((((toLinearMap₂' 𝕜 : Matrix n n 𝕜 ≃ₗ[𝕜] (n → 𝕜) →ₗ[𝕜] (n → 𝕜) →ₗ[𝕜] 𝕜) :
                        (a : Matrix n n 𝕜) → (n → 𝕜) →ₗ[𝕜] (n → 𝕜) →ₗ[𝕜] 𝕜)
                      A :
                    (n → 𝕜) →ₗ[𝕜] (n → 𝕜) →ₗ[𝕜] 𝕜) :
                  (a : n → 𝕜) → (n → 𝕜) →ₗ[𝕜] 𝕜)
                (star x) :
              (n → 𝕜) →ₗ[𝕜] 𝕜) :
            (a : n → 𝕜) → 𝕜)
          x :
        𝕜)
      (0 : 𝕜) ↔
    A *ᵥ x = 0

Tactic:
simpa only [toLinearMap₂'_apply'] using hA.dotProduct_mulVec_zero_iff x

Premises used: Matrix.toLinearMap₂'_apply', Matrix.PosSemidef.dotProduct_mulVec_zero_iff
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
rw :
  (⋯.cfc fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : NNReal) → NNReal) x.toNNReal) : ℝ)).det =
    (↑√((RCLike.re : (a : 𝕜) → ℝ) A.det) : 𝕜)
⊢ (CFC.sqrt A).det = RCLike.sqrt A.det

Tactic:
rw [CFC.sqrt_eq_cfc, cfc_nnreal_eq_real _ A, hA.1.cfc_eq, RCLike.sqrt_of_nonneg hA.det_nonneg]

Premises used: Matrix.IsHermitian.cfc_eq, cfc_nnreal_eq_real, RCLike.sqrt_of_nonneg, Matrix.PosSemidef.det_nonneg, And.left, CFC.sqrt_eq_cfc
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
simp : Eq.{u_1 + 1} (α := 𝕜) (↑(∏ i : n, √(max (⋯.eigenvalues i) 0)) : 𝕜) (↑(∏ i : n, √(⋯.eigenvalues i)) : 𝕜)
⊢ (⋯.cfc fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : NNReal) → NNReal) x.toNNReal) : ℝ)).det =
    (↑√((RCLike.re : (a : 𝕜) → ℝ) A.det) : 𝕜)

Tactic:
simp only [IsHermitian.cfc, Real.coe_sqrt, Real.coe_toNNReal', det_map, det_diagonal,
    Function.comp_apply, hA.isHermitian.det_eq_prod_eigenvalues, ← RCLike.ofReal_prod,
    RCLike.ofReal_re, Real.sqrt_prod _ fun _ _ ↦ hA.eigenvalues_nonneg _]

Premises used: Matrix.PosSemidef.isHermitian, RCLike.ofReal_re, Real.coe_toNNReal', Matrix.det_map, Matrix.PosSemidef.eigenvalues_nonneg, RCLike.ofReal_prod, Matrix.det_diagonal, Matrix.IsHermitian.det_eq_prod_eigenvalues, Matrix.IsHermitian.cfc, Function.comp_apply, Real.coe_sqrt, Real.sqrt_prod
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ Eq.{u_1 + 1} (α := 𝕜) (↑(∏ i : n, √(max (⋯.eigenvalues i) 0)) : 𝕜) (↑(∏ i : n, √(⋯.eigenvalues i)) : 𝕜)

Tactic:
grind
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ (hA.cfc fun (x : ℝ) ↦ ‖x‖).det = (↑‖A.det‖ : 𝕜)

Tactic:
simp [IsHermitian.cfc, -Unitary.conjStarAlgAut_apply, hA.det_eq_prod_eigenvalues]

Premises used: Unitary.conjStarAlgAut_apply, Matrix.IsHermitian.det_eq_prod_eigenvalues, Matrix.IsHermitian.cfc
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
⊢ A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}

Tactic:
⟨fun h => ⟨h.isHermitian, fun a => ?_⟩, fun ⟨h1, h2⟩ => ?_⟩

Premises used: Matrix.PosSemidef.isHermitian, Matrix.PosSemidef, And.intro, Iff.intro, _private.0.Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg.match_1
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
refine_1 : ∀ (h : A.PosSemidef), ∀ a ∈ spectrum 𝕜 A, Membership.mem (γ := Set 𝕜) {a : 𝕜 | 0 ≤ a} a
refine_2 :
  A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a} →
    ∀ (h1 : A.IsHermitian) (h2 : spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}), A.PosSemidef
⊢ A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}

Tactic:
refine ⟨fun h => ⟨h.isHermitian, fun a => ?_⟩, fun ⟨h1, h2⟩ => ?_⟩
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
h : A.PosSemidef
a : 𝕜
refine_1 : ∀ (x : n) (h : (↑(⋯.eigenvalues x) : 𝕜) = a), 0 ≤ a
⊢ a ∈ spectrum 𝕜 A → Membership.mem (γ := Set 𝕜) {a : 𝕜 | 0 ≤ a} a

Tactic:
simp only [h.isHermitian.spectrum_eq_image_range, Set.mem_image, Set.mem_range,
      exists_exists_eq_and, Set.mem_setOf_eq, forall_exists_index]

Premises used: Set.mem_range, Matrix.PosSemidef.isHermitian, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, Matrix.IsHermitian.spectrum_eq_image_range, exists_exists_eq_and
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
h : A.PosSemidef
i : n
⊢ LE.le.{u_1} (α := 𝕜) 0 (↑(⋯.eigenvalues i) : 𝕜)

Tactic:
exact_mod_cast h.eigenvalues_nonneg _

Premises used: Matrix.PosSemidef.eigenvalues_nonneg
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
h : A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
h1 : A.IsHermitian
h2 : spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
refine_2 : 0 ≤ h1.eigenvalues
⊢ A.PosSemidef

Tactic:
rw [h1.posSemidef_iff_eigenvalues_nonneg]

Premises used: Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
h : A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
h1 : A.IsHermitian
h2 : spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a}
i : n
⊢ 0 i ≤ h1.eigenvalues i

Tactic:
simpa [h1.spectrum_eq_image_range] using @h2 (h1.eigenvalues i)

Premises used: Matrix.IsHermitian.spectrum_eq_image_range
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
x : Matrix n n 𝕜
hx : x.PosSemidef
⊢ x.PosDef ↔ IsUnit x

Tactic:
⟨fun h => h.isUnit, fun h => .of_dotProduct_mulVec_pos hx.1 fun v hv => ?_⟩

Premises used: Matrix.PosDef.isUnit, And.left, Iff.intro, Matrix.PosDef.of_dotProduct_mulVec_pos
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
x : Matrix n n 𝕜
hx : x.PosSemidef
refine : ∀ (h : IsUnit x) (v : n → 𝕜) (hv : v ≠ 0), 0 < star v ⬝ᵥ x *ᵥ v
⊢ x.PosDef ↔ IsUnit x

Tactic:
refine ⟨fun h => h.isUnit, fun h => .of_dotProduct_mulVec_pos hx.1 fun v hv => ?_⟩
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
x : Matrix n n 𝕜
hx : x.PosSemidef
h : IsUnit x
v : n → 𝕜
hv : v ≠ 0
obtain : ∀ (y : Matrix n n 𝕜) (hx : (star y * y).PosSemidef) (h : IsUnit (star y * y)), 0 < star v ⬝ᵥ (star y * y) *ᵥ v
⊢ 0 < star v ⬝ᵥ x *ᵥ v

Tactic:
obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg

Premises used: Matrix.PosSemidef.nonneg, CStarAlgebra.nonneg_iff_eq_star_mul_self, Iff.mp, rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
hv : v ≠ 0
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
simp_rw : y *ᵥ v ≠ 0
⊢ 0 < star v ⬝ᵥ (star y * y) *ᵥ v

Tactic:
simp_rw [dotProduct_mulVec, ← vecMul_vecMul, star_eq_conjTranspose, ← star_mulVec,
    ← dotProduct_mulVec, dotProduct_star_self_pos_iff]

Premises used: Matrix.star_eq_conjTranspose, Matrix.dotProduct_star_self_pos_iff, Matrix.vecMul_vecMul, Matrix.dotProduct_mulVec, Matrix.star_mulVec
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
hv : v ≠ 0
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
contrapose : ∀ (hv : y *ᵥ v = 0), v = 0
⊢ y *ᵥ v ≠ 0

Tactic:
contrapose hv
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → 𝕜
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
hv : y *ᵥ v = 0
rw : Eq (α := n → 𝕜) (((yᴴ * y).mulVecLin : (a : n → 𝕜) → n → 𝕜) v : n → 𝕜) (0 : n → 𝕜)
rw₁ : (yᴴ * y) *ᵥ v = 0
rw₂ : yᴴ *ᵥ y *ᵥ v = 0
rw₃ : yᴴ *ᵥ 0 = 0
rw₄ rw₅ : Eq (α := n → 𝕜) 0 0
⊢ v = 0

Tactic:
rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]

Premises used: Iff.mpr, HMul.hMul, Matrix.mulVecLin_apply, Matrix.mulVec_zero, Matrix.mulVecLin, map_eq_zero_iff, Matrix.conjTranspose, Matrix.mulVec_injective_iff_isUnit, Matrix.mulVec_mulVec
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
x : Matrix n n 𝕜
⊢ IsStrictlyPositive x ↔ x.PosDef

Tactic:
⟨fun h => h.nonneg.posSemidef.posDef_iff_isUnit.mpr h.isUnit,
  fun h => h.isUnit.isStrictlyPositive h.posSemidef.nonneg⟩

Premises used: Iff.mpr, Matrix.PosSemidef.posDef_iff_isUnit, Matrix.LE.le.posSemidef, Matrix.PosDef.isUnit, Matrix.PosSemidef.nonneg, IsUnit.isStrictlyPositive, Matrix.PosDef.posSemidef, Iff.intro, IsStrictlyPositive.isUnit, IsStrictlyPositive.nonneg
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ A.PosDef ↔ A.det ≠ 0

Tactic:
simp [hA.posDef_iff_isUnit, isUnit_iff_isUnit_det]

Premises used: Matrix.PosSemidef.posDef_iff_isUnit, Matrix.isUnit_iff_isUnit_det
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosSemidef
hy : y.PosSemidef
have : ∀ (this : Fintype n), PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
have := Fintype.ofFinite n
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosSemidef
hy : y.PosSemidef
this : Fintype n
have : ∀ (this : Fintype m), PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
have := Fintype.ofFinite m
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosSemidef
hy : y.PosSemidef
this_1 : Fintype n
this : Fintype m
obtain :
  ∀ (a : Matrix n n 𝕜) (hx : (star a * a).PosSemidef),
    PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) y)
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
obtain ⟨a, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg

Premises used: Matrix.PosSemidef.nonneg, CStarAlgebra.nonneg_iff_eq_star_mul_self, Iff.mp, rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
y : Matrix m m 𝕜
hy : y.PosSemidef
this_1 : Fintype n
this : Fintype m
a : Matrix n n 𝕜
hx : (star a * a).PosSemidef
obtain :
  ∀ (b : Matrix m m 𝕜) (hy : (star b * b).PosSemidef),
    PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) (star b * b))
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) y)

Tactic:
obtain ⟨b, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hy.nonneg

Premises used: Matrix.PosSemidef.nonneg, CStarAlgebra.nonneg_iff_eq_star_mul_self, Iff.mp, rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
this_1 : Fintype n
this : Fintype m
a : Matrix n n 𝕜
hx : (star a * a).PosSemidef
b : Matrix m m 𝕜
hy : (star b * b).PosSemidef
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) (star b * b))

Tactic:
simpa [mul_kronecker_mul, ← conjTranspose_kronecker, star_eq_conjTranspose] using
    posSemidef_conjTranspose_mul_self _

Premises used: Matrix.posSemidef_conjTranspose_mul_self, Matrix.star_eq_conjTranspose, Matrix.conjTranspose_kronecker, Matrix.mul_kronecker_mul
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosSemidef
hy : y.PosSemidef
have have₁ have₂ have₃ : ∀ (this : Fintype n), PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have₄ : ∀ (this : Fintype n) (this : Fintype m), PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have₅ :
  ∀ (this : Fintype n) (this_1 : Fintype m) (a : Matrix n n 𝕜) (hx : (star a * a).PosSemidef),
    PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) y)
have₆ :
  ∀ (this : Fintype n) (this_1 : Fintype m) (a : Matrix n n 𝕜) (hx : (star a * a).PosSemidef) (b : Matrix m m 𝕜)
    (hy : (star b * b).PosSemidef),
    PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) (star b * b))
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
classical
  have := Fintype.ofFinite n; have := Fintype.ofFinite m
  obtain ⟨a, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
  obtain ⟨b, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hy.nonneg
  simpa [mul_kronecker_mul, ← conjTranspose_kronecker, star_eq_conjTranspose] using
    posSemidef_conjTranspose_mul_self _

Premises used: Matrix.posSemidef_conjTranspose_mul_self, Matrix.star_eq_conjTranspose, Matrix.conjTranspose_kronecker, Matrix.mul_kronecker_mul, CStarAlgebra.nonneg_iff_eq_star_mul_self, Iff.mp, rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosDef
hy : y.PosDef
have : ∀ (this : Fintype n), PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
have := Fintype.ofFinite n
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosDef
hy : y.PosDef
this : Fintype n
have : ∀ (this : Fintype m), PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
have := Fintype.ofFinite m
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosDef
hy : y.PosDef
this_1 : Fintype n
this : Fintype m
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
hx.posSemidef.kronecker hy.posSemidef |>.posDef_iff_isUnit.mpr <|
    hx.isUnit.kronecker hy.isUnit

Premises used: Iff.mpr, Matrix.PosSemidef.posDef_iff_isUnit, Matrix.PosDef.isUnit, Matrix.IsUnit.kronecker, Matrix.PosSemidef.kronecker, Matrix.PosDef.posSemidef
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosDef
hy : y.PosDef
this_1 : Fintype n
this : Fintype m
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
exact hx.posSemidef.kronecker hy.posSemidef |>.posDef_iff_isUnit.mpr <|
    hx.isUnit.kronecker hy.isUnit

Premises used: Iff.mpr, Matrix.PosSemidef.posDef_iff_isUnit, Matrix.PosDef.isUnit, Matrix.IsUnit.kronecker, Matrix.PosSemidef.kronecker, Matrix.PosDef.posSemidef
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
inst_1 : Finite n
m : Type u_3
inst_2 : Finite m
x : Matrix n n 𝕜
y : Matrix m m 𝕜
hx : x.PosDef
hy : y.PosDef
have have₁ have₂ have₃ : ∀ (this : Fintype n), PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have₄ : ∀ (this : Fintype n) (this : Fintype m), PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)

Tactic:
classical
  have := Fintype.ofFinite n; have := Fintype.ofFinite m
  exact hx.posSemidef.kronecker hy.posSemidef |>.posDef_iff_isUnit.mpr <|
    hx.isUnit.kronecker hy.isUnit
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
⊢ (A ⊙ B).PosSemidef

Tactic:
⟨hA.isHermitian.hadamard hB.isHermitian, fun x ↦ ?_⟩

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.hadamard, Matrix.PosSemidef, And.intro
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
refine :
  ∀ (x : ι →₀ 𝕜),
    LE.le (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
⊢ (A ⊙ B).PosSemidef

Tactic:
refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
⊢ PosSemidef (n := ↥x.support)
    (A.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))

Tactic:
have hAs := hA.submatrix ((↑) : x.support → ι)
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs :
  PosSemidef (n := ↥x.support)
    (A.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
⊢ PosSemidef (n := ↥x.support)
    (B.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))

Tactic:
have hBs := hB.submatrix ((↑) : x.support → ι)
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs :
  PosSemidef (n := ↥x.support)
    (A.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
hBs :
  PosSemidef (n := ↥x.support)
    (B.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
rw :
  IsHermitian (n := ↥x.support)
      (A.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
          (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)) ⊙
        B.submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
          (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))) ∧
    ∀ (x_1 : ↥x.support → 𝕜),
      0 ≤
        star x_1 ⬝ᵥ
          A.submatrix (Subtype.val (p := fun (x_2 : ι) ↦ x_2 ∈ x.support))
                (Subtype.val (p := fun (x_2 : ι) ↦ x_2 ∈ x.support)) ⊙
              B.submatrix (Subtype.val (p := fun (x_2 : ι) ↦ x_2 ∈ x.support))
                (Subtype.val (p := fun (x_2 : ι) ↦ x_2 ∈ x.support)) *ᵥ
            x_1
⊢ PosSemidef (n := ↥x.support)
    ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))

Tactic:
rw [submatrix_hadamard, posSemidef_iff_dotProduct_mulVec]

Premises used: Matrix.submatrix_hadamard, Matrix.posSemidef_iff_dotProduct_mulVec