awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux
⊢ ContinuousOn f (spectrum ℝ A)
have rw : Continuous ((spectrum ℝ A).restrict (π := fun (a : ℝ) ↦ ℝ) f)
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : Eq (α := C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (cfcHom (p := IsSelfAdjoint) hA') hA.cfcAux
⊢ cfc (p := IsSelfAdjoint) f A = hA.cfc f
have rw : (hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
    { toFun := (spectrum ℝ A).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := sorry } =
  hA.cfc f
Tactic: rw [cfc_apply f A hA' (by rw [continuousOn_iff_continuous_restrict]; fun_prop), this]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ Eq (α := 𝕜[X]) (cfc (p := IsSelfAdjoint) f A).charpoly
    (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(f (hA.eigenvalues i)) : 𝕜)))
have rw : Eq (α := 𝕜[X])
  (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
      diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues)).charpoly
  (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(f (hA.eigenvalues i)) : 𝕜)))
Tactic: rw [cfc_eq hA f, IsHermitian.cfc, conjStarAlgAut_apply, charpoly_mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
this_1 : NormedAddCommGroup (n → 𝕜) := Sᵀ.toNormedAddCommGroup ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := Sᵀ.toInnerProductSpace ⋯
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ
have a : ∀ (i j : n),
  lowerInv hS i j = (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
this_1 : NormedAddCommGroup (n → 𝕜) := Sᵀ.toNormedAddCommGroup ⋯
this : InnerProductSpace 𝕜 (n → 𝕜) := Sᵀ.toInnerProductSpace ⋯
i j : n
⊢ lowerInv hS i j = (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ i j
have a : Eq.{u_1 + 1} (α := 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j)
  ((gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜))ᵀᵀ i j)
Tactic: rw [LDL.lowerInv, Basis.coePiBasisFun.toMatrix_eq_transpose, coe_gramSchmidtBasis]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
⊢ Invertible (lowerInv hS)
have rw : Invertible (α := Matrix n n 𝕜)
  (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ
Tactic: rw [LDL.lowerInv_eq_gramSchmidtBasis]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
⊢ Invertible (α := Matrix n n 𝕜)
    (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ
have haveI : (this :
    Invertible (α := Matrix n n 𝕜)
      (Basis.toMatrix (Pi.basisFun 𝕜 n)
        (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n) : Basis n 𝕜 (n → 𝕜)) : (a : n) → n → 𝕜))) →
  Invertible (α := Matrix n n 𝕜)
    (Basis.toMatrix (Pi.basisFun 𝕜 n) (⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)) : (a : n) → n → 𝕜))ᵀ
