awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)))
⊢ 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:
⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩

Premises used: Matrix.PosSemidef.isHermitian, Matrix.IsHermitian.hadamard, 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
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)))
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
⊢ 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:
refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩
-- 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)))
y : ↥x.support → 𝕜
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
⊢ 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:
rw [star_dotProduct_hadamard_mulVec_eq_kronecker]

Premises used: Matrix.star_dotProduct_hadamard_mulVec_eq_kronecker
-- 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)))
y : ↥x.support → 𝕜
⊢ 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:
(hAs.kronecker hBs).dotProduct_mulVec_nonneg _

Premises used: Matrix.PosSemidef.kronecker, Matrix.PosSemidef.dotProduct_mulVec_nonneg
-- 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)))
y : ↥x.support → 𝕜
⊢ 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:
exact (hAs.kronecker hBs).dotProduct_mulVec_nonneg _

Premises used: Matrix.PosSemidef.kronecker, Matrix.PosSemidef.dotProduct_mulVec_nonneg
-- 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 ⊙ 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 _
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
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:
simpa [Finsupp.sum, ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain] using hAB.2 _

Premises used: Finsupp.sum, Finset.subtype_mem_eq_attach, Finsupp.support, Finset.sum_attach, Finsupp.subtypeDomain_apply, Finsupp.support_subtypeDomain, And.right
-- 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)
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)
⊢ (A ⊙ B).PosSemidef

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 _

Premises used: Finsupp.sum, Finset.subtype_mem_eq_attach, Finsupp.subtypeDomain_apply, Finsupp.support_subtypeDomain
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
⊢ (A ⊙ B).PosDef

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

Premises used: Matrix.IsHermitian.hadamard, And.intro, Matrix.PosDef, Matrix.PosDef.isHermitian
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
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)
⊢ (A ⊙ B).PosDef

Tactic:
refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Matrix.Order
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.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
-- Module: Mathlib.Analysis.Matrix.Order
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)
    (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
-- Module: Mathlib.Analysis.Matrix.Order
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)))
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
⊢ 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)))

Tactic:
rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]

Premises used: Matrix.posDef_iff_dotProduct_mulVec, Matrix.submatrix_hadamard
-- Module: Mathlib.Analysis.Matrix.Order
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

Tactic:
⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩

Premises used: Matrix.IsHermitian.hadamard, And.intro, Matrix.PosDef.isHermitian
-- Module: Mathlib.Analysis.Matrix.Order
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)))
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
⊢ 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:
refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
-- Module: Mathlib.Analysis.Matrix.Order
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)))
y : ↥x.support → 𝕜
hy : y ≠ 0
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
⊢ 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:
rw [star_dotProduct_hadamard_mulVec_eq_kronecker]

Premises used: Matrix.star_dotProduct_hadamard_mulVec_eq_kronecker
-- Module: Mathlib.Analysis.Matrix.Order
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)))
y : ↥x.support → 𝕜
hy : y ≠ 0
⊢ (diagonal y).vec ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Matrix.Order
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)))
y : ↥x.support → 𝕜
hy : y ≠ 0
⊢ 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:
exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa

Premises used: Matrix.PosDef.kronecker, Matrix.PosDef.dotProduct_mulVec_pos
-- Module: Mathlib.Analysis.Matrix.Order
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)))

Tactic:
have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB :
  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)))
simp_rw :
  LT.lt.{u_1} (α := 𝕜) 0
    (∑ x_1 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x),
      ∑ x_2 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_2 : ι) ↦ x_2 ∈ x.support) x),
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜)
            ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
                ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_1 : 𝕜) :
              𝕜)
            (A (↑x_1 : ι) (↑x_2 : ι) * B (↑x_1 : ι) (↑x_2 : ι)))
          ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_2 : 𝕜))
⊢ LT.lt (α := 𝕜) 0 (x.sum fun (i : ι) (xi : 𝕜) ↦ x.sum fun (j : ι) (xj : 𝕜) ↦ star xi * (A ⊙ B) i j * xj)

Tactic:
simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]

Premises used: RCLike.star_def, Finsupp.sum, Finset.subtype_mem_eq_attach, Finsupp.support, Finset.sum_attach, Matrix.hadamard_apply, Finsupp.subtypeDomain_apply, Finsupp.support_subtypeDomain
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB :
  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)))
⊢ LT.lt.{u_1} (α := 𝕜) 0
    (∑ x_1 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x),
      ∑ x_2 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_2 : ι) ↦ x_2 ∈ x.support) x),
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜)
            ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
                ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_1 : 𝕜) :
              𝕜)
            (A (↑x_1 : ι) (↑x_2 : ι) * B (↑x_1 : ι) (↑x_2 : ι)))
          ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_2 : 𝕜))

Tactic:
hAB.2 ?_

Premises used: Matrix.submatrix, Finsupp.sum, Matrix.hadamard, And.right
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB :
  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)))
refine : Ne (α := Finsupp.{u_3, u_1} (↥x.support) 𝕜) (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x) 0
⊢ LT.lt.{u_1} (α := 𝕜) 0
    (∑ x_1 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x),
      ∑ x_2 ∈ Finsupp.support (Finsupp.subtypeDomain (fun (x_2 : ι) ↦ x_2 ∈ x.support) x),
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜)
            ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜)
                ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_1 : 𝕜) :
              𝕜)
            (A (↑x_1 : ι) (↑x_2 : ι) * B (↑x_1 : ι) (↑x_2 : ι)))
          ((Finsupp.subtypeDomain (fun (x_3 : ι) ↦ x_3 ∈ x.support) x : (a : ↥x.support) → 𝕜) x_2 : 𝕜))

Tactic:
refine hAB.2 ?_

Premises used: And.right
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB :
  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)))
⊢ Ne (α := Finsupp.{u_3, u_1} (↥x.support) 𝕜) (Finsupp.subtypeDomain (fun (x_1 : ι) ↦ x_1 ∈ x.support) x) 0

Tactic:
simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr hx

Premises used: Iff.mpr, Finsupp.support_nonempty_iff