awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using strictAntiOn_of_lt_pred hs (f := f)

Premises used: Order.pred_eq_sub_one, strictAntiOn_of_lt_pred
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f (a - 1) ≤ f a) → Monotone f

Tactic:
simpa [Order.pred_eq_sub_one] using monotone_of_pred_le (f := f)

Premises used: Order.pred_eq_sub_one, monotone_of_pred_le
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f a ≤ f (a - 1)) → Antitone f

Tactic:
simpa [Order.pred_eq_sub_one] using antitone_of_le_pred (f := f)

Premises used: Order.pred_eq_sub_one, antitone_of_le_pred
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f (a - 1) < f a) → StrictMono f

Tactic:
simpa [Order.pred_eq_sub_one] using strictMono_of_pred_lt (f := f)

Premises used: Order.pred_eq_sub_one, strictMono_of_pred_lt
-- Module: Mathlib.Algebra.Order.SuccPred
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Sub α
inst_3 : One α
inst_4 : PredSubOrder α
inst_5 : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f a < f (a - 1)) → StrictAnti f

Tactic:
simpa [Order.pred_eq_sub_one] using strictAnti_of_lt_pred (f := f)

Premises used: Order.pred_eq_sub_one, strictAnti_of_lt_pred
-- Module: Mathlib.Algebra.Order.Sum
Goal:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
inst : LE β
inst_1 : One β
v₁ : α₁ → β
v₂ : α₂ → β
⊢ 1 ≤ Sum.elim v₁ v₂ ↔ 1 ≤ v₁ ∧ 1 ≤ v₂

Tactic:
const_le_elim_iff

Premises used: Sum.const_le_elim_iff
-- Module: Mathlib.Algebra.Order.Sum
Goal:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
inst : LE β
inst_1 : One β
v₁ : α₁ → β
v₂ : α₂ → β
⊢ Sum.elim v₁ v₂ ≤ 1 ↔ v₁ ≤ 1 ∧ v₂ ≤ 1

Tactic:
elim_le_const_iff

Premises used: Sum.elim_le_const_iff
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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.Ico a (a + p)

Tactic:
(existsUnique_sub_zsmul_mem_Ico hp b a).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, toIcoDiv, And.left, existsUnique_sub_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
⊢ toIcoDiv hp a b = n ↔ b - n • p ∈ Set.Ico a (a + p)

Tactic:
(existsUnique_sub_zsmul_mem_Ico hp b a).choose_eq_iff

Premises used: Set.Mem, ExistsUnique.choose_eq_iff, toIcoDiv, existsUnique_sub_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocDiv hp a b • p ∈ Set.Ioc a (a + p)

Tactic:
(existsUnique_sub_zsmul_mem_Ioc hp b a).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, existsUnique_sub_zsmul_mem_Ioc, And.left, toIocDiv
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
⊢ toIocDiv hp a b = n ↔ b - n • p ∈ Set.Ioc a (a + p)

Tactic:
(existsUnique_sub_zsmul_mem_Ioc hp b a).choose_eq_iff

Premises used: Set.Mem, ExistsUnique.choose_eq_iff, existsUnique_sub_zsmul_mem_Ioc, toIocDiv
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b ∈ Set.Ico a (a + p)

Tactic:
sub_toIcoDiv_zsmul_mem_Ico hp a b

Premises used: Set.Mem, sub_toIcoDiv_zsmul_mem_Ico, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ toIcoMod hp 0 b ∈ Set.Ico 0 (0 + p)

Tactic:
toIcoMod_mem_Ico hp 0 b

Premises used: toIcoMod_mem_Ico, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
h : p = 0 + p
⊢ toIcoMod hp 0 b ∈ Set.Ico 0 p

Tactic:
convert! toIcoMod_mem_Ico hp 0 b

Premises used: toIcoMod_mem_Ico, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ p = 0 + p

Tactic:
(zero_add p).symm