Tactic: haveI :=
    Basis.invertibleToMatrix (Pi.basisFun 𝕜 n)
      (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
        (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ (Pi.basisFun 𝕜 n))
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : i < j
⊢ lowerInv hS i j = 0
have rw : lowerInv hS i j =
  ((Basis.repr (Pi.basisFun 𝕜 n) : (a : n → 𝕜) → n →₀ 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i) :
      (a : n) → 𝕜)
    j
Tactic: rw [← @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
      (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ i j hij (Pi.basisFun 𝕜 n),
    Pi.basisFun_repr, LDL.lowerInv]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : i < j
rw :
  lowerInv hS i j =
    ((Basis.repr (Pi.basisFun 𝕜 n) : (a : n → 𝕜) → n →₀ 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i) :
        (a : n) → 𝕜)
      j
⊢ lowerInv hS i j = 0
have rw₁ : lowerInv hS i j = gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j
Tactic: rw [← @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
      (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ i j hij (Pi.basisFun 𝕜 n),
    Pi.basisFun_repr, LDL.lowerInv]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : i < j
rw :
  lowerInv hS i j =
    ((Basis.repr (Pi.basisFun 𝕜 n) : (a : n → 𝕜) → n →₀ 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i) :
        (a : n) → 𝕜)
      j
rw₁ : lowerInv hS i j = gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j
⊢ lowerInv hS i j = 0
have rw₂ : Eq.{u_1 + 1} (α := 𝕜) (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j)
  (gramSchmidt 𝕜 (⇑(Pi.basisFun 𝕜 n) : (a : n) → n → 𝕜) i j)
Tactic: rw [← @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
      (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ i j hij (Pi.basisFun 𝕜 n),
    Pi.basisFun_repr, LDL.lowerInv]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
have a : ∀ (i j : n), diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
have pos : ∀ (hij : i = j), diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
pos : ∀ (hij : i = j), diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
have neg : ∀ (hij : ¬i = j), diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : i = j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
have pos : lowerInv hS j ⬝ᵥ S *ᵥ star (lowerInv hS j) = (lowerInv hS * (S * (lowerInv hS)ᴴ)) j j
Tactic: simp only [diag, diagEntries, EuclideanSpace.inner_toLp_toLp, star_star, hij,
      diagonal_apply_eq, Matrix.mul_assoc, dotProduct_comm]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : ¬i = j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
have neg : 0 = lowerInv hS i ⬝ᵥ S *ᵥ (lowerInv hS)ᴴᵀ j
Tactic: simp only [LDL.diag, hij, diagonal_apply_ne, Ne, not_false_iff, mul_mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
i j : n
hij : ¬i = j
⊢ 0 = lowerInv hS i ⬝ᵥ S *ᵥ (lowerInv hS)ᴴᵀ j
have neg : lowerInv hS i ᵥ* S ⬝ᵥ star (lowerInv hS j) = lowerInv hS i ᵥ* S ⬝ᵥ (lowerInv hS).map star j
Tactic: rw [conjTranspose, transpose_map, transpose_transpose, dotProduct_mulVec,
      (LDL.lowerInv_orthogonal hS fun h : j = i => hij h.symm).symm, ← inner_conj_symm,
      mulVec_transpose, EuclideanSpace.inner_toLp_toLp, ← RCLike.star_def, ←
      star_dotProduct_star, star_star]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.LDL (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : LinearOrder n
inst_2 : WellFoundedLT n
inst_3 : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst_4 : Fintype n
hS : S.PosDef
⊢ lower hS * diag hS * (lower hS)ᴴ = S
have rw : diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
Tactic: rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
    Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS),
    Matrix.mul_inv_eq_iff_eq_mul_of_invertible]
-- 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‖ = (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)
have simp_rw : (norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) =
  (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)
Tactic: simp_rw [Matrix.norm_def, Pi.norm_def, Pi.nnnorm_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 : SeminormedAddCommGroup α
A : Matrix m n α
simp_rw :
  (norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) =
    (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)
⊢ ‖A‖ = (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)
have simp_rw₁ : (↑(Finset.sup Finset.univ fun (b : m) ↦ nnnorm (E := (j : n) → α) fun (j : n) ↦ A b j) : ℝ) =
  (↑(Finset.sup Finset.univ fun (i : m) ↦ Finset.sup Finset.univ fun (j : n) ↦ ‖A i j‖₊) : ℝ)
Tactic: simp_rw [Matrix.norm_def, Pi.norm_def, Pi.nnnorm_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 : SeminormedAddCommGroup α
r : ℝ
hr : 0 ≤ r
A : Matrix m n α
⊢ ‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
have simp_rw : (norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
Tactic: simp_rw [norm_def, pi_norm_le_iff_of_nonneg hr]
-- 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 α
r : ℝ≥0
A : Matrix m n α
⊢ ‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
have simp_rw : (nnnorm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
Tactic: simp_rw [nnnorm_def, pi_nnnorm_le_iff]
-- 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 α
r : ℝ
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
have simp_rw : (norm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
Tactic: simp_rw [norm_def, pi_norm_lt_iff hr]
-- 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 α
r : ℝ≥0
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r
have simp_rw : (nnnorm (E := (i : m) → (j : n) → α) fun (i : m) (j : n) ↦ A i j) < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r
Tactic: simp_rw [nnnorm_def, pi_nnnorm_lt_iff hr]
-- 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‖₊ = ‖v‖₊
have 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‖₊)
Tactic: simp_rw [nnnorm_def, Pi.nnnorm_def]
-- 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 → α
⊢ 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‖₊)
have e_f : ∀ (i : n), (Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊) = ‖v i‖₊
Tactic: congr 1 with i : 1
-- 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 → α
i : n
⊢ (Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊) = ‖v i‖₊
have e_f : ∀ (j : n) (hj : Membership.mem (γ := Finset n) Finset.univ j), ‖diagonal v i j‖₊ ≤ ‖v i‖₊
Tactic: refine le_antisymm (Finset.sup_le fun j hj => ?_) ?_
-- 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 → α
i : n
e_f : ∀ (j : n) (hj : Membership.mem (γ := Finset n) Finset.univ j), ‖diagonal v i j‖₊ ≤ ‖v i‖₊
⊢ (Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊) = ‖v i‖₊
have e_f₁ : ‖v i‖₊ ≤ Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊
Tactic: refine le_antisymm (Finset.sup_le fun j hj => ?_) ?_
-- 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 → α
i j : n
hj : Membership.mem (γ := Finset n) Finset.univ j
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊
have e_f : ∀ (hj : Membership.mem (γ := Finset n) Finset.univ i), ‖diagonal v i i‖₊ ≤ ‖v i‖₊
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j, hj
-- 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 → α
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‖₊
⊢ ‖diagonal v i j‖₊ ≤ ‖v i‖₊
have e_f₁ : ∀ (hij : i ≠ j), ‖diagonal v i j‖₊ ≤ ‖v i‖₊
Tactic: obtain rfl | hij := eq_or_ne i j
-- 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 → α
i : n
hj : Membership.mem (γ := Finset n) Finset.univ i
⊢ ‖diagonal v i i‖₊ ≤ ‖v i‖₊
have e_f : ‖v i‖₊ ≤ ‖v i‖₊
Tactic: rw [diagonal_apply_eq]
-- 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 → α
i : n
⊢ ‖v i‖₊ ≤ Finset.sup Finset.univ fun (b : n) ↦ ‖diagonal v i b‖₊
have e_f : ‖v i‖₊ = ‖diagonal v i i‖₊
Tactic: refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))
-- 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 → α
i : n
⊢ ‖v i‖₊ = ‖diagonal v i i‖₊
have e_f : ‖v i‖₊ = ‖v i‖₊
Tactic: rw [diagonal_apply_eq]
-- 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‖ = (↑(Finset.sup Finset.univ fun (i : m) ↦ ∑ j : n, ‖A i j‖₊) : ℝ)
have 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‖₊) : ℝ)
Tactic: change ‖fun i => toLp 1 (A i)‖ = _
-- 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 → α
⊢ ‖replicateCol ι v‖₊ = ‖v‖₊
have rw : Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : ι, ‖replicateCol ι v i j‖₊)
  (Finset.sup Finset.univ fun (b : m) ↦ ‖v b‖₊)
Tactic: rw [linfty_opNNNorm_def, Pi.nnnorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
⊢ ‖diagonal v‖₊ = ‖v‖₊
have 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‖₊)
Tactic: rw [linfty_opNNNorm_def, Pi.nnnorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
⊢ Eq (α := ℝ≥0) (Finset.sup Finset.univ fun (i : m) ↦ ∑ j : m, ‖diagonal v i j‖₊)
    (Finset.sup Finset.univ fun (b : m) ↦ ‖v b‖₊)
have e_f : ∀ (i : m), ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊
Tactic: congr 1 with i : 1
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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‖₊
have e_f : ∀ (j : m) (_hj : Membership.mem (γ := Finset m) Finset.univ j) (hij : j ≠ i), ‖diagonal v i j‖₊ = 0
Tactic: refine (Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => ?_).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊
have e_f₁ : ‖diagonal v i i‖₊ = ‖v i‖₊
Tactic: refine (Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => ?_).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ ‖diagonal v i j‖₊ = 0
have e_f : nnnorm.{u_5} (E := α) 0 = 0
Tactic: rw [diagonal_apply_ne' _ hij, nnnorm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
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
⊢ ‖diagonal v i j‖₊ = 0
have e_f₁ : Eq (α := ℝ≥0) 0 0
Tactic: rw [diagonal_apply_ne' _ hij, nnnorm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Normed (goal)
Goal:
m : Type u_3
α : Type u_5
inst : Fintype m
inst_1 : SeminormedAddCommGroup α
inst_2 : DecidableEq m
v : m → α
i : m
⊢ ‖diagonal v i i‖₊ = ‖v i‖₊
have e_f : ‖v i‖₊ = ‖v i‖₊
Tactic: rw [diagonal_apply_eq]
-- 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 α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
have 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‖₊)
Tactic: simp_rw [linfty_opNNNorm_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 : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ 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‖₊)
have 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‖₊)
Tactic: simp_rw [@Finset.sum_comm m, Finset.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 : 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‖₊)
have 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‖₊)
Tactic: refine Finset.sup_mono_fun fun i _hi => ?_
-- 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 α
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‖₊)
have 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‖₊)
Tactic: gcongr with j hj
-- 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) ↦ ∑ 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‖₊)
have 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‖₊)
Tactic: simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]