bump to nightly-2023-04-17-14

mathlib commit leanprover-community/mathlib@17ad94b
leanprover-community · Apr 17, 2023 · ce47306 · ce47306
1 parent ab6befd
commit ce47306
Show file tree

Hide file tree

Showing 21 changed files with 656 additions and 572 deletions.
diff --git a/Mathbin/Algebra/Lie/CartanMatrix.lean b/Mathbin/Algebra/Lie/CartanMatrix.lean
@@ -201,8 +201,7 @@ def Matrix.ToLieAlgebra :=
 
 namespace CartanMatrix
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 /-- The Cartan matrix of type e₆. See [bourbaki1968] plate V, page 277.
 
 The corresponding Dynkin diagram is:
@@ -213,12 +212,11 @@ o --- o --- o --- o --- o
 ```
 -/
 def e₆ : Matrix (Fin 6) (Fin 6) ℤ :=
-  «expr!![ »
-    "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation"
+  !![2, 0, -1, 0, 0, 0; 0, 2, 0, -1, 0, 0; -1, 0, 2, -1, 0, 0; 0, -1, -1, 2, -1, 0; 0, 0, 0, -1, 2,
+    -1; 0, 0, 0, 0, -1, 2]
 #align cartan_matrix.E₆ CartanMatrix.e₆
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 /-- The Cartan matrix of type e₇. See [bourbaki1968] plate VI, page 281.
 
 The corresponding Dynkin diagram is:
@@ -229,12 +227,11 @@ o --- o --- o --- o --- o --- o
 ```
 -/
 def e₇ : Matrix (Fin 7) (Fin 7) ℤ :=
-  «expr!![ »
-    "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation"
+  !![2, 0, -1, 0, 0, 0, 0; 0, 2, 0, -1, 0, 0, 0; -1, 0, 2, -1, 0, 0, 0; 0, -1, -1, 2, -1, 0, 0; 0,
+    0, 0, -1, 2, -1, 0; 0, 0, 0, 0, -1, 2, -1; 0, 0, 0, 0, 0, -1, 2]
 #align cartan_matrix.E₇ CartanMatrix.e₇
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 /-- The Cartan matrix of type e₈. See [bourbaki1968] plate VII, page 285.
 
 The corresponding Dynkin diagram is:
@@ -245,12 +242,12 @@ o --- o --- o --- o --- o --- o --- o
 ```
 -/
 def e₈ : Matrix (Fin 8) (Fin 8) ℤ :=
-  «expr!![ »
-    "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation"
+  !![2, 0, -1, 0, 0, 0, 0, 0; 0, 2, 0, -1, 0, 0, 0, 0; -1, 0, 2, -1, 0, 0, 0, 0; 0, -1, -1, 2, -1,
+    0, 0, 0; 0, 0, 0, -1, 2, -1, 0, 0; 0, 0, 0, 0, -1, 2, -1, 0; 0, 0, 0, 0, 0, -1, 2, -1; 0, 0, 0,
+    0, 0, 0, -1, 2]
 #align cartan_matrix.E₈ CartanMatrix.e₈
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 /-- The Cartan matrix of type f₄. See [bourbaki1968] plate VIII, page 288.
 
 The corresponding Dynkin diagram is:
@@ -259,12 +256,10 @@ o --- o =>= o --- o
 ```
 -/
 def f₄ : Matrix (Fin 4) (Fin 4) ℤ :=
-  «expr!![ »
-    "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation"
+  !![2, -1, 0, 0; -1, 2, -2, 0; 0, -1, 2, -1; 0, 0, -1, 2]
 #align cartan_matrix.F₄ CartanMatrix.f₄
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 /-- The Cartan matrix of type g₂. See [bourbaki1968] plate IX, page 290.
 
 The corresponding Dynkin diagram is:
@@ -274,8 +269,7 @@ o ≡>≡ o
 Actually we are using the transpose of Bourbaki's matrix. This is to make this matrix consistent
 with `cartan_matrix.F₄`, in the sense that all non-zero values below the diagonal are -1. -/
 def g₂ : Matrix (Fin 2) (Fin 2) ℤ :=
-  «expr!![ »
-    "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation"
+  !![2, -3; -1, 2]
 #align cartan_matrix.G₂ CartanMatrix.g₂
 
 end CartanMatrix

diff --git a/Mathbin/Analysis/SpecialFunctions/PolarCoord.lean b/Mathbin/Analysis/SpecialFunctions/PolarCoord.lean
@@ -101,13 +101,11 @@ def polarCoord : LocalHomeomorph (ℝ × ℝ) (ℝ × ℝ)
     · exact complex.equiv_real_prod_clm.symm.continuous.continuous_on
 #align polar_coord polarCoord
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 theorem hasFderivAt_polarCoord_symm (p : ℝ × ℝ) :
     HasFderivAt polarCoord.symm
       (Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)
-          («expr!![ »
-            "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation")).toContinuousLinearMap
+          !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2]).toContinuousLinearMap
       p :=
   by
   rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]
