TEST - DO NOT MERGE

Physlib/Electromagnetism/Kinematics/EMPotential.lean

@@ -273,7 +273,7 @@ noncomputable instance {d} :
     simp
   smul_add Λ A B := by
     ext x μ
-    simp [Lorentz.Vector.smul_add]
+    simp
 
 /-!
 

Physlib/FluidDynamics/NavierStokes/Momentum.lean

@@ -251,5 +251,23 @@ theorem momentumEquation_iff_convectiveMomentumEquation
   exact ⟨fun h t x => (conservative_eq_convective_lhs t x).symm.trans (h t x),
     fun h t x => (conservative_eq_convective_lhs t x).trans (h t x)⟩
 
+/-!
+
+## E. Basic properties of momentum fields
+
+-/
+
+/-- The momentum density vanishes wherever the mass density is zero. -/
+lemma momentumDensity_zero_of_rho_zero (d : ℕ) (fluid : FluidState d)
+    (t : Time) (x : Space d) (h : fluid.rho t x = 0) :
+    momentumDensity d fluid t x = 0 := by
+  simp [momentumDensity, h]
+
+/-- The momentum flux vanishes wherever the mass density is zero. -/
+lemma momentumFlux_zero_of_rho_zero (d : ℕ) (fluid : FluidState d)
+    (t : Time) (x : Space d) (h : fluid.rho t x = 0) :
+    momentumFlux d fluid t x = 0 := by
+  simp [momentumFlux, h]
+
 end NavierStokes
 end FluidDynamics

Physlib/Mathematics/PiTensorProduct.lean

@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 module
 
-public import Mathlib.LinearAlgebra.PiTensorProduct
+public import Mathlib.LinearAlgebra.PiTensorProduct.Basic
 /-!
 # Pi Tensor Products
 

Physlib/Mathematics/RatComplexNum.lean

@@ -83,8 +83,8 @@ instance : AddCommGroup RatComplexNum where
         simp
       · change a2 + 0 = a2
         simp
-  nsmul := fun n x => ⟨n • x.fst, n • x.snd⟩
   neg := fun x => ⟨-x.fst, -x.snd⟩
+  nsmul := fun n x => ⟨n • x.fst, n • x.snd⟩
   zsmul := fun n x => ⟨n • x.1, n • x.2⟩
   neg_add_cancel := by
     intro a
@@ -102,42 +102,17 @@ instance : AddCommGroup RatComplexNum where
       ring
     · simp only [add_snd]
       ring
-  nsmul_zero := by
-    intro x
-    simp only [zero_nsmul]
-    rfl
-  nsmul_succ := by
-    intro x y
-    ext
-    · simp only [add_fst]
-      ring
-    · simp only [add_snd]
-      ring
-  zsmul_zero' := by
-    intro a
-    ext
-    · simp only [zero_smul]
-      rfl
-    · simp only [zero_smul]
-      rfl
+  nsmul_zero := by intro x; ext <;> exact zero_nsmul _
+  nsmul_succ := by intro n x; ext <;> exact succ_nsmul _ _
+  zsmul_zero' := by intro a; ext <;> exact zero_zsmul _
   zsmul_succ' := by
-    intro a n
-    ext
-    · simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, zsmul_eq_mul, Int.cast_add,
-      Int.cast_natCast, Int.cast_one, add_fst]
-      ring
-    · simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, zsmul_eq_mul, Int.cast_add,
-      Int.cast_natCast, Int.cast_one, add_snd]
-      ring
-  zsmul_neg' := by
-    intro a n
+    intro n a
     ext
-    · simp only [zsmul_eq_mul, Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev,
-      Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast, Int.cast_one]
-      ring
-    · simp only [zsmul_eq_mul, Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev,
-      Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast, Int.cast_one]
-      ring
+    · show ((n : ℤ) + 1) • a.fst = (n : ℤ) • a.fst + a.fst
+      exact add_one_zsmul _ _
+    · show ((n : ℤ) + 1) • a.snd = (n : ℤ) • a.snd + a.snd
+      exact add_one_zsmul _ _
+  zsmul_neg' := by intro n a; ext <;> exact negSucc_zsmul _ _
 
 instance : Mul RatComplexNum where
   mul := fun x y => ⟨x.fst * y.fst - x.snd * y.snd, x.fst * y.snd + x.snd * y.fst⟩

Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean

@@ -187,7 +187,9 @@ lemma _root_.Option.toFinset_inj {x y : Option 𝓩} :
   cases x <;> cases y <;> simp [Option.toFinset]
 
 lemma subset_trans {x y z : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyz : y ⊆ z) : x ⊆ z := by
