awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → α
⊢ ‖replicateCol ι v‖₊ = nnnorm (E := WithLp 2 (n → α)) (toLp 2 v)

Tactic:
Subtype.ext <| frobenius_norm_replicateCol v

Premises used: Matrix.frobenius_norm_replicateCol, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
simp_rw :
  HPow.hPow (α := ℝ≥0) (∑ x : n × n, HPow.hPow (β := ℝ) ‖diagonal v x.1 x.2‖₊ 2) (1 / 2) =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2)
⊢ ‖diagonal v‖₊ = nnnorm (E := WithLp 2 (n → α)) (toLp 2 v)

Tactic:
simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ,
    PiLp.nnnorm_eq_of_L2]

Premises used: PiLp.nnnorm_eq_of_L2, Finset.univ_product_univ, Finset.sum_product', Matrix.frobenius_nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
rw :
  HPow.hPow (α := ℝ≥0) (∑ x ∈ s, HPow.hPow (β := ℝ) ‖diagonal v x.1 x.2‖₊ 2) (1 / 2) =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2)
rw₁ :
  ∀ (i : n × n) (_hi : Membership.mem (γ := Finset (n × n)) Finset.univ i) (his : i ∉ s),
    HPow.hPow (β := ℝ) ‖diagonal v i.1 i.2‖₊ 2 = 0
⊢ HPow.hPow (α := ℝ≥0) (∑ x : n × n, HPow.hPow (β := ℝ) ‖diagonal v x.1 x.2‖₊ 2) (1 / 2) =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2)

Tactic:
rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]

