awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : n) ↦ Finset.sup Finset.univ fun (b_1 : n) ↦ ‖diagonal v b b_1‖₊)
    (Finset.sup Finset.univ fun (b : n) ↦ ‖v b‖₊)
⊢ ‖diagonal v‖₊ = ‖v‖₊

Tactic:
simp_rw [nnnorm_def, Pi.nnnorm_def]

Premises used: Pi.nnnorm_def, Matrix.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 → α
e_f : ∀ (i : n), (Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊) = ‖v i‖₊
⊢ Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (b : n) ↦ Finset.sup Finset.univ fun (b_1 : n) ↦ ‖diagonal v b b_1‖₊)
    (Finset.sup Finset.univ fun (b : n) ↦ ‖v b‖₊)

Tactic:
congr 1 with i : 1
-- 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 → α
i : n
⊢ (Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊) = ‖v i‖₊

Tactic:
le_antisymm (Finset.sup_le fun j hj => ?_) ?_

Premises used: Finset.sup_le, le_antisymm
-- 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 → α
i : n
e_f : ∀ (j : n) (hj : Membership.mem (γ := Finset n) Finset.univ j), ‖diagonal v i j‖₊ ≤ ‖v i‖₊
e_f₁ : ‖v i‖₊ ≤ Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊
⊢ (Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊) = ‖v i‖₊

Tactic:
refine le_antisymm (Finset.sup_le fun j hj => ?_) ?_

Premises used: Finset.sup_le, le_antisymm
-- 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 → α
i j : n
hj : Membership.mem (γ := Finset n) Finset.univ j
e_f : ∀ (hj : Membership.mem (γ := Finset n) Finset.univ i), ‖diagonal v i i‖₊ ≤ ‖v i‖₊
e_f₁ : ∀ (hij : i ≠ j), ‖diagonal v i j‖₊ ≤ ‖v i‖₊
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, 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 → α
i : n
hj : Membership.mem (γ := Finset n) Finset.univ i
e_f e_f₁ : ‖v i‖₊ ≤ ‖v i‖₊
⊢ ‖diagonal v i i‖₊ ≤ ‖v i‖₊

Tactic:
rw [diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq
-- 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 → α
i j : n
hj : Membership.mem (γ := Finset n) Finset.univ j
hij : i ≠ j
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊

Tactic:
simp [hij]
-- 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 → α
i : n
⊢ ‖v i‖₊ ≤ Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊

Tactic:
Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))

Premises used: Finset.mem_univ, Eq.trans_le, Finset.le_sup
-- 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 → α
i : n
e_f : ‖v i‖₊ = ‖diagonal v i i‖₊
⊢ ‖v i‖₊ ≤ Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊

Tactic:
refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))

Premises used: Finset.mem_univ, Eq.trans_le, Finset.le_sup
-- 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 → α
i : n
e_f e_f₁ : ‖v i‖₊ = ‖v i‖₊
⊢ ‖v i‖₊ = ‖diagonal v i i‖₊

