case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : toIocMod hp a b = toIocMod hp a c
⊢ c - b = (toIocDiv hp a c - toIocDiv hp a b) • p

case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : ∃ n, c - b = n • p
⊢ toIocMod hp a b = toIocMod hp a c
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
⊢ toIocMod hp a b = toIocMod hp a c ↔ ∃ n, c - b = n • p
refine' ⟨fun h => ⟨toIocDiv hp a c - toIocDiv hp a b, _⟩, fun h => _⟩
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a b + toIocDiv hp a b • p) =
    (toIocDiv hp a c - toIocDiv hp a b) • p
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : toIocMod hp a b = toIocMod hp a c
⊢ c - b = (toIocDiv hp a c - toIocDiv hp a b) • p
conv_lhs => rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a c + toIocDiv hp a b • p) =
    toIocDiv hp a c • p - toIocDiv hp a b • p
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a b + toIocDiv hp a b • p) =
    (toIocDiv hp a c - toIocDiv hp a b) • p
rw [h, sub_smul]
no goals
case refine'_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a c + toIocDiv hp a b • p) =
    toIocDiv hp a c • p - toIocDiv hp a b • p
abel
case refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n z : ℤ
hz : c - b = z • p
⊢ toIocMod hp a b = toIocMod hp a c
case refine'_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
h : ∃ n, c - b = n • p
⊢ toIocMod hp a b = toIocMod hp a c
rcases h with ⟨z, hz⟩
case refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a c
case refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n z : ℤ
hz : c - b = z • p
⊢ toIocMod hp a b = toIocMod hp a c
rw [sub_eq_iff_eq_add] at hz
no goals
case refine'_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a c
rw [hz, toIocMod_zsmul_add]