Premises used: Finset.sum_subset, Finset.subset_univ
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
rw :
  HPow.hPow (α := ℝ≥0)
      (∑ x : n,
        HPow.hPow (β := ℝ)
          ‖diagonal v (({ toFun := fun (i : n) ↦ (i, i), inj' := ⋯ : n ↪ n × n } : (a : n) → n × n) x).1
              (({ toFun := fun (i : n) ↦ (i, i), inj' := ⋯ : n ↪ n × n } : (a : n) → n × n) x).2‖₊
          2)
      (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2) (1 / 2)
⊢ HPow.hPow (α := ℝ≥0) (∑ x ∈ s, HPow.hPow (β := ℝ) ‖diagonal v x.1 x.2‖₊ 2) (1 / 2) =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2)

Tactic:
rw [Finset.sum_map, NNReal.sqrt_eq_rpow]

Premises used: NNReal.sqrt_eq_rpow, Finset.sum_map
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
dsimp :
  HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℝ) ‖diagonal v x x‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2) (1 / 2)
⊢ HPow.hPow (α := ℝ≥0)
      (∑ x : n,
        HPow.hPow (β := ℝ)
          ‖diagonal v (({ toFun := fun (i : n) ↦ (i, i), inj' := ⋯ : n ↪ n × n } : (a : n) → n × n) x).1
              (({ toFun := fun (i : n) ↦ (i, i), inj' := ⋯ : n ↪ n × n } : (a : n) → n × n) x).2‖₊
          2)
      (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2) (1 / 2)

Tactic:
dsimp
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
simp_rw :
  HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℝ) ‖v x‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2) (1 / 2)
⊢ HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℝ) ‖diagonal v x x‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ x : n, HPow.hPow (β := ℕ) ‖v x‖₊ 2) (1 / 2)

Tactic:
simp_rw [diagonal_apply_eq, NNReal.rpow_two]

Premises used: Matrix.diagonal_apply_eq, NNReal.rpow_two
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : Membership.mem (γ := Finset (n × n)) Finset.univ i
his : i ∉ s
this : i.1 ≠ i.2
rw : HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) 0) 2 = 0
rw₁ : HPow.hPow (α := ℝ≥0) (β := ℝ) 0 2 = 0
rw₂ rw₃ : Eq (α := ℝ≥0) 0 0
⊢ HPow.hPow (β := ℝ) ‖diagonal v i.1 i.2‖₊ 2 = 0

Tactic:
rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]

Premises used: NNReal.zero_rpow, two_ne_zero, nnnorm_zero, Matrix.diagonal_apply_ne
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : Membership.mem (γ := Finset (n × n)) Finset.univ i
his : i ∉ s
suffices : i.1 ≠ i.2
⊢ HPow.hPow (β := ℝ) ‖diagonal v i.1 i.2‖₊ 2 = 0

Tactic:
suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : Membership.mem (γ := Finset (n × n)) Finset.univ i
his : i ∉ s
h : i.1 = i.2
⊢ False

Tactic:
Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩

Premises used: Finset.mem_univ, Iff.not, Prod.fst, Prod.ext, And.intro, Exists.intro, Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map (α := n) { toFun := fun (i : n) ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : Membership.mem (γ := Finset (n × n)) Finset.univ i
his : i ∉ s
h : i.1 = i.2
⊢ False

Tactic:
exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩

Premises used: Finset.mem_univ, Iff.not, Prod.fst, Prod.ext, And.intro, Exists.intro, Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
⊢ ‖diagonal v‖ = norm (E := WithLp 2 (n → α)) (toLp 2 v)

Tactic:
(congr_arg ((↑) : ℝ≥0 → ℝ) <| frobenius_nnnorm_diagonal v :).trans rfl

Premises used: congr_arg, Matrix.frobenius_nnnorm_diagonal, NNReal.toReal, rfl, Eq.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : SeminormedAddCommGroup α
inst_3 : One α
⊢ nnnorm (E := Matrix n n α) (diagonal 1) = nnnorm (E := WithLp 2 (n → α)) (toLp 2 (Function.const n 1))

Tactic:
frobenius_nnnorm_diagonal _

Premises used: setOf, Matrix.frobenius_nnnorm_diagonal
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : SeminormedAddCommGroup α
inst_3 : One α
rw :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (HDiv.hDiv (α := ENNReal) 1 (OfNat.ofNat 2)).toReal *
      nnnorm.{u_5} (E := α) 1 =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑(Fintype.card n) : ℝ≥0) * nnnorm.{u_5} (E := α) 1
⊢ nnnorm (E := WithLp 2 (n → α)) (toLp 2 (Function.const n 1)) =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑(Fintype.card n) : ℝ≥0) * nnnorm.{u_5} (E := α) 1

Tactic:
rw [PiLp.nnnorm_toLp_const (ENNReal.ofNat_ne_top (n := 2))]

Premises used: ENNReal.ofNat_ne_top, PiLp.nnnorm_toLp_const
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : SeminormedAddCommGroup α
inst_3 : One α
⊢ HPow.hPow (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (HDiv.hDiv (α := ENNReal) 1 (OfNat.ofNat 2)).toReal *
      nnnorm.{u_5} (E := α) 1 =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑(Fintype.card n) : ℝ≥0) * nnnorm.{u_5} (E := α) 1

Tactic:
simp [NNReal.sqrt_eq_rpow]

Premises used: NNReal.sqrt_eq_rpow
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : SeminormedAddCommGroup α
inst_3 : One α
Matrix :
  nnnorm (E := WithLp 2 (n → α)) (toLp 2 (Function.const n 1)) =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑(Fintype.card n) : ℝ≥0) * nnnorm.{u_5} (E := α) 1
⊢ nnnorm (E := _root_.Matrix n n α) 1 =
    (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑(Fintype.card n) : ℝ≥0) * nnnorm.{u_5} (E := α) 1

Tactic:
calc
    ‖(diagonal 1 : Matrix n n α)‖₊
    _ = ‖toLp 2 (Function.const _ 1)‖₊ := frobenius_nnnorm_diagonal _
    _ = .sqrt (Fintype.card n) * ‖(1 : α)‖₊ := by
      rw [PiLp.nnnorm_toLp_const (ENNReal.ofNat_ne_top (n := 2))]
      simp [NNReal.sqrt_eq_rpow]

Premises used: WithLp.toLp, Matrix.frobenius_nnnorm_diagonal, Function.const, OfNat.ofNat, Matrix.diagonal
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : RCLike α
A : Matrix l m α
B : Matrix m n α
simp_rw :
  HPow.hPow (α := ℝ≥0) (∑ x : l, ∑ x_1 : n, HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) (∑ j : m, A x j * B j x_1)) 2)
      (1 / 2) ≤
    HPow.hPow (α := ℝ≥0) (∑ i : l, ∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2) *
      HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖B i j‖₊ 2) (1 / 2)
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Tactic:
simp_rw [frobenius_nnnorm_def, Matrix.mul_apply]

