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

doc: fix

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-08 14:54:52 +01:00
parent 4bbf498004
commit 683c9d7cd3
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/tactics.md
View file

@ -173,7 +173,7 @@ theorem Nat.mod.inductionOn
theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
induction x, y using Nat.mod.inductionOn generalizing h with
| ind x y h₁ ih =>
rw [Nat.modEqSubMod h₁.2]
rw [Nat.mod_eq_sub_mod h₁.2]
exact ih h
| base x y h₁ =>
have ¬ 0 < y ∨ ¬ y ≤ x from Iff.mp (Decidable.notAndIffOrNot ..) h₁
@ -181,7 +181,7 @@ theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
| Or.inl h₁ => exact absurd h h₁
| Or.inr h₁ =>
have hgt : y > x from Nat.gtOfNotLe h₁
rw [← Nat.modEqOfLt hgt] at hgt
rw [← Nat.mod_eq_of_lt hgt] at hgt
assumption
```