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 : α
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
tfae_2_to_1 : ∀ (a_1 : ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)), toIcoMod hp a b = a
⊢ [toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE

Tactic:
tfae_finish
-- 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] ↔ ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)

Tactic:
(tfae_modEq hp a b).out 0 1

Premises used: List.TFAE.out, AddCommGroup.tfae_modEq, 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 : α
⊢ a ≡ b [PMOD p] ↔ toIcoMod hp a b ≠ toIocMod hp a b

Tactic:
(tfae_modEq hp a b).out 0 2

Premises used: List.TFAE.out, AddCommGroup.tfae_modEq, 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 : α
⊢ a ≡ b [PMOD p] ↔ toIcoMod hp a b + p = toIocMod hp a b

Tactic:
(tfae_modEq hp a b).out 0 3

Premises used: List.TFAE.out, AddCommGroup.tfae_modEq, 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 : α
⊢ ¬a ≡ b [PMOD p] ↔ toIcoMod hp a b = toIocMod hp a b

Tactic:
(modEq_iff_toIcoMod_ne_toIocMod _).not_left

Premises used: Iff.not_left, AddCommGroup.modEq_iff_toIcoMod_ne_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 : toIcoMod hp a b = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b
rw₁ : b - toIcoDiv hp a b • p = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b
rw₂ : b - toIcoDiv hp a b • p = b - toIocDiv hp a b • p ↔ toIcoDiv hp a b = toIocDiv hp a b
rw₃ : toIcoDiv hp a b • p = toIocDiv hp a b • p ↔ toIcoDiv hp a b = toIocDiv hp a b
rw₄ rw₅ : toIcoDiv hp a b = toIocDiv hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b

Tactic:
rw [not_modEq_iff_toIcoMod_eq_toIocMod hp, toIcoMod, toIocMod, sub_right_inj,
    zsmul_left_inj hp]

Premises used: zsmul_left_inj, AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod, sub_right_inj, toIocMod, 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 : toIcoMod hp a b + p = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
rw₁ : b - toIcoDiv hp a b • p + p = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
rw₂ : b - toIcoDiv hp a b • p + p = b - toIocDiv hp a b • p ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
rw₃ : b - toIcoDiv hp a b • p = b - toIocDiv hp a b • p - p ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
rw₄ : b - toIcoDiv hp a b • p = b - (toIocDiv hp a b • p + p) ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
rw₅ : toIcoDiv hp a b • p = toIocDiv hp a b • p + p ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
rw₆ : toIcoDiv hp a b • p = (toIocDiv hp a b + 1) • p ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
rw₇ rw₈ : toIcoDiv hp a b = toIocDiv hp a b + 1 ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
rw [modEq_iff_toIcoMod_add_period_eq_toIocMod hp, toIcoMod, toIocMod, ← eq_sub_iff_add_eq,
    sub_sub, sub_right_inj, ← add_one_zsmul, zsmul_left_inj hp]

Premises used: zsmul_left_inj, sub_right_inj, AddCommGroup.modEq_iff_toIcoMod_add_period_eq_toIocMod, eq_sub_iff_add_eq, add_one_zsmul, sub_sub, toIocMod, 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 : α
rw : (∃ (n : ℤ), b - a = n • p) ↔ a ≡ b [PMOD p]
rw₁ rw₂ : (∃ (n : ℤ), b - a = n • p) ↔ ∃ (m : ℤ), b - a = m • p
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]

Tactic:
rw [toIcoMod_eq_toIcoMod, AddCommGroup.modEq_iff_zsmul']

Premises used: toIcoMod_eq_toIcoMod, AddCommGroup.modEq_iff_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 : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {b : α | toIcoMod hp a b = toIocMod hp a b} x ↔
      Membership.mem (γ := Set α) (⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p)) x
⊢ Eq.{u_1 + 1} (α := Set α) {b : α | toIcoMod hp a b = toIocMod hp a b} (⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p))

Tactic:
ext1
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x : α
h : toIcoMod hp a x = toIocMod hp a x ↔ Membership.mem (γ := Set α) (⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p)) x
h₁ : toIcoMod hp a x = toIocMod hp a x ↔ ∃ (i : ℤ), x ∈ Set.Ioo (a + i • p) (a + p + i • p)
h₂ : toIcoMod hp a x = toIocMod hp a x ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
h₃ : ¬a ≡ x [PMOD p] ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
h₄ : (¬∀ (z : ℤ), x - z • p ∉ Set.Ioo a (a + p)) ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
h₅ : (∃ (x_1 : ℤ), ¬x - x_1 • p ∉ Set.Ioo a (a + p)) ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
⊢ Membership.mem (γ := Set α) {b : α | toIcoMod hp a b = toIocMod hp a b} x ↔
    Membership.mem (γ := Set α) (⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p)) x