Premises used: Matrix.mul_apply, Matrix.frobenius_nnnorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : RCLike α
A : Matrix l m α
B : Matrix m n α
rw :
  HPow.hPow (α := ℝ≥0) (∑ x : l, ∑ x_1 : n, HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) (∑ j : m, A x j * B j x_1)) 2)
      (1 / 2) ≤
    HPow.hPow (α := ℝ≥0)
      (∑ i : l,
        ∑ j : n, HMul.hMul (α := ℝ≥0) (∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (∑ x : m, HPow.hPow (β := ℝ) ‖B x j‖₊ 2))
      (1 / 2)
⊢ HPow.hPow (α := ℝ≥0) (∑ x : l, ∑ x_1 : n, HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) (∑ j : m, A x j * B j x_1)) 2)
      (1 / 2) ≤
    HPow.hPow (α := ℝ≥0) (∑ i : l, ∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2) *
      HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖B i j‖₊ 2) (1 / 2)

Tactic:
rw [← NNReal.mul_rpow, @Finset.sum_comm _ _ m, Finset.sum_mul_sum]

Premises used: Finset.sum_comm, NNReal.mul_rpow, Finset.sum_mul_sum
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : RCLike α
A : Matrix l m α
B : Matrix m n α
h₁ :
  ∀ (i : l),
    Membership.mem (γ := Finset l) Finset.univ i →
      ∀ (j : n),
        Membership.mem (γ := Finset n) Finset.univ j →
          HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) (∑ j_1 : m, A i j_1 * B j_1 j)) 2 ≤
            HMul.hMul (α := ℝ≥0) (∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (∑ x : m, HPow.hPow (β := ℝ) ‖B x j‖₊ 2)
⊢ HPow.hPow (α := ℝ≥0) (∑ x : l, ∑ x_1 : n, HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) (∑ j : m, A x j * B j x_1)) 2)
      (1 / 2) ≤
    HPow.hPow (α := ℝ≥0)
      (∑ i : l,
        ∑ j : n, HMul.hMul (α := ℝ≥0) (∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (∑ x : m, HPow.hPow (β := ℝ) ‖B x j‖₊ 2))
      (1 / 2)

Tactic:
gcongr with i _ j
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
h : Membership.mem (γ := Finset l) Finset.univ i
j : n
h_1 : Membership.mem (γ := Finset n) Finset.univ j
h₁ :
  nnnorm.{u_5} (E := α) (∑ j_1 : m, A i j_1 * B j_1 j) ≤
    HPow.hPow (α := ℝ≥0) (∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2) *
      HPow.hPow (α := ℝ≥0) (∑ x : m, HPow.hPow (β := ℝ) ‖B x j‖₊ 2) (1 / 2)
⊢ HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) (∑ j_1 : m, A i j_1 * B j_1 j)) 2 ≤
    HMul.hMul (α := ℝ≥0) (∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (∑ x : m, HPow.hPow (β := ℝ) ‖B x j‖₊ 2)

Tactic:
rw [← NNReal.rpow_le_rpow_iff one_half_pos, ← NNReal.rpow_mul,
    mul_div_cancel₀ (1 : ℝ) two_ne_zero, NNReal.rpow_one, NNReal.mul_rpow]

Premises used: NNReal.rpow_mul, mul_div_cancel₀, two_ne_zero, one_half_pos, OfNat.ofNat, NNReal.rpow_one, NNReal.mul_rpow, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
h : Membership.mem (γ := Finset l) Finset.univ i
j : n
h_1 : Membership.mem (γ := Finset n) Finset.univ j
⊢ nnnorm.{u_5} (E := α) (∑ j_1 : m, A i j_1 * B j_1 j) ≤
    HPow.hPow (α := ℝ≥0) (∑ j : m, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2) *
      HPow.hPow (α := ℝ≥0) (∑ x : m, HPow.hPow (β := ℝ) ‖B x j‖₊ 2) (1 / 2)

Tactic:
simpa only [PiLp.toLp_apply, PiLp.inner_apply, RCLike.inner_apply', starRingEnd_apply,
    Pi.nnnorm_def, PiLp.nnnorm_eq_of_L2, star_star, nnnorm_star, NNReal.sqrt_eq_rpow,
    NNReal.rpow_two] using nnnorm_inner_le_nnnorm (𝕜 := α) (toLp 2 (star <| A i ·)) (toLp 2 (B · j))

Premises used: RCLike.inner_apply', star_star, NNReal.sqrt_eq_rpow, PiLp.nnnorm_eq_of_L2, nnnorm_star, WithLp.toLp, NNReal.rpow_two, starRingEnd_apply, nnnorm_inner_le_nnnorm, PiLp.toLp_apply, Pi.nnnorm_def, PiLp.inner_apply, OfNat.ofNat, Star.star
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖ ≤ ‖A‖ * ‖B‖

Tactic:
frobenius_nnnorm_mul A B

Premises used: Matrix.frobenius_nnnorm_mul, setOf
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A B : Matrix n n 𝕜
⊢ A ≤ B ↔ (B - A).PosSemidef

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
rw : (A - 0).PosSemidef ↔ A.PosSemidef
rw₁ rw₂ : A.PosSemidef ↔ A.PosSemidef
⊢ 0 ≤ A ↔ A.PosSemidef

Tactic:
rw [le_iff, sub_zero]

Premises used: Matrix.le_iff, sub_zero
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
a : ∀ (i j : n), A i j = 0 i j
⊢ A = 0

Tactic:
ext i j
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i_1 j i : n
⊢ A i i ≤ 0

Tactic:
simpa using h₂.diag_nonneg

Premises used: Matrix.PosSemidef.diag_nonneg
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i_1 j i : n
⊢ 0 ≤ A i i

Tactic:
simpa using h₁.diag_nonneg

Premises used: Matrix.PosSemidef.diag_nonneg
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
⊢ ∀ (i : n), A i i = 0

Tactic:
have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
hdiag : ∀ (i : n), A i i = 0
⊢ LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * A i_1 j * xj)

