属性: csimp 属性

[Seasawher]

使用例: Mathlib.NumberTheory.Padics.PadicVal

/-- Allows for more efficient code for `padicValNat` -/
@[csimp]
theorem padicValNat_eq_maxPowDiv : @padicValNat = @maxPowDiv := by
  ext p n
  by_cases h : 1 < p ∧ 0 < n
  · dsimp [padicValNat]
    rw [dif_pos ⟨Nat.ne_of_gt h.1,h.2⟩, maxPowDiv_eq_multiplicity_get h.1 h.2]
  · simp only [not_and_or,not_gt_eq,le_zero_iff] at h
    apply h.elim
    · intro h
      interval_cases p
      · simp [Classical.em]
      · dsimp [padicValNat, maxPowDiv]
        rw [go_eq, if_neg, dif_neg] <;> simp
    · intro h
      simp [h]