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 c : α
⊢ b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)
have a₁ : b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)
Tactic: rw [← sub_right_comm, Set.sub_mem_Ioc_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 : α
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)
have rw : toIcoDiv hp (a - c) b = toIcoDiv hp a (b - -c)
Tactic: rw [← sub_neg_eq_add, toIcoDiv_sub_eq_toIcoDiv_add, 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 c : α
rw : toIcoDiv hp (a - c) b = toIcoDiv hp a (b - -c)
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)
have rw₁ : toIcoDiv hp (a - c) b = toIcoDiv hp (a + -c) b
Tactic: rw [← sub_neg_eq_add, toIcoDiv_sub_eq_toIcoDiv_add, 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 c : α
rw : toIcoDiv hp (a - c) b = toIcoDiv hp a (b - -c)
rw₁ : toIcoDiv hp (a - c) b = toIcoDiv hp (a + -c) b
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)
have rw₂ : toIcoDiv hp (a + -c) b = toIcoDiv hp (a + -c) b
Tactic: rw [← sub_neg_eq_add, toIcoDiv_sub_eq_toIcoDiv_add, 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 c : α
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)
have rw : toIocDiv hp (a - c) b = toIocDiv hp a (b - -c)
Tactic: rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, 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 c : α
rw : toIocDiv hp (a - c) b = toIocDiv hp a (b - -c)
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)
have rw₁ : toIocDiv hp (a - c) b = toIocDiv hp (a + -c) b
Tactic: rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, 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 c : α
rw : toIocDiv hp (a - c) b = toIocDiv hp a (b - -c)
rw₁ : toIocDiv hp (a - c) b = toIocDiv hp (a + -c) b
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)
have rw₂ : toIocDiv hp (a + -c) b = toIocDiv hp (a + -c) b
Tactic: rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, 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 : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
have rwa : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a + -p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
Tactic: rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
Cleared hypotheses: this
-- 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 : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
rwa : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a + -p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
have rwa₁ : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a - p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
Tactic: rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
Cleared hypotheses: this
-- 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 : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
rwa : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a + -p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
rwa₁ : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a - p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
have rwa₂ : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a) (b + p)), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
Tactic: rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
Cleared hypotheses: this
-- 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 : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
rwa : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a + -p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
rwa₁ : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a - p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
rwa₂ : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a) (b + p)), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
have rwa₃ : ∀ (this : toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
Tactic: rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
Cleared hypotheses: this
-- 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) = -(toIocDiv hp (-a) b + 1)
have suffices : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
Tactic: suffices toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b by
    rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