Tactic:
have h1 := h₁.2 (.single i 1 + .single j (A j i))
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
hdiag : ∀ (i : n), A i i = 0
h1 :
  LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * A i_1 j * xj)
⊢ LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * (-A) i_1 j * xj)

Tactic:
have h2 := h₂.2 (.single i 1 + .single j (A j i))
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
hdiag : ∀ (i : n), A i i = 0
h1 :
  LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * A i_1 j * xj)
h2 :
  LE.le (α := 𝕜) 0
    ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
      (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
        star xi * (-A) i_1 j * xj)
a :
  ∀ (hdiag : True) (h1 : 0 ≤ A i j * star (A i j) + A i j * star (A i j))
    (h2 : A i j * star (A i j) + A i j * star (A i j) ≤ 0), A i j = 0
⊢ A i j = 0 i j

Tactic:
simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *

Premises used: neg_add_rev, add_mul, RCLike.star_def, Matrix.IsHermitian.apply, And.left, mul_add, Finsupp.sum_add_index
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
hdiag : True
h1 : 0 ≤ A i j * star (A i j) + A i j * star (A i j)
h2 : A i j * star (A i j) + A i j * star (A i j) ≤ 0
⊢ A i j = 0

Tactic:
simpa using le_antisymm h2 h1

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
a : ∀ (i j : n), A i j = 0 i j
a₁ : ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0), A i j = 0 i j
a₂ :
  ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0)
    (h1 :
      LE.le (α := 𝕜) 0
        ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
          (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
            star xi * A i_1 j * xj)),
    A i j = 0 i j
