awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
inr inr₁ inr₂ : ∑ j : n, ‖A i j‖₊ ≤ N
inr₃ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1), ∑ j : n, ‖A i j‖₊ ≤ N
inr₄ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      nnnorm (E := m → α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
        N * ‖x‖₊),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₅ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      ∀ (b : m),
        Membership.mem (γ := Finset m) Finset.univ b →
          nnnorm.{u_5} (E := α)
              (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x b : α) ≤
            N),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₆ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      nnnorm.{u_5} (E := α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x i : α) ≤
        N),
    ∑ j : n, ‖A i j‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have inr₇ : let x : n → α := fun (j : n) ↦ unitOf (A i j);
∀ (hxn : ‖x‖₊ = 1) (hN : nnnorm.{u_5} (E := α) (∑ i_1 : n, A i i_1 * x i_1) ≤ N), ∑ j : n, ‖A i j‖₊ ≤ N
Tactic: classical
  let x : n → α := fun j => unitOf (A i j)
  have hxn : ‖x‖₊ = 1 := by
    simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
  specialize hN x
  rw [hxn, mul_one, Pi.nnnorm_def, Finset.sup_le_iff] at hN
  replace hN := hN i (Finset.mem_univ _)
  dsimp [mulVec, dotProduct] at hN
  simp_rw [x, mul_unitOf, ← map_sum, nnnorm_algebraMap, ← NNReal.coe_sum, NNReal.nnnorm_eq,
    nnnorm_one, mul_one] at hN
  exact hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN :
  ∀ (x : n → α),
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
inr inr₁ inr₂ : ∑ j : n, ‖A i j‖₊ ≤ N
inr₃ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1), ∑ j : n, ‖A i j‖₊ ≤ N
inr₄ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      nnnorm (E := m → α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
        N * ‖x‖₊),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₅ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      ∀ (b : m),
        Membership.mem (γ := Finset m) Finset.univ b →
          nnnorm.{u_5} (E := α)
              (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x b : α) ≤
            N),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₆ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1)
    (hN :
      nnnorm.{u_5} (E := α)
          (({ toLinearMap := A.mulVecLin, cont := ⋯ : (n → α) →L[α] m → α } : (a : n → α) → m → α) x i : α) ≤
        N),
    ∑ j : n, ‖A i j‖₊ ≤ N
inr₇ :
  let x : n → α := fun (j : n) ↦ unitOf (A i j);
  ∀ (hxn : ‖x‖₊ = 1) (hN : nnnorm.{u_5} (E := α) (∑ i_1 : n, A i i_1 * x i_1) ≤ N), ∑ j : n, ‖A i j‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have inr₈ : let x : n → α := fun (j : n) ↦ unitOf (A i j);
∀ (hxn : ‖x‖₊ = 1) (hN : ∑ i_1 : n, ‖A i i_1‖₊ ≤ N), ∑ j : n, ‖A i j‖₊ ≤ N
Tactic: classical
  let x : n → α := fun j => unitOf (A i j)
  have hxn : ‖x‖₊ = 1 := by
    simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
  specialize hN x
  rw [hxn, mul_one, Pi.nnnorm_def, Finset.sup_le_iff] at hN
  replace hN := hN i (Finset.mem_univ _)
  dsimp [mulVec, dotProduct] at hN
  simp_rw [x, mul_unitOf, ← map_sum, nnnorm_algebraMap, ← NNReal.coe_sum, NNReal.nnnorm_eq,
    nnnorm_one, mul_one] at hN
  exact hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : NontriviallyNormedField α
inst_3 : NormedAlgebra ℝ α
inst_4 : DecidableEq n
f : (n → α) →L[α] m → α
⊢ nnnorm (E := Matrix m n α)
      ((LinearMap.toMatrix' : (a : (n → α) →ₗ[α] m → α) → Matrix m n α) (↑f : (n → α) →ₗ[α] m → α) : Matrix m n α) =
    ‖f‖₊
have rw : nnnorm (E := (n → α) →L[α] m → α)
    {
      toLinearMap :=
        mulVecLin ((LinearMap.toMatrix' : (a : (n → α) →ₗ[α] m → α) → Matrix m n α) (↑f : (n → α) →ₗ[α] m → α)),
      cont := sorry : (n → α) →L[α] m → α } =
  ‖f‖₊
Tactic: rw [linfty_opNNNorm_eq_opNNNorm]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖₊ = HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
have change : nnnorm (E := WithLp 2 ((i : m) → WithLp 2 ((j : n) → α))) (toLp 2 fun (i : m) ↦ toLp 2 fun (j : n) ↦ A i j) =
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
Tactic: change ‖toLp 2 fun i => toLp 2 fun j => A i j‖₊ = _
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ nnnorm (E := WithLp 2 ((i : m) → WithLp 2 ((j : n) → α))) (toLp 2 fun (i : m) ↦ toLp 2 fun (j : n) ↦ A i j) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
have simp_rw : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0)
    (∑ x : m,
      HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2)) 2) =
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
Tactic: simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
simp_rw :
  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0)
      (∑ x : m,
        HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2))
          2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
⊢ nnnorm (E := WithLp 2 ((i : m) → WithLp 2 ((j : n) → α))) (toLp 2 fun (i : m) ↦ toLp 2 fun (j : n) ↦ A i j) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
have simp_rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x : m, ∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2) =
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
Tactic: simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
simp_rw :
  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0)
      (∑ x : m,
        HPow.hPow (α := ℝ≥0) (β := ℕ) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2))
          2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
