awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (p + a) b = p + toIcoMod hp a b
have rw : toIcoMod hp (a + p) b = p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_right', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIcoMod hp (a + p) b = p + toIcoMod hp a b
⊢ toIcoMod hp (p + a) b = p + toIcoMod hp a b
have rw₁ : toIcoMod hp a b + p = p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_right', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIcoMod hp (a + p) b = p + toIcoMod hp a b
rw₁ : toIcoMod hp a b + p = p + toIcoMod hp a b
⊢ toIcoMod hp (p + a) b = p + toIcoMod hp a b
have rw₂ : p + toIcoMod hp a b = p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_right', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (p + b) = toIocMod hp a b
have rw : toIocMod hp a (b + p) = toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIocMod hp a (b + p) = toIocMod hp a b
⊢ toIocMod hp a (p + b) = toIocMod hp a b
have rw₁ : toIocMod hp a b = toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (p + a) b = p + toIocMod hp a b
have rw : toIocMod hp (a + p) b = p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_right', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIocMod hp (a + p) b = p + toIocMod hp a b
⊢ toIocMod hp (p + a) b = p + toIocMod hp a b
have rw₁ : toIocMod hp a b + p = p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_right', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIocMod hp (a + p) b = p + toIocMod hp a b
rw₁ : toIocMod hp a b + p = p + toIocMod hp a b
⊢ toIocMod hp (p + a) b = p + toIocMod hp a b
have rw₂ : p + toIocMod hp a b = p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_right', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c
have simp_rw : b - c - toIcoDiv hp a (b - c) • p = b - toIcoDiv hp (a + c) b • p - c
Tactic: simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add, sub_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b - c - toIcoDiv hp a (b - c) • p = b - toIcoDiv hp (a + c) b • p - c
⊢ toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c
have simp_rw₁ : b - c - toIcoDiv hp (a + c) b • p = b - toIcoDiv hp (a + c) b • p - c
Tactic: simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add, sub_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c
have simp_rw : b - c - toIocDiv hp a (b - c) • p = b - toIocDiv hp (a + c) b • p - c
Tactic: simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add, sub_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b - c - toIocDiv hp a (b - c) • p = b - toIocDiv hp (a + c) b • p - c
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c
have simp_rw₁ : b - c - toIocDiv hp (a + c) b • p = b - toIocDiv hp (a + c) b • p - c
Tactic: simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add, sub_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c
have simp_rw : b + c - toIcoDiv hp a (b + c) • p = b - toIcoDiv hp (a - c) b • p + c
Tactic: simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b + c - toIcoDiv hp a (b + c) • p = b - toIcoDiv hp (a - c) b • p + c
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c
have simp_rw₁ : b + c - toIcoDiv hp a (b + c) • p = b - toIcoDiv hp a (b + c) • p + c
Tactic: simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a (b + c) = toIocMod hp (a - c) b + c
have simp_rw : b + c - toIocDiv hp a (b + c) • p = b - toIocDiv hp (a - c) b • p + c
Tactic: simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add', sub_add_eq_add_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b + c - toIocDiv hp a (b + c) • p = b - toIocDiv hp (a - c) b • p + c
⊢ toIocMod hp a (b + c) = toIocMod hp (a - c) b + c
have simp_rw₁ : b + c - toIocDiv hp a (b + c) • p = b - toIocDiv hp a (b + c) • p + c
Tactic: simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add', sub_add_eq_add_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (-b) = p - toIocMod hp (-a) b
have simp_rw : -b - -(toIocDiv hp (-a) b • p + HSMul.hSMul (α := ℤ) 1 p) = p - (b - toIocDiv hp (-a) b • p)
Tactic: simp_rw [toIcoMod, toIocMod, toIcoDiv_neg, neg_smul, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (-b) = p - toIcoMod hp (-a) b
have simp_rw : -b - -(toIcoDiv hp (-a) b • p + HSMul.hSMul (α := ℤ) 1 p) = p - (b - toIcoDiv hp (-a) b • p)
Tactic: simp_rw [toIocMod, toIcoMod, toIocDiv_neg, neg_smul, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a b = toIcoMod hp a c ↔ ∃ (n : ℤ), c - b = n • p
have refine_1 : ∀ (h : toIcoMod hp a b = toIcoMod hp a c), c - b = (toIcoDiv hp a c - toIcoDiv hp a b) • p
Tactic: refine ⟨fun h => ⟨toIcoDiv hp a c - toIcoDiv hp a b, ?_⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
refine_1 : ∀ (h : toIcoMod hp a b = toIcoMod hp a c), c - b = (toIcoDiv hp a c - toIcoDiv hp a b) • p
⊢ toIcoMod hp a b = toIcoMod hp a c ↔ ∃ (n : ℤ), c - b = n • p
have refine_2 : ∀ (h : ∃ (n : ℤ), c - b = n • p), toIcoMod hp a b = toIcoMod hp a c
Tactic: refine ⟨fun h => ⟨toIcoDiv hp a c - toIcoDiv hp a b, ?_⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
| c - b
have rw : toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p)
Tactic: rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
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
have refine_1 : 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: conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
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
have refine_1 : 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: rw [h, sub_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : ∃ (n : ℤ), c - b = n • p
⊢ toIcoMod hp a b = toIcoMod hp a c
have refine_2 : ∀ (z : ℤ) (hz : c - b = z • p), toIcoMod hp a b = toIcoMod hp a c
Tactic: rcases h with ⟨z, hz⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c - b = z • p
⊢ toIcoMod hp a b = toIcoMod hp a c
have hz₁ : c = z • p + b
Tactic: rw [sub_eq_iff_eq_add] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c
have refine_2 : toIcoMod hp a b = toIcoMod hp a (z • p + b)
Tactic: rw [hz, toIcoMod_zsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
refine_2 : toIcoMod hp a b = toIcoMod hp a (z • p + b)
⊢ toIcoMod hp a b = toIcoMod hp a c
have refine_2₁ : toIcoMod hp a b = toIcoMod hp a b
Tactic: rw [hz, toIcoMod_zsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a b = toIocMod hp a c ↔ ∃ (n : ℤ), c - b = n • p
have refine_1 : ∀ (h : toIocMod hp a b = toIocMod hp a c), c - b = (toIocDiv hp a c - toIocDiv hp a b) • p
Tactic: refine ⟨fun h => ⟨toIocDiv hp a c - toIocDiv hp a b, ?_⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
refine_1 : ∀ (h : toIocMod hp a b = toIocMod hp a c), c - b = (toIocDiv hp a c - toIocDiv hp a b) • p
⊢ toIocMod hp a b = toIocMod hp a c ↔ ∃ (n : ℤ), c - b = n • p
have refine_2 : ∀ (h : ∃ (n : ℤ), c - b = n • p), toIocMod hp a b = toIocMod hp a c
Tactic: refine ⟨fun h => ⟨toIocDiv hp a c - toIocDiv hp a b, ?_⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
| c - b
have rw : toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a b + toIocDiv hp a b • p)
Tactic: rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
⊢ c - b = (toIocDiv hp a c - toIocDiv hp a b) • p
have refine_1 : 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
Tactic: conv_lhs => rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
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
have refine_1 : 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
Tactic: rw [h, sub_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : ∃ (n : ℤ), c - b = n • p
⊢ toIocMod hp a b = toIocMod hp a c
have refine_2 : ∀ (z : ℤ) (hz : c - b = z • p), toIocMod hp a b = toIocMod hp a c
Tactic: rcases h with ⟨z, hz⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c - b = z • p
⊢ toIocMod hp a b = toIocMod hp a c
have hz₁ : c = z • p + b
Tactic: rw [sub_eq_iff_eq_add] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a c
have refine_2 : toIocMod hp a b = toIocMod hp a (z • p + b)
Tactic: rw [hz, toIocMod_zsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
refine_2 : toIocMod hp a b = toIocMod hp a (z • p + b)
⊢ toIocMod hp a b = toIocMod hp a c
have refine_2₁ : toIocMod hp a b = toIocMod hp a b
Tactic: rw [hz, toIocMod_zsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
n : ℤ
⊢ toIcoMod hp a (a + n • p) = a
have rw : toIcoMod hp a a = a
Tactic: rw [toIcoMod_add_zsmul, toIcoMod_apply_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
n : ℤ
rw : toIcoMod hp a a = a
⊢ toIcoMod hp a (a + n • p) = a
have rw₁ : a = a
Tactic: rw [toIcoMod_add_zsmul, toIcoMod_apply_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p
have refine_1 : (∃ (z : ℤ), b = a + z • p) → toIocMod hp a b = a + p
Tactic: refine modEq_iff_eq_add_zsmul.trans ⟨?_, fun h => ⟨toIocDiv hp a b + 1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
refine_1 : (∃ (z : ℤ), b = a + z • p) → toIocMod hp a b = a + p
⊢ a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p
have refine_2 : ∀ (h : toIocMod hp a b = a + p), b = a + (toIocDiv hp a b + 1) • p
Tactic: refine modEq_iff_eq_add_zsmul.trans ⟨?_, fun h => ⟨toIocDiv hp a b + 1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ toIocMod hp a (a + z • p) = a + p
have refine_1 : toIocMod hp a a = a + p
Tactic: rw [toIocMod_add_zsmul, toIocMod_apply_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
refine_1 : toIocMod hp a a = a + p
⊢ toIocMod hp a (a + z • p) = a + p
have refine_1₁ : a + p = a + p
Tactic: rw [toIocMod_add_zsmul, toIocMod_apply_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b = a + (toIocDiv hp a b + 1) • p
have refine_2 : b = a + (toIocDiv hp a b • p + p)
Tactic: rwa [add_one_zsmul, add_left_comm, ← sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
refine_2 : b = a + (toIocDiv hp a b • p + p)
⊢ b = a + (toIocDiv hp a b + 1) • p
have refine_2₁ : b = toIocDiv hp a b • p + (a + p)
Tactic: rwa [add_one_zsmul, add_left_comm, ← sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
refine_2 : b = a + (toIocDiv hp a b • p + p)
refine_2₁ : b = toIocDiv hp a b • p + (a + p)
⊢ b = a + (toIocDiv hp a b + 1) • p
have refine_2₂ : b - toIocDiv hp a b • p = a + p
Tactic: rwa [add_one_zsmul, add_left_comm, ← sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ [a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE
have rw : [toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
    toIcoMod hp a b + p = toIocMod hp a b].TFAE
Tactic: rw [modEq_iff_toIcoMod_eq_left hp]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
have rw : (∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b
Tactic: rw [← not_exists, not_imp_not]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ [toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE
have tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
Tactic: tfae_have 3 → 2 := by
    rw [← not_exists, not_imp_not]
    exact fun ⟨i, hi⟩ =>
      ((toIcoMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ico_self hi, i, (sub_add_cancel b _).symm⟩).trans
        ((toIocMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ioc_self hi, i, (sub_add_cancel b _).symm⟩).symm
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
h_1 : toIcoMod hp a b + p = toIocMod hp a b
h : toIcoMod hp a b + p = toIocMod hp a b := h_1
⊢ toIcoMod hp a b ≠ toIocMod hp a b
have rw : ¬p = 0
Tactic: rw [← h, Ne, eq_comm, add_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
⊢ [toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE
have tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
Tactic: tfae_have 4 → 3
  | h => by
    rw [← h, Ne, eq_comm, add_eq_left]
    exact hp.ne'
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
h_1 : toIcoMod hp a b = a
h : toIcoMod hp a b = a := h_1
⊢ toIcoMod hp a b + p = toIocMod hp a b
have rw : a < a + p ∧ ∃ (z : ℤ), b = a + p + z • p
Tactic: rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
h_1 : toIcoMod hp a b = a
h : toIcoMod hp a b = a := h_1
⊢ a < a + p ∧ ∃ (z : ℤ), b = a + p + z • p
have refine : b = a + p + (toIcoDiv hp a b - 1) • p
Tactic: refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
h_1 : toIcoMod hp a b = a
h : toIcoMod hp a b = a := h_1
⊢ b = a + p + (toIcoDiv hp a b - 1) • p
have rw : b = a + toIcoDiv hp a b • p
Tactic: rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]