Skip to content

Commit

Permalink
Some reasonable fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Aug 16, 2024
1 parent 14247a2 commit 8bca337
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ theorem of_s_head_aux (v : K) : (of v).s.get? 0 = (IntFractPair.stream v 1).bind
rw [of, IntFractPair.seq1]
simp only [of, Stream'.Seq.map_tail, Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.head,
Stream'.Seq.get?, Stream'.map]
rw [← Stream'.get_succ, Stream'.get, Option.map]
rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]
split <;> simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]

/-- This gives the first pair of coefficients of the continued fraction of a non-integer `v`.
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Data/List/Intervals.lean
Original file line number Diff line number Diff line change
Expand Up @@ -42,15 +42,15 @@ theorem zero_bot (n : ℕ) : Ico 0 n = range n := by rw [Ico, Nat.sub_zero, rang
@[simp]
theorem length (n m : ℕ) : length (Ico n m) = m - n := by
dsimp [Ico]
simp [length_range', autoParam]
simp [length_range']

theorem pairwise_lt (n m : ℕ) : Pairwise (· < ·) (Ico n m) := by
dsimp [Ico]
simp [pairwise_lt_range', autoParam]
simp [pairwise_lt_range']

theorem nodup (n m : ℕ) : Nodup (Ico n m) := by
dsimp [Ico]
simp [nodup_range', autoParam]
simp [nodup_range']

@[simp]
theorem mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m := by
Expand Down

0 comments on commit 8bca337

Please sign in to comment.