fix: PlaneNonSols

HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean

@@ -66,7 +66,7 @@ def speciesEmbed (m n : ℕ) :
     by_cases hi : i.val < m
     · erw [dif_pos hi, dif_pos hi, dif_pos hi]
     · erw [dif_neg hi, dif_neg hi, dif_neg hi]
-      rfl
+      with_unfolding_all rfl
   map_smul' a S := by
     funext i
     simp only [SMνSpecies_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul,

HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean

@@ -75,7 +75,7 @@ def B : Fin 11 → (PlusU1 3).Charges := fun i =>
 
 lemma Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : quadBiLin (B i) (B j) = 0 := by
   fin_cases i <;> fin_cases j
-  any_goals rfl
+  any_goals with_unfolding_all rfl
   all_goals simp at hi
 
 lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
@@ -92,7 +92,7 @@ def quadCoeff : Fin 11 → ℚ := ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]
 
 lemma quadCoeff_eq_bilinear (i : Fin 11) : quadCoeff i = quadBiLin (B i) (B i) := by
   fin_cases i
-  all_goals rfl
+  all_goals with_unfolding_all rfl
 
 lemma on_accQuad (f : Fin 11 → ℚ) :
     accQuad (∑ i, f i • B i) = ∑ i, quadCoeff i * (f i)^2 := by
@@ -170,8 +170,9 @@ lemma isSolution_grav (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f
   have hx := isSolution_sum_part f hS
   obtain ⟨S, hS'⟩ := hS
   have hg := gravSol S.toLinSols
-  rw [hS', hx, accGrav.map_add, accGrav.map_smul, accGrav.map_smul, show accGrav B₉ = 3 by rfl,
-    show accGrav B₁₀ = 1 by rfl] at hg
+  rw [hS', hx, accGrav.map_add, accGrav.map_smul, accGrav.map_smul,
+    show accGrav B₉ = 3 by with_unfolding_all rfl,
+    show accGrav B₁₀ = 1 by with_unfolding_all rfl] at hg
   simp only [Fin.isValue, smul_eq_mul, mul_one] at hg
   linear_combination hg
 
@@ -191,8 +192,10 @@ lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i
   erw [accCube.map_smul (- 3 * f 9) B₁₀] at hc
   rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₂,
     cubeTriLin.map_smul₃, cubeTriLin.map_smul₃] at hc
-  rw [show accCube B₉ = 9 by rfl, show accCube B₁₀ = 1 by rfl, show cubeTriLin B₉ B₉ B₁₀ = 0 by rfl,
-    show cubeTriLin B₁₀ B₁₀ B₉ = 0 by rfl] at hc
+  rw [show accCube B₉ = 9 by with_unfolding_all rfl,
+    show accCube B₁₀ = 1 by with_unfolding_all rfl,
+    show cubeTriLin B₉ B₉ B₁₀ = 0 by with_unfolding_all rfl,
+    show cubeTriLin B₁₀ B₁₀ B₉ = 0 by with_unfolding_all rfl] at hc
   simp only [Fin.isValue, neg_mul, mul_one, mul_zero, add_zero] at hc
   have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by ring
   rw [h1] at hc
@@ -201,7 +204,7 @@ lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i
 lemma isSolution_f10 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
     f 10 = 0 := by
   rw [isSolution_grav f hS, isSolution_f9 f hS]
-  rfl
+  with_unfolding_all rfl
 
 lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i))
     (k : Fin 11) : f k = 0 := by
@@ -225,7 +228,9 @@ lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (
 
 theorem basis_linear_independent : LinearIndependent ℚ B :=
   Fintype.linearIndependent_iff.mpr fun f h ↦ isSolution_f_zero f
-    ⟨chargeToAF 0 (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl), id (Eq.symm h)⟩
+    ⟨chargeToAF 0 (by with_unfolding_all rfl) (by with_unfolding_all rfl)
+      (by with_unfolding_all rfl) (by with_unfolding_all rfl) (by with_unfolding_all rfl)
+      (by with_unfolding_all rfl), id (Eq.symm h)⟩
 
 end ElevenPlane
 

HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean

@@ -391,11 +391,11 @@ lemma mulExpδ₁₃_on_param_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ)
 lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₃ ⟦V⟧) = 0) :
     standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
   have hS13 := congrArg ofReal (S₁₃_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h))
-  simp only [ofReal_eq_coe, ← S₁₃_eq_ℂsin_θ₁₃, _root_.map_one] at hS13
+  simp only [← S₁₃_eq_ℂsin_θ₁₃] at hS13
   have hC12 := congrArg ofReal (C₁₂_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h))
-  simp only [ofReal_eq_coe, ← C₁₂_eq_ℂcos_θ₁₂, _root_.map_one] at hC12
+  simp only [← C₁₂_eq_ℂcos_θ₁₂] at hC12
   have hS12 := congrArg ofReal (S₁₂_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h))
-  simp only [ofReal_eq_coe, ← S₁₂_eq_ℂsin_θ₁₂, map_zero] at hS12
+  simp only [← S₁₂_eq_ℂsin_θ₁₂] at hS12
   use 0, 0, 0, δ₁₃, 0, -δ₁₃
   simp only [standParam, standParamAsMatrix, ofReal_cos, hC12, h, ofReal_zero, mul_zero, ofReal_sin,
     hS12, hS13, neg_mul, one_mul, neg_zero, zero_mul, mul_one, zero_sub, sub_zero, phaseShift,
@@ -407,7 +407,8 @@ lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
       cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const,
       vecCons_const, mul_zero, tail_val', head_val', zero_add, Fin.mk_one, Fin.reduceFinMk,
       neg_mul, mul_one]
-  · rfl
+  · simp_all only [ofReal_one, ofReal_zero, one_mul]
+    rfl
   · rfl
 
 lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) :
@@ -527,11 +528,11 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
   have hb' : VubAbs ⟦V⟧ ≠ 1 := by
     rw [ud_us_neq_zero_iff_ub_neq_one] at hb
     exact hb
-  have h1 : ofReal (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) *
-    ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) = ofReal (VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) := by
+  have h1 : ofRealHom (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) *
+    ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) = ofRealHom (VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) := by
     rw [Real.mul_self_sqrt]
     apply add_nonneg (sq_nonneg _) (sq_nonneg _)
-  simp only [Fin.isValue, _root_.map_mul, ofReal_eq_coe, map_add, map_pow] at h1
+  simp only [Fin.isValue, _root_.map_mul, ofRealHom_eq_coe, map_add, map_pow] at h1
   have hx := Vabs_sq_add_neq_zero hb
   refine eq_rows V ?_ ?_ hV.2.2.2.2
   · funext i