-  simp_all [Subset]
+  rw [subset_def] at hxy hyz ⊢
+  exact ⟨Finset.Subset.trans hxy.1 hyz.1, Finset.Subset.trans hxy.2.1 hyz.2.1,
+    Finset.Subset.trans hxy.2.2.1 hyz.2.2.1, Finset.Subset.trans hxy.2.2.2 hyz.2.2.2⟩
 
 lemma subset_antisymm {x y : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y :=
   eq_of_parts
@@ -328,6 +330,9 @@ lemma powerset_mono {x y : ChargeSpectrum 𝓩} :
   · intro h z hz
     exact mem_powerset_iff_subset.mpr (subset_trans (mem_powerset_iff_subset.mp hz) h)
 
+-- `unusedArguments` (newly flagged under v4.32.0): `hn` names the induction
+-- target but the proof discharges it directly via `exists_min_image`.
+@[nolint unusedArguments]
 lemma min_exists_inductive (S : Finset (ChargeSpectrum 𝓩)) (hS : S ≠ ∅) :
     (n : ℕ) → (hn : S.card = n) →
     ∃ y ∈ S, powerset y ∩ S = {y} := by

Physlib/QFT/AnomalyCancellation/Basic.lean

@@ -227,7 +227,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
   zero_add S := LinSols.ext (χ.chargesAddCommMonoid.zero_add _)
   add_zero S := LinSols.ext (χ.chargesAddCommMonoid.add_zero _)
   nsmul n S := ⟨n • S.val, fun _ ↦ by simp [S.linearSol _]⟩
-  nsmul_zero n := by ext; simp only [zero_nsmul]; rfl
+  nsmul_zero n := LinSols.ext (χ.chargesAddCommMonoid.nsmul_zero _)
   nsmul_succ n S := LinSols.ext (χ.chargesAddCommMonoid.nsmul_succ _ _)
 
 /-- An instance providing the operations and properties for `LinSols` to form a

Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -210,20 +210,28 @@ lemma ofFieldOpF_eq_crPartF_add_anPartF (φ : 𝓕.FieldOp) :
 
 /-- The basis of the free creation and annihilation algebra formed by lists of CrAnFieldOp. -/
 noncomputable def ofCrAnListFBasis : Basis (List 𝓕.CrAnFieldOp) ℂ (FieldOpFreeAlgebra 𝓕) where
-  repr := FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
+  repr := FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv ≪≫ₗ
+    MonoidAlgebra.coeffLinearEquiv ℂ
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma ofListBasis_eq_ofList (φs : List 𝓕.CrAnFieldOp) :
     ofCrAnListFBasis φs = ofCrAnListF φs := by
-  simp only [ofCrAnListFBasis, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
-    Basis.coe_ofRepr, ofCrAnListF]
-  erw [MonoidAlgebra.lift_apply]
-  simp only [zero_smul, Finsupp.sum_single_index, one_smul]
-  rw [@FreeMonoid.lift_apply]
-  match φs with
-  | [] => rfl
-  | φ :: φs => erw [List.map_cons]
+  have key : ∀ ψs : List 𝓕.CrAnFieldOp, FreeAlgebra.equivMonoidAlgebraFreeMonoid (ofCrAnListF ψs)
+      = MonoidAlgebra.single (FreeMonoid.ofList ψs) 1 := by
+    intro ψs
+    induction ψs with
+    | nil => simp [ofCrAnListF, MonoidAlgebra.one_def]
+    | cons φ ψs ih =>
+      rw [ofCrAnListF, List.map_cons, List.prod_cons, ← ofCrAnListF, map_mul, ih,
+        FreeMonoid.ofList_cons,
+        show FreeAlgebra.equivMonoidAlgebraFreeMonoid (ofCrAnOpF φ)
+          = MonoidAlgebra.single (FreeMonoid.of φ) 1 by
+          simp [ofCrAnOpF, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply],
+        MonoidAlgebra.single_mul_single, one_mul]
+  rw [Basis.apply_eq_iff]
+  simp only [ofCrAnListFBasis, LinearEquiv.trans_apply, AlgEquiv.toLinearEquiv_apply, key]
+  rfl
 
 lemma ofCrAnListF_injective : Function.Injective (ofCrAnListF (𝓕 := 𝓕)) := by
   intro φs φs' h

Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean

@@ -310,11 +310,11 @@ instance : AddMonoid FieldStatistic where
   add_assoc a b c := by
     cases a <;> cases b <;> cases c <;> rfl
   nsmul_zero a := by
-    simp only [Finset.univ_eq_empty, Finset.prod_const, Finset.card_empty, pow_zero]
-    rfl
+    show (∏ _i : Fin 0, a) = (1 : FieldStatistic)
+    rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin, pow_zero]
   nsmul_succ a n := by