Premises used: zero_add, Eq.symm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ p = 0 + p

Tactic:
exact (zero_add p).symm

Premises used: zero_add, Eq.symm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b ∈ Set.Ioc a (a + p)

Tactic:
sub_toIocDiv_zsmul_mem_Ioc hp a b

Premises used: Set.Mem, sub_toIocDiv_zsmul_mem_Ioc, toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ a ≤ toIcoMod hp a b

Tactic:
(Set.mem_Ico.1 (toIcoMod_mem_Ico hp a b)).1

Premises used: Set.mem_Ico, toIcoMod_mem_Ico, And.left, Iff.mp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ a < toIocMod hp a b

Tactic:
(Set.mem_Ioc.1 (toIocMod_mem_Ioc hp a b)).1

Premises used: And.left, Iff.mp, toIocMod_mem_Ioc, Set.mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 + p

Tactic:
(Set.mem_Ico.1 (toIcoMod_mem_Ico hp a b)).2

Premises used: Set.mem_Ico, toIcoMod_mem_Ico, And.right, Iff.mp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b ≤ a + p

Tactic:
(Set.mem_Ioc.1 (toIocMod_mem_Ioc hp a b)).2

Premises used: And.right, Iff.mp, toIocMod_mem_Ioc, Set.mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 = toIcoMod hp a b

Tactic:
rfl

Premises used: toIcoMod, rfl
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocDiv hp a b • p = toIocMod hp a b

Tactic:
rfl

Premises used: toIocMod, rfl
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 - b = -(b - toIcoDiv hp a b • p)
rw₁ rw₂ : toIcoDiv hp a b • p - b = toIcoDiv hp a b • p - b
⊢ toIcoDiv hp a b • p - b = -toIcoMod hp a b

Tactic:
rw [toIcoMod, neg_sub]

Premises used: neg_sub, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 - b = -(b - toIocDiv hp a b • p)
rw₁ rw₂ : toIocDiv hp a b • p - b = toIocDiv hp a b • p - b
⊢ toIocDiv hp a b • p - b = -toIocMod hp a b

Tactic:
rw [toIocMod, neg_sub]

Premises used: neg_sub, toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 - b = -toIcoDiv hp a b • p
rw₁ : -(toIcoDiv hp a b • p) = -toIcoDiv hp a b • p
rw₂ rw₃ : -(toIcoDiv hp a b • p) = -(toIcoDiv hp a b • p)
⊢ toIcoMod hp a b - b = -toIcoDiv hp a b • p

Tactic:
rw [toIcoMod, sub_sub_cancel_left, neg_smul]

Premises used: neg_smul, sub_sub_cancel_left, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 - b = -toIocDiv hp a b • p
rw₁ : -(toIocDiv hp a b • p) = -toIocDiv hp a b • p
rw₂ rw₃ : -(toIocDiv hp a b • p) = -(toIocDiv hp a b • p)
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p

Tactic:
rw [toIocMod, sub_sub_cancel_left, neg_smul]

Premises used: neg_smul, sub_sub_cancel_left, toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : b - (b - toIcoDiv hp a b • p) = toIcoDiv hp a b • p
rw₁ rw₂ : toIcoDiv hp a b • p = toIcoDiv hp a b • p
⊢ b - toIcoMod hp a b = toIcoDiv hp a b • p

Tactic:
rw [toIcoMod, sub_sub_cancel]

Premises used: sub_sub_cancel, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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
rw₁ rw₂ : toIocDiv hp a b • p = toIocDiv hp a b • p
⊢ b - toIocMod hp a b = toIocDiv hp a b • p

Tactic:
rw [toIocMod, sub_sub_cancel]

Premises used: sub_sub_cancel, toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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
rw₁ rw₂ : b = b
⊢ toIcoMod hp a b + toIcoDiv hp a b • p = b

Tactic:
rw [toIcoMod, sub_add_cancel]

