clear most of warnings

Author: lecopivo

SciLean/AD/FDeriv.lean

@@ -34,7 +34,7 @@ attribute [fun_trans] fderiv
 theorem deriv_fderiv'
   {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {X : Type*} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
-  (f : 𝕜 → X) : deriv f = fun x => fderiv 𝕜 f x 1 := by funext x; rw[← deriv_fderiv]; simp
+  (f : 𝕜 → X) : deriv f = fun x => fderiv 𝕜 f x 1 := by funext x; rw[← toSpanSingleton_deriv]; simp
 
 -- SciLean prefers `fderiv` over `deriv`
 attribute [-simp] fderiv_eq_smul_deriv
@@ -327,7 +327,7 @@ theorem HDiv.hDiv.arg_a0a1.fderiv_rule_at
   rw [h (fun x => f x / g x) x, h f x, h g x]
   have hdiv := deriv_fun_div (c := (fun h : K => f (x + h • dx))) (d := (fun h : K => g (x + h • dx)))
     (x := 0) (hc := by sorry_proof) (hd := by sorry_proof) (hx := by sorry_proof)
-  convert hdiv using 1 <;> rw [zero_smul, add_zero]
+  convert hdiv using 1; rw [zero_smul, add_zero]
 
 
 -- Inv.inv -------------------------------------------------------------------

SciLean/AD/HasRevFDeriv.lean

@@ -875,7 +875,7 @@ theorem Finset.sum.arg_f.HasRevFDeriv_rule
     HasRevFDeriv K
       (fun f : I → X => A.sum (fun i => f i))
       (fun f =>
-        (A.sum (fun i => f i), fun dx i => A.toSet.indicator (fun _ => dx) i)) := by
+        (A.sum (fun i => f i), fun dx i => (A : Set I).indicator (fun _ => dx) i)) := by
   apply hasRevFDeriv_from_hasFDerivAt_hasAdjoint
   case deriv => intro; data_synth
   case adjoint => intro x; simp; data_synth
@@ -889,7 +889,7 @@ theorem Finset.sum.arg_f.HasRevFDeriv_rule'
     HasRevFDeriv K
       (fun f : I → X => A.sum f)
       (fun f =>
-        (A.sum (fun i => f i), fun dx i => A.toSet.indicator (fun _ => dx) i)) := by
+        (A.sum (fun i => f i), fun dx i => (A : Set I).indicator (fun _ => dx) i)) := by
   apply Finset.sum.arg_f.HasRevFDeriv_rule
 
 @[data_synth]
@@ -898,7 +898,7 @@ theorem Finset.sum.arg_f.HasRevFDerivUpdate_rule
     HasRevFDerivUpdate K
       (fun f : I → X => A.sum (fun i => f i))
       (fun f =>
-        (A.sum (fun i => f i), fun dx df i => df i + A.toSet.indicator (fun _ => dx) i)) := by
+        (A.sum (fun i => f i), fun dx df i => df i + (A : Set I).indicator (fun _ => dx) i)) := by
   apply hasRevFDerivUpdate_from_hasFDerivAt_hasAdjointUpdate
   case deriv => intro; data_synth
   case adjoint => intro x; simp; data_synth
@@ -914,7 +914,7 @@ theorem Finset.sum.arg_f.HasRevFDerivUpdate_rule'
       (fun f =>
         (A.sum (fun i => f i), fun dx df i =>
           let dxi := df i
-          let dx := dxi + A.toSet.indicator (fun _ => dx) i
+          let dx := dxi + (A : Set I).indicator (fun _ => dx) i
           dx)) := by
   apply Finset.sum.arg_f.HasRevFDerivUpdate_rule
 

SciLean/AD/RevFDeriv.lean

@@ -126,7 +126,7 @@ theorem pi_rule [Fold ι] [Fold ι] -- these instances have different universes
        := by
 
   unfold revFDeriv
-  simp (disch:=fun_prop) only [fderiv.pi_rule_at,adjoint.pi_rule]
+  simp (disch:=fun_prop) only [fderiv.pi_rule_at]
   fun_trans
   sorry_proof
 

SciLean/AD/Rules/Log.lean

@@ -58,6 +58,7 @@ theorem log.arg_x.HasFwdFDerivAt_rule
 
 
 omit [CompleteSpace U] in
+set_option linter.unusedVariables false in
 @[data_synth]
 theorem log.arg_x.HasRevFDeriv_rule
     (x : U → R) {x'} (hx : HasRevFDeriv R x x') (hu : ∀ u, x u ≠ 0) :
@@ -70,6 +71,7 @@ theorem log.arg_x.HasRevFDeriv_rule
   sorry_proof
 
 omit [CompleteSpace U] in
