max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename Nat.not_eq_zero_of_lt (#6968)

Browse source 
Renames a lemma.

Closes #6714
This commit is contained in:
Kim Morrison 2025-02-06 21:20:17 +11:00 • committed by GitHub
parent 947cd742bf
commit a00cc12436
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Init/Data/Nat/Basic.lean
View file

@ -780,16 +780,19 @@ protected theorem max_def {n m : Nat} : max n m = if n ≤ m then m else n := rf
/-! # Auxiliary theorems for well-founded recursion -/
theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by
protected theorem ne_zero_of_lt (h : b < a) : a ≠ 0 := by
cases a
exact absurd h (Nat.not_lt_zero _)
apply Nat.noConfusion
@[deprecated Nat.ne_zero_of_lt (since := "2025-02-06")]
theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := Nat.ne_zero_of_lt h
theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n :=
pred_lt (not_eq_zero_of_lt h)
pred_lt (Nat.ne_zero_of_lt h)
theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n :=
sub_one_lt (not_eq_zero_of_lt h)
sub_one_lt (Nat.ne_zero_of_lt h)
/-! # pred theorems -/
@ -854,7 +857,7 @@ theorem zero_lt_sub_of_lt (h : i < a) : 0 < a - i := by
theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
rw [Nat.add_succ, Nat.sub_succ]
apply Nat.pred_lt
apply Nat.not_eq_zero_of_lt
apply Nat.ne_zero_of_lt
apply Nat.zero_lt_sub_of_lt
assumption

4
src/Init/Data/Nat/Linear.lean
View file

@ -637,8 +637,8 @@ theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsa
simp [isUnsat]
by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]
· intro
| Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
| Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
| Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.ne_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
| Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.ne_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
· intro ⟨h₁, h₂⟩
simp [Poly.of_isZero, h₂]
exact Poly.of_isNonZero ctx h₁