Premises used: sub_add_cancel, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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
rw₁ rw₂ : b = b
⊢ toIocMod hp a b + toIocDiv hp a b • p = b

Tactic:
rw [toIocMod, sub_add_cancel]

Premises used: toIocMod, sub_add_cancel
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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
rw₁ rw₂ : b = b
⊢ toIcoDiv hp a b • p + toIcoMod hp a b = b

Tactic:
rw [add_comm, toIcoMod_add_toIcoDiv_zsmul]

Premises used: add_comm, toIcoMod_add_toIcoDiv_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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
rw₁ rw₂ : b = b
⊢ toIocDiv hp a b • p + toIocMod hp a b = b

Tactic:
rw [add_comm, toIocMod_add_toIocDiv_zsmul]

Premises used: toIocMod_add_toIocDiv_zsmul, add_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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

Tactic:
⟨fun h =>
      ⟨h ▸ toIcoMod_mem_Ico hp a b, toIcoDiv hp a b, h ▸ (toIcoMod_add_toIcoDiv_zsmul _ _ _).symm⟩,
      ?_⟩

Premises used: Eq.rec, toIcoDiv, toIcoMod_mem_Ico, And.intro, Iff.intro, Exists.intro, toIcoMod_add_toIcoDiv_zsmul, Eq.symm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : (c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIcoMod hp a b = c
⊢ toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b = c + z • p

Tactic:
refine
    ⟨fun h =>
      ⟨h ▸ toIcoMod_mem_Ico hp a b, toIcoDiv hp a b, h ▸ (toIcoMod_add_toIcoDiv_zsmul _ _ _).symm⟩,
      ?_⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : (c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b - z • p = c) → toIcoMod hp a b = c
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIcoMod hp a b = c

Tactic:
simp_rw [← @sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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
rw₁ rw₂ : b - toIcoDiv hp a b • p = b - toIcoDiv hp a b • p
⊢ toIcoMod hp a b = b - n • p

Tactic:
rw [← toIcoDiv_eq_of_sub_zsmul_mem_Ico hp hc, toIcoMod]

Premises used: toIcoDiv_eq_of_sub_zsmul_mem_Ico, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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

Tactic:
⟨fun h =>
      ⟨h ▸ toIocMod_mem_Ioc hp a b, toIocDiv hp a b, h ▸ (toIocMod_add_toIocDiv_zsmul hp _ _).symm⟩,
      ?_⟩

Premises used: toIocMod_add_toIocDiv_zsmul, Eq.rec, And.intro, Iff.intro, Exists.intro, toIocMod_mem_Ioc, Eq.symm, toIocDiv
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : (c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIocMod hp a b = c
⊢ toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b = c + z • p

Tactic:
refine
    ⟨fun h =>
      ⟨h ▸ toIocMod_mem_Ioc hp a b, toIocDiv hp a b, h ▸ (toIocMod_add_toIocDiv_zsmul hp _ _).symm⟩,
      ?_⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : (c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b - z • p = c) → toIocMod hp a b = c
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ (z : ℤ), b = c + z • p) → toIocMod hp a b = c

Tactic:
simp_rw [← @sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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
rw₁ rw₂ : b - toIocDiv hp a b • p = b - toIocDiv hp a b • p
⊢ toIocMod hp a b = b - n • p

Tactic:
rw [← toIocDiv_eq_of_sub_zsmul_mem_Ioc hp hc, toIocMod]

Premises used: toIocDiv_eq_of_sub_zsmul_mem_Ioc, toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a - HSMul.hSMul (α := ℤ) 0 p ∈ Set.Ico a (a + p)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a - HSMul.hSMul (α := ℤ) (-1) p ∈ Set.Ioc a (a + p)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
rw : a < a + p ∧ ∃ (z : ℤ), a = a + z • p
⊢ toIcoMod hp a a = a

Tactic:
rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]

Premises used: Set.left_mem_Ico, toIcoMod_eq_iff
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a = a + HSMul.hSMul (α := ℤ) 0 p

Tactic:
simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ (z : ℤ), a = a + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
rw : a < a + p ∧ ∃ (z : ℤ), a = a + p + z • p
⊢ toIocMod hp a a = a + p

Tactic:
rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]

Premises used: toIocMod_eq_iff, Set.right_mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a = a + p + HSMul.hSMul (α := ℤ) (-1) p

Tactic:
simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ (z : ℤ), a = a + p + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, -1, by simp⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p - HSMul.hSMul (α := ℤ) 1 p ∈ Set.Ico a (a + p)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p - HSMul.hSMul (α := ℤ) 0 p ∈ Set.Ioc a (a + p)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
rw : a < a + p ∧ ∃ (z : ℤ), a + p = a + z • p
⊢ toIcoMod hp a (a + p) = a

Tactic:
rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]