+set_option linter.unusedVariables false in
 @[data_synth]
 theorem log.arg_x.HasRevFDerivUpdate_rule
     (x : U → R) {x'} (hx : HasRevFDerivUpdate R x x') (hu : ∀ u, x u ≠ 0) :

SciLean/Algebra/Dimension.lean

@@ -64,7 +64,7 @@ instance {R} [Field R] {n m}
     {Y} [AddCommGroup Y] [Module R Y] [Module.Finite R Y] [dY : Dimension R Y m] :
     Dimension R (X×Y) (n+m) where
   is_dim := by
-    simp [dX.is_dim, dY.is_dim]
+    simp []
 
 -- instance {R} [Field R] {n}
 --     {I} [IndexType I]

SciLean/Algebra/IsAddGroupHom.lean

@@ -110,7 +110,7 @@ theorem HAdd.hAdd.arg_a0a1.IsAddGroupHom_rule
     (f g : X → Y) (hf : IsAddGroupHom f) (hg : IsAddGroupHom g) :
     IsAddGroupHom fun x => f x + g x := by
   constructor
-  · simp [hf.map_add,hg.map_add,add_comm]; sorry_proof
+  · simp [hf.map_add,hg.map_add]; sorry_proof
   · simp [hf.map_neg,hg.map_neg,add_comm]
 
 
@@ -124,7 +124,7 @@ theorem HSub.hSub.arg_a0a1.IsAddGroupHom_rule
     (f g : X → Y) (hf : IsAddGroupHom f) (hg : IsAddGroupHom g) :
     IsAddGroupHom fun x => f x - g x := by
   constructor
-  · simp [hf.map_add,hg.map_add,add_comm]; sorry_proof
+  · simp [hf.map_add,hg.map_add]; sorry_proof
   · simp [hf.map_neg,hg.map_neg,add_comm,←neg_add_eq_sub]
 
 

SciLean/Algebra/VectorOptimize/Basic.lean

@@ -140,7 +140,7 @@ theorem tmulAdd_smul_y (a b : R) (y : Y) (x : X) (A : YX) :
 @[simp, simp_core, vector_optimize]
 theorem tmulAdd_smul_x (a b : R) (y : Y) (x : X) (A : YX) :
     tmulAdd a y (b•x) A = tmulAdd (a*b) y x A := by
-  simp [axpby_spec,tmulAdd_spec]
+  simp [tmulAdd_spec]
   sorry_proof
 
 

SciLean/Analysis/AdjointSpace/Adjoint.lean

@@ -334,7 +334,7 @@ theorem HMul.hMul.arg_a0.adjoint_rule
 by
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   simp (disch:=fun_prop)
-    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+    [adjoint_inner_left,AdjointSpace.inner_smul_left]
   intros; ac_rfl
 
 open ComplexConjugate in
@@ -347,7 +347,7 @@ theorem HMul.hMul.arg_a1.adjoint_rule
 by
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   simp (disch:=fun_prop)
-    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+    [adjoint_inner_left,AdjointSpace.inner_smul_left]
   intros; ac_rfl
 
 
@@ -394,7 +394,7 @@ theorem HDiv.hDiv.arg_a0.adjoint_rule
 by
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   simp (disch:=fun_prop)
-    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+    [adjoint_inner_left,AdjointSpace.inner_smul_left]
   simp [div_eq_mul_inv]
   intros; ac_rfl
 
@@ -481,7 +481,7 @@ theorem Inner.inner.arg_a1.adjoint_rule
 by
   rw[← (eq_adjoint_iff _ _ (by sorry_proof)).2]
   simp (disch:=fun_prop)
-    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.conj_symm,mul_comm]
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,mul_comm]
 
 
 section OnRealSpace

SciLean/Analysis/AdjointSpace/Basic.lean

@@ -144,7 +144,7 @@ theorem inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 := by
   constructor
   · have ⟨c,d,hc,_,h⟩ := inner_top_equiv_norm (𝕜:=𝕜) (E:=E)
     have ⟨h,_⟩ := h x
-    intro h'; simp[h'] at h
+    intro h'; simp[] at h
     have : ‖x‖^2 ≤ 0 := by nlinarith
     have : ‖x‖ ≤ 0 := by nlinarith
     simp_all only [gt_iff_lt, smul_eq_mul, norm_le_zero_iff]

SciLean/Analysis/AdjointSpace/HasAdjoint.lean

