refactor: golf proofs

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean

@@ -178,15 +178,13 @@ 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 [fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop)]
+  rw [Time.deriv, fderiv_fun_smul (by fun_prop) (hy t), 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,
     _root_.neg_apply, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]
   rw [← Time.deriv_eq]
-  simp [smul_sub, smul_smul]
-  module
+  simp [smul_smul, sub_eq_add_neg]
 
 private lemma exp_decay_smul_acceleration
     (a μ : ℝ) (y : Time → EuclideanSpace ℝ (Fin 1))
@@ -197,11 +195,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 [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 [Time.deriv, fderiv_fun_smul (by fun_prop) (by fun_prop),
+    fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop),
+    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,
@@ -210,7 +206,7 @@ private lemma exp_decay_smul_acceleration
     FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]
   rw [hy''_t, ← Time.deriv_eq]
   simp [smul_add, smul_sub, smul_smul]
-  module
+  ext i; simp; ring
 
 private lemma exp_decay_smul_equationOfMotion
     (a μ : ℝ) (y : Time → EuclideanSpace ℝ (Fin 1))
@@ -219,11 +215,10 @@ 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
+  ext i; simp; ring
 
 /-!
 
@@ -234,12 +229,17 @@ polynomial, and hyperbolic base trajectories before the exponential decay factor
 
 -/
 
+private lemma fderiv_comp_val_eq_deriv {t : Time} (g : ℝ → ℝ)
+    (hg : DifferentiableAt ℝ g t.val) :
+    (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
+  rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
+  simp
+
 private lemma criticallyDampedBase_velocity (IC : InitialConditions) :
     ∂ₜ (S.criticallyDampedBase IC) =
       fun _ : Time => IC.v₀ + S.decayRate • IC.x₀ := by
   funext t
-  change ∂ₜ (fun t : Time =>
-    IC.x₀ + t.val • (IC.v₀ + S.decayRate • IC.x₀)) t = _
+  unfold criticallyDampedBase
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_fun_const, fderiv_smul_const (by fun_prop)]
   simp
@@ -262,11 +262,6 @@ private lemma underdampedBase_velocity (IC : InitialConditions) (hS : S.IsUnderd
           (IC.v₀ + S.decayRate • IC.x₀) := by
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_underdamped hS
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -287,11 +282,6 @@ private lemma underdampedBase_acceleration (IC : InitialConditions) (hS : S.IsUn
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_underdamped hS
   rw [S.underdampedBase_velocity IC hS]
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -312,11 +302,6 @@ private lemma overdampedBase_velocity (IC : InitialConditions) (hS : S.IsOverdam
           (IC.v₀ + S.decayRate • IC.x₀) := by
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_overdamped hS
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -337,11 +322,6 @@ private lemma overdampedBase_acceleration (IC : InitialConditions) (hS : S.IsOve
   have hΩ : S.angularFrequency ≠ 0 := S.angularFrequency_ne_zero_of_overdamped hS
   rw [S.overdampedBase_velocity IC hS]
   funext t
-  have fderiv_comp_val_eq_deriv : ∀ g : ℝ → ℝ, DifferentiableAt ℝ g t.val →
-      (fderiv ℝ (fun s : Time => g s.val) t) 1 = _root_.deriv g t.val := by
-    intro g hg
-    rw [fderiv_fun_comp t hg (by fun_prop), ContinuousLinearMap.comp_apply, Time.fderiv_val]
-    simp
   rw [Time.deriv_eq, fderiv_fun_add (by fun_prop) (by fun_prop),
     fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   simp only [add_apply, ContinuousLinearMap.smulRight_apply]
@@ -375,8 +355,9 @@ lemma trajectory_equationOfMotion_of_criticallyDamped (IC : InitialConditions)
       fun_prop)
     (by
       rw [S.criticallyDampedBase_velocity IC]
-      fun_prop) ?_ hγ hk
-  simpa using S.criticallyDampedBase_acceleration IC
+      fun_prop)
+    (by
+      simpa using S.criticallyDampedBase_acceleration IC) hγ hk
 
 /-- In the underdamped regime, the selected trajectory satisfies the damped equation of
 motion. -/
@@ -388,13 +369,14 @@ lemma trajectory_equationOfMotion_of_underdamped (IC : InitialConditions)
   have hk : S.k = S.m * (S.decayRate^2 - (-S.angularFrequency^2)) := by
     rw [S.k_eq_m_mul_ω_sq, S.angularFrequency_sq_of_underdamped hS]
     ring
-  refine S.exp_decay_smul_equationOfMotion S.decayRate
-    (-S.angularFrequency^2) (S.underdampedBase IC)
+  refine S.exp_decay_smul_equationOfMotion S.decayRate (-S.angularFrequency^2)
+    (S.underdampedBase IC)
     (by
       unfold underdampedBase
       fun_prop) ?_
     (S.underdampedBase_acceleration IC hS) hγ hk
-  rw [show ∂ₜ (S.underdampedBase IC) = _ from S.underdampedBase_velocity IC hS]
+  unfold underdampedBase
+  rw [S.underdampedBase_velocity IC hS]
   fun_prop
 
 /-- In the overdamped regime, the selected trajectory satisfies the damped equation of
@@ -413,7 +395,8 @@ lemma trajectory_equationOfMotion_of_overdamped (IC : InitialConditions)
       unfold overdampedBase
       fun_prop) ?_
     (S.overdampedBase_acceleration IC hS) hγ hk
-  rw [show ∂ₜ (S.overdampedBase IC) = _ from S.overdampedBase_velocity IC hS]
+  unfold overdampedBase
+  rw [S.overdampedBase_velocity IC hS]
   fun_prop
 
 /-- The selected trajectory satisfies the damped equation of motion. -/

Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -273,7 +273,7 @@ lemma kineticEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : Con
   congr 1
   simp only [smul_add]
   module
-  repeat fun_prop
+  all_goals fun_prop
 
 lemma potentialEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) :
     ∂ₜ (fun t => potentialEnergy S (xₜ t)) = fun t => ⟪∂ₜ xₜ t, S.k • xₜ t⟫_ℝ := by
@@ -293,10 +293,7 @@ lemma potentialEnergy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : C
     congr 1
     module
   rw [real_inner_comm, ← inner_smul_right]
-  repeat fun_prop
-  apply Differentiable.differentiableAt
-  rw [contDiff_infty_iff_fderiv] at hx
-  exact hx.1
+  all_goals (first | fun_prop | exact (hx.contDiffAt (x := t)).differentiableAt (by simp))
 
 lemma energy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) :
     ∂ₜ (energy S xₜ) = fun t => ⟪∂ₜ xₜ t, S.m • ∂ₜ (∂ₜ xₜ) t + S.k • xₜ t⟫_ℝ := by
