Skip to content

Commit c65b54c

Browse files
CoolRmalEtienneC30
andauthored
Update Mathlib/Data/Setoid/Partition.lean
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
1 parent cb93fc3 commit c65b54c

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Data/Setoid/Partition.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -522,7 +522,7 @@ theorem range_piecewise : range (hs.piecewise f) = ⋃ i, f i '' s i := by
522522
simp only [← hi, mem_image] at ht
523523
obtain ⟨a, ha1, ha2⟩ := ht
524524
refine ⟨a, ?_⟩
525-
simp [hs.mem_iff_index_eq] at ha1
525+
simp only [hs.mem_iff_index_eq] at ha1
526526
simpa [hs.mem_iff_index_eq, ← ha1] using ha2
527527

528528
theorem range_piecewise_subset : range (hs.piecewise f) ⊆ ⋃ i, range (f i) :=

0 commit comments

Comments
 (0)