Tactic:
rw [diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq
-- 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‖ = ‖v‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_diagonal v

Premises used: congr_arg, Matrix.nnnorm_diagonal, NNReal.toReal
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
ι : Type u_7
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : Unique ι
inst_4 : SeminormedAddCommGroup α
inst_5 : SeminormedAddCommGroup β
inst_6 : Nonempty n
inst_7 : DecidableEq n
inst_8 : One α
inst_9 : NormOneClass α
⊢ NormOneClass (Matrix n n α)

Tactic:
⟨(norm_diagonal _).trans <| norm_one⟩

Premises used: Matrix.norm_diagonal, NormOneClass.mk, NormOneClass.norm_one, Eq.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedRing R
inst_3 : SeminormedAddCommGroup α
inst_4 : Module R α
inst_5 : IsBoundedSMul R α
⊢ IsBoundedSMul R (Matrix m n α)

Tactic:
Pi.instIsBoundedSMul

Premises used: Matrix, Pi.instIsBoundedSMul
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedRing R
inst_3 : SeminormedAddCommGroup α
inst_4 : Module R α
inst_5 : NormSMulClass R α
⊢ NormSMulClass R (Matrix m n α)

Tactic:
Pi.instNormSMulClass

Premises used: Matrix, Pi.instNormSMulClass
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedRing R
inst_3 : SeminormedAddCommGroup α
inst_4 : Module R α
inst_5 : IsBoundedSMul R α
⊢ IsBoundedSMul R (Matrix m n α)

Tactic:
letI := PiLp.pseudoMetricSpaceToPi 1 (fun _ : n ↦ α)
  letI := PiLp.isBoundedSMulSeminormedAddCommGroupToPi (R := R) 1 (fun _ : n ↦ α)
  inferInstanceAs (IsBoundedSMul R (m → n → α))

Premises used: _private.0.Matrix.linftyOpIsBoundedSMul._proof_1
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : SeminormedRing R
inst_3 : SeminormedAddCommGroup α
inst_4 : Module R α
inst_5 : NormSMulClass R α
⊢ NormSMulClass R (Matrix m n α)

Tactic:
letI := PiLp.seminormedAddCommGroupToPi 1 (fun _ : n ↦ α)
  letI := PiLp.normSMulClassSeminormedAddCommGroupToPi (R := R) 1 (fun _ : n ↦ α)
  inferInstanceAs (NormSMulClass R (m → n → α))

Premises used: _private.0.Matrix.linftyOpNormSMulClass._proof_1
-- Module: Mathlib.Analysis.Matrix.Normed
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 α
change :
  (norm (E := (i : m) → WithLp 1 (n → α)) fun (i : m) ↦ toLp 1 (A i)) =
    (↑(Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) : ℝ)
⊢ ‖A‖ = (↑(Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) : ℝ)

Tactic:
change ‖fun i => toLp 1 (A i)‖ = _

Premises used: WithLp.toLp, OfNat.ofNat
-- Module: Mathlib.Analysis.Matrix.Normed
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 α
⊢ (norm (E := (i : m) → WithLp 1 (n → α)) fun (i : m) ↦ toLp 1 (A i)) =
    (↑(Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) : ℝ)

Tactic:
simp [Pi.norm_def, PiLp.nnnorm_eq_of_L1]

Premises used: Pi.norm_def, PiLp.nnnorm_eq_of_L1
-- Module: Mathlib.Analysis.Matrix.Normed
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‖₊ = Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊

Tactic:
Subtype.ext <| linfty_opNorm_def A

Premises used: NNReal, Matrix.linfty_opNorm_def, Subtype.ext
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
rw :
  Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : ι, ‖replicateCol ι v i j‖₊)
    (Finset.sup Finset.univ fun (b : m) ↦ ‖v b‖₊)
⊢ ‖replicateCol ι v‖₊ = ‖v‖₊

Tactic:
rw [linfty_opNNNorm_def, Pi.nnnorm_def]

Premises used: Pi.nnnorm_def, Matrix.linfty_opNNNorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
⊢ Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : ι, ‖replicateCol ι v i j‖₊)
    (Finset.sup Finset.univ fun (b : m) ↦ ‖v b‖₊)

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
ι : Type u_7
inst : Fintype m
inst_1 : Unique ι
inst_2 : SeminormedAddCommGroup α
v : m → α
⊢ ‖replicateCol ι v‖ = ‖v‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_replicateCol v

Premises used: congr_arg, Matrix.linfty_opNNNorm_replicateCol, NNReal.toReal
-- 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 → α
⊢ ‖replicateRow ι v‖₊ = ∑ i : n, ‖v i‖₊

Tactic:
simp [linfty_opNNNorm_def]

Premises used: Matrix.linfty_opNNNorm_def
-- 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 → α
⊢ (↑(∑ i : n, ‖v i‖₊) : ℝ) = ∑ i : n, ‖v i‖

Tactic:
simp [NNReal.coe_sum]

Premises used: NNReal.coe_sum
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
rw :
  Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : m, ‖diagonal v i j‖₊)
    (Finset.sup Finset.univ fun (b : m) ↦ ‖v b‖₊)
⊢ ‖diagonal v‖₊ = ‖v‖₊

Tactic:
rw [linfty_opNNNorm_def, Pi.nnnorm_def]

Premises used: Pi.nnnorm_def, Matrix.linfty_opNNNorm_def
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
e_f : ∀ (i : m), ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊
⊢ Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : m, ‖diagonal v i j‖₊)
    (Finset.sup Finset.univ fun (b : m) ↦ ‖v b‖₊)

Tactic:
congr 1 with i : 1
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
i : m
⊢ ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊

Tactic:
(Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => ?_).trans ?_