@@ -309,8 +306,7 @@ lemma energy_deriv (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff 
   rw [potentialEnergy_deriv, kineticEnergy_deriv]
   simp only
   rw [← inner_add_right]
-  fun_prop
-  fun_prop
+  all_goals fun_prop
 
 /-!
 
@@ -400,8 +396,6 @@ lemma gradient_inner_self (x : EuclideanSpace ℝ (Fin 1)) :
   unfold gradient
   rw [InnerProductSpace.toDual_symm_apply]
   have hid : DifferentiableAt ℝ (fun y : EuclideanSpace ℝ (Fin 1) => y) x := differentiableAt_id
-  rw [show (fun y : EuclideanSpace ℝ (Fin 1) => ⟪y, y⟫_ℝ) =
-      fun y => ⟪(fun y => y) y, (fun y => y) y⟫_ℝ from rfl]
   rw [fderiv_inner_apply (𝕜 := ℝ) hid hid]
   simp only [fderiv_fun_id, ContinuousLinearMap.coe_id', id_eq, real_inner_comm, inner_smul_left',
     ringHom_apply]

Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean

@@ -430,11 +430,9 @@ lemma trajectory_velocity (IC : InitialConditions) : ∂ₜ (IC.trajectory S) =
   rw [fderiv_smul_const (by fun_prop), fderiv_smul_const (by fun_prop)]
   have h1 : (fderiv ℝ (fun t => sin (S.ω * t.val) / S.ω) t) =
     (1/ S.ω) • (fderiv ℝ (fun t => sin (S.ω * t.val)) t) := by
-    rw [← fderiv_mul_const]
-    congr
-    funext t
-    field_simp
-    fun_prop
+    rw [div_eq_mul_inv, ← fderiv_mul_const (hc := ?_)]
+    · congr; funext t; ring
+    · fun_prop
   simp [h1]
   rw [fderiv_cos (by fun_prop), fderiv_sin (by fun_prop),
     fderiv_fun_mul (by fun_prop) (by fun_prop)]
@@ -507,8 +505,7 @@ lemma trajectory_equationOfMotion (IC : InitialConditions) :
   ext
   have hω : S.ω ≠ 0 := ω_ne_zero S
   have hωm : S.ω ^ 2 * S.m = S.k := by
-    rw [ω_sq]
-    field_simp [m_ne_zero S]
+    rw [ω_sq]; field_simp [m_ne_zero S]
   simp [trajectory_eq, smul_add, smul_smul, mul_comm]
   rw [← hωm]
   field_simp [hω]
@@ -529,57 +526,53 @@ for the given initial conditions.
   position and velocity, the difference `y = x - IC.trajectory S` also solves the
   equation of motion with zero initial conditions; energy conservation then forces
   its energy, and hence `y`, to vanish identically, so `x = IC.trajectory S`. -/
+private lemma timeDeriv_sub {f g : Time → EuclideanSpace ℝ (Fin 1)}
+    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
+    ∂ₜ (fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g t := by
+  funext s; simp [Time.deriv_eq, fderiv_fun_sub (hf s) (hg s)]
+
 lemma trajectories_unique (IC : InitialConditions) (x : Time → EuclideanSpace ℝ (Fin 1))
     (hx : ContDiff ℝ ∞ x) :
     S.EquationOfMotion x ∧ x 0 = IC.x₀ ∧ ∂ₜ x 0 = IC.v₀ →
     x = IC.trajectory S := by
   rintro ⟨hEOM, hx0, hv0⟩
   have hTraj : ContDiff ℝ ∞ (IC.trajectory S) := by fun_prop
-  -- Time-derivative of a difference of differentiable functions, used below on `x - traj`.
-  have dsub : ∀ f g : Time → EuclideanSpace ℝ (Fin 1),
-      Differentiable ℝ f → Differentiable ℝ g →
-      ∂ₜ (fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g t := by
-    intro f g hf hg
-    funext t
-    simp only [Time.deriv_eq, fderiv_fun_sub (hf t) (hg t), sub_apply]
-  -- The difference `y := x - traj` is smooth, again solves the equation of motion (the force is
-  -- linear), and has vanishing initial data; energy conservation then forces `y = 0`.
   set y : Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - IC.trajectory S t with hydef
   have hyContDiff : ContDiff ℝ ∞ y := hx.sub hTraj
-  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)
-      (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
     (trajectory_equationOfMotion S IC)
   have hEOM_y : S.EquationOfMotion y :=
     (S.equationOfMotion_iff_newtons_2nd_law y hyContDiff).2 fun t => by
+      have hy_deriv2 : ∂ₜ (∂ₜ y) t = ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (IC.trajectory S)) t := by
+        have hy_deriv : ∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (IC.trajectory S) t :=
+          timeDeriv_sub (hx.differentiable (by simp)) (hTraj.differentiable (by simp))
+        rw [hy_deriv]
+        exact congrFun (timeDeriv_sub
+          (deriv_differentiable_of_contDiff _ hx) (deriv_differentiable_of_contDiff _ hTraj)) t
       rw [hy_deriv2]
       simp [smul_sub, hNewt_x, hNewt_traj, hydef, force_eq_linear]
   have hE : ∀ t, S.energy y t = 0 := fun t =>
     (S.energy_conservation_of_equationOfMotion' y hyContDiff hEOM_y t).trans <| by
       have hy0 : y 0 = 0 := by simp [hydef, hx0]
       have hyv0 : ∂ₜ y 0 = 0 := by
-        rw [congrFun hy_deriv 0, hv0, trajectory_velocity_at_zero S IC]; simp
+        have hy_deriv : ∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (IC.trajectory S) t :=
+          timeDeriv_sub (hx.differentiable (by simp)) (hTraj.differentiable (by simp))
+        rw [congrFun hy_deriv 0, hv0, trajectory_velocity_at_zero S IC]
+        simp
       simp [HarmonicOscillator.energy, HarmonicOscillator.kineticEnergy,
-        HarmonicOscillator.potentialEnergy, hy0, hyv0, one_div, smul_eq_mul]
-  -- Both energies are nonnegative, so a vanishing total energy forces `y t = 0`.
+        HarmonicOscillator.potentialEnergy, hy0, hyv0]
   funext t
   have hk : 0 ≤ S.kineticEnergy y t := by
-    simp only [HarmonicOscillator.kineticEnergy]
-    exact mul_nonneg (mul_nonneg (by norm_num) S.m_pos.le) real_inner_self_nonneg
+    simp [HarmonicOscillator.kineticEnergy, mul_nonneg, S.m_pos.le]
   have hp : 0 ≤ S.potentialEnergy (y t) := by
-    simp only [HarmonicOscillator.potentialEnergy, smul_eq_mul]
-    exact mul_nonneg (by norm_num) (mul_nonneg S.k_pos.le real_inner_self_nonneg)
-  have hpe : S.potentialEnergy (y t) = 0 := ((add_eq_zero_iff_of_nonneg hk hp).mp (hE t)).2
-  simp only [HarmonicOscillator.potentialEnergy, smul_eq_mul] at hpe
-  rcases mul_eq_zero.mp hpe with h | h
-  · norm_num at h
-  · have hyt : x t - IC.trajectory S t = 0 :=
-      inner_self_eq_zero.mp ((mul_eq_zero.mp h).resolve_left S.k_ne_zero)
+    simp [HarmonicOscillator.potentialEnergy, mul_nonneg, S.k_pos.le]
+  have hpe' : S.k * inner ℝ (y t) (y t) = 0 := by
+    have hpe : S.potentialEnergy (y t) = 0 := ((add_eq_zero_iff_of_nonneg hk hp).mp (hE t)).2
+    simpa [HarmonicOscillator.potentialEnergy, smul_eq_mul] using hpe
+  rcases eq_zero_or_eq_zero_of_mul_eq_zero hpe' with h | h
+  · exact (S.k_pos.ne' h).elim
+  · have hyt : x t - IC.trajectory S t = 0 := inner_self_eq_zero.mp h
     exact sub_eq_zero.mp hyt
 
 /-!