simp_rw₁ :
  (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (∑ x : m, ∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
⊢ nnnorm (E := WithLp 2 ((i : m) → WithLp 2 ((j : n) → α))) (toLp 2 fun (i : m) ↦ toLp 2 fun (j : n) ↦ A i j) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
have simp_rw₂ : HPow.hPow (α := ℝ≥0) (∑ x : m, ∑ x_1 : n, HPow.hPow (β := ℕ) ‖A x x_1‖₊ 2) (1 / 2) =
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
Tactic: simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
⊢ ‖A.map f‖₊ = ‖A‖₊
have simp_rw : HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A.map f i j‖₊ 2) (1 / 2) =
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
Tactic: simp_rw [frobenius_nnnorm_def, Matrix.map_apply, hf]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
A : Matrix m n α
f : α → β
hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊
simp_rw :
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A.map f i j‖₊ 2) (1 / 2) =
    HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
⊢ ‖A.map f‖₊ = ‖A‖₊
have simp_rw₁ : HPow.hPow (α := ℝ≥0) (∑ x : m, ∑ x_1 : n, HPow.hPow (β := ℝ) ‖f (A x x_1)‖₊ 2) (1 / 2) =
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
Tactic: simp_rw [frobenius_nnnorm_def, Matrix.map_apply, hf]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖Aᵀ‖₊ = ‖A‖₊
have rw : HPow.hPow (α := ℝ≥0) (∑ y : m, ∑ x : n, HPow.hPow (β := ℝ) ‖Aᵀ x y‖₊ 2) (1 / 2) =
  HPow.hPow (α := ℝ≥0) (∑ i : m, ∑ j : n, HPow.hPow (β := ℝ) ‖A i j‖₊ 2) (1 / 2)
Tactic: rw [frobenius_nnnorm_def, frobenius_nnnorm_def, Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
⊢ ‖replicateRow ι v‖ = norm (E := WithLp 2 (m → α)) (toLp 2 v)
have rw : HPow.hPow (α := ℝ) (∑ j : m, HPow.hPow (β := ℝ) ‖replicateRow ι v default j‖ 2) (1 / 2) =
  HPow.hPow (α := ℝ) (∑ i : m, HPow.hPow (β := ℕ) ‖ofLp (p := 2) (toLp 2 v) i‖ 2) (1 / 2)
Tactic: rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = nnnorm (E := WithLp 2 (n → α)) (toLp 2 v)
have 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)
Tactic: simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ,
    PiLp.nnnorm_eq_of_L2]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ 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)
have 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)
Tactic: rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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)
⊢ 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)
have 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
Tactic: rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ 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)
have rw : HPow.hPow (α := ℝ≥0)
    (∑ x : n,
      HPow.hPow (β := ℝ)
        ‖diagonal v (({ toFun := fun (i : n) ↦ (i, i), inj' := sorry : n ↪ n × n } : (a : n) → n × n) x).1
            (({ toFun := fun (i : n) ↦ (i, i), inj' := sorry : 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: rw [Finset.sum_map, NNReal.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [diagonal_apply_eq, NNReal.rpow_two]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ HPow.hPow (β := ℝ) ‖diagonal v i.1 i.2‖₊ 2 = 0
have rw : HPow.hPow (β := ℝ) (nnnorm.{u_5} (E := α) 0) 2 = 0
Tactic: rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ HPow.hPow (β := ℝ) ‖diagonal v i.1 i.2‖₊ 2 = 0
have rw₁ : HPow.hPow (α := ℝ≥0) (β := ℝ) 0 2 = 0
Tactic: rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ HPow.hPow (β := ℝ) ‖diagonal v i.1 i.2‖₊ 2 = 0
have rw₂ : Eq (α := ℝ≥0) 0 0
Tactic: rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ HPow.hPow (β := ℝ) ‖diagonal v i.1 i.2‖₊ 2 = 0
have suffices : i.1 ≠ i.2
Tactic: suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : SeminormedAddCommGroup α
inst_3 : One α
⊢ 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
have 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
Tactic: rw [PiLp.nnnorm_toLp_const (ENNReal.ofNat_ne_top (n := 2))]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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 α) 1 = (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑(Fintype.card n) : ℝ≥0) * nnnorm.{u_5} (E := α) 1
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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‖₊
have 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)
Tactic: simp_rw [frobenius_nnnorm_def, Matrix.mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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 α
⊢ 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)
have 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)
Tactic: rw [← NNReal.mul_rpow, @Finset.sum_comm _ _ m, Finset.sum_mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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 α
⊢ 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)
have 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)
Tactic: gcongr with i _ j
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
⊢ 0 ≤ A ↔ A.PosSemidef
have rw : (A - 0).PosSemidef ↔ A.PosSemidef
Tactic: rw [le_iff, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
rw : (A - 0).PosSemidef ↔ A.PosSemidef
⊢ 0 ≤ A ↔ A.PosSemidef
have rw₁ : A.PosSemidef ↔ A.PosSemidef
Tactic: rw [le_iff, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (goal)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
⊢ A = 0
have a : ∀ (i j : n), A i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_2
inst : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
⊢ A i j = 0 i j
have hdiag : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Order (hypothesis)
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
⊢ A i j = 0 i j
have 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)
Tactic: have h1 := h₁.2 (.single i 1 + .single j (A j i))