Premises used: Finset.mem_univ, Finset.sum_eq_single_of_mem, Eq.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
i : m
e_f : ∀ (j : m) (_hj : Membership.mem (γ := Finset m) Finset.univ j) (hij : j ≠ i), ‖diagonal v i j‖₊ = 0
e_f₁ : ‖diagonal v i i‖₊ = ‖v i‖₊
⊢ ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊

Tactic:
refine (Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => ?_).trans ?_

Premises used: Finset.mem_univ, Finset.sum_eq_single_of_mem, Eq.trans
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
i j : m
_hj : Membership.mem (γ := Finset m) Finset.univ j
hij : j ≠ i
e_f : nnnorm.{u_5} (E := α) 0 = 0
e_f₁ e_f₂ : Eq (α := ℝ≥0) 0 0
⊢ ‖diagonal v i j‖₊ = 0

Tactic:
rw [diagonal_apply_ne' _ hij, nnnorm_zero]

Premises used: Matrix.diagonal_apply_ne', nnnorm_zero
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
i : m
e_f e_f₁ : ‖v i‖₊ = ‖v i‖₊
⊢ ‖diagonal v i i‖₊ = ‖v i‖₊

Tactic:
rw [diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
⊢ ‖diagonal v‖ = ‖v‖

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_diagonal v

Premises used: congr_arg, NNReal.toReal, Matrix.linfty_opNNNorm_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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
simp_rw :
  (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‖₊)
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Tactic:
simp_rw [linfty_opNNNorm_def, Matrix.mul_apply]

Premises used: Matrix.mul_apply, Matrix.linfty_opNNNorm_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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ LE.le (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ k : n, nnnorm.{u_5} (E := α) (∑ j : m, A i j * B j k))
    (Finset.sup Finset.univ fun (i : l) ↦ ∑ k : n, ∑ j : m, ‖A i j‖₊ * ‖B j k‖₊)

Tactic:
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 _ _

Premises used: Finset.univ, nnnorm_mul_le, Finset.sup_mono_fun, Finset.sum_le_sum, nnnorm_sum_le_of_le
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
simp_rw :
  Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : l) ↦ ∑ y : m, ∑ x : n, ‖A i y‖₊ * ‖B y x‖₊)
    (Finset.sup Finset.univ fun (i : l) ↦ ∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
⊢ 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:
simp_rw [@Finset.sum_comm m, Finset.mul_sum]

Premises used: Finset.mul_sum, Finset.sum_comm
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ 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:
Finset.sup_mono_fun fun i _hi => ?_

Premises used: Finset.sup_mono_fun
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
refine :
  ∀ (i : l) (_hi : Membership.mem (γ := Finset l) Finset.univ i),
    LE.le (α := ℝ≥0) (∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
      (∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
⊢ 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:
refine Finset.sup_mono_fun fun i _hi => ?_

Premises used: Finset.sup_mono_fun
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : Membership.mem (γ := Finset l) Finset.univ i
h :
  ∀ (j : m) (hj : Membership.mem (γ := Finset m) Finset.univ j),
    LE.le (α := ℝ≥0) (∑ k : n, ‖B j k‖₊) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
⊢ LE.le (α := ℝ≥0) (∑ j : m, ‖A i j‖₊ * ∑ k : n, ‖B j k‖₊)
    (∑ j : m, ‖A i j‖₊ * Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)

Tactic:
gcongr with j hj
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : Membership.mem (γ := Finset l) Finset.univ i
j : m
hj : Membership.mem (γ := Finset m) Finset.univ j
⊢ LE.le (α := ℝ≥0) (∑ k : n, ‖B j k‖₊) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)

Tactic:
Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj

Premises used: Finset.le_sup
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : Membership.mem (γ := Finset l) Finset.univ i
j : m
hj : Membership.mem (γ := Finset m) Finset.univ j
⊢ LE.le (α := ℝ≥0) (∑ k : n, ‖B j k‖₊) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)

Tactic:
exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj

Premises used: Finset.le_sup
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
simp_rw :
  HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (a : l) ↦ ∑ i : m, ‖A a i‖₊)
      (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊) ≤
    HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (a : l) ↦ ∑ i : m, ‖A a i‖₊)
      (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)
⊢ (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:
simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]

