refactor: golf Physlib proofs — proof-body only, no new declarations (~−4,390 lines, 109 files)

Physlib/ClassicalMechanics/EulerLagrange.lean

@@ -45,8 +45,7 @@ theorem euler_lagrange_varGradient
     (L : Time → X → X → ℝ) (q : Time → X)
     (hq : ContDiff ℝ ∞ q) (hL : ContDiff ℝ ∞ ↿L) :
     (δ (q':=q), ∫ t, L t (q' t) (fderiv ℝ q' t 1)) = eulerLagrangeOp L q := by
-  rw [eulerLagrangeOp_eq]
-  simp only [Time.deriv_eq]
+  simp only [eulerLagrangeOp_eq, Time.deriv_eq]
   apply HasVarGradientAt.varGradient
   apply HasVarGradientAt.intro _
   · apply HasVarAdjDerivAt.comp
@@ -57,25 +56,17 @@ theorem euler_lagrange_varGradient
       · fun_prop
       intro x u
       apply DifferentiableAt.hasAdjFDerivAt
-      apply Differentiable.differentiableAt
-      apply ContDiff.differentiable
-      fun_prop
-      simp
+      apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)
     · apply HasVarAdjDerivAt.prod (F:=fun φ => φ)
       · apply HasVarAdjDerivAt.id _ hq
-      · apply HasVarAdjDerivAt.fderiv
-        · exact hq
+      · apply HasVarAdjDerivAt.fderiv (hu := hq)
   case hgrad =>
     funext t
-    simp (disch:=fun_prop) only
-    simp[sub_eq_add_neg]
+    simp (disch := fun_prop) [sub_eq_add_neg]
     congr
-    rw [gradient_eq_adjFDeriv, adjFDeriv_uncurry]
-    apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)
-    apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)
-    funext t
-    rw [gradient_eq_adjFDeriv, adjFDeriv_uncurry]
-    apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)
-    apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)
+    all_goals
+      try funext t
+      rw [gradient_eq_adjFDeriv, adjFDeriv_uncurry] <;>
+        apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)
 
 end ClassicalMechanics

Physlib/ClassicalMechanics/HamiltonsEquations.lean

