awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
refine_1 : ∀ (h : toIocMod hp a b = toIocMod hp a c), c - b = (toIocDiv hp a c - toIocDiv hp a b) • p
refine_2 : ∀ (h : ∃ (n : ℤ), c - b = n • p), toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a b = toIocMod hp a c ↔ ∃ (n : ℤ), c - b = n • p

Tactic:
refine ⟨fun h => ⟨toIocDiv hp a c - toIocDiv hp a b, ?_⟩, fun h => ?_⟩
-- 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 : toIocMod hp a b = toIocMod hp a c
rw : toIocMod hp a c + toIocDiv hp a c • p - (toIocMod hp a b + toIocDiv hp a b • p)
| c - b

Tactic:
rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]

Premises used: toIocMod_add_toIocDiv_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 c : α
h : toIocMod hp a b = toIocMod hp a c
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
⊢ c - b = (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]

Premises used: toIocMod_add_toIocDiv_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 c : α
h : toIocMod hp a b = toIocMod hp a c
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
⊢ 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:
rw [h, sub_smul]

Premises used: sub_smul
-- 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 : toIocMod hp a b = toIocMod hp a c
⊢ 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:
abel
-- 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 : ∃ (n : ℤ), c - b = n • p
refine_2 : ∀ (z : ℤ) (hz : c - b = z • p), toIocMod hp a b = toIocMod hp a c
⊢ toIocMod hp a b = toIocMod hp a c

Tactic:
rcases h with ⟨z, hz⟩
-- 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 : α
z : ℤ
hz : c = z • p + b
refine_2 : toIocMod hp a b = toIocMod hp a (z • p + b)
refine_2₁ refine_2₂ : toIocMod hp a b = toIocMod hp a b
⊢ toIocMod hp a b = toIocMod hp a c

Tactic:
rw [hz, toIocMod_zsmul_add]

Premises used: toIocMod_zsmul_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 : α
n : ℤ
rw : toIcoMod hp a a = a
rw₁ rw₂ : a = a
⊢ toIcoMod hp a (a + n • p) = a

Tactic:
rw [toIcoMod_add_zsmul, toIcoMod_apply_left]

Premises used: toIcoMod_add_zsmul, toIcoMod_apply_left
-- 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 ≡ b [PMOD p] ↔ toIocMod hp a b = a + p

Tactic:
modEq_iff_eq_add_zsmul.trans ⟨?_, fun h => ⟨toIocDiv hp a b + 1, ?_⟩⟩

Premises used: HAdd.hAdd, Iff.intro, Exists.intro, Iff.trans, AddCommGroup.modEq_iff_eq_add_zsmul, OfNat.ofNat, 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 : α
refine_1 : (∃ (z : ℤ), b = a + z • p) → toIocMod hp a b = a + p
refine_2 : ∀ (h : toIocMod hp a b = a + p), b = a + (toIocDiv hp a b + 1) • p
⊢ a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p

Tactic:
refine modEq_iff_eq_add_zsmul.trans ⟨?_, fun h => ⟨toIocDiv hp a b + 1, ?_⟩⟩

Premises used: HAdd.hAdd, Iff.intro, Exists.intro, Iff.trans, AddCommGroup.modEq_iff_eq_add_zsmul, OfNat.ofNat, 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 : α
z : ℤ
refine_1 : toIocMod hp a a = a + p
refine_1₁ refine_1₂ : a + p = a + p
⊢ toIocMod hp a (a + z • p) = a + p

Tactic:
rw [toIocMod_add_zsmul, toIocMod_apply_left]

Premises used: toIocMod_apply_left, toIocMod_add_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 : α
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)
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : b - toIocDiv hp a b • p = a + p
⊢ b = a + (toIocDiv hp a b + 1) • p