Premises used: NNReal.finset_sup_mul, Finset.sum_mul
-- 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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (a : l) ↦ ∑ i : m, ‖A a i‖₊)
      (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊) ≤
    HMul.hMul (α := ℝ≥0) (Finset.sup Finset.univ fun (a : l) ↦ ∑ i : m, ‖A a i‖₊)
      (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖B i j‖₊)

Tactic:
rfl
-- 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 : 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‖₊)
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‖₊)
⊢ (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‖₊)

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

Premises used: HMul.hMul, Finset.univ, NNNorm.nnnorm, nnnorm_mul_le, Finset.sup_mono_fun, Finset.sup, Finset.sum_le_sum, nnnorm_sum_le_of_le, Finset.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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖ ≤ ‖A‖ * ‖B‖

Tactic:
linfty_opNNNorm_mul _ _

Premises used: Matrix.linfty_opNNNorm_mul
-- Module: Mathlib.Analysis.Matrix.Normed
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 → α
rw :
  nnnorm (E := Matrix l (Fin 1) α) (replicateCol (Fin 1) (A *ᵥ v)) ≤
    ‖A‖₊ * nnnorm (E := Matrix m (Fin 1) α) (replicateCol (Fin 1) v)
⊢ ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊

Tactic:
rw [← linfty_opNNNorm_replicateCol (ι := Fin 1) (A *ᵥ v),
    ← linfty_opNNNorm_replicateCol v (ι := Fin 1)]

Premises used: Matrix.linfty_opNNNorm_replicateCol, Matrix.mulVec
-- Module: Mathlib.Analysis.Matrix.Normed
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 → α
⊢ nnnorm (E := Matrix l (Fin 1) α) (replicateCol (Fin 1) (A *ᵥ v)) ≤
    ‖A‖₊ * nnnorm (E := Matrix m (Fin 1) α) (replicateCol (Fin 1) v)

Tactic:
linfty_opNNNorm_mul A (replicateCol (Fin 1) v)

Premises used: Multiset.sum, Multiset.foldr, dotProduct, setOf, List.ofFn, Fin.ofNat, Matrix.replicateCol, Fin.foldr.loop, Multiset.cons, Multiset.ofList, Matrix.linfty_opNNNorm_mul, OfNat.ofNat, Fin, List.finRange, Matrix.mulVec, Finset.sum
-- Module: Mathlib.Analysis.Matrix.Normed
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 → α
⊢ nnnorm (E := Matrix l (Fin 1) α) (replicateCol (Fin 1) (A *ᵥ v)) ≤
    ‖A‖₊ * nnnorm (E := Matrix m (Fin 1) α) (replicateCol (Fin 1) v)

Tactic:
exact linfty_opNNNorm_mul A (replicateCol (Fin 1) v)

Premises used: Matrix.replicateCol, Matrix.linfty_opNNNorm_mul, OfNat.ofNat, Fin
-- Module: Mathlib.Analysis.Matrix.Normed
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‖

Tactic:
linfty_opNNNorm_mulVec _ _

Premises used: Matrix.linfty_opNNNorm_mulVec
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
ι : Type u_7
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : Unique ι
inst_4 : NormedDivisionRing α
inst_5 : NormedAlgebra ℝ α
a : α
⊢ α

Tactic:
exact if a = 0 then 1 else ‖a‖ • a⁻¹
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
ι : Type u_7
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : Unique ι
inst_4 : NormedDivisionRing α
inst_5 : NormedAlgebra ℝ α
a : α
⊢ α

Tactic:
classical exact if a = 0 then 1 else ‖a‖ • a⁻¹
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
rw : ‖if a = 0 then 1 else ‖a‖ • a⁻¹‖₊ = 1
⊢ ‖unitOf a‖₊ = 1

Tactic:
rw [unitOf]

Premises used: _private.0.Matrix.unitOf
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
pos : ∀ (h : a = 0), nnnorm.{u_5} (E := α) 1 = 1
neg : ∀ (h : ¬a = 0), ‖‖a‖ • a⁻¹‖₊ = 1
⊢ ‖if a = 0 then 1 else ‖a‖ • a⁻¹‖₊ = 1

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : a = 0
⊢ nnnorm.{u_5} (E := α) 1 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Normed
Goal:
α : Type u_5
inst : NormedDivisionRing α
inst_1 : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ ¬‖a‖₊ = 0

Tactic:
rw [← nnnorm_eq_zero] at h

Premises used: nnnorm_eq_zero