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 : α
⊢ b - toIocMod hp a b = toIocDiv hp a b • p
have rw : b - (b - toIocDiv hp a b • p) = toIocDiv hp a b • p
Tactic: rw [toIocMod, sub_sub_cancel]
-- 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 : b - (b - toIocDiv hp a b • p) = toIocDiv hp a b • p
⊢ b - toIocMod hp a b = toIocDiv hp a b • p
have rw₁ : toIocDiv hp a b • p = toIocDiv hp a b • p
Tactic: rw [toIocMod, sub_sub_cancel]
-- 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 + toIcoDiv hp a b • p = b
have rw : b - toIcoDiv hp a b • p + toIcoDiv hp a b • p = b
Tactic: rw [toIcoMod, sub_add_cancel]
-- 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 : b - toIcoDiv hp a b • p + toIcoDiv hp a b • p = b
⊢ toIcoMod hp a b + toIcoDiv hp a b • p = b
have rw₁ : b = b
Tactic: rw [toIcoMod, sub_add_cancel]
-- 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 + toIocDiv hp a b • p = b
have rw : b - toIocDiv hp a b • p + toIocDiv hp a b • p = b
Tactic: rw [toIocMod, sub_add_cancel]
-- 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 : b - toIocDiv hp a b • p + toIocDiv hp a b • p = b
⊢ toIocMod hp a b + toIocDiv hp a b • p = b
have rw₁ : b = b
Tactic: rw [toIocMod, sub_add_cancel]
-- 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 : α
⊢ toIcoDiv hp a b • p + toIcoMod hp a b = b
have rw : toIcoMod hp a b + toIcoDiv hp a b • p = b
Tactic: rw [add_comm, toIcoMod_add_toIcoDiv_zsmul]
-- 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 b + toIcoDiv hp a b • p = b
⊢ toIcoDiv hp a b • p + toIcoMod hp a b = b
have rw₁ : b = b
Tactic: rw [add_comm, toIcoMod_add_toIcoDiv_zsmul]
-- 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 : α
⊢ toIocDiv hp a b • p + toIocMod hp a b = b
have rw : toIocMod hp a b + toIocDiv hp a b • p = b
Tactic: rw [add_comm, toIocMod_add_toIocDiv_zsmul]
-- 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 + toIocDiv hp a b • p = b
⊢ toIocDiv hp a b • p + toIocMod hp a b = b
have rw₁ : b = b
Tactic: rw [add_comm, toIocMod_add_toIocDiv_zsmul]
-- 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 ↔ c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b = c + z • p
have h : (c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIcoMod hp a b = c
Tactic: refine
    ⟨fun h =>
      ⟨h ▸ toIcoMod_mem_Ico hp a b, toIcoDiv hp a b, h ▸ (toIcoMod_add_toIcoDiv_zsmul _ _ _).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 c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIcoMod hp a b = c
have simp_rw : (c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b - z • p = c) → toIcoMod hp a b = c
Tactic: simp_rw [← @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 : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
⊢ toIcoMod hp a b = b - n • p
have rw : toIcoMod hp a b = b - toIcoDiv hp a b • p
Tactic: rw [← toIcoDiv_eq_of_sub_zsmul_mem_Ico hp hc, toIcoMod]
-- 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 : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
rw : toIcoMod hp a b = b - toIcoDiv hp a b • p
⊢ toIcoMod hp a b = b - n • p
have rw₁ : b - toIcoDiv hp a b • p = b - toIcoDiv hp a b • p
Tactic: rw [← toIcoDiv_eq_of_sub_zsmul_mem_Ico hp hc, toIcoMod]
-- 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 ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b = c + z • p
have h : (c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIocMod hp a b = c
Tactic: refine
    ⟨fun h =>
      ⟨h ▸ toIocMod_mem_Ioc hp a b, toIocDiv hp a b, h ▸ (toIocMod_add_toIocDiv_zsmul hp _ _).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 c : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIocMod hp a b = c
have simp_rw : (c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b - z • p = c) → toIocMod hp a b = c
Tactic: simp_rw [← @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 : α
n : ℤ
hc : b - n • p ∈ Set.Ioc a (a + p)
⊢ toIocMod hp a b = b - n • p
have rw : toIocMod hp a b = b - toIocDiv hp a b • p
Tactic: rw [← toIocDiv_eq_of_sub_zsmul_mem_Ioc hp hc, toIocMod]
-- 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 : α
n : ℤ
hc : b - n • p ∈ Set.Ioc a (a + p)
rw : toIocMod hp a b = b - toIocDiv hp a b • p
⊢ toIocMod hp a b = b - n • p
have rw₁ : b - toIocDiv hp a b • p = b - toIocDiv hp a b • p
Tactic: rw [← toIocDiv_eq_of_sub_zsmul_mem_Ioc hp hc, toIocMod]
-- 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 : α
⊢ toIcoMod hp a a = a
have rw : a < a + p ∧ ∃ (z : ℤ), a = a + z • p
Tactic: rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]
-- 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 : α
⊢ toIocMod hp a a = a + p
have rw : a < a + p ∧ ∃ (z : ℤ), a = a + p + z • p
Tactic: rw [toIocMod_eq_iff hp, 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 : α
⊢ toIcoMod hp a (a + p) = a
have rw : a < a + p ∧ ∃ (z : ℤ), a + p = a + z • p
Tactic: rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]
-- 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 : α
⊢ toIocMod hp a (a + p) = a + p
have rw : a < a + p ∧ ∃ (z : ℤ), a + p = a + p + z • p
Tactic: rw [toIocMod_eq_iff hp, 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 : α
m : ℤ
⊢ toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m
have refine : b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)
Tactic: refine toIcoDiv_eq_of_sub_zsmul_mem_Ico _ ?_
-- 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 : α
m : ℤ
⊢ b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)
have rw : b - toIcoDiv hp a b • p + m • p ∈ Set.Ico (a + m • p) (a + p + m • p)
Tactic: rw [sub_smul, ← sub_add, add_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 : α
m : ℤ
⊢ toIocDiv hp (a + m • p) b = toIocDiv hp a b - m
have refine : b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)
Tactic: refine toIocDiv_eq_of_sub_zsmul_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 : α
m : ℤ
⊢ b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)
have rw : b - toIocDiv hp a b • p + m • p ∈ Set.Ioc (a + m • p) (a + p + m • p)
Tactic: rw [sub_smul, ← sub_add, add_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 : α
m : ℤ
⊢ toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b
have rw : toIcoDiv hp a (b + m • p) = m + toIcoDiv hp a b
Tactic: rw [add_comm, toIcoDiv_add_zsmul, 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 : α
m : ℤ
rw : toIcoDiv hp a (b + m • p) = m + toIcoDiv hp a b
⊢ toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b
have rw₁ : toIcoDiv hp a b + m = m + toIcoDiv hp a b
Tactic: rw [add_comm, toIcoDiv_add_zsmul, 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 : α
m : ℤ
rw : toIcoDiv hp a (b + m • p) = m + toIcoDiv hp a b
rw₁ : toIcoDiv hp a b + m = m + toIcoDiv hp a b
⊢ toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b
have rw₂ : m + toIcoDiv hp a b = m + toIcoDiv hp a b
Tactic: rw [add_comm, toIcoDiv_add_zsmul, 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 : α
m : ℤ
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b
have rw : toIocDiv hp a (b + m • p) = m + toIocDiv hp a b
Tactic: rw [add_comm, toIocDiv_add_zsmul, 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 : α
m : ℤ
rw : toIocDiv hp a (b + m • p) = m + toIocDiv hp a b
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b
have rw₁ : toIocDiv hp a b + m = m + toIocDiv hp a b
Tactic: rw [add_comm, toIocDiv_add_zsmul, 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 : α
m : ℤ
rw : toIocDiv hp a (b + m • p) = m + toIocDiv hp a b
rw₁ : toIocDiv hp a b + m = m + toIocDiv hp a b
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b
have rw₂ : m + toIocDiv hp a b = m + toIocDiv hp a b
Tactic: rw [add_comm, toIocDiv_add_zsmul, 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 : α
m : ℤ
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m
have rw : toIcoDiv hp a (b + -(m • p)) = toIcoDiv hp a b - m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
rw : toIcoDiv hp a (b + -(m • p)) = toIcoDiv hp a b - m
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m
have rw₁ : toIcoDiv hp a (b + -m • p) = toIcoDiv hp a b - m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
rw : toIcoDiv hp a (b + -(m • p)) = toIcoDiv hp a b - m
rw₁ : toIcoDiv hp a (b + -m • p) = toIcoDiv hp a b - m
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m
have rw₂ : toIcoDiv hp a b + -m = toIcoDiv hp a b - m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
rw : toIcoDiv hp a (b + -(m • p)) = toIcoDiv hp a b - m
rw₁ : toIcoDiv hp a (b + -m • p) = toIcoDiv hp a b - m
rw₂ : toIcoDiv hp a b + -m = toIcoDiv hp a b - m
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m
have rw₃ : toIcoDiv hp a b + -m = toIcoDiv hp a b + -m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m
have rw : toIcoDiv hp (a + -(m • p)) b = toIcoDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul', sub_neg_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 : α
m : ℤ
rw : toIcoDiv hp (a + -(m • p)) b = toIcoDiv hp a b + m
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m
have rw₁ : toIcoDiv hp (a + -m • p) b = toIcoDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul', sub_neg_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 : α
m : ℤ
rw : toIcoDiv hp (a + -(m • p)) b = toIcoDiv hp a b + m
rw₁ : toIcoDiv hp (a + -m • p) b = toIcoDiv hp a b + m
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m
have rw₂ : toIcoDiv hp a b - -m = toIcoDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul', sub_neg_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 : α
m : ℤ
rw : toIcoDiv hp (a + -(m • p)) b = toIcoDiv hp a b + m
rw₁ : toIcoDiv hp (a + -m • p) b = toIcoDiv hp a b + m
rw₂ : toIcoDiv hp a b - -m = toIcoDiv hp a b + m
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m
have rw₃ : toIcoDiv hp a b + m = toIcoDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul', sub_neg_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 : α
m : ℤ
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m
have rw : toIocDiv hp a (b + -(m • p)) = toIocDiv hp a b - m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
rw : toIocDiv hp a (b + -(m • p)) = toIocDiv hp a b - m
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m
have rw₁ : toIocDiv hp a (b + -m • p) = toIocDiv hp a b - m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
rw : toIocDiv hp a (b + -(m • p)) = toIocDiv hp a b - m
rw₁ : toIocDiv hp a (b + -m • p) = toIocDiv hp a b - m
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m
have rw₂ : toIocDiv hp a b + -m = toIocDiv hp a b - m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
rw : toIocDiv hp a (b + -(m • p)) = toIocDiv hp a b - m
rw₁ : toIocDiv hp a (b + -m • p) = toIocDiv hp a b - m
rw₂ : toIocDiv hp a b + -m = toIocDiv hp a b - m
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m
have rw₃ : toIocDiv hp a b + -m = toIocDiv hp a b + -m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul, sub_eq_add_neg]
-- 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 : α
m : ℤ
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m
have rw : toIocDiv hp (a + -(m • p)) b = toIocDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_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 : α
m : ℤ
rw : toIocDiv hp (a + -(m • p)) b = toIocDiv hp a b + m
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m
have rw₁ : toIocDiv hp (a + -m • p) b = toIocDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_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 : α
m : ℤ
rw : toIocDiv hp (a + -(m • p)) b = toIocDiv hp a b + m
rw₁ : toIocDiv hp (a + -m • p) b = toIocDiv hp a b + m
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m
have rw₂ : toIocDiv hp a b - -m = toIocDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_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 : α
m : ℤ
rw : toIocDiv hp (a + -(m • p)) b = toIocDiv hp a b + m
rw₁ : toIocDiv hp (a + -m • p) b = toIocDiv hp a b + m
rw₂ : toIocDiv hp a b - -m = toIocDiv hp a b + m
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m
have rw₃ : toIocDiv hp a b + m = toIocDiv hp a b + m
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_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 : α
⊢ toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1
have rw : toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1
Tactic: rw [add_comm, toIcoDiv_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 : toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1
⊢ toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1
have rw₁ : toIcoDiv hp a b + 1 = toIcoDiv hp a b + 1
Tactic: rw [add_comm, toIcoDiv_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 : α
⊢ toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1
have rw : toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1
Tactic: rw [add_comm, toIcoDiv_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 : toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1
⊢ toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1
have rw₁ : toIcoDiv hp a b - 1 = toIcoDiv hp a b - 1
Tactic: rw [add_comm, toIcoDiv_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 : α
⊢ toIocDiv hp a (p + b) = toIocDiv hp a b + 1
have rw : toIocDiv hp a (b + p) = toIocDiv hp a b + 1
Tactic: rw [add_comm, toIocDiv_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 : toIocDiv hp a (b + p) = toIocDiv hp a b + 1
⊢ toIocDiv hp a (p + b) = toIocDiv hp a b + 1
have rw₁ : toIocDiv hp a b + 1 = toIocDiv hp a b + 1
Tactic: rw [add_comm, toIocDiv_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 : α
⊢ toIocDiv hp (p + a) b = toIocDiv hp a b - 1
have rw : toIocDiv hp (a + p) b = toIocDiv hp a b - 1
Tactic: rw [add_comm, toIocDiv_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 : toIocDiv hp (a + p) b = toIocDiv hp a b - 1
⊢ toIocDiv hp (p + a) b = toIocDiv hp a b - 1
have rw₁ : toIocDiv hp a b - 1 = toIocDiv hp a b - 1
Tactic: rw [add_comm, toIocDiv_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 c : α
⊢ toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b
have a₁ : b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)
Tactic: apply toIcoDiv_eq_of_sub_zsmul_mem_Ico
-- 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 : α
⊢ b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)
have a₁ : b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)
Tactic: rw [← sub_right_comm, Set.sub_mem_Ico_iff_left, add_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 : α
⊢ toIocDiv hp a (b - c) = toIocDiv hp (a + c) b
have a₁ : b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)
Tactic: apply toIocDiv_eq_of_sub_zsmul_mem_Ioc