@@ -137,16 +135,14 @@ theorem polarCoord_source_ae_eq_univ : polarCoord.source =ᵐ[volume] univ :=
   exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le
 #align polar_coord_source_ae_eq_univ polarCoord_source_ae_eq_univ
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 theorem integral_comp_polarCoord_symm {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [CompleteSpace E] (f : ℝ × ℝ → E) :
     (∫ p in polarCoord.target, p.1 • f (polarCoord.symm p)) = ∫ p, f p :=
   by
   set B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ := fun p =>
     (Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)
-        («expr!![ »
-          "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation")).toContinuousLinearMap with
+        !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2]).toContinuousLinearMap with
     hB
   have A : ∀ p ∈ polar_coord.symm.source, HasFderivAt polar_coord.symm (B p) p := fun p hp =>
     hasFderivAt_polarCoord_symm p

diff --git a/Mathbin/Data/Complex/Module.lean b/Mathbin/Data/Complex/Module.lean
@@ -310,14 +310,11 @@ theorem conjAe_coe : ⇑conjAe = conj :=
   rfl
 #align complex.conj_ae_coe Complex.conjAe_coe
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 /-- The matrix representation of `conj_ae`. -/
 @[simp]
 theorem toMatrix_conjAe :
-    LinearMap.toMatrix basisOneI basisOneI conjAe.toLinearMap =
-      «expr!![ »
-        "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" :=
+    LinearMap.toMatrix basisOneI basisOneI conjAe.toLinearMap = !![1, 0; 0, -1] :=
   by
   ext (i j)
   simp [LinearMap.toMatrix_apply]

diff --git a/Mathbin/Data/Matrix/Notation.lean b/Mathbin/Data/Matrix/Notation.lean
@@ -440,84 +440,61 @@ section One
 
 variable [Zero α] [One α]
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
-theorem one_fin_two :
-    (1 : Matrix (Fin 2) (Fin 2) α) =
-      «expr!![ »
-        "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" :=
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
+theorem one_fin_two : (1 : Matrix (Fin 2) (Fin 2) α) = !![1, 0; 0, 1] :=
   by
   ext (i j)
   fin_cases i <;> fin_cases j <;> rfl
 #align matrix.one_fin_two Matrix.one_fin_two
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
-theorem one_fin_three :
-    (1 : Matrix (Fin 3) (Fin 3) α) =
-      «expr!![ »
-        "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" :=
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
+theorem one_fin_three : (1 : Matrix (Fin 3) (Fin 3) α) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] :=
   by
   ext (i j)
   fin_cases i <;> fin_cases j <;> rfl
 #align matrix.one_fin_three Matrix.one_fin_three
 
 end One
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
-theorem eta_fin_two (A : Matrix (Fin 2) (Fin 2) α) :
-    A =
-      «expr!![ »
-        "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" :=
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
+theorem eta_fin_two (A : Matrix (Fin 2) (Fin 2) α) : A = !![A 0 0, A 0 1; A 1 0, A 1 1] :=
   by
   ext (i j)
   fin_cases i <;> fin_cases j <;> rfl
 #align matrix.eta_fin_two Matrix.eta_fin_two
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 theorem eta_fin_three (A : Matrix (Fin 3) (Fin 3) α) :
-    A =
-      «expr!![ »
-        "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" :=
+    A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] :=
   by
   ext (i j)
   fin_cases i <;> fin_cases j <;> rfl
 #align matrix.eta_fin_three Matrix.eta_fin_three
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 theorem mul_fin_two [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
-    «expr!![ »
-          "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" ⬝
-        «expr!![ »
-          "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" =
-      «expr!![ »
-        "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" :=
+    !![a₁₁, a₁₂; a₂₁, a₂₂] ⬝ !![b₁₁, b₁₂; b₂₁, b₂₂] =
+      !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁,
+        a₂₁ * b₁₂ + a₂₂ * b₂₂] :=
   by
   ext (i j)
   fin_cases i <;> fin_cases j <;> simp [Matrix.mul, dot_product, Fin.sum_univ_succ]
 #align matrix.mul_fin_two Matrix.mul_fin_two
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `«expr!![ » -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/
 theorem mul_fin_three [AddCommMonoid α] [Mul α]
     (a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α) :
-    «expr!![ »
-          "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" ⬝
-        «expr!![ »
-          "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" =
-      «expr!![ »
-        "./././Mathport/Syntax/Translate/Expr.lean:387:14: unsupported user notation matrix.notation" :=
+    !![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] ⬝
+        !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] =
+      !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂,
+        a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃; a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁,
+        a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
+        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂,
+        a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃] :=
   by
   ext (i j)
   fin_cases i <;> fin_cases j <;> simp [Matrix.mul, dot_product, Fin.sum_univ_succ, ← add_assoc]