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
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
left : toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃
right : ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
⊢ toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂

Tactic:
have h₁₂₃' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₁₂₃.1)
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
⊢ toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄

Tactic:
have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
h₂₃₄' : toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
⊢ toIocMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄

Tactic:
rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'

Premises used: AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod, 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
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
h₂₃₄' : toIocMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

Tactic:
toIxxMod_cyclic_left _ (h₁₂₃'.trans h₂₃₄')

Premises used: _private.0.toIxxMod_cyclic_left, LE.le.trans
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
h₂₃₄' : toIocMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

Tactic:
exact toIxxMod_cyclic_left _ (h₁₂₃'.trans h₂₃₄')

Premises used: _private.0.toIxxMod_cyclic_left, LE.le.trans
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
left : ¬x₃ ≡ x₂ [PMOD p]
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

Tactic:
suffices h : ¬x₃ ≡ x₂ [PMOD p] by
      have h₁₂₃' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₁₂₃.1)
      have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)
      rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'
      exact toIxxMod_cyclic_left _ (h₁₂₃'.trans h₂₃₄')
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
left : ∀ (h : x₃ ≡ x₂ [PMOD p]), False
⊢ ¬x₃ ≡ x₂ [PMOD p]

Tactic:
by_contra h
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁

Tactic:
rw [(modEq_iff_toIcoMod_eq_left hp).1 h] at h₁₂₃

Premises used: AddCommGroup.modEq_iff_toIcoMod_eq_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
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
h₁₂₄ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁
⊢ toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂

Tactic:
rw [(modEq_iff_toIcoMod_eq_left hp).1 h] at h₁₂₃

Premises used: AddCommGroup.modEq_iff_toIcoMod_eq_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
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
h₁₂₄ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁
h₂₃₅ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
⊢ x₃ ≡ x₂ [PMOD p]

Tactic:
rw [(modEq_iff_toIcoMod_eq_left hp).1 h] at h₁₂₃

Premises used: AddCommGroup.modEq_iff_toIcoMod_eq_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
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ False

Tactic:
h₁₂₃.2 (left_lt_toIocMod _ _ _).le

Premises used: left_lt_toIocMod, LT.lt.le, And.right
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬x₃ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : x₃ ≡ x₂ [PMOD p]
⊢ False

Tactic:
exact h₁₂₃.2 (left_lt_toIocMod _ _ _).le

Premises used: left_lt_toIocMod, LT.lt.le, And.right
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
right :
  ∀ (h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₂)
    (h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ toIocMod hp x₃ x₂ < toIcoMod hp x₃ x₄),
    toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₄
⊢ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁

Tactic:
rw [not_le] at h₁₂₃ h₂₃₄ ⊢

Premises used: not_le
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₂
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ toIocMod hp x₃ x₂ < toIcoMod hp x₃ x₄
⊢ toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₄

Tactic:
(h₁₂₃.2.trans_le (toIcoMod_le_toIocMod _ x₃ x₂)).trans h₂₃₄.2

Premises used: And.right, LT.lt.trans_le, LT.lt.trans, toIcoMod_le_toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₂
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ toIocMod hp x₃ x₂ < toIcoMod hp x₃ x₄
⊢ toIocMod hp x₃ x₁ < toIcoMod hp x₃ x₄

Tactic:
exact (h₁₂₃.2.trans_le (toIcoMod_le_toIocMod _ x₃ x₂)).trans h₂₃₄.2

Premises used: And.right, LT.lt.trans_le, LT.lt.trans, toIcoMod_le_toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑x₁ : α ⧸ AddSubgroup.zmultiples p)
      (↑x₂ : α ⧸ AddSubgroup.zmultiples p) (↑x₃ : α ⧸ AddSubgroup.zmultiples p) ↔
    toIcoMod (p := p) ⋯ 0 (x₂ - x₁) ≤ toIocMod (p := p) ⋯ 0 (x₃ - x₁)

Tactic:
Iff.rfl

Premises used: Quotient.liftOn', Iff.rfl, Function.Periodic.lift, toIocMod, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp' : Fact (0 < p)
x₁ x₂ x₃ : α
rw :
  toIcoMod (p := p) ⋯ 0 (x₂ - x₁) ≤ toIocMod (p := p) ⋯ 0 (x₃ - x₁) ↔
    toIcoMod (p := p) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃
rw₁ :
  toIcoMod (p := p) ⋯ 0 (x₂ - x₁) ≤ toIocMod (p := p) ⋯ (0 + x₁) x₃ - x₁ ↔
    toIcoMod (p := p) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃
rw₂ :
  toIcoMod (p := p) ⋯ (0 + x₁) x₂ - x₁ ≤ toIocMod (p := p) ⋯ (0 + x₁) x₃ - x₁ ↔
    toIcoMod (p := p) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃
rw₃ :
  toIcoMod (p := p) ⋯ x₁ x₂ - x₁ ≤ toIocMod (p := p) ⋯ x₁ x₃ - x₁ ↔
    toIcoMod (p := p) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃
rw₄ rw₅ : toIcoMod (p := p) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃ ↔ toIcoMod (p := p) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑x₁ : α ⧸ AddSubgroup.zmultiples p)
      (↑x₂ : α ⧸ AddSubgroup.zmultiples p) (↑x₃ : α ⧸ AddSubgroup.zmultiples p) ↔
    toIcoMod (p := p) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃

Tactic:
rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_right]