@@ -253,7 +253,7 @@ theorem pi_rule {I : Type*} {n} [IndexType I n] [Fold.{_,u'} I] [Fold.{_,u} I]
   case adjoint =>
     intro x y
     have h := fun i => (hf i).adjoint
-    simp[Inner.inner, h]
+    simp[Inner.inner]
     sorry_proof
   case is_linear => apply IsContinuousLinearMap.pi_rule _ (fun i => (hf i).is_linear)
 
@@ -376,7 +376,7 @@ theorem HAdd.hAdd.arg_a0a1.HasAdjoint_simple_rule :
       (fun x : X×X => x.1 + x.2)
       (fun x => (x,x)) := by
   constructor
-  case adjoint => simp[AdjointSpace.inner_prod_split, AdjointSpace.inner_add_left, AdjointSpace.inner_add_right]
+  case adjoint => simp[AdjointSpace.inner_prod_split, AdjointSpace.inner_add_left]
   case is_linear => fun_prop
 
 @[data_synth]
@@ -396,7 +396,7 @@ theorem HSub.hSub.arg_a0a1.HasAdjoint_simple_rule :
       (fun x : X×X => x.1 - x.2)
       (fun x => (x, -x)) := by
   constructor
-  case adjoint => simp[AdjointSpace.inner_prod_split, AdjointSpace.inner_add_left, AdjointSpace.inner_add_right,sub_eq_add_neg]
+  case adjoint => simp[AdjointSpace.inner_prod_split, AdjointSpace.inner_add_left,sub_eq_add_neg]
   case is_linear => fun_prop
 
 @[data_synth]
@@ -480,7 +480,7 @@ theorem HSMul.hSMul.arg_a1.HasAdjoint_simple_rule_nat (n : ℕ) :
   case adjoint =>
     intro x y;
     simp [← Nat.cast_smul_eq_nsmul (R:=K),AdjointSpace.inner_smul_left,
-          AdjointSpace.inner_smul_right,AdjointSpace.inner_add_right]
+          AdjointSpace.inner_smul_right]
   case is_linear =>
     simp [← Nat.cast_smul_eq_nsmul (R:=K)]; fun_prop
 
@@ -507,7 +507,7 @@ theorem HSMul.hSMul.arg_a1.HasAdjointUpdate_simple_rule_nat (n : ℕ) :
     case adjoint =>
       intro x y;
       simp [← Int.cast_smul_eq_zsmul (R:=K),AdjointSpace.inner_smul_left,
-            AdjointSpace.inner_smul_right,AdjointSpace.inner_add_right]
+            AdjointSpace.inner_smul_right]
     case is_linear =>
       simp [← Int.cast_smul_eq_zsmul (R:=K)]; fun_prop
 
@@ -684,7 +684,7 @@ theorem Finset.sum.arg_f.HasAdjoint_simp_rule
     (A : Finset I) :
     HasAdjoint K
       (fun f : I → X => A.sum (fun i => f i))
-      (fun k i => A.toSet.indicator (fun _ => k) i) := by
+      (fun k i => (A : Set I).indicator (fun _ => k) i) := by
   constructor
   case adjoint => intro f y; simp[Inner.inner]; sorry_proof -- missing API
   case is_linear => fun_prop
@@ -697,7 +697,7 @@ theorem Finset.sum.arg_f.HasAdjoint_simp_rule'
     (A : Finset I) :
     HasAdjoint K
       (fun f : I → X => A.sum f)
-      (fun k i => A.toSet.indicator (fun _ => k) i) := by
+      (fun k i => (A : Set I).indicator (fun _ => k) i) := by
   constructor
   case adjoint => intro f y; simp[Inner.inner]; sorry_proof -- missing API
   case is_linear => fun_prop
@@ -708,7 +708,7 @@ theorem Finset.sum.arg_f.HasAdjointUpdate_simp_rule
     (A : Finset I) :
     HasAdjointUpdate K
       (fun f : I → X => A.sum (fun i => f i))
-      (fun k f i => f i + A.toSet.indicator (fun _ => k) i) := by
+      (fun k f i => f i + (A : Set I).indicator (fun _ => k) i) := by
   constructor
   case adjoint => intro f y; simp[Inner.inner]; sorry_proof -- missing API
   case is_linear => fun_prop
@@ -721,7 +721,7 @@ theorem Finset.sum.arg_f.HasAdjointUpdate_simp_rule'
     (A : Finset I) :
     HasAdjointUpdate K
       (fun f : I → X => A.sum f)
-      (fun k f i => f i + A.toSet.indicator (fun _ => k) i) := by
+      (fun k f i => f i + (A : Set I).indicator (fun _ => k) i) := by
   constructor
   case adjoint => intro f y; simp[Inner.inner]; sorry_proof -- missing API
   case is_linear => fun_prop
@@ -763,7 +763,7 @@ theorem Inner.inner.arg_a0.HasAdjoint_simple_rule_real
   constructor
   case adjoint =>
     intro x k
-    simp[AdjointSpace.inner_smul_right,ScalarInner.inner_eq_inner_re_im]
+    simp[ScalarInner.inner_eq_inner_re_im]
     -- lhs has complex inner product and rhs has real inner product
     -- it should work out
     sorry_proof