English
For i ≤ j, (cycleIcc i j) j = i.
Русский
При i ≤ j, (cycleIcc i j) j = i.
LaTeX
$$$ (cycleIcc\ i\ j)\ j = i $$$
Lean4
@[simp]
theorem cycleIcc_of_le_of_le (hik : i ≤ k) (hkj : k ≤ j) [NeZero n] : (cycleIcc i j) k = if k = j then i else k + 1 :=
by
have hij : i ≤ j := le_trans hik hkj
have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by simpa [range_natAdd_castLEEmb] using by cutsat
have :
(((addNatEmb (n - (n - i.1))).trans (finCongr _).toEmbedding).toEquivRange.symm ⟨k, kin⟩) =
subNat i.1 (k.cast (by cutsat)) (by simpa using by cutsat) :=
by simpa [symm_apply_eq] using eq_of_val_eq (by simpa using by cutsat)
simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this, Function.Embedding.trans_apply, addNatEmb_apply,
coe_toEmbedding, finCongr_apply]
refine eq_of_val_eq ?_
split_ifs with ch
· have : subNat i.1 (j.cast (by cutsat)) (by simp [hij]) = (j - i).castLT (sub_val_lt_sub hij) :=
eq_of_val_eq (by simp [sub_val_of_le hij])
simpa [ch, cycleRange_of_eq this] using by cutsat
· have : subNat i.1 (k.cast (by cutsat)) (by simp [hik]) < (j - i).castLT (sub_val_lt_sub hij) := by
simpa [lt_iff_val_lt_val, sub_val_of_le hij] using by cutsat
rw [cycleRange_of_lt this, subNat]
simp only [coe_cast, add_def, val_one', Nat.add_mod_mod, addNat_mk, cast_mk]
rw [Nat.mod_eq_of_lt (by cutsat), Nat.mod_eq_of_lt (by cutsat)]
cutsat