Tactic:
rwa [add_one_zsmul, add_left_comm, ← sub_eq_iff_eq_add']

Premises used: add_left_comm, add_one_zsmul, 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 : α
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
⊢ [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

Tactic:
rw [modEq_iff_toIcoMod_eq_left hp]

Premises used: AddCommGroup.modEq_iff_toIcoMod_eq_left
-- 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 ≠ toIocMod hp a b

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
⊢ ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

Tactic:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : (∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b
⊢ ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

Tactic:
rw [← not_exists, not_imp_not]

Premises used: not_exists, not_imp_not
-- 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 : α
⊢ (∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b

Tactic:
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

Premises used: Iff.mpr, toIcoMod_eq_iff, _private.0.AddCommGroup.tfae_modEq.match_1, Set.Ioo_subset_Ico_self, toIocMod_eq_iff, Set.Ioo_subset_Ioc_self, And.intro, toIocMod, Exists.intro, HSMul.hSMul, Eq.symm, Eq, sub_add_cancel, toIcoMod, Eq.trans
-- 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 : α
⊢ (∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b

Tactic:
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
-- 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_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
-- 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 : α
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 + p = toIocMod hp a b

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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 ≠ toIocMod hp a b

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
⊢ ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b

Tactic:
4 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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
rw : ¬p = 0
⊢ toIcoMod hp a b ≠ toIocMod hp a b

Tactic:
rw [← h, Ne, eq_comm, add_eq_left]

Premises used: Ne, eq_comm, add_eq_left
-- 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 : α
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
⊢ ¬p = 0

Tactic:
hp.ne'

Premises used: LT.lt.ne'
-- 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 : α
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
⊢ ¬p = 0

Tactic:
exact hp.ne'

Premises used: LT.lt.ne'
-- 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 : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
⊢ ∀ (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'
-- 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 : α
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
⊢ toIcoMod hp a b = a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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
⊢ toIcoMod hp a b + p = toIocMod hp a b

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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
⊢ ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b

Tactic:
1 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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
rw : a < a + p ∧ ∃ (z : ℤ), b = a + p + z • p
⊢ toIcoMod hp a b + p = toIocMod hp a b

Tactic:
rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]

Premises used: eq_comm, 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 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

Tactic:
⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩

Premises used: lt_add_of_pos_right, HSub.hSub, toIcoDiv, And.intro, Exists.intro, 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
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
refine : b = a + p + (toIcoDiv hp a b - 1) • p
⊢ a < a + p ∧ ∃ (z : ℤ), b = a + p + z • p

Tactic:
refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
-- 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 : α
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
rw : b = a + toIcoDiv hp a b • p
⊢ b = a + p + (toIcoDiv hp a b - 1) • p

Tactic:
rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]

Premises used: add_neg_cancel, sub_one_zsmul, add_add_add_comm, add_zero
-- 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 : α
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
rw : a + toIcoDiv hp a b • p
| b

Tactic:
rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]

Premises used: 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 : α
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
conv_lhs : b = a + toIcoDiv hp a b • p
conv_lhs₁ : a + toIcoDiv hp a b • p = a + toIcoDiv hp a b • p
⊢ b = a + toIcoDiv hp a b • p

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

Premises used: 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 : α
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
⊢ ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b

Tactic:
tfae_have 1 → 4
  | h => by
    rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]
    refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
    rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]
    conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ toIcoMod hp a b = a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ ∀ (a_1 : ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)), toIcoMod hp a b = a

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
rw : ¬toIcoMod hp a b = a → ∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)
⊢ ∀ (a_1 : ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)), toIcoMod hp a b = a

Tactic:
rw [← not_exists, not_imp_comm]

Premises used: not_imp_comm, not_exists
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ toIcoMod hp a b ∈ Set.Ico a (a + p)

Tactic:
have h' := toIcoMod_mem_Ico hp a b
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
h' : toIcoMod hp a b ∈ Set.Ico a (a + p)
⊢ ¬toIcoMod hp a b = a → ∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)

Tactic:
fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩

Premises used: toIcoDiv, And.right, And.left, And.intro, Exists.intro, LE.le.lt_of_ne'
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
h' : toIcoMod hp a b ∈ Set.Ico a (a + p)
⊢ ¬toIcoMod hp a b = a → ∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)

Tactic:
exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩
-- 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 : α
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
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ ∀ (a_1 : ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)), toIcoMod hp a b = a

Tactic:
tfae_have 2 → 1 := by
    rw [← not_exists, not_imp_comm]
    have h' := toIcoMod_mem_Ico hp a b
    exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