Tactic:
simp_rw [Set.mem_setOf, Set.mem_iUnion, ← Set.sub_mem_Ioo_iff_left, ←
    not_modEq_iff_toIcoMod_eq_toIocMod, modEq_iff_forall_notMem_Ioo_mod hp, not_forall,
    Classical.not_not]

Premises used: AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod, Classical.not_not, AddCommGroup.modEq_iff_forall_notMem_Ioo_mod, Set.mem_iUnion, Set.mem_setOf, Classical.not_forall, Set.sub_mem_Ioo_iff_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 : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
rwa : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b ⋖ toIcoDiv hp a b
rwa₁ rwa₂ rwa₃ rwa₄ : toIocDiv hp a b = toIcoDiv hp a b ∨ Order.succ (toIocDiv hp a b) = toIcoDiv hp a b
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]

Premises used: wcovBy_iff_eq_or_covBy, Order.succ_eq_iff_covBy
-- 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 : α
suffices : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
    rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]
-- 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 : ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b

Tactic:
rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ←
    modEq_iff_toIcoDiv_eq_toIocDiv_add_one]

Premises used: AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, AddCommGroup.modEq_iff_toIcoDiv_eq_toIocDiv_add_one
-- 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] ∨ a ≡ b [PMOD p]

Tactic:
em' _

Premises used: em'
-- 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] ∨ a ≡ b [PMOD p]

Tactic:
exact em' _

Premises used: em'
-- 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 ≤ toIcoDiv hp a b • p
⊢ toIcoMod hp a b ≤ toIocMod hp a b

Tactic:
rw [toIcoMod, toIocMod, sub_le_sub_iff_left]

Premises used: sub_le_sub_iff_left, toIocMod, 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 : α
⊢ toIocDiv hp a b • p ≤ toIcoDiv hp a b • p

Tactic:
zsmul_left_mono hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le

Premises used: toIocDiv_wcovBy_toIcoDiv, LT.lt.le, WCovBy.le, zsmul_left_mono
-- 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 : α
⊢ toIocDiv hp a b • p ≤ toIcoDiv hp a b • p

Tactic:
exact zsmul_left_mono hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le

Premises used: toIocDiv_wcovBy_toIcoDiv, LT.lt.le, WCovBy.le, zsmul_left_mono
-- 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 ≤ toIocDiv hp a b + 1
⊢ toIocMod hp a b ≤ toIcoMod hp a b + p

Tactic:
rw [toIcoMod, toIocMod, sub_add, sub_le_sub_iff_left, sub_le_iff_le_add, ← add_one_zsmul,
    (zsmul_left_strictMono hp).le_iff_le]

Premises used: sub_add, sub_le_iff_le_add, sub_le_sub_iff_left, add_one_zsmul, zsmul_left_strictMono, toIocMod, StrictMono.le_iff_le, 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 : α
⊢ toIcoDiv hp a b ≤ toIocDiv hp a b + 1

Tactic:
apply (toIocDiv_wcovBy_toIcoDiv _ _ _).le_succ

Premises used: toIocDiv_wcovBy_toIcoDiv, WCovBy.le_succ
-- 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 : ∃ (z : ℤ), b = b + z • p
⊢ toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)

Tactic:
rw [toIcoMod_eq_iff, and_iff_left]

Premises used: and_iff_left, 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 b : α
⊢ b = b + 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 b : α
⊢ ∃ (z : ℤ), b = b + z • p

Tactic:
exact ⟨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 : α
rw : ∃ (z : ℤ), b = b + z • p
⊢ toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)

Tactic:
rw [toIocMod_eq_iff, and_iff_left]

Premises used: and_iff_left, toIocMod_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₂ b : α
⊢ toIcoMod hp a₁ (toIcoMod hp a₂ b) = toIcoMod hp a₁ b

Tactic:
(toIcoMod_eq_toIcoMod _).2 ⟨toIcoDiv hp a₂ b, self_sub_toIcoMod hp a₂ b⟩

