refactor: golf wrapper proofs

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

@@ -166,9 +166,8 @@ decreasing at that time. -/
 lemma energy_not_conserved (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (t : Time)
     (h1 : S.EquationOfMotion xₜ) (hx : ContDiff ℝ ∞ xₜ) (hdx : ∂ₜ xₜ t ≠ 0) (hγ : 0 < S.γ) :
     ∂ₜ (S.energy xₜ) t < 0 := by
-  rw [energy_dissipation_rate S xₜ t h1 hx]
-  rw [neg_mul]
-  exact neg_neg_of_pos (mul_pos hγ (real_inner_self_pos.mpr hdx))
+  simpa [energy_dissipation_rate S xₜ t h1 hx, neg_mul] using
+    neg_neg_of_pos (mul_pos hγ (real_inner_self_pos.mpr hdx))
 
 /-!
 ## C. Newton's second law
@@ -206,8 +205,7 @@ lemma equationOfMotion_iff_newtons_2nd_law (xₜ : Time → EuclideanSpace ℝ (
   constructor
   · intro h t
     have h' :
-        S.m • ∂ₜ (∂ₜ xₜ) t + (S.γ • ∂ₜ xₜ t + S.k • xₜ t) = 0 := by
-      simpa [add_assoc] using h t
+        S.m • ∂ₜ (∂ₜ xₜ) t + (S.γ • ∂ₜ xₜ t + S.k • xₜ t) = 0 := by simpa [add_assoc] using h t
     have ha :
         S.m • ∂ₜ (∂ₜ xₜ) t = -(S.γ • ∂ₜ xₜ t + S.k • xₜ t) :=
       eq_neg_of_add_eq_zero_left h'
@@ -267,39 +265,33 @@ lemma discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq :
 
 /-- The decay rate is nonnegative. -/
 lemma decayRate_nonneg : 0 ≤ S.decayRate := by
-  rw [decayRate]
-  exact div_nonneg S.γ_nonneg (by nlinarith [S.m_pos])
+  simpa [decayRate] using div_nonneg S.γ_nonneg (by nlinarith [S.m_pos])
 
 /-- An undamped oscillator lies in the underdamped regime. -/
 lemma isUnderdamped_of_gamma_eq_zero (hγ : S.γ = 0) : S.IsUnderdamped := by
-  rw [IsUnderdamped, discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq S, decayRate]
-  rw [hγ]
+  rw [IsUnderdamped, discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq S, decayRate, hγ]
   ring_nf
   nlinarith [sq_pos_of_pos S.m_pos, sq_pos_of_pos S.ω_pos]
 
 /-- An underdamped system has decay rate less than the natural frequency. -/
 lemma isUnderdamped_decayRate (hS : S.IsUnderdamped) : S.decayRate < S.ω := by
-  rw [IsUnderdamped] at hS
-  rw [discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq] at hS
+  rw [IsUnderdamped, discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq] at hS
   have hm_sq_pos : 0 < 4 * S.m^2 := by
     have hsq : 0 < S.m^2 := sq_pos_of_pos S.m_pos
     nlinarith
-  have hsq : S.decayRate^2 < S.ω^2 := by
-    nlinarith
+  have hsq : S.decayRate^2 < S.ω^2 := by nlinarith
   nlinarith [S.decayRate_nonneg, S.ω_pos]
 
 /-- A critically damped system has decay rate equal to the natural frequency. -/
 lemma isCriticallyDamped_decayRate (hS : S.IsCriticallyDamped) : S.ω = S.decayRate := by
-  rw [IsCriticallyDamped] at hS
-  rw [discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq] at hS
+  rw [IsCriticallyDamped, discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq] at hS
   have hm_sq_ne_zero : 4 * S.m^2 ≠ 0 := by
     have hm_sq_pos : 0 < 4 * S.m^2 := by
       have hsq : 0 < S.m^2 := sq_pos_of_pos S.m_pos
       nlinarith
     exact ne_of_gt hm_sq_pos
   have hsq : S.decayRate^2 = S.ω^2 := by
-    have hsub : S.decayRate^2 - S.ω^2 = 0 := by
-      exact (mul_eq_zero.mp hS).resolve_left hm_sq_ne_zero
+    have hsub : S.decayRate^2 - S.ω^2 = 0 := (mul_eq_zero.mp hS).resolve_left hm_sq_ne_zero
     linarith
   nlinarith [S.decayRate_nonneg, S.ω_pos]
 
@@ -317,20 +309,17 @@ lemma k_eq_m_mul_ω_sq : S.k = S.m * S.ω^2 := by
 lemma k_eq_m_mul_decayRate_sq_of_criticallyDamped (hS : S.IsCriticallyDamped) :
     S.k = S.m * S.decayRate^2 := by
   have hωa : S.ω = S.decayRate := S.isCriticallyDamped_decayRate hS
-  have hωsq : S.decayRate ^ 2 = S.k / S.m := by
-    simpa [hωa] using S.ω_sq
+  have hωsq : S.decayRate ^ 2 = S.k / S.m := by simpa [hωa] using S.ω_sq
   field_simp [S.m_ne_zero] at hωsq
   nlinarith
 
 /-- An overdamped system has decay rate greater than the natural frequency. -/
 lemma isOverdamped_decayRate (hS : S.IsOverdamped) : S.ω < S.decayRate := by
-  rw [IsOverdamped] at hS
-  rw [discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq] at hS
+  rw [IsOverdamped, discriminant_eq_four_mul_m_sq_mul_decayRate_sq_sub_ω_sq] at hS
   have hm_sq_pos : 0 < 4 * S.m^2 := by
     have hsq : 0 < S.m^2 := sq_pos_of_pos S.m_pos
     nlinarith
-  have hsq : S.ω^2 < S.decayRate^2 := by
-    nlinarith
+  have hsq : S.ω^2 < S.decayRate^2 := by nlinarith
   nlinarith [S.decayRate_nonneg, S.ω_pos]
 
 /-- In the underdamped regime, the selected frequency uses the oscillation frequency. -/
@@ -439,8 +428,7 @@ for the corresponding undamped harmonic oscillator. -/
 lemma toUndamped_equationOfMotion (S : DampedHarmonicOscillator) (hS : S.IsUndamped)
     (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) :
     S.EquationOfMotion xₜ ↔ (S.toUndamped hS).EquationOfMotion xₜ := by
-  have hγ : S.γ = 0 := by
-    simpa [IsUndamped] using hS
+  have hγ : S.γ = 0 := by simpa [IsUndamped] using hS
   rw [S.equationOfMotion_iff_newtons_2nd_law xₜ,
     (S.toUndamped hS).equationOfMotion_iff_newtons_2nd_law xₜ hx]
   constructor
@@ -454,8 +442,7 @@ lemma toUndamped_equationOfMotion (S : DampedHarmonicOscillator) (hS : S.IsUndam
     calc
       S.m • ∂ₜ (∂ₜ xₜ) t = (S.toUndamped hS).m • ∂ₜ (∂ₜ xₜ) t := rfl
       _ = HarmonicOscillator.force (S.toUndamped hS) (xₜ t) := h t
-      _ = force S xₜ t := by
-        simp [force, HarmonicOscillator.force_eq_linear, toUndamped, hγ]
+      _ = force S xₜ t := by simp [force, HarmonicOscillator.force_eq_linear, toUndamped, hγ]
 
 end DampedHarmonicOscillator
 

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean

@@ -178,8 +178,7 @@ private lemma exp_decay_smul_velocity
     ∂ₜ (fun t : Time => exp (-a * t.val) • y t) =
       fun t : Time => exp (-a * t.val) • (∂ₜ y t - a • y t) := by
   funext t
-  rw [Time.deriv]
-  rw [fderiv_fun_smul (by fun_prop) (hy t)]
+  rw [Time.deriv, fderiv_fun_smul (by fun_prop) (hy t)]
   rw [fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply,
     fderiv_fun_neg, fderiv_fun_const, Pi.zero_apply, Time.fderiv_val,
@@ -197,11 +196,9 @@ private lemma exp_decay_smul_acceleration
         (μ • y t - (2 * a) • ∂ₜ y t + a^2 • y t) := by
   rw [exp_decay_smul_velocity a y hy]
   funext t
-  rw [Time.deriv]
-  rw [fderiv_fun_smul (by fun_prop) (by fun_prop)]
+  rw [Time.deriv, fderiv_fun_smul (by fun_prop) (by fun_prop)]
   rw [fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop)]
-  rw [fderiv_fun_sub (hdy t) (by fun_prop)]
-  rw [fderiv_fun_const_smul (hy t)]
+  rw [fderiv_fun_sub (hdy t) (by fun_prop), fderiv_fun_const_smul (hy t)]
   have hy''_t := congrFun hy'' t
   rw [Time.deriv] at hy''_t
   simp only [add_apply, _root_.sub_apply,
@@ -219,9 +216,7 @@ private lemma exp_decay_smul_equationOfMotion
     (hγ : S.γ = 2 * S.m * a) (hk : S.k = S.m * (a^2 - μ)) :
     S.EquationOfMotion (fun t : Time => exp (-a * t.val) • y t) := by
   intro t
-  rw [exp_decay_smul_acceleration a μ y hy hdy hy'']
-  rw [exp_decay_smul_velocity a y hy]
-  rw [hγ, hk]
+  rw [exp_decay_smul_acceleration a μ y hy hdy hy'', exp_decay_smul_velocity a y hy, hγ, hk]
   simp [smul_add, smul_sub, smul_smul]
   module
 

Physlib/ClassicalMechanics/EulerLagrange.lean

@@ -36,8 +36,7 @@ lemma eulerLagrangeOp_eq (L : Time → X → X → ℝ) (q : Time → X) :
     - ∂ₜ (fun t' => gradient (L t' (q t') ·) (∂ₜ q t')) t := by rfl
 
 lemma eulerLagrangeOp_zero (q : Time → X) :
-    eulerLagrangeOp (fun _ _ _ => 0) q = fun _ => 0 := by
-  simp [eulerLagrangeOp_eq, Time.deriv_eq]
+    eulerLagrangeOp (fun _ _ _ => 0) q = fun _ => 0 := by simp [eulerLagrangeOp_eq, Time.deriv_eq]
 
 /- The variational derivative of `L t (q' t) (deriv q' t))` for a lagrangian `L`
   is equal to the `eulerLagrangeOp`. -/

Physlib/ClassicalMechanics/HamiltonsEquations.lean

@@ -43,8 +43,7 @@ noncomputable def hamiltonEqOp (H : Time → X → X → ℝ) (p : Time → X) (
 
 lemma hamiltonEqOp_eq (H : Time → X → X → ℝ) (p : Time → X) (q : Time → X) :
     hamiltonEqOp H p q = fun t => (∂ₜ q t + -gradient (fun x => H t x (q t)) (p t),
-      - ∂ₜ p t + -gradient (fun x => H t (p t) x) (q t)) := by
-  rfl
+      - ∂ₜ p t + -gradient (fun x => H t (p t) x) (q t)) := rfl
 
 lemma hamiltonEqOp_eq_zero_iff_hamiltons_equations (H : Time → X → X → ℝ)
     (p : Time → X) (q : Time → X) :

Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -155,8 +155,7 @@ lemma ω_pos : 0 < S.ω := sqrt_pos.mpr (div_pos S.k_pos S.m_pos)
 
 /-- The square of the angular frequency of the classical harmonic oscillator is equal to `k/m`. -/
 lemma ω_sq : S.ω^2 = S.k / S.m := by
-  rw [ω, sq_sqrt]
-  exact div_nonneg (le_of_lt S.k_pos) (le_of_lt S.m_pos)
+  simpa only [ω] using sq_sqrt (div_nonneg (le_of_lt S.k_pos) (le_of_lt S.m_pos))
 
 /-- The angular frequency of the classical harmonic oscillator is not equal to zero. -/
 lemma ω_ne_zero : S.ω ≠ 0 := Ne.symm (ne_of_lt S.ω_pos)
@@ -263,8 +262,7 @@ lemma kineticEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : Con
   unfold kineticEnergy
   conv_lhs => simp only [Time.deriv, one_div, ringHom_apply]
   change (fderiv ℝ ((fun x => 2⁻¹ * S.m * ⟪x, x⟫_ℝ) ∘ (fun t => ∂ₜ xₜ t)) t) 1 = _
-  rw [fderiv_comp]
-  rw [fderiv_const_mul (by fun_prop)]
+  rw [fderiv_comp, fderiv_const_mul (by fun_prop)]
   simp only [ContinuousLinearMap.smul_comp, FunLike.coe_smul,
     ContinuousLinearMap.coe_comp, Pi.smul_apply, Function.comp_apply, smul_eq_mul]
   rw [fderiv_inner_apply]
@@ -281,8 +279,7 @@ lemma potentialEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : C
   unfold potentialEnergy
   conv_lhs => simp only [Time.deriv, one_div, smul_eq_mul]
   change (fderiv ℝ ((fun x => 2⁻¹ * (S.k * ⟪x, x⟫_ℝ)) ∘ (fun t => xₜ t)) t) 1 = _
-  rw [fderiv_comp]
-  rw [fderiv_const_mul (by fun_prop), fderiv_const_mul (by fun_prop)]
+  rw [fderiv_comp, fderiv_const_mul (by fun_prop), fderiv_const_mul (by fun_prop)]
   simp only [ContinuousLinearMap.smul_comp, FunLike.coe_smul,
     ContinuousLinearMap.coe_comp, Pi.smul_apply, Function.comp_apply, smul_eq_mul]
   rw [fderiv_inner_apply]
@@ -302,11 +299,9 @@ lemma energy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff 
     ∂ₜ (energy S xₜ) = fun t => ⟪∂ₜ xₜ t, S.m • ∂ₜ (∂ₜ xₜ) t + S.k • xₜ t⟫_ℝ := by
   unfold energy
   funext t
-  rw [Time.deriv_eq]
-  rw [fderiv_fun_add (by fun_prop) (by apply S.potentialEnergy_differentiable xₜ hx)]
+  rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by apply S.potentialEnergy_differentiable xₜ hx)]
   simp only [_root_.add_apply]
-  rw [← Time.deriv_eq, ← Time.deriv_eq]
-  rw [potentialEnergy_deriv, kineticEnergy_deriv]
+  rw [← Time.deriv_eq, ← Time.deriv_eq, potentialEnergy_deriv, kineticEnergy_deriv]
   simp only
   rw [← inner_add_right]
   fun_prop
@@ -418,10 +413,8 @@ lemma gradient_const_mul_inner_self (c : ℝ) (x : EuclideanSpace ℝ (Fin 1)) :
           rw [fderiv_const_mul]; fun_prop
     _ = c • gradient (fun y : EuclideanSpace ℝ (Fin 1) => ⟪y, y⟫_ℝ) x := by
           simp only [gradient, map_smul]
-    _ = c • ((2 : ℝ) • x) := by
-          rw [gradient_inner_self]
-    _ = (2 * c) • x := by
-          rw [smul_smul, mul_comm]
+    _ = c • ((2 : ℝ) • x) := by rw [gradient_inner_self]
+    _ = (2 * c) • x := by rw [smul_smul, mul_comm]
 
 /-!
 
@@ -689,12 +682,9 @@ noncomputable def toCanonicalMomentum (t : Time) (x : EuclideanSpace ℝ (Fin 1)
     EuclideanSpace ℝ (Fin 1) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 1) where
   toFun v := gradient (S.lagrangian t x ·) v
   invFun p := (1 / S.m) • p
-  left_inv v := by
-    simp [gradient_lagrangian_velocity_eq]
-  right_inv p := by
-    simp [gradient_lagrangian_velocity_eq]
-  map_add' v1 v2 := by
-    simp [gradient_lagrangian_velocity_eq]
+  left_inv v := by simp [gradient_lagrangian_velocity_eq]
+  right_inv p := by simp [gradient_lagrangian_velocity_eq]
+  map_add' v1 v2 := by simp [gradient_lagrangian_velocity_eq]
   map_smul' c v := by
     simp [gradient_lagrangian_velocity_eq]
     module

Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean

@@ -122,9 +122,7 @@ homeomorphism underlies the single global chart used for the smooth-manifold str
 def valHomeomorphism : ConfigurationSpace ≃ₜ EuclideanSpace ℝ (Fin 1) where
   toEquiv := valEquiv
   continuous_toFun := continuous_induced_dom
-  continuous_invFun := by
-    apply continuous_induced_rng.mpr
-    exact continuous_id
+  continuous_invFun := continuous_induced_rng.mpr continuous_id
 
 /-- Configuration space is Hausdorff, transported from `EuclideanSpace ℝ (Fin 1)` across the
 coordinate homeomorphism. -/
@@ -148,8 +146,7 @@ chart's self-transition, which is analytic, so chart compatibility is immediate.
 instance : ChartedSpace (EuclideanSpace ℝ (Fin 1)) ConfigurationSpace where
   atlas := { valHomeomorphism.toOpenPartialHomeomorph }
   chartAt _ := valHomeomorphism.toOpenPartialHomeomorph
-  mem_chart_source := by
-    simp
+  mem_chart_source := by simp
   chart_mem_atlas := by
     intro x
     simp

Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean

@@ -386,8 +386,7 @@ The trajectory for zero initial conditions is the zero function.
 
 /-- For zero initial conditions, the trajectory is zero. -/
 @[simp]
-lemma trajectory_zero : trajectory S 0 = fun _ => 0 := by
-  simp [trajectory_eq]
+lemma trajectory_zero : trajectory S 0 = fun _ => 0 := by simp [trajectory_eq]
 
 /-!
 
@@ -549,8 +548,7 @@ lemma trajectories_unique (IC : InitialConditions) (x : Time → EuclideanSpace
   have hy_deriv : ∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (IC.trajectory S) t :=
     dsub x _ (hx.differentiable (by simp)) (hTraj.differentiable (by simp))
   have hy_deriv2 : ∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (IC.trajectory S)) t := by
-    rw [hy_deriv]
-    exact dsub _ _ (deriv_differentiable_of_contDiff _ hx)
+    simpa [hy_deriv] using dsub _ _ (deriv_differentiable_of_contDiff _ hx)
       (deriv_differentiable_of_contDiff _ hTraj)
   have hNewt_x := (S.equationOfMotion_iff_newtons_2nd_law x hx).1 hEOM
   have hNewt_traj := (S.equationOfMotion_iff_newtons_2nd_law (IC.trajectory S) hTraj).1
@@ -1000,8 +998,7 @@ lemma trajectory_velocity_eq_zero_iff_exists_int (IC : InitialConditions)
       linarith
     calc
       (t : ℝ) = (S.ω * t) / S.ω := by field_simp [hω]
-      _ = ((AmplitudePhase.fromInitialConditions S IC).φ + n * π) / S.ω := by
-        rw [ht]
+      _ = ((AmplitudePhase.fromInitialConditions S IC).φ + n * π) / S.ω := by rw [ht]
   · intro h
     obtain ⟨n, hn⟩ := h
     rw [Real.sin_eq_zero_iff]
@@ -1039,8 +1036,7 @@ lemma trajectory_velocity_eq_zero_iff_norm_eq_amplitude (IC : InitialConditions)
       ext i
       fin_cases i
       simp [hA]
-  rw [trajectory_velocity_eq_zero_iff_sin_eq_zero S IC hA t]
-  rw [trajectory_eq_cos]
+  rw [trajectory_velocity_eq_zero_iff_sin_eq_zero S IC hA t, trajectory_eq_cos]
   set A := (AmplitudePhase.fromInitialConditions S IC).A
   set θ := S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ
   show sin θ = 0 ↔ ‖EuclideanSpace.single 0 (A * cos θ)‖ = A
@@ -1055,8 +1051,7 @@ lemma trajectory_velocity_eq_zero_iff_norm_eq_amplitude (IC : InitialConditions)
     · simp [hcos, abs_of_pos hA_pos]
     · simp [hcos, abs_of_pos hA_pos]
   · intro hnorm
-    have hnorm' : |A * cos θ| = A := by
-      simpa using hnorm
+    have hnorm' : |A * cos θ| = A := by simpa using hnorm
     have hcos_abs : |cos θ| = 1 := by
       calc
         |cos θ| = |A * cos θ| / A := by
@@ -1118,8 +1113,7 @@ lemma trajectory_eq_zero_iff_exists_int (IC : InitialConditions)
       linarith
     calc
       (t : ℝ) = (S.ω * t) / S.ω := by field_simp [hω]
-      _ = ((AmplitudePhase.fromInitialConditions S IC).φ + (2 * n + 1) * π / 2) / S.ω := by
-        rw [ht]
+      _ = ((AmplitudePhase.fromInitialConditions S IC).φ + (2 * n + 1) * π / 2) / S.ω := by rw [ht]
   · intro h
     obtain ⟨n, hn⟩ := h
     rw [Real.cos_eq_zero_iff]
@@ -1182,8 +1176,7 @@ lemma trajectory_periodic (IC : InitialConditions) :
   have h : S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π := by
     have := S.ω_ne_zero
     ring_nf; field_simp
-  rw [InitialConditions.trajectory, add_val, period_eq, h, cos_add_two_pi, sin_add_two_pi]
-  rfl
+  simp [InitialConditions.trajectory, add_val, period_eq, h, cos_add_two_pi, sin_add_two_pi]
 
 /-!
 
@@ -1217,18 +1210,14 @@ lemma return_time (IC : InitialConditions) (non_trivial : IC.x₀ ≠ 0 ∨ IC.v
   have zero_lt_det :  0 < det := by
    cases non_trivial with
    | inl hx =>
-    have  xx_gt_zero : 0 < xx  := by
-        apply real_inner_self_pos.mpr
-        exact hx
+    have  xx_gt_zero : 0 < xx  := real_inner_self_pos.mpr hx
     calc
       0 < xx * S.ω^2 := by bound
       _ ≤  ‖IC.v₀‖^2 +   xx * S.ω^2  := by bound
       _ = vv +   xx * S.ω^2 := by rw [← real_inner_self_eq_norm_sq IC.v₀]
       _ = det := by rfl
    | inr hv =>
-     have vv_gt_zero : 0 < vv := by
-        apply real_inner_self_pos.mpr
-        exact hv
+     have vv_gt_zero : 0 < vv := real_inner_self_pos.mpr hv
      calc
         0 <  vv := vv_gt_zero
         _ ≤ vv +   ‖IC.x₀‖^2 * S.ω^2 := by bound