a₃ :
  ∀ (i j : n) (hdiag : ∀ (i : n), A i i = 0)
    (h1 :
      LE.le (α := 𝕜) 0
        ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
          (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
            star xi * A i_1 j * xj))
    (h2 :
      LE.le (α := 𝕜) 0
        ((HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (i_1 : n) (xi : 𝕜) ↦
          (HAdd.hAdd (α := n →₀ 𝕜) (Finsupp.single i 1) (Finsupp.single j (A j i))).sum fun (j : n) (xj : 𝕜) ↦
            star xi * (-A) i_1 j * xj)),
    A i j = 0 i j
a₄ :
  ∀ (i j : n) (hdiag : True) (h1 : 0 ≤ A i j * star (A i j) + A i j * star (A i j))
    (h2 : A i j * star (A i j) + A i j * star (A i j) ≤ 0), A i j = 0
⊢ A = 0

Tactic:
classical
  ext i j
  have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
  have h1 := h₁.2 (.single i 1 + .single j (A j i))
  have h2 := h₂.2 (.single i 1 + .single j (A j i))
  simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
  simpa using le_antisymm h2 h1

Premises used: neg_add_rev, add_mul, RCLike.star_def, mul_add, Finsupp.sum_add_index
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A B : Matrix n n 𝕜
h₁ : A ≤ B
h₂ : B ≤ A
⊢ (-(B - A)).PosSemidef

Tactic:
simpa only [← neg_sub B, le_iff] using h₂

Premises used: Matrix.le_iff, neg_sub
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A B : Matrix n n 𝕜
h₁ : A ≤ B
h₂ : B ≤ A
⊢ A = B

Tactic:
simpa [sub_eq_zero, eq_comm] using le_antisymm_aux h₁
     (by simpa only [← neg_sub B, le_iff] using h₂)

Premises used: sub_eq_zero, eq_comm, _private.0.Matrix.le_antisymm_aux
-- Module: Mathlib.Analysis.Matrix.Order
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
x x_1 : Matrix n n 𝕜
h : x ≤ x_1
x_2 : Matrix n n 𝕜
rwa : (x_1 + x_2 - (x + x_2)).PosSemidef
rwa₁ rwa₂ rwa₃ rwa₄ : (x_1 - x).PosSemidef
⊢ x + x_2 ≤ x_1 + x_2

Tactic:
rwa [le_iff, add_sub_add_right_eq_sub]

Premises used: Matrix.le_iff, add_sub_add_right_eq_sub
-- 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
simp : ∀ a ∈ spectrum ℝ A, 0 ≤ a
⊢ ∀ x ∈ quasispectrum ℝ A, 0 ≤ x

Tactic:
simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff,
      forall_eq_or_imp, le_refl, true_and]

Premises used: le_refl, Real, forall_eq_or_imp, Set.mem_insert_iff, quasispectrum_eq_spectrum_union_zero, Set.union_singleton, true_and
-- 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
x : ℝ
hx : x ∈ spectrum ℝ A
obtain : ∀ (i : n) (hx : ⋯.eigenvalues i ∈ spectrum ℝ A), 0 ≤ ⋯.eigenvalues i
⊢ 0 ≤ x

Tactic:
obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx

Premises used: Matrix.LE.le.posSemidef, And.left, Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues, Iff.mp, Set.ext_iff, 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
i : n
hx : ⋯.eigenvalues i ∈ spectrum ℝ A
⊢ 0 ≤ ⋯.eigenvalues i

Tactic:
hA.posSemidef.eigenvalues_nonneg _

Premises used: Matrix.LE.le.posSemidef, Matrix.PosSemidef.eigenvalues_nonneg
-- 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
i : n
hx : ⋯.eigenvalues i ∈ spectrum ℝ A
⊢ 0 ≤ ⋯.eigenvalues i

Tactic:
exact hA.posSemidef.eigenvalues_nonneg _

Premises used: Matrix.LE.le.posSemidef, Matrix.PosSemidef.eigenvalues_nonneg
-- 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
simp simp₁ : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ A), 0 ≤ x
simp₂ : ∀ (i : n) (hx : ⋯.eigenvalues i ∈ spectrum ℝ A), 0 ≤ ⋯.eigenvalues i
⊢ ∀ x ∈ quasispectrum ℝ A, 0 ≤ x

Tactic:
classical
    simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff,
      forall_eq_or_imp, le_refl, true_and]
    intro x hx
    obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx
    exact hA.posSemidef.eigenvalues_nonneg _

Premises used: le_refl, forall_eq_or_imp, Set.mem_insert_iff, Set.union_singleton, rfl, true_and
-- 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:
obtain ⟨X, hX, -, rfl⟩ :=
        sub_zero A ▸ CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hA.isHermitian
          (QuasispectrumRestricts.nnreal_of_nonneg hA.nonneg)

Premises used: rfl
-- 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:
⟨X, hX.star_eq.symm ▸ rfl⟩

Premises used: Eq.rec, Exists.intro, Eq.symm, IsSelfAdjoint.star_eq, rfl