-    simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin]
-    rfl
+    show (∏ _i : Fin (a + 1), n) = (∏ _i : Fin a, n) * n
+    simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin, pow_succ]
 
 @[simp]
 lemma add_eq_mul (a b : FieldStatistic) : a + b = a * b := rfl

Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean

@@ -225,7 +225,7 @@ lemma ι_eq_zero_iff_mem_ideal (x : FieldOpFreeAlgebra 𝓕) :
     ι x = 0 ↔ x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet := by
   rw [ι_apply]
   change ⟦x⟧ = ⟦0⟧ ↔ _
-  simp_all only [Quotient.eq, Con.rel_eq_coe, RingCon.toCon_coe_eq_coe, TwoSidedIdeal.mem_mk]
+  simp_all only [Quotient.eq, Con.rel_eq_coe, RingCon.toCon_coe_eq_coe, TwoSidedIdeal.mem_ofRingCon]
 
 lemma bosonicProjF_mem_fieldOpIdealSet_or_zero (x : FieldOpFreeAlgebra 𝓕)
     (hx : x ∈ 𝓕.fieldOpIdealSet) :
@@ -322,7 +322,7 @@ lemma bosonicProjF_mem_ideal (x : FieldOpFreeAlgebra 𝓕)
       · exact TwoSidedIdeal.mem_span_iff.mpr fun I hI => hI h
       · simp [h]
     exact add_mem (add_mem (key hBy) (key hFy)) (add_mem (key hFy) (key hBy))
-  · simp only [TwoSidedIdeal.mem_mk, map_zero, ZeroMemClass.coe_zero, p]
+  · simp only [TwoSidedIdeal.mem_ofRingCon, map_zero, ZeroMemClass.coe_zero, p]
     exact (RingCon.eq (ringConGen fun a b => a - b ∈ 𝓕.fieldOpIdealSet)).mp rfl
   · intro x y hx hy hpx hpy
     simp_all only [map_add, Submodule.coe_add, p]

Physlib/QFT/PerturbationTheory/WickContraction/Card.lean

@@ -72,7 +72,7 @@ def consAddContract (i : Fin n.succ) (c : WickContraction n) :
   ⟨(c.1.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding).map
     (Finset.mapEmbedding (Fin.succEmb n.succ)).toEmbedding ∪ {{0, i.succ}}, by
     intro a
-    simp only [succ_eq_add_one, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
+    simp only [succ_eq_add_one, Finset.mem_union, Finset.mem_map,
       RelEmbedding.coe_toEmbedding, exists_exists_and_eq_and, Finset.mem_singleton]
     intro h
     rcases h with h | h
@@ -86,7 +86,7 @@ def consAddContract (i : Fin n.succ) (c : WickContraction n) :
       simp only [succ_eq_add_one, ne_eq, and_true]
       exact ne_of_beq_false rfl, by
     intro a ha b hb
-    simp only [succ_eq_add_one, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
+    simp only [succ_eq_add_one, Finset.mem_union, Finset.mem_map,
       RelEmbedding.coe_toEmbedding, exists_exists_and_eq_and, Finset.mem_singleton] at ha hb
     rcases ha with ha | ha <;> rcases hb with hb | hb
     · obtain ⟨a, ha, rfl⟩ := ha
@@ -122,7 +122,7 @@ lemma consAddContract_getDual?_self_succ (i : Fin n.succ) (c : WickContraction n
 
 lemma mem_consAddContract_of_mem_iff (i : Fin n.succ) (c : WickContraction n) (a : Finset (Fin n)) :
     a ∈ c.1 ↔ (a.map i.succAboveEmb).map (Fin.succEmb n.succ) ∈ (consAddContract i c).1 := by
-  simp only [succ_eq_add_one, consAddContract, Finset.le_eq_subset, Finset.mem_union,
+  simp only [succ_eq_add_one, consAddContract, Finset.mem_union,
     Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_exists_and_eq_and, Finset.mem_singleton]
   apply Iff.intro
   · intro h
@@ -186,7 +186,6 @@ lemma consAddContract_surjective_on_zero_contract (i : Fin n.succ)
       rw [← h2]
       simp
     · obtain ⟨b, hb, rfl⟩ := h
-      rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply]
       simp only [succ_eq_add_one, Finset.mem_filter, Finset.mem_univ, true_and, c'] at hb
       exact hb
   · intro h
@@ -207,7 +206,6 @@ lemma consAddContract_surjective_on_zero_contract (i : Fin n.succ)
       obtain ⟨y, rfl⟩ := (Fin.exists_succAbove_eq (x := y) (y := i)) (by omega)
       use {x, y}
       simp only [c']
-      rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply]
       simpa using h
 
 lemma consAddContract_bijection (i : Fin n.succ) :