Premises used: Iff.mpr, toIcoMod_eq_toIcoMod, toIcoDiv, self_sub_toIcoMod, Exists.intro
-- 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₂ b : α
⊢ toIcoMod hp a₁ (toIocMod hp a₂ b) = toIcoMod hp a₁ b

Tactic:
(toIcoMod_eq_toIcoMod _).2 ⟨toIocDiv hp a₂ b, self_sub_toIocMod hp a₂ b⟩

Premises used: Iff.mpr, toIcoMod_eq_toIcoMod, self_sub_toIocMod, Exists.intro, 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₁ a₂ b : α
⊢ toIocMod hp a₁ (toIocMod hp a₂ b) = toIocMod hp a₁ b

Tactic:
(toIocMod_eq_toIocMod _).2 ⟨toIocDiv hp a₂ b, self_sub_toIocMod hp a₂ b⟩

Premises used: Iff.mpr, self_sub_toIocMod, toIocMod_eq_toIocMod, Exists.intro, 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₁ a₂ b : α
⊢ toIocMod hp a₁ (toIcoMod hp a₂ b) = toIocMod hp a₁ b

Tactic:
(toIocMod_eq_toIocMod _).2 ⟨toIcoDiv hp a₂ b, self_sub_toIcoMod hp a₂ b⟩

Premises used: Iff.mpr, toIcoDiv, self_sub_toIcoMod, toIocMod_eq_toIocMod, Exists.intro
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ Function.Periodic (toIcoMod hp a) p

Tactic:
toIcoMod_add_right hp a

Premises used: toIcoMod_add_right, Function.Periodic
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ Function.Periodic (toIocMod hp a) p

Tactic:
toIocMod_add_right hp a

Premises used: toIocMod_add_right, Function.Periodic
-- 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 0 (-(b - a)) = p - toIocMod hp 0 (b - a)
rw₁ : p - toIocMod hp (-0) (b - a) = p - toIocMod hp 0 (b - a)
rw₂ rw₃ : p - toIocMod hp 0 (b - a) = p - toIocMod hp 0 (b - a)
⊢ toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)

Tactic:
rw [← neg_sub, toIcoMod_neg, neg_zero]

Premises used: neg_sub, toIcoMod_neg, neg_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 : α
rw : toIocMod hp 0 (-(b - a)) = p - toIcoMod hp 0 (b - a)
rw₁ : p - toIcoMod hp (-0) (b - a) = p - toIcoMod hp 0 (b - a)
rw₂ rw₃ : p - toIcoMod hp 0 (b - a) = p - toIcoMod hp 0 (b - a)
⊢ toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)

Tactic:
rw [← neg_sub, toIocMod_neg, neg_zero]

Premises used: neg_sub, toIocMod_neg, neg_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 : α
rw : toIcoDiv hp a b = toIcoDiv hp (0 + a) b
rw₁ rw₂ : toIcoDiv hp a b = toIcoDiv hp a b
⊢ toIcoDiv hp a b = toIcoDiv hp 0 (b - a)

Tactic:
rw [toIcoDiv_sub_eq_toIcoDiv_add, zero_add]

Premises used: toIcoDiv_sub_eq_toIcoDiv_add, zero_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 : toIocDiv hp a b = toIocDiv hp (0 + a) b
rw₁ rw₂ : toIocDiv hp a b = toIocDiv hp a b
⊢ toIocDiv hp a b = toIocDiv hp 0 (b - a)

Tactic:
rw [toIocDiv_sub_eq_toIocDiv_add, zero_add]

Premises used: toIocDiv_sub_eq_toIocDiv_add, zero_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 = toIcoMod hp (0 + a) b - a + a
rw₁ : toIcoMod hp a b = toIcoMod hp a b - a + a
rw₂ rw₃ : toIcoMod hp a b = toIcoMod hp a b
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a

Tactic:
rw [toIcoMod_sub_eq_sub, zero_add, sub_add_cancel]

Premises used: toIcoMod_sub_eq_sub, zero_add, 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 : toIocMod hp a b = toIocMod hp (0 + a) b - a + a
rw₁ : toIocMod hp a b = toIocMod hp a b - a + a
rw₂ rw₃ : toIocMod hp a b = toIocMod hp a b
⊢ toIocMod hp a b = toIocMod hp 0 (b - a) + a

Tactic:
rw [toIocMod_sub_eq_sub, zero_add, sub_add_cancel]

Premises used: toIocMod_sub_eq_sub, zero_add, 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 : p - toIocMod hp 0 (b - a) + toIocMod hp 0 (b - a) = p
rw₁ rw₂ : p = p
⊢ toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p

Tactic:
rw [toIcoMod_zero_sub_comm, sub_add_cancel]

Premises used: toIcoMod_zero_sub_comm, 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 0 (b - a) + toIocMod hp 0 (a - b) = p
rw₁ rw₂ : p = p
⊢ toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p

Tactic:
rw [_root_.add_comm, toIcoMod_add_toIocMod_zero]

Premises used: toIcoMod_add_toIocMod_zero, 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_1 b_1 c : α
n : ℤ
a : α
b : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
H :
  ∀ (z : α),
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      ((fun (x : (↑(Set.Ico a (a + p)) : Type u_1)) ↦
          ((↑(↑x : α) : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) :
            HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)))
        ((fun (b : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ico a (a + p)) (Function.Periodic.lift (f := toIcoMod hp a) ⋯ b) ⋯ :
              { x : α // x ∈ Set.Ico a (a + p) }))
          (↑z : α ⧸ AddSubgroup.zmultiples p)))
      (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ (fun (x : (↑(Set.Ico a (a + p)) : Type u_1)) ↦
        ((↑(↑x : α) : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) :
          HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)))
      ((fun (b : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ico a (a + p)) (Function.Periodic.lift (f := toIcoMod hp a) ⋯ b) ⋯ :
            { x : α // x ∈ Set.Ico a (a + p) }))
        b) =
    b

Tactic:
induction b using QuotientAddGroup.induction_on
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a_1 b c : α
n : ℤ
a z : α
H :
  Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑(toIcoMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    ((fun (x : (↑(Set.Ico a (a + p)) : Type u_1)) ↦
        ((↑(↑x : α) : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) :
          HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)))
      ((fun (b : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ico a (a + p)) (Function.Periodic.lift (f := toIcoMod hp a) ⋯ b) ⋯ :
            { x : α // x ∈ Set.Ico a (a + p) }))
        (↑z : α ⧸ AddSubgroup.zmultiples p)))
    (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a_1 b c : α
n : ℤ
a z : α
H : Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples p) (-toIcoDiv hp a z • p)
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑(toIcoMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
rw [QuotientAddGroup.eq_iff_sub_mem, toIcoMod_sub_self]

Premises used: QuotientAddGroup.eq_iff_sub_mem, toIcoMod_sub_self
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a_1 b c : α
n : ℤ
a z : α
⊢ Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples p) (-toIcoDiv hp a z • p)

Tactic:
apply AddSubgroup.zsmul_mem_zmultiples

Premises used: AddSubgroup.zsmul_mem_zmultiples
-- 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 : α
⊢ (equivIcoMod hp a : (a_1 : α ⧸ AddSubgroup.zmultiples p) → (↑(Set.Ico a (a + p)) : Type u_1))
      (↑b : α ⧸ AddSubgroup.zmultiples p) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ico a (a + p)) (toIcoMod hp a b) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, 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 : α
⊢ (equivIcoMod hp a : (a_1 : α ⧸ AddSubgroup.zmultiples p) → (↑(Set.Ico a (a + p)) : Type u_1)) 0 =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ico a (a + p)) (toIcoMod hp a 0) ⋯

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, 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_1 b_1 c : α
n : ℤ
a : α
b : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
H :
  ∀ (z : α),
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      ((fun (x : (↑(Set.Ioc a (a + p)) : Type u_1)) ↦
          ((↑(↑x : α) : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) :
            HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)))
        ((fun (b : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ioc a (a + p)) (Function.Periodic.lift (f := toIocMod hp a) ⋯ b) ⋯ :
              { x : α // x ∈ Set.Ioc a (a + p) }))
          (↑z : α ⧸ AddSubgroup.zmultiples p)))
      (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ (fun (x : (↑(Set.Ioc a (a + p)) : Type u_1)) ↦
        ((↑(↑x : α) : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) :
          HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)))
      ((fun (b : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ioc a (a + p)) (Function.Periodic.lift (f := toIocMod hp a) ⋯ b) ⋯ :
            { x : α // x ∈ Set.Ioc a (a + p) }))
        b) =
    b

Tactic:
induction b using QuotientAddGroup.induction_on