Premises used: Set.left_mem_Ico, toIcoMod_eq_iff
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p = a + HSMul.hSMul (α := ℤ) 1 p

Tactic:
simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ (z : ℤ), a + p = a + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, 1, by simp⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
rw : a < a + p ∧ ∃ (z : ℤ), a + p = a + p + z • p
⊢ toIocMod hp a (a + p) = a + p

Tactic:
rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]

Premises used: toIocMod_eq_iff, Set.right_mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p = a + p + HSMul.hSMul (α := ℤ) 0 p

Tactic:
simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ (z : ℤ), a + p = a + p + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIcoDiv hp a b + m) • p ∈ Set.Ico a (a + p)

Tactic:
simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIcoDiv_zsmul_mem_Ico hp a b

Premises used: sub_toIcoDiv_zsmul_mem_Ico, add_smul, add_sub_add_right_eq_sub
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 : ℤ)

Tactic:
mod_cast toIcoDiv_add_zsmul hp a b m

Premises used: congrArg, cast, toIcoDiv.congr_simp, toIcoDiv, toIcoDiv_add_zsmul, Int, Nat.cast, HAdd.hAdd, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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

Tactic:
toIcoDiv_eq_of_sub_zsmul_mem_Ico _ ?_

Premises used: toIcoDiv_eq_of_sub_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
refine : b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)
⊢ toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m

Tactic:
refine toIcoDiv_eq_of_sub_zsmul_mem_Ico _ ?_

Premises used: toIcoDiv_eq_of_sub_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : b - toIcoDiv hp a b • p + m • p ∈ Set.Ico (a + m • p) (a + p + m • p)
⊢ b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)

Tactic:
rw [sub_smul, ← sub_add, add_right_comm]

Premises used: sub_add, sub_smul, add_right_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 • p + m • p ∈ Set.Ico (a + m • p) (a + p + m • p)

Tactic:
simpa using sub_toIcoDiv_zsmul_mem_Ico hp a b

Premises used: sub_toIcoDiv_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 : ℤ)

Tactic:
mod_cast toIcoDiv_add_zsmul' hp a b m

Premises used: congrArg, HSub.hSub, cast, toIcoDiv.congr_simp, toIcoDiv, Int, Nat.cast, HAdd.hAdd, toIcoDiv_add_zsmul', Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b + m) • p ∈ Set.Ioc a (a + p)

Tactic:
simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIocDiv_zsmul_mem_Ioc hp a b

Premises used: add_smul, sub_toIocDiv_zsmul_mem_Ioc, add_sub_add_right_eq_sub
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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 : ℤ)

Tactic:
mod_cast toIocDiv_add_zsmul hp a b m

Premises used: congrArg, cast, Int, toIocDiv.congr_simp, Nat.cast, HAdd.hAdd, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', toIocDiv_add_zsmul, Eq, toIocDiv
-- Module: Mathlib.Algebra.Order.ToIntervalMod
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

Tactic:
toIocDiv_eq_of_sub_zsmul_mem_Ioc _ ?_

Premises used: toIocDiv_eq_of_sub_zsmul_mem_Ioc