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_1 b c : α
n : ℤ
a z : α
H :
  Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑(toIocMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ 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)

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) (-toIocDiv hp a z • p)
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑(toIocMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
rw [QuotientAddGroup.eq_iff_sub_mem, toIocMod_sub_self]

Premises used: QuotientAddGroup.eq_iff_sub_mem, toIocMod_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) (-toIocDiv 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 : α
⊢ (equivIocMod hp a : (a_1 : α ⧸ AddSubgroup.zmultiples p) → (↑(Set.Ioc a (a + p)) : Type u_1))
      (↑b : α ⧸ AddSubgroup.zmultiples p) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ioc a (a + p)) (toIocMod hp a b) ⋯

Tactic:
rfl

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

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, 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
x₁ x₂ x₃ : α
rw : toIcoMod hp 0 (x₂ - x₁) + x₁ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
rw₁ :
  toIcoMod hp 0 (x₂ - x₁) + x₁ ≤ toIocMod hp 0 (x₃ - x₁) + x₁ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
rw₂ : toIcoMod hp 0 (x₂ - x₁) ≤ toIocMod hp 0 (x₃ - x₁) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
rw₃ : toIcoMod hp 0 (x₂ - x₁) ≤ toIocMod hp 0 (-(x₁ - x₃)) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
rw₄ : toIcoMod hp 0 (x₂ - x₁) ≤ p - toIcoMod hp (-0) (x₁ - x₃) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
rw₅ : toIcoMod hp 0 (x₂ - x₁) ≤ p - toIcoMod hp 0 (x₁ - x₃) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
rw₆ rw₇ : toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Tactic:
rw [toIcoMod_eq_sub, toIocMod_eq_sub _ x₁, add_le_add_iff_right, ← neg_sub x₁ x₃, toIocMod_neg,
    neg_zero, le_sub_iff_add_le]

Premises used: neg_sub, toIocMod_neg, toIcoMod_eq_sub, add_le_add_iff_right, toIocMod_eq_sub, le_sub_iff_add_le, 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
x₁ x₂ x₃ : α
h : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
⊢ x₂' ≤ toIocMod hp x₁ x₃'

Tactic:
simpa [x₃']
-- 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₃ : α
h : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
⊢ x₂' ≤ toIocMod hp x₁ x₃'

Tactic:
have h : x₂' ≤ toIocMod hp x₁ x₃' := by simpa [x₃']
-- 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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
⊢ x₂' < x₁ + p

Tactic:
have h₂₁ : x₂' < x₁ + p := toIcoMod_lt_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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
⊢ x₃' - p < x₂'

Tactic:
have h₃₂ : x₃' - p < x₂' := sub_lt_iff_lt_add.2 (toIcoMod_lt_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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
hequiv : x₃' ≤ toIocMod hp x₂' x₁
⊢ ∃ (z : ℤ), x₂ = x₂' + z • p

Tactic:
((toIcoMod_eq_iff hp).1 rfl).2

Premises used: toIcoMod_eq_iff, And.right, Iff.mp, rfl
-- 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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
hequiv : x₃' ≤ toIocMod hp x₂' x₁
obtain : ∀ (z : ℤ) (hd : x₂ = x₂' + z • p), toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
obtain ⟨z, hd⟩ : ∃ z : ℤ, x₂ = x₂' + z • p := ((toIcoMod_eq_iff hp).1 rfl).2

Premises used: toIcoMod_eq_iff, And.right, Iff.mp, rfl
-- 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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
hequiv : x₃' ≤ toIocMod hp x₂' x₁
z : ℤ
hd : x₂ = x₂' + z • p
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
simpa [hd, toIocMod_add_zsmul', toIcoMod_add_zsmul', add_le_add_iff_right]

Premises used: toIocMod_add_zsmul', add_le_add_iff_right, toIcoMod_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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
suffices : x₃' ≤ toIocMod hp x₂' x₁
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁

Tactic:
suffices hequiv : x₃' ≤ toIocMod hp x₂' x₁ by
    obtain ⟨z, hd⟩ : ∃ z : ℤ, x₂ = x₂' + z • p := ((toIcoMod_eq_iff hp).1 rfl).2
    simpa [hd, toIocMod_add_zsmul', toIcoMod_add_zsmul', add_le_add_iff_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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
inl : ∀ (h₃₁ : x₃' ≤ x₁ + p), x₃' ≤ toIocMod hp x₂' x₁
inr : ∀ (h₁₃ : x₁ + p < x₃'), x₃' ≤ toIocMod hp x₂' x₁
⊢ x₃' ≤ toIocMod hp x₂' x₁

Tactic:
rcases le_or_gt x₃' (x₁ + p) with h₃₁ | h₁₃

Premises used: le_or_gt, HAdd.hAdd
-- 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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
inl : toIocMod hp x₂' x₁ = x₁ + p
⊢ x₃' ≤ toIocMod hp x₂' x₁

Tactic:
suffices hIoc₂₁ : toIocMod hp x₂' x₁ = x₁ + p from hIoc₂₁.trans_ge 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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
inl : x₁ + p ∈ Set.Ioc x₂' (x₂' + p) ∧ ∃ (z : ℤ), x₁ = x₁ + p + z • p
⊢ toIocMod hp x₂' x₁ = x₁ + p

Tactic:
apply (toIocMod_eq_iff hp).2

Premises used: Iff.mpr, 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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ + p ≤ x₂' + p

Tactic:
simp [x₂', left_le_toIcoMod]

Premises used: left_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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ = x₁ + 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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ + p ∈ Set.Ioc x₂' (x₂' + p) ∧ ∃ (z : ℤ), x₁ = x₁ + p + z • p

Tactic:
exact ⟨⟨h₂₁, by simp [x₂', left_le_toIcoMod]⟩, -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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
apply : x₃' - p ∈ Set.Ioc x₁ (x₁ + p) ∧ ∃ (z : ℤ), x₃' = x₃' - p + z • p
⊢ toIocMod hp x₁ x₃' = x₃' - p

Tactic:
apply (toIocMod_eq_iff hp).2

Premises used: Iff.mpr, 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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
⊢ x₃' = x₃' - 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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
⊢ x₃' - p ∈ Set.Ioc x₁ (x₁ + p) ∧ ∃ (z : ℤ), x₃' = x₃' - p + z • p

Tactic:
exact ⟨⟨lt_sub_iff_add_lt.2 h₁₃, le_of_lt (h₃₂.trans h₂₁)⟩, 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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
⊢ toIocMod hp x₁ x₃' = x₃' - p

Tactic:
have hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p := by
    apply (toIocMod_eq_iff hp).2
    exact ⟨⟨lt_sub_iff_add_lt.2 h₁₃, le_of_lt (h₃₂.trans h₂₁)⟩, 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
x₁ x₂ x₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p
⊢ ¬x₃' - p < x₂'

Tactic:
have not_h₃₂ := (h.trans hIoc₁₃.le).not_gt
-- 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₃ : α
h_1 : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p
not_h₃₂ : ¬x₃' - p < x₂'
⊢ x₃' ≤ toIocMod hp x₂' x₁

Tactic:
contradiction
-- 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₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
by_contra! : ∀ (h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]), False
⊢ b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [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
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]

Tactic:
rw [modEq_comm] at h

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

Tactic:
rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.2.2] at h₁₂₃

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

Tactic:
rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.2.2] at h₁₂₃

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

Tactic:
rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.2.2] at h₁₂₃

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

Tactic:
rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.1] at h₁₃₂

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

Tactic:
rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.1] at h₁₃₂

Premises used: AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod, 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 c : α
h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIcoMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
h.2.1 ((toIcoMod_inj _).1 <| h₁₃₂.antisymm h₁₂₃)

Premises used: toIcoMod_inj, LE.le.antisymm, And.right, 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 c : α
h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIcoMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
exact h.2.1 ((toIcoMod_inj _).1 <| h₁₃₂.antisymm h₁₂₃)

Premises used: toIcoMod_inj, LE.le.antisymm, And.right, 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 c : α
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (x1 x2 : α) ↦ x1 + x2) (toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a))
      (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - c)))
    ((fun (x1 x2 : α) ↦ x1 + x2) p p)

Tactic:
have := congr_arg₂ (· + ·) (toIcoMod_add_toIocMod_zero hp a b) (toIcoMod_add_toIocMod_zero hp c 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 c : α
this :
  Eq.{u_1 + 1} (α := α)
    ((fun (x1 x2 : α) ↦ x1 + x2) (toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a))
      (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - c)))
    ((fun (x1 x2 : α) ↦ x1 + x2) p p)
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (c - b) + (toIocMod hp 0 (b - a) + toIocMod hp 0 (b - c)) = p + p

Tactic:
simp only [add_add_add_comm] at this

Premises used: add_add_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 : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (c - b) + (toIocMod hp 0 (b - a) + toIocMod hp 0 (b - c)) = p + p
⊢ toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) + (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) =
    HSMul.hSMul (α := ℕ) 2 p

Tactic:
rw [_root_.add_comm (toIocMod _ _ _), add_add_add_comm, ← two_nsmul] at this

Premises used: add_comm, toIocMod, add_add_add_comm, two_nsmul
-- 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 : α
this :
  toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) + (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) =
    HSMul.hSMul (α := ℕ) 2 p
⊢ min (toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c)) (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) ≤ p

Tactic:
replace := min_le_of_add_le_two_nsmul this.le
-- 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 : α
this : min (toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c)) (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p

Tactic:
rw [min_le_iff] at this

Premises used: min_le_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 : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p
rw : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a

Tactic:
rw [toIxxMod_iff, toIxxMod_iff]

Premises used: _private.0.toIxxMod_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 : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p

Tactic:
grw [← toIcoMod_le_toIocMod, ← toIcoMod_le_toIocMod] at this

Premises used: 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
a b c : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p

Tactic:
this
-- 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 : α
this : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p

Tactic:
exact this
-- 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 ≤ toIocMod hp a c ∨ toIcoMod hp c b ≤ toIocMod hp c a

Tactic:
(toIxxMod_total' _ _ _ _).imp_right <| toIxxMod_cyclic_left _

Premises used: _private.0.toIxxMod_cyclic_left, Or.imp_right, _private.0.toIxxMod_total'