-- 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) = -toIocDiv hp (-(a + p)) b
have rw : toIocDiv hp (-(a + p)) b = -toIcoDiv hp a (-b)
Tactic: rw [← neg_eq_iff_eq_neg, eq_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 : α
⊢ toIocDiv hp (-(a + p)) b = -toIcoDiv hp a (-b)
have a₁ : b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
Tactic: apply toIocDiv_eq_of_sub_zsmul_mem_Ioc
-- 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 : α
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
have hc : a ≤ -b - toIcoDiv hp a (-b) • p
Tactic: obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)
-- 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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
have ho : -b - toIcoDiv hp a (-b) • p < a + p
Tactic: obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)
-- 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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -b - toIcoDiv hp a (-b) • p < a + p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
have ho₁ : -(a + p) < b - -toIcoDiv hp a (-b) • p
Tactic: rw [← neg_lt_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at ho
Cleared hypotheses: ho
-- 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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
have hc₁ : b - -toIcoDiv hp a (-b) • p ≤ -a
Tactic: rw [← neg_le_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at hc
Cleared hypotheses: hc, ho
-- 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 : α
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
have a₁ : -a = -(a + p) + p
Tactic: refine ⟨ho, hc.trans_eq ?_⟩
-- 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 : α
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ -a = -(a + p) + p
have a₁ : -a = -a + -p + p
Tactic: rw [neg_add, neg_add_cancel_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 : α
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
a₁ : -a = -a + -p + p
⊢ -a = -(a + p) + p
have a₂ : -a = -a
Tactic: rw [neg_add, neg_add_cancel_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 (-b) = -(toIcoDiv hp (-a) b + 1)
have rw : toIocDiv hp a (- - -b) = -(toIcoDiv hp (-a) (- -b) + 1)
Tactic: rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_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) = -(toIcoDiv hp (-a) (- -b) + 1)
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
have rw₁ : toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
Tactic: rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_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) = -(toIcoDiv hp (-a) (- -b) + 1)
rw₁ : toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
have rw₂ : toIocDiv hp a (-b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
Tactic: rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_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) = -(toIcoDiv hp (-a) (- -b) + 1)
rw₁ : toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₂ : toIocDiv hp a (-b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
have rw₃ : toIocDiv hp a (-b) = -(-(toIocDiv hp a (-b) + 1) + 1)
Tactic: rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_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) = -(toIcoDiv hp (-a) (- -b) + 1)
rw₁ : toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₂ : toIocDiv hp a (-b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₃ : toIocDiv hp a (-b) = -(-(toIocDiv hp a (-b) + 1) + 1)
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
have rw₄ : toIocDiv hp a (-b) = - -(toIocDiv hp a (-b) + 1) - 1
Tactic: rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_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) = -(toIcoDiv hp (-a) (- -b) + 1)
rw₁ : toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₂ : toIocDiv hp a (-b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₃ : toIocDiv hp a (-b) = -(-(toIocDiv hp a (-b) + 1) + 1)
rw₄ : toIocDiv hp a (-b) = - -(toIocDiv hp a (-b) + 1) - 1
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
have rw₅ : toIocDiv hp a (-b) = toIocDiv hp a (-b) + 1 - 1
Tactic: rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_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) = -(toIcoDiv hp (-a) (- -b) + 1)
rw₁ : toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₂ : toIocDiv hp a (-b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₃ : toIocDiv hp a (-b) = -(-(toIocDiv hp a (-b) + 1) + 1)
rw₄ : toIocDiv hp a (-b) = - -(toIocDiv hp a (-b) + 1) - 1
rw₅ : toIocDiv hp a (-b) = toIocDiv hp a (-b) + 1 - 1
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
have rw₆ : toIocDiv hp a (-b) = toIocDiv hp a (-b)
Tactic: rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_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 : α
m : ℤ
⊢ toIcoMod hp a (b + m • p) = toIcoMod hp a b
have rw : b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p
Tactic: rw [toIcoMod, toIcoDiv_add_zsmul, toIcoMod, 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 : α
m : ℤ
⊢ toIocMod hp a (b + m • p) = toIocMod hp a b
have rw : b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p
Tactic: rw [toIocMod, toIocDiv_add_zsmul, toIocMod, 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 : α
m : ℤ
⊢ toIcoMod hp a (m • p + b) = toIcoMod hp a b
have rw : toIcoMod hp a (b + m • p) = toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_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 : α
m : ℤ
rw : toIcoMod hp a (b + m • p) = toIcoMod hp a b
⊢ toIcoMod hp a (m • p + b) = toIcoMod hp a b
have rw₁ : toIcoMod hp a b = toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_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 : α
m : ℤ
⊢ toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b
have rw : toIcoMod hp (a + m • p) b = m • p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_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 : toIcoMod hp (a + m • p) b = m • p + toIcoMod hp a b
⊢ toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b
have rw₁ : toIcoMod hp a b + m • p = m • p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_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 : toIcoMod hp (a + m • p) b = m • p + toIcoMod hp a b
rw₁ : toIcoMod hp a b + m • p = m • p + toIcoMod hp a b
⊢ toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b
have rw₂ : m • p + toIcoMod hp a b = m • p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_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 : ℤ
⊢ toIocMod hp a (m • p + b) = toIocMod hp a b
have rw : toIocMod hp a (b + m • p) = toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_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 : α
m : ℤ
rw : toIocMod hp a (b + m • p) = toIocMod hp a b
⊢ toIocMod hp a (m • p + b) = toIocMod hp a b
have rw₁ : toIocMod hp a b = toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_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 : α
m : ℤ
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b
have rw : toIocMod hp (a + m • p) b = m • p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_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 : toIocMod hp (a + m • p) b = m • p + toIocMod hp a b
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b
have rw₁ : toIocMod hp a b + m • p = m • p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_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 : toIocMod hp (a + m • p) b = m • p + toIocMod hp a b
rw₁ : toIocMod hp a b + m • p = m • p + toIocMod hp a b
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b
have rw₂ : m • p + toIocMod hp a b = m • p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_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 : ℤ
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b
have rw : toIcoMod hp a (b + -(m • p)) = toIcoMod hp a b
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_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 : α
m : ℤ
rw : toIcoMod hp a (b + -(m • p)) = toIcoMod hp a b
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b
have rw₁ : toIcoMod hp a (b + -m • p) = toIcoMod hp a b
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_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 : α
m : ℤ
rw : toIcoMod hp a (b + -(m • p)) = toIcoMod hp a b
rw₁ : toIcoMod hp a (b + -m • p) = toIcoMod hp a b
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b
have rw₂ : toIcoMod hp a b = toIcoMod hp a b
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_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 : α
m : ℤ
⊢ toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p
have simp_rw : toIcoMod hp (a + -(m • p)) b = toIcoMod hp a b + -(m • p)
Tactic: simp_rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_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 : α
m : ℤ
simp_rw : toIcoMod hp (a + -(m • p)) b = toIcoMod hp a b + -(m • p)
⊢ toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p
have simp_rw₁ : toIcoMod hp (a + -m • p) b = toIcoMod hp a b + -m • p
Tactic: simp_rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_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 : α
m : ℤ
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b
have rw : toIocMod hp a (b + -(m • p)) = toIocMod hp a b
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_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 : α
m : ℤ
rw : toIocMod hp a (b + -(m • p)) = toIocMod hp a b
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b
have rw₁ : toIocMod hp a (b + -m • p) = toIocMod hp a b
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_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 : α
m : ℤ
rw : toIocMod hp a (b + -(m • p)) = toIocMod hp a b
rw₁ : toIocMod hp a (b + -m • p) = toIocMod hp a b
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b
have rw₂ : toIocMod hp a b = toIocMod hp a b
Tactic: rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_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 : α
m : ℤ
⊢ toIocMod hp (a - m • p) b = toIocMod hp a b - m • p
have simp_rw : toIocMod hp (a + -(m • p)) b = toIocMod hp a b + -(m • p)
Tactic: simp_rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_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 : α
m : ℤ
simp_rw : toIocMod hp (a + -(m • p)) b = toIocMod hp a b + -(m • p)
⊢ toIocMod hp (a - m • p) b = toIocMod hp a b - m • p
have simp_rw₁ : toIocMod hp (a + -m • p) b = toIocMod hp a b + -m • p
Tactic: simp_rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_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 : α
⊢ toIcoMod hp a (p + b) = toIcoMod hp a b
have rw : toIcoMod hp a (b + p) = toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_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 : toIcoMod hp a (b + p) = toIcoMod hp a b
⊢ toIcoMod hp a (p + b) = toIcoMod hp a b
have rw₁ : toIcoMod hp a b = toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_right]