DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2025-02-12 15:09:41 +00:00
parent fce5d9b03c
commit 0a712ea894
2 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/FlavorPhysics/CKMMatrix/Basic.lean
View file

@ -323,8 +323,8 @@ lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
fin_cases i <;> fin_cases j <;>
simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, zero_mul, add_zero, mul_zero,
_root_.map_mul, mul_re, I_re, ofReal_re, I_im, ofReal_im, sub_self, Real.exp_zero,
one_mul, mul_one, Complex.abs_exp, Fin.mk_one, cons_val_one, head_cons, zero_add, head_fin_const,
Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
one_mul, mul_one, Complex.abs_exp, Fin.mk_one, cons_val_one, head_cons, zero_add,
head_fin_const, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
tail_val', head_val']
all_goals change Complex.abs (0 * _ + _) = _
all_goals simp [Complex.abs_exp]

7
HepLean/Mathematics/List.lean
View file

@ -78,11 +78,12 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
split
next x heq =>
simp_all only [decide_eq_true_eq, decide_true, List.dropWhile_cons_of_pos, List.dropWhile_nil,
List.length_singleton, le_add_iff_nonneg_left, zero_le, ↓reduceIte, add_tsub_cancel_right, List.eraseIdx_nil]
List.length_singleton, le_add_iff_nonneg_left, zero_le, ↓reduceIte,
add_tsub_cancel_right, List.eraseIdx_nil]
next x heq =>
simp_all only [decide_eq_false_iff_not, decide_false, Bool.false_eq_true, not_false_eq_true,
List.dropWhile_cons_of_neg, List.length_nil, le_add_iff_nonneg_left, zero_le, ↓reduceIte, tsub_zero,
List.eraseIdx_cons_succ, List.eraseIdx_nil]
List.dropWhile_cons_of_neg, List.length_nil, le_add_iff_nonneg_left,
zero_le, ↓reduceIte, tsub_zero, List.eraseIdx_cons_succ, List.eraseIdx_nil]
exact Nat.le_add_left [a].length n
| a :: b :: l, 0, h => by
simp only [List.dropWhile, List.takeWhile, nonpos_iff_eq_zero, List.length_eq_zero, zero_le,