awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ v = 0
have rw₃ : yᴴ *ᵥ 0 = 0
Tactic: rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ v = 0
have rw₄ : Eq (α := n → 𝕜) 0 0
Tactic: rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h),
    mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have : ∀ (this : Fintype n), PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
Tactic: have := Fintype.ofFinite n
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have : ∀ (this : Fintype m), PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
Tactic: have := Fintype.ofFinite m
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have obtain : ∀ (a : Matrix n n 𝕜) (hx : (star a * a).PosSemidef),
  PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) y)
Tactic: obtain ⟨a, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) y)
have obtain : ∀ (b : Matrix m m 𝕜) (hy : (star b * b).PosSemidef),
  PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) (star a * a) (star b * b))
Tactic: obtain ⟨b, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hy.nonneg
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have : ∀ (this : Fintype n), 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 _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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)
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have₄ : ∀ (this : Fintype n) (this : Fintype m), 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 _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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)
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have 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)
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 _
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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)
⊢ PosSemidef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have 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))
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 _
Cleared hypotheses: x, y, hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have : ∀ (this : Fintype n), PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
Tactic: have := Fintype.ofFinite n
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have : ∀ (this : Fintype m), PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
Tactic: have := Fintype.ofFinite m
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have : ∀ (this : Fintype n), 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
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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)
⊢ PosDef (R := 𝕜) (kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2) x y)
have have₄ : ∀ (this : Fintype n) (this : Fintype m), 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
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
⊢ (A ⊙ B).PosSemidef
have refine : ∀ (x : ι →₀ 𝕜), LE.le (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
Tactic: refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
⊢ 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)))
have 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)))
Tactic: have hAs := hA.submatrix ((↑) : x.support → ι)
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
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)
    ((A ⊙ B).submatrix (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support))
      (Subtype.val (p := fun (x_1 : ι) ↦ x_1 ∈ x.support)))
have 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)))
Tactic: have hBs := hB.submatrix ((↑) : x.support → ι)
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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)))
⊢ 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)))
have 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
Tactic: rw [submatrix_hadamard, posSemidef_iff_dotProduct_mulVec]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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)))
⊢ 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
have refine : ∀ (y : ↥x.support → 𝕜),
  0 ≤
    star y ⬝ᵥ
      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)) *ᵥ
        y
Tactic: refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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)))
y : ↥x.support → 𝕜
⊢ 0 ≤
    star y ⬝ᵥ
      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)) *ᵥ
        y
have rw : 0 ≤
  star (diagonal y).vec ⬝ᵥ
    kroneckerMap (fun (x1 x2 : 𝕜) ↦ x1 * x2)
        (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))) *ᵥ
      (diagonal y).vec
Tactic: rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
⊢ LE.le (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
have hAB : 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: have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosSemidef := by
    have hAs := hA.submatrix ((↑) : x.support → ι)
    have hBs := hB.submatrix ((↑) : x.support → ι)
    rw [submatrix_hadamard, posSemidef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
⊢ (A ⊙ B).PosSemidef
have refine : ∀ (x : ι →₀ 𝕜), LE.le (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
Tactic: classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosSemidef := by
    have hAs := hA.submatrix ((↑) : x.support → ι)
    have hBs := hB.submatrix ((↑) : x.support → ι)
    rw [submatrix_hadamard, posSemidef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_nonneg _
  simpa [Finsupp.sum, ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain] using hAB.2 _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
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
have refine₁ : ∀ (x : ι →₀ 𝕜)
  (hAB :
    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)))),
  LE.le (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
Tactic: classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosSemidef := by
    have hAs := hA.submatrix ((↑) : x.support → ι)
    have hBs := hB.submatrix ((↑) : x.support → ι)
    rw [submatrix_hadamard, posSemidef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_nonneg _
  simpa [Finsupp.sum, ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain] using hAB.2 _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
⊢ (A ⊙ B).PosDef
have refine : ∀ (x : ι →₀ 𝕜) (hx : x ≠ 0),
  LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)
Tactic: refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
⊢ PosDef (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)))
have hAs : PosDef (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 : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs :
  PosDef (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)))
⊢ PosDef (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)))
have hBs : PosDef (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 : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs :
  PosDef (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 :
  PosDef (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)))
⊢ PosDef (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)))
have 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 → 𝕜⦄,
    x_1 ≠ 0 →
      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
Tactic: rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs :
  PosDef (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 :
  PosDef (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)))
⊢ 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 → 𝕜⦄,
      x_1 ≠ 0 →
        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
have refine : ∀ (y : ↥x.support → 𝕜) (hy : y ≠ 0),
  0 <
    star y ⬝ᵥ
      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)) *ᵥ
        y
Tactic: refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