@@ -51,23 +51,7 @@ lemma hamiltonEqOp_eq_zero_iff_hamiltons_equations (H : Time → X → X → ℝ
     hamiltonEqOp H p q = 0 ↔
     (∀ t, ∂ₜ q t = gradient (fun x => H t x (q t)) (p t)) ∧
     (∀ t, ∂ₜ p t = -gradient (fun x => H t (p t) x) (q t)) := by
-  simp [hamiltonEqOp_eq]
-  simp_all only [Time.deriv_eq]
-  rw [funext_iff]
-  simp_all only [Pi.zero_apply, Prod.mk_eq_zero]
-  apply Iff.intro
-  · intro h1
-    apply And.intro
-    · intro t
-      conv_rhs =>
-        rw [← add_zero (gradient (fun x => H t x (q t)) (p t)), ← (h1 t).1]
-      simp
-    · intro t
-      conv_lhs =>
-        rw [← add_zero (fderiv ℝ p t 1), ← (h1 t).2]
-      simp
-  · intro a x
-    simp_all only [add_neg_cancel, neg_neg, and_self]
+  simp [hamiltonEqOp_eq, funext_iff, Prod.mk_eq_zero, forall_and, add_eq_zero_iff_neg_eq]
 
 theorem hamiltons_equations_varGradient
     (H : Time → X → X → ℝ) (pq : Time → X × X) (hp : ContDiff ℝ ∞ pq)
@@ -81,42 +65,21 @@ theorem hamiltons_equations_varGradient
       apply HasVarAdjDerivAt.comp
         (F := fun (φ : Time → X × X) t => i t (φ t))
         (G := fun (φ : Time → X × X) t => ((φ t).1, fderiv ℝ (Prod.snd ∘ φ) t 1))
-      · apply HasVarAdjDerivAt.fmap
-        · fun_prop
-        · fun_prop
-        intro t x
-        apply DifferentiableAt.hasAdjFDerivAt
-        fun_prop
+      · exact HasVarAdjDerivAt.fmap _ _ (by fun_prop) (by fun_prop)
+          fun x _ => (by fun_prop : DifferentiableAt ℝ _ _).hasAdjFDerivAt
       · apply HasVarAdjDerivAt.prod
-        · apply HasVarAdjDerivAt.fst
-          apply HasVarAdjDerivAt.id
-          fun_prop
+        · exact HasVarAdjDerivAt.fst (HasVarAdjDerivAt.id _ (by fun_prop))
         · apply HasVarAdjDerivAt.fderiv' (F := fun (φ : Time → X × X) t => (φ t).2)
-          apply HasVarAdjDerivAt.fmap
-          · fun_prop
-          · fun_prop
-          intro t x
-          apply DifferentiableAt.hasAdjFDerivAt
-          fun_prop
+          exact HasVarAdjDerivAt.fmap _ _ (by fun_prop) (by fun_prop)
+            fun x _ => (by fun_prop : DifferentiableAt ℝ _ _).hasAdjFDerivAt
     · apply HasVarAdjDerivAt.neg
-      let H' := fun t => ↿(H t)
-      change HasVarAdjDerivAt (fun φ x => H' x (φ x)) _ pq
-      apply HasVarAdjDerivAt.fmap
-      · fun_prop
-      · fun_prop
-      intro x u
-      apply DifferentiableAt.hasAdjFDerivAt
-      apply Differentiable.differentiableAt
-      apply ContDiff.differentiable
-      fun_prop
-      simp
+      exact HasVarAdjDerivAt.fmap (fun t => ↿(H t)) _ (by fun_prop) (by fun_prop)
+        fun x _ => (((by fun_prop : ContDiff ℝ ∞ _).differentiable
+          (by simp)).differentiableAt).hasAdjFDerivAt
   · simp only [adjFDeriv_prod_snd, Prod.mk_add_mk, add_zero, zero_add]
     funext x
-    rw [adjFDeriv_uncurry]
-    swap
-    · apply ContDiff.differentiable
-      fun_prop
-      simp
+    rw [adjFDeriv_uncurry
+      ((by fun_prop : ContDiff ℝ ∞ _).differentiable (by simp)).differentiableAt]
     simp only [Prod.neg_mk, Prod.mk_add_mk]
     rw [adjFDeriv_inner]
     simp only [one_smul]
@@ -126,11 +89,6 @@ theorem hamiltons_equations_varGradient
       simp
     rw [← gradient_eq_adjFDeriv, ← gradient_eq_adjFDeriv]
     rfl
-    · apply ContDiff.differentiable
-      fun_prop
-      simp
-    · apply ContDiff.differentiable
-      fun_prop
-      simp
+    all_goals exact ((by fun_prop : ContDiff ℝ ∞ _).differentiable (by simp)).differentiableAt
 
 end ClassicalMechanics

Physlib/ClassicalMechanics/WaveEquation/Basic.lean

@@ -92,9 +92,7 @@ lemma planeWave_differentiable_time {d f₀ c x} {s : Direction d}
     (h' : Differentiable ℝ f₀) :
     Differentiable ℝ (fun t => planeWave f₀ c s t x) := by
   simp only [planeWave_eq]
-  apply Differentiable.comp
-  · fun_prop
-  · fun_prop
+  apply Differentiable.comp <;> fun_prop
 
 @[fun_prop]
 lemma planeWave_differentiable_space {d f₀ c t} {s : Direction d}

Physlib/Electromagnetism/Current/InfiniteWire.lean

@@ -159,12 +159,7 @@ lemma infiniteWire_vectorPotential (𝓕 : FreeSpace) (I : ℝ) :
   ext η i
   simp [vectorPotential, infiniteWire, constantTime_apply,
   constantSliceDist_apply, Lorentz.Vector.spatialCLM, distOfFunction_vector_eval,
-  distOfFunction_eculid_eval]
-  left
-  congr
-  funext x
-  congr 1
-  exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
+  distOfFunction_eculid_eval, eq_comm]
 
 lemma infiniteWire_vectorPotential_fst (𝓕 : FreeSpace) (I : ℝ)(η : 𝓢(Time × Space 3, ℝ)) :
     (infiniteWire 𝓕 I).vectorPotential 𝓕.c η 0 =
@@ -192,18 +187,14 @@ lemma infiniteWire_vectorPotential_distTimeDeriv (𝓕 : FreeSpace) (I : ℝ) :
     distTimeDeriv ((infiniteWire 𝓕 I).vectorPotential 𝓕.c) = 0 := by
   ext1 η
   ext i
-  simp only [_root_.zero_apply, PiLp.zero_apply]
   rw [infiniteWire_vectorPotential _ I, constantTime_distTimeDeriv]
-  simp
 
 @[simp]
 lemma infiniteWire_vectorPotential_distSpaceDeriv_0 (𝓕 : FreeSpace) (I : ℝ) :
     distSpaceDeriv 0 ((infiniteWire 𝓕 I).vectorPotential 𝓕.c) = 0 := by
   ext1 η
-  simp [infiniteWire_vectorPotential _ I]
-  right
-  rw [constantTime_distSpaceDeriv, distDeriv_constantSliceDist_same]
-  simp
+  simp [infiniteWire_vectorPotential _ I, constantTime_distSpaceDeriv,
+    distDeriv_constantSliceDist_same]
 
 /-!
 
@@ -233,7 +224,6 @@ lemma infiniteWire_isExterma {𝓕 : FreeSpace} {I : ℝ} :
     _root_.zero_apply, one_div, wireCurrentDensity_chargeDesnity, mul_zero,
     implies_true, PiLp.zero_apply, zero_sub, true_and]
   intro ε i
-  field_simp
   rw [neg_add_eq_zero]
   fin_cases i
   · simp [Fin.sum_univ_three]
@@ -257,27 +247,15 @@ lemma infiniteWire_isExterma {𝓕 : FreeSpace} {I : ℝ} :
     · ext ε
       simp [distDiv_apply_eq_sum_distDeriv]
       rw [add_comm]
-      congr
-      · rw [distDeriv_apply, fderivD_apply]
-        conv_rhs => rw [distDeriv_apply, fderivD_apply]
-        simp [distGrad_apply]
-      · rw [distDeriv_apply, fderivD_apply]
-        conv_rhs => rw [distDeriv_apply, fderivD_apply]
-        simp [distGrad_apply]
+      congr 1 <;>
+        simp [distDeriv_apply, fderivD_apply, distGrad_apply]
     rw [distGrad_distOfFunction_log_norm]
-    have h1 := distDiv_inv_pow_eq_dim (d := 2)
-    simp at h1
-    simp [h1]
-  · simp only [Fin.mk_one, Fin.isValue, neg_sub, Finset.sum_sub_distrib, Fin.sum_univ_three,
-    infiniteWire_vectorPotential_distSpaceDeriv_0, map_zero, _root_.zero_apply,
-    PiLp.zero_apply, zero_add, wireCurrentDensity_currentDensity_snd, mul_zero]
-    ring_nf
-    rw [distSpaceDeriv_commute]
-    simp [distSpaceDeriv_apply']
-  · simp only [Fin.reduceFinMk, Fin.isValue, neg_sub, Finset.sum_sub_distrib, Fin.sum_univ_three,
-    infiniteWire_vectorPotential_distSpaceDeriv_0, map_zero, _root_.zero_apply,
-    PiLp.zero_apply, zero_add, add_sub_add_right_eq_sub, wireCurrentDensity_currentDensity_thrd,
-    mul_zero]
+    simpa using distDiv_inv_pow_eq_dim (d := 2)
+  all_goals
+    simp only [Fin.mk_one, Fin.reduceFinMk, Fin.isValue, neg_sub, Finset.sum_sub_distrib,
+      Fin.sum_univ_three, infiniteWire_vectorPotential_distSpaceDeriv_0, map_zero,
+      _root_.zero_apply, PiLp.zero_apply, zero_add, add_sub_add_right_eq_sub,
+      wireCurrentDensity_currentDensity_snd, wireCurrentDensity_currentDensity_thrd, mul_zero]
     ring_nf
     rw [distSpaceDeriv_commute]
     simp [distSpaceDeriv_apply']

Physlib/Electromagnetism/Distributional/Dynamics/IsExtrema.lean

@@ -67,17 +67,13 @@ lemma isExtrema_iff_components {𝓕 : FreeSpace}
     (J : DistLorentzCurrentDensity d) :
     IsExtrema 𝓕 A J ↔ (∀ ε, A.gradLagrangian 𝓕 J ε (Sum.inl 0) = 0)
     ∧ (∀ ε i, A.gradLagrangian 𝓕 J ε (Sum.inr i) = 0) := by
-  apply Iff.intro
-  · intro h
-    rw [isExtrema_iff_gradLagrangian] at h
-    simp [h]
-  · intro h
-    rw [isExtrema_iff_gradLagrangian]
-    ext1 ε
-    funext i
-    match i with
-    | Sum.inl 0 => exact h.1 ε
-    | Sum.inr j => exact h.2 ε j
+  rw [isExtrema_iff_gradLagrangian]
+  refine ⟨fun h => by simp [h], fun h => ?_⟩
+  ext1 ε
+  funext i
+  match i with
+  | Sum.inl 0 => exact h.1 ε
+  | Sum.inr j => exact h.2 ε j
 /-!
 
 ### A.1. IsExtrema and Gauss's law and Ampère's law
@@ -103,51 +99,37 @@ lemma isExtrema_iff_space_time {𝓕 : FreeSpace}
         ((Space.distSpaceDeriv j (A.magneticFieldMatrix 𝓕.c)) ε) (j, i) +
       𝓕.μ₀ * J.currentDensity 𝓕.c ε i = 0) := by
   rw [isExtrema_iff_components]
-  refine and_congr ?_ ?_
-  · simp [gradLagrangian_sum_inl_0]
-    field_simp
-    simp [𝓕.c_sq]
-    field_simp
-    simp [sub_eq_zero]
-    apply Iff.intro
-    · intro h ε
-      convert h (SchwartzMap.compCLMOfContinuousLinearEquiv (F := ℝ) ℝ
-        (SpaceTime.toTimeAndSpace 𝓕.c (d := d)) ε) using 1
-      · simp [SpaceTime.distTimeSlice_symm_apply]
-        ring_nf
-        congr
-        ext x
-        simp
-      · simp [SpaceTime.distTimeSlice_symm_apply]
-        congr
-        ext x
-        simp
-    · intro h ε
-      convert! h (SchwartzMap.compCLMOfContinuousLinearEquiv (F := ℝ) ℝ
-        (SpaceTime.toTimeAndSpace 𝓕.c (d := d)).symm ε) using 1
-      · simp [SpaceTime.distTimeSlice_symm_apply]
-        ring_nf
-  · apply Iff.intro
-    · intro h ε i
-      specialize h (SchwartzMap.compCLMOfContinuousLinearEquiv (F := ℝ) ℝ
-        (SpaceTime.toTimeAndSpace 𝓕.c (d := d)) ε) i
-      linear_combination (norm := field_simp) (𝓕.μ₀) * h
-      simp [gradLagrangian_sum_inr_i, SpaceTime.distTimeSlice_symm_apply]
-      have hx : (SchwartzMap.compCLMOfContinuousLinearEquiv ℝ (SpaceTime.toTimeAndSpace 𝓕.c).symm)
-          ((SchwartzMap.compCLMOfContinuousLinearEquiv ℝ (SpaceTime.toTimeAndSpace 𝓕.c)) ε)
-          = ε := by
-        ext i
-        simp
-      simp [hx, 𝓕.c_sq]
+  have hsurj : Function.Surjective (SchwartzMap.compCLMOfContinuousLinearEquiv (F := ℝ) ℝ
+      (SpaceTime.toTimeAndSpace 𝓕.c (d := d)).symm) := by
+    intro f
+    refine ⟨SchwartzMap.compCLMOfContinuousLinearEquiv ℝ
+      (SpaceTime.toTimeAndSpace 𝓕.c (d := d)).symm.symm f, ?_⟩
+    ext x
+    simp
+  have hgauss : ∀ a b : ℝ,
+      1 / (𝓕.μ₀ * 𝓕.c.val) * a - 𝓕.c.val * b = 0 ↔ a = 1 / 𝓕.ε₀ * b := by
+    intro a b
+    have c_sq_mul_eq : 𝓕.c.val * b * (𝓕.μ₀ * 𝓕.c.val) = 1 / 𝓕.ε₀ * b := by
+      have hcb : 𝓕.c.val * b * (𝓕.μ₀ * 𝓕.c.val) = 𝓕.μ₀ * 𝓕.c.val ^ 2 * b := by ring
+      rw [hcb, 𝓕.c_sq]
       field_simp
-      ring
-    · intro h ε i
-      specialize h (SchwartzMap.compCLMOfContinuousLinearEquiv (F := ℝ) ℝ
-        (SpaceTime.toTimeAndSpace 𝓕.c (d := d)).symm ε) i
-      linear_combination (norm := field_simp) (𝓕.μ₀⁻¹) * h
-      simp [gradLagrangian_sum_inr_i, SpaceTime.distTimeSlice_symm_apply, 𝓕.c_sq]
+    rw [sub_eq_zero, div_mul_eq_mul_div, one_mul,
+      div_eq_iff (mul_ne_zero 𝓕.μ₀_ne_zero 𝓕.c.val_ne_zero), c_sq_mul_eq]
+  have hampere : ∀ T S C : ℝ, 𝓕.μ₀⁻¹ * (1 / 𝓕.c.val ^ 2 * T - S) + C = 0 ↔
+      𝓕.μ₀ * 𝓕.ε₀ * T - S + 𝓕.μ₀ * C = 0 := by
+    intro T S C
+    have mu0_factor_eq : 𝓕.μ₀ * 𝓕.ε₀ * T - S + 𝓕.μ₀ * C
+        = 𝓕.μ₀ * (𝓕.μ₀⁻¹ * (1 / 𝓕.c.val ^ 2 * T - S) + C) := by
+      rw [𝓕.c_sq]
       field_simp
-      ring
+    rw [mu0_factor_eq, mul_eq_zero, or_iff_right 𝓕.μ₀_ne_zero]
+  refine and_congr ?_ ?_
+  · simp only [gradLagrangian_sum_inl_0, SpaceTime.distTimeSlice_symm_apply]
+    rw [hsurj.forall]
+    exact forall_congr' fun ε => hgauss _ _
+  · simp only [gradLagrangian_sum_inr_i, SpaceTime.distTimeSlice_symm_apply]
+    rw [hsurj.forall]
+    exact forall_congr' fun ε => forall_congr' fun i => hampere _ _ _
 
 /-!