awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.sup Finset.univ fun (i : l) ↦ ∑ x : n, nnnorm.{u_5} (E := α) (∑ j : m, A i j * B j x)) ≤
    HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊)
      (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
have fun : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ k : n, ∑ j : m, ‖A i j‖₊ * ‖B j k‖₊)
  (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
Tactic: calc
    (Finset.univ.sup fun i => ∑ k, ‖∑ j, A i j * B j k‖₊) ≤
        Finset.univ.sup fun i => ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ :=
      Finset.sup_mono_fun fun i _hi =>
        Finset.sum_le_sum fun k _hk => nnnorm_sum_le_of_le _ fun j _hj => nnnorm_mul_le _ _
    _ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ := by
      simp_rw [@Finset.sum_comm m, Finset.mul_sum]
    _ ≤ Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
      refine Finset.sup_mono_fun fun i _hi => ?_
      gcongr with j hj
      exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
    _ ≤ (Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
      simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
      rfl
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
fun :
  Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ k : n, ∑ j : m, ‖A i j‖₊ * ‖B j k‖₊)
    (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
⊢ (Finset.sup Finset.univ fun (i : l) ↦ ∑ x : n, nnnorm.{u_5} (E := α) (∑ j : m, A i j * B j x)) ≤
    HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊)
      (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
have fun₁ : LE.le (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
  (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
Tactic: calc
    (Finset.univ.sup fun i => ∑ k, ‖∑ j, A i j * B j k‖₊) ≤
        Finset.univ.sup fun i => ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ :=
      Finset.sup_mono_fun fun i _hi =>
        Finset.sum_le_sum fun k _hk => nnnorm_sum_le_of_le _ fun j _hj => nnnorm_mul_le _ _
    _ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ := by
      simp_rw [@Finset.sum_comm m, Finset.mul_sum]
    _ ≤ Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
      refine Finset.sup_mono_fun fun i _hi => ?_
      gcongr with j hj
      exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
    _ ≤ (Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
      simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
      rfl
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
fun :
  Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ k : n, ∑ j : m, ‖A i j‖₊ * ‖B j k‖₊)
    (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
fun₁ :
  LE.le (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
    (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
⊢ (Finset.sup Finset.univ fun (i : l) ↦ ∑ x : n, nnnorm.{u_5} (E := α) (∑ j : m, A i j * B j x)) ≤
    HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊)
      (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
have fun₂ : (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊) ≤
  HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊)
    (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
Tactic: calc
    (Finset.univ.sup fun i => ∑ k, ‖∑ j, A i j * B j k‖₊) ≤
        Finset.univ.sup fun i => ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ :=
      Finset.sup_mono_fun fun i _hi =>
        Finset.sum_le_sum fun k _hk => nnnorm_sum_le_of_le _ fun j _hj => nnnorm_mul_le _ _
    _ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ := by
      simp_rw [@Finset.sum_comm m, Finset.mul_sum]
    _ ≤ Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
      refine Finset.sup_mono_fun fun i _hi => ?_
      gcongr with j hj
      exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
    _ ≤ (Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ := by
      simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
      rfl
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
l : Type u_2
m : Type u_3
α : Type u_5
inst : Fintype l
inst_1 : Fintype m
inst_2 : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊
have rw : nnnorm (E := Matrix l (Fin 1) α) (replicateCol (Fin 1) (A *ᵥ v)) ≤
  ‖A‖₊ * nnnorm (E := Matrix m (Fin 1) α) (replicateCol (Fin 1) v)
Tactic: rw [← linfty_opNNNorm_replicateCol (ι := Fin 1) (A *ᵥ v),
    ← linfty_opNNNorm_replicateCol v (ι := Fin 1)]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
⊢ ‖unitOf a‖₊ = 1
have rw : ‖if a = 0 then 1 else ‖a‖ • a⁻¹‖₊ = 1
Tactic: rw [unitOf]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
⊢ ‖if a = 0 then 1 else ‖a‖ • a⁻¹‖₊ = 1
have pos : ∀ (h : a = 0), nnnorm.{u_5} (E := α) 1 = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
pos : ∀ (h : a = 0), nnnorm.{u_5} (E := α) 1 = 1
⊢ ‖if a = 0 then 1 else ‖a‖ • a⁻¹‖₊ = 1
have neg : ∀ (h : ¬a = 0), ‖‖a‖ • a⁻¹‖₊ = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (hypothesis)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ ‖‖a‖ • a⁻¹‖₊ = 1
have h₁ : ¬‖a‖₊ = 0
Tactic: rw [← nnnorm_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬‖a‖₊ = 0
⊢ ‖‖a‖ • a⁻¹‖₊ = 1
have neg : ‖‖a‖‖₊ * ‖a⁻¹‖₊ = 1
Tactic: rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬‖a‖₊ = 0
neg : ‖‖a‖‖₊ * ‖a⁻¹‖₊ = 1
⊢ ‖‖a‖ • a⁻¹‖₊ = 1
have neg₁ : ‖‖a‖‖₊ * ‖a‖₊⁻¹ = 1
Tactic: rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬‖a‖₊ = 0
neg : ‖‖a‖‖₊ * ‖a⁻¹‖₊ = 1
neg₁ : ‖‖a‖‖₊ * ‖a‖₊⁻¹ = 1
⊢ ‖‖a‖ • a⁻¹‖₊ = 1
have neg₂ : ‖a‖₊ * ‖a‖₊⁻¹ = 1
Tactic: rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬‖a‖₊ = 0
neg : ‖‖a‖‖₊ * ‖a⁻¹‖₊ = 1
neg₁ : ‖‖a‖‖₊ * ‖a‖₊⁻¹ = 1
neg₂ : ‖a‖₊ * ‖a‖₊⁻¹ = 1
⊢ ‖‖a‖ • a⁻¹‖₊ = 1
have neg₃ : Eq (α := ℝ≥0) 1 1
Tactic: rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
⊢ a * unitOf a = (algebraMap ℝ α : (a : ℝ) → α) (↑‖a‖₊ : ℝ)
have simp : (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
Tactic: simp only [unitOf, coe_nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
⊢ (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
have pos : ∀ (h : a = 0), a * 1 = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
pos : ∀ (h : a = 0), a * 1 = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
⊢ (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
have neg : ∀ (h : ¬a = 0), a * ‖a‖ • a⁻¹ = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ a * ‖a‖ • a⁻¹ = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
have neg : ‖a‖ • (a * a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
Tactic: rw [mul_smul_comm, mul_inv_cancel₀ h, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬a = 0
neg : ‖a‖ • (a * a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
⊢ a * ‖a‖ • a⁻¹ = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
have neg₁ : HSMul.hSMul (β := α) ‖a‖ 1 = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
Tactic: rw [mul_smul_comm, mul_inv_cancel₀ h, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬a = 0
neg : ‖a‖ • (a * a⁻¹) = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
neg₁ : HSMul.hSMul (β := α) ‖a‖ 1 = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
⊢ a * ‖a‖ • a⁻¹ = (algebraMap ℝ α : (a : ℝ) → α) ‖a‖
have neg₂ : HSMul.hSMul (β := α) ‖a‖ 1 = HSMul.hSMul (β := α) ‖a‖ 1
Tactic: rw [mul_smul_comm, mul_inv_cancel₀ h, Algebra.algebraMap_eq_smul_one]
-- 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 α
⊢ ‖A‖₊ = nnnorm (E := (n → α) →L[α] m → α) { toLinearMap := A.mulVecLin, cont := ⋯ }
have rw : ∀ (N : ℝ≥0)
  (hN :
    ∀ (x : n → α),
      nnnorm (E := m → α)
          (({ toLinearMap := A.mulVecLin, cont := sorry : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
        N * ‖x‖₊),
  ‖A‖₊ ≤ N
Tactic: rw [ContinuousLinearMap.opNNNorm_eq_of_bounds _ (linfty_opNNNorm_mulVec _) fun N 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‖₊
⊢ ‖A‖₊ ≤ N
have rw : (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) ≤ N
Tactic: rw [linfty_opNNNorm_def]
-- 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‖₊
⊢ (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) ≤ N
have refine : ∀ (i : m), Membership.mem (γ := Finset m) Finset.univ i → ∑ j : n, ‖A i j‖₊ ≤ N
Tactic: refine Finset.sup_le fun i _ => ?_
-- 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
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have inl : IsEmpty n → ∑ j : n, ‖A i j‖₊ ≤ N
Tactic: cases isEmpty_or_nonempty n
-- 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
inl : IsEmpty n → ∑ j : n, ‖A i j‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have inr : Nonempty n → ∑ j : n, ‖A i j‖₊ ≤ N
Tactic: cases isEmpty_or_nonempty n
-- 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
x : n → α := fun (j : n) ↦ unitOf (A i j)
simp_rw : (nnnorm (E := n → α) fun (j : n) ↦ unitOf (A i j)) = 1
⊢ ‖x‖₊ = 1
have simp_rw₁ : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : n) ↦ ‖unitOf (A i b)‖₊) 1
Tactic: simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
-- 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
x : n → α := fun (j : n) ↦ unitOf (A i j)
simp_rw : (nnnorm (E := n → α) fun (j : n) ↦ unitOf (A i j)) = 1
simp_rw₁ : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : n) ↦ ‖unitOf (A i b)‖₊) 1
⊢ ‖x‖₊ = 1
have simp_rw₂ : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : n) ↦ 1) 1
Tactic: simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (hypothesis)
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
x : n → α := fun (j : n) ↦ unitOf (A i j)
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have hxn : ‖x‖₊ = 1
Tactic: have hxn : ‖x‖₊ = 1 := by
    simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (hypothesis)
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
x : n → α := fun (j : n) ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have hN₁ : nnnorm (E := m → α)
    (({ toLinearMap := A.mulVecLin, cont := sorry : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
  N * ‖x‖₊
Tactic: specialize hN x
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (hypothesis)
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
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
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
have hN₁ : ∀ (b : m),
  Membership.mem (γ := Finset m) Finset.univ b →
    nnnorm.{u_5} (E := α)
        (({ toLinearMap := A.mulVecLin, cont := sorry : (n → α) →L[α] m → α } : (a : n → α) → m → α) x b : α) ≤
      N
Tactic: rw [hxn, mul_one, Pi.nnnorm_def, Finset.sup_le_iff] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (hypothesis)
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
i : m
h : Membership.mem (γ := Finset m) Finset.univ i
h_1 : Nonempty n
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
have hN₁ : nnnorm.{u_5} (E := α)
    (({ toLinearMap := A.mulVecLin, cont := sorry : (n → α) →L[α] m → α } : (a : n → α) → m → α) x i : α) ≤
  N
Tactic: replace hN := hN i (Finset.mem_univ _)
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
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have inr₃ : let x : n → α := fun (j : n) ↦ unitOf (A i j);
∀ (hxn : ‖x‖₊ = 1), ∑ 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
-- 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
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have inr₄ : let x : n → α := fun (j : n) ↦ unitOf (A i j);
∀ (hxn : ‖x‖₊ = 1)
  (hN :
    nnnorm (E := m → α)
        (({ toLinearMap := A.mulVecLin, cont := sorry : (n → α) →L[α] m → α } : (a : n → α) → m → α) x : m → α) ≤
      N * ‖x‖₊),
  ∑ 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
⊢ ∑ j : n, ‖A i j‖₊ ≤ N
have 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 := sorry : (n → α) →L[α] m → α } : (a : n → α) → m → α) x b : α) ≤
          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
⊢ ∑ 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 := α)
        (({ toLinearMap := A.mulVecLin, cont := sorry : (n → α) →L[α] m → α } : (a : n → α) → m → α) x i : α) ≤
      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