-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_eq_toIcoMod : toIcoMod hp a b = toIcoMod hp a c ↔ ∃ n : ℤ, c - b = n • p

Proof state:
case refine_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rw [hz, toIcoMod_zsmul_add]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ c - b = (toIcoDiv hp a c - toIcoDiv hp a b) • p

Tactic:
conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p) =
    (toIcoDiv hp a c - toIcoDiv hp a b) • p

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : ∃ n, c - b = n • p
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rcases h with ⟨z, hz⟩

Result:
case refine_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c - b = z • p
⊢ toIcoMod hp a b = toIcoMod hp a c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a b = toIcoMod hp a c ↔ ∃ n, c - b = n • p

Tactic:
refine ⟨fun h => ⟨toIcoDiv hp a c - toIcoDiv hp a b, ?_⟩, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ c - b = (toIcoDiv hp a c - toIcoDiv hp a b) • p

case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : ∃ n, c - b = n • p
⊢ toIcoMod hp a b = toIcoMod hp a c

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p) =
    (toIcoDiv hp a c - toIcoDiv hp a b) • p

Tactic:
rw [h, sub_smul]

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    toIcoDiv hp a c • p - toIcoDiv hp a b • p

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    toIcoDiv hp a c • p - toIcoDiv hp a b • p

Tactic:
abel

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c - b = z • p
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rw [sub_eq_iff_eq_add] at hz

Result:
case refine_2.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c