Premises used: toIcoMod_sub_eq_sub, toIocMod_sub_eq_sub, sub_le_sub_iff_right, zero_add, QuotientAddGroup.btw_coe_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 c : α
n : ℤ
hp' : Fact (0 < p)
x : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
⊢ LE.le.{u_1} (α := α)
    (↑((equivIcoMod ⋯ 0 : (a : α ⧸ AddSubgroup.zmultiples p) → (↑(Set.Ico 0 (0 + p)) : Type u_1)) (x - x)) : α)
    (↑((equivIocMod ⋯ 0 : (a : α ⧸ AddSubgroup.zmultiples p) → (↑(Set.Ioc 0 (0 + p)) : Type u_1)) (x - x)) : α)

Tactic:
simp [sub_self, hp'.out.le]

Premises used: sub_self, LT.lt.le, Fact.out
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
h : btw x₁ x₂ x₃
H : ∀ (z : α) (h : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃), btw x₂ x₃ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw x₂ x₃ x₁

Tactic:
induction x₁ 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 b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z : α
h : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃
H :
  ∀ (z_1 : α) (h : btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃),
    btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw x₂ x₃ (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₂ 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 b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 : α
h : btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃
H :
  ∀ (z_2 : α)
    (h :
      btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p)),
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₃ 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 b c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p)
H :
  ∀ (h : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2), toIcoMod (p := p) ⋯ z_1 z_2 ≤ toIocMod (p := p) ⋯ z_1 z
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
simp_rw [btw_coe_iff] at h ⊢

Premises used: QuotientAddGroup.btw_coe_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 c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2
⊢ toIcoMod (p := p) ⋯ z_1 z_2 ≤ toIocMod (p := p) ⋯ z_1 z

Tactic:
apply toIxxMod_cyclic_left _ h

Premises used: _private.0.toIxxMod_cyclic_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 c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ x₄ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
h₁₂₃ : btw x₁ x₂ x₃ ∧ ¬btw x₃ x₂ x₁
h₂₃₄ : btw x₂ x₄ x₃ ∧ ¬btw x₃ x₄ x₂
H :
  ∀ (z : α) (h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ∧ ¬btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)),
    btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw x₁ x₄ x₃ ∧ ¬btw x₃ x₄ x₁

Tactic:
induction x₁ 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 b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ x₄ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
h₂₃₄ : btw x₂ x₄ x₃ ∧ ¬btw x₃ x₄ x₂
z : α
h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ∧ ¬btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)
H :
  ∀ (z_1 : α)
    (h₂₃₄ : btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p))
    (h₁₂₃ :
      btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∧
        ¬btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)),
    btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₂ 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 b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ x₄ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 : α
h₂₃₄ : btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
h₁₂₃ :
  btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∧
    ¬btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
H :
  ∀ (z_2 : α)
    (h₂₃₄ :
      btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
        ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p))
    (h₁₂₃ :
      btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
          (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
          (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
        ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
            (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
            (↑z : α ⧸ AddSubgroup.zmultiples p)),
    btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
      ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₃ 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 b c : α
n : ℤ
hp' : Fact (0 < p)
x₄ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 z_2 : α
h₂₃₄ :
  btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
H :
  ∀ (z_3 : α)
    (h₂₃₄ :
      btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
          (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
          (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
        ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
            (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
            (↑z_1 : α ⧸ AddSubgroup.zmultiples p)),
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
      ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
          (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
          (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₄ 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 b c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
z_3 : α
h₂₃₄ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
      (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
H :
  ∀
    (h₁₂₃ :
      toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2 ∧ ¬toIcoMod (p := p) ⋯ z_2 z_1 ≤ toIocMod (p := p) ⋯ z_2 z)
    (h₂₃₄ :
      toIcoMod (p := p) ⋯ z_1 z_3 ≤ toIocMod (p := p) ⋯ z_1 z_2 ∧
        ¬toIcoMod (p := p) ⋯ z_2 z_3 ≤ toIocMod (p := p) ⋯ z_2 z_1),
    toIcoMod (p := p) ⋯ z z_3 ≤ toIocMod (p := p) ⋯ z z_2 ∧ ¬toIcoMod (p := p) ⋯ z_2 z_3 ≤ toIocMod (p := p) ⋯ z_2 z
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_3 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
simp_rw [btw_coe_iff] at h₁₂₃ h₂₃₄ ⊢

Premises used: QuotientAddGroup.btw_coe_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 c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 z_3 : α
h₁₂₃ : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2 ∧ ¬toIcoMod (p := p) ⋯ z_2 z_1 ≤ toIocMod (p := p) ⋯ z_2 z
h₂₃₄ :
  toIcoMod (p := p) ⋯ z_1 z_3 ≤ toIocMod (p := p) ⋯ z_1 z_2 ∧ ¬toIcoMod (p := p) ⋯ z_2 z_3 ≤ toIocMod (p := p) ⋯ z_2 z_1
⊢ toIcoMod (p := p) ⋯ z z_3 ≤ toIocMod (p := p) ⋯ z z_2 ∧ ¬toIcoMod (p := p) ⋯ z_2 z_3 ≤ toIocMod (p := p) ⋯ z_2 z

Tactic:
apply toIxxMod_trans _ h₁₂₃ h₂₃₄

Premises used: _private.0.toIxxMod_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 c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
h₁₂₃ : btw x₁ x₂ x₃
h₃₂₁ : btw x₃ x₂ x₁
H :
  ∀ (z : α) (h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃)
    (h₃₂₁ : btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)),
    (↑z : α ⧸ AddSubgroup.zmultiples p) = x₂ ∨ x₂ = x₃ ∨ x₃ = (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ x₁ = x₂ ∨ x₂ = x₃ ∨ x₃ = x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on