awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)
have rw : ∃ (z : ℤ), b = b + z • p
Tactic: rw [toIcoMod_eq_iff, and_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)
have rw : ∃ (z : ℤ), b = b + z • p
Tactic: rw [toIocMod_eq_iff, and_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)
have rw : toIcoMod hp 0 (-(b - a)) = p - toIocMod hp 0 (b - a)
Tactic: rw [← neg_sub, toIcoMod_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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)
⊢ toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)
have rw₁ : p - toIocMod hp (-0) (b - a) = p - toIocMod hp 0 (b - a)
Tactic: rw [← neg_sub, toIcoMod_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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)
⊢ toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a)
have rw₂ : p - toIocMod hp 0 (b - a) = p - toIocMod hp 0 (b - a)
Tactic: rw [← neg_sub, toIcoMod_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)
have rw : toIocMod hp 0 (-(b - a)) = p - toIcoMod hp 0 (b - a)
Tactic: rw [← neg_sub, toIocMod_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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)
⊢ toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)
have rw₁ : p - toIcoMod hp (-0) (b - a) = p - toIcoMod hp 0 (b - a)
Tactic: rw [← neg_sub, toIocMod_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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)
⊢ toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)
have rw₂ : p - toIcoMod hp 0 (b - a) = p - toIcoMod hp 0 (b - a)
Tactic: rw [← neg_sub, toIocMod_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b = toIcoDiv hp 0 (b - a)
have rw : toIcoDiv hp a b = toIcoDiv hp (0 + a) b
Tactic: rw [toIcoDiv_sub_eq_toIcoDiv_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoDiv hp a b = toIcoDiv hp 0 (b - a)
have rw₁ : toIcoDiv hp a b = toIcoDiv hp a b
Tactic: rw [toIcoDiv_sub_eq_toIcoDiv_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b = toIocDiv hp 0 (b - a)
have rw : toIocDiv hp a b = toIocDiv hp (0 + a) b
Tactic: rw [toIocDiv_sub_eq_toIocDiv_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIocDiv hp a b = toIocDiv hp 0 (b - a)
have rw₁ : toIocDiv hp a b = toIocDiv hp a b
Tactic: rw [toIocDiv_sub_eq_toIocDiv_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
have rw : toIcoMod hp a b = toIcoMod hp (0 + a) b - a + a
Tactic: rw [toIcoMod_sub_eq_sub, zero_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
have rw₁ : toIcoMod hp a b = toIcoMod hp a b - a + a
Tactic: rw [toIcoMod_sub_eq_sub, zero_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
have rw₂ : toIcoMod hp a b = toIcoMod hp a b
Tactic: rw [toIcoMod_sub_eq_sub, zero_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = toIocMod hp 0 (b - a) + a
have rw : toIocMod hp a b = toIocMod hp (0 + a) b - a + a
Tactic: rw [toIocMod_sub_eq_sub, zero_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIocMod hp a b = toIocMod hp 0 (b - a) + a
have rw₁ : toIocMod hp a b = toIocMod hp a b - a + a
Tactic: rw [toIocMod_sub_eq_sub, zero_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIocMod hp a b = toIocMod hp 0 (b - a) + a
have rw₂ : toIocMod hp a b = toIocMod hp a b
Tactic: rw [toIocMod_sub_eq_sub, zero_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p
have rw : p - toIocMod hp 0 (b - a) + toIocMod hp 0 (b - a) = p
Tactic: rw [toIcoMod_zero_sub_comm, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p
have rw₁ : p = p
Tactic: rw [toIcoMod_zero_sub_comm, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p
have rw : toIcoMod hp 0 (b - a) + toIocMod hp 0 (a - b) = p
Tactic: rw [_root_.add_comm, toIcoMod_add_toIocMod_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIocMod hp 0 (a - b) + toIcoMod hp 0 (b - a) = p
have rw₁ : p = p
Tactic: rw [_root_.add_comm, toIcoMod_add_toIocMod_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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)
⊢ (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
have 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) sorry b) sorry :
            { x : α // x ∈ Set.Ico a (a + p) }))
        (↑z : α ⧸ AddSubgroup.zmultiples p)))
    (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction b using QuotientAddGroup.induction_on
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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 : α
⊢ 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)
have H : Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
  (↑(toIcoMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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 : α
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑(toIcoMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples p) (-toIcoDiv hp a z • p)
Tactic: rw [QuotientAddGroup.eq_iff_sub_mem, toIcoMod_sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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)
⊢ (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
have 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) sorry b) sorry :
            { x : α // x ∈ Set.Ioc a (a + p) }))
        (↑z : α ⧸ AddSubgroup.zmultiples p)))
    (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction b using QuotientAddGroup.induction_on
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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 : α
⊢ 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)
have H : Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
  (↑(toIocMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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 : α
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑(toIocMod hp a z) : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : Membership.mem (γ := AddSubgroup α) (AddSubgroup.zmultiples p) (-toIocDiv hp a z • p)
Tactic: rw [QuotientAddGroup.eq_iff_sub_mem, toIocMod_sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
have rw : toIcoMod hp 0 (x₂ - 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
have rw₁ : toIcoMod hp 0 (x₂ - x₁) + x₁ ≤ toIocMod hp 0 (x₃ - 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
have rw₂ : toIcoMod hp 0 (x₂ - x₁) ≤ toIocMod hp 0 (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
have rw₃ : toIcoMod hp 0 (x₂ - x₁) ≤ toIocMod hp 0 (-(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]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
have rw₄ : toIcoMod hp 0 (x₂ - x₁) ≤ p - toIcoMod hp (-0) (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
have rw₅ : toIcoMod hp 0 (x₂ - x₁) ≤ p - toIcoMod hp 0 (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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
⊢ toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
have rw₆ : toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
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₃
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
have h₁ : x₂' ≤ toIocMod hp x₁ x₃'
Tactic: have h : x₂' ≤ toIocMod hp x₁ x₃' := by simpa [x₃']
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
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₃'
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
have h₂₁ : x₂' < x₁ + p
Tactic: have h₂₁ : x₂' < x₁ + p := toIcoMod_lt_right _ _ _
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (hypothesis)
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
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
have h₃₂ : x₃' - p < x₂'
Tactic: have h₃₂ : x₃' - p < x₂' := sub_lt_iff_lt_add.2 (toIcoMod_lt_right _ _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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₁
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
have obtain : ∀ (z : ℤ) (hd : x₂ = x₂' + z • p), toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
Tactic: obtain ⟨z, hd⟩ : ∃ z : ℤ, x₂ = x₂' + z • p := ((toIcoMod_eq_iff hp).1 rfl).2
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
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₂'
⊢ toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
have suffices : 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]