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 : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
h_1 : toIcoMod hp a b = a
h : toIcoMod hp a b = a := h_1
| b
have rw : a + toIcoDiv hp a b • p
Tactic: rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
-- 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 : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
h_1 : toIcoMod hp a b = a
h : toIcoMod hp a b = a := h_1
⊢ b = a + toIcoDiv hp a b • p
have conv_lhs : b = a + toIcoDiv hp a b • p
Tactic: conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
-- 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 : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
h_1 : toIcoMod hp a b = a
h : toIcoMod hp a b = a := h_1
conv_lhs : b = a + toIcoDiv hp a b • p
⊢ b = a + toIcoDiv hp a b • p
have conv_lhs₁ : a + toIcoDiv hp a b • p = a + toIcoDiv hp a b • p
Tactic: conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
-- 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
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
⊢ [toIcoMod hp a b = a, ∀ (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
have tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
Tactic: tfae_have 1 → 4
  | h => by
    rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]
    refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
    rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]
    conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
-- 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 : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ ∀ (a_1 : ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)), toIcoMod hp a b = a
have rw : ¬toIcoMod hp a b = a → ∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)
Tactic: rw [← not_exists, not_imp_comm]
-- 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
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ ¬toIcoMod hp a b = a → ∃ (x : ℤ), b - x • p ∈ Set.Ioo a (a + p)
have h' : toIcoMod hp a b ∈ Set.Ico a (a + p)
Tactic: have h' := toIcoMod_mem_Ico hp a b
-- 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
a b : α
tfae_3_to_2 : ∀ (a_1 : toIcoMod hp a b ≠ toIocMod hp a b) (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : ∀ (a_1 : toIcoMod hp a b + p = toIocMod hp a b), toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : ∀ (a_1 : toIcoMod hp a b = a), toIcoMod hp a b + p = toIocMod hp a b
⊢ [toIcoMod hp a b = a, ∀ (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
have tfae_2_to_1 : ∀ (a_1 : ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)), toIcoMod hp a b = a
Tactic: tfae_have 2 → 1 := by
    rw [← not_exists, not_imp_comm]
    have h' := toIcoMod_mem_Ico hp a b
    exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩
-- 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 : α
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
have rw : toIcoMod hp a b = toIocMod hp a b ↔ 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]
-- 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 = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
have rw₁ : b - toIcoDiv hp a b • p = toIocMod hp a b ↔ 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]
-- 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 = 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
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
have rw₂ : b - toIcoDiv hp a b • p = b - toIocDiv hp a b • 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]
-- 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 = 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
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
have rw₃ : toIcoDiv hp a b • p = toIocDiv hp a b • 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]
-- 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 = 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
⊢ ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
have rw₄ : toIcoDiv hp a b = toIocDiv hp a b ↔ 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]
-- 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 : α
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw : toIcoMod hp a b + p = toIocMod hp a b ↔ 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]
-- 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 + p = toIocMod hp a b ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw₁ : b - toIcoDiv hp a b • p + p = toIocMod hp a b ↔ 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]
-- 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 + 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
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw₂ : b - toIcoDiv hp a b • p + p = b - toIocDiv hp a b • 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]
-- 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 + 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
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw₃ : b - toIcoDiv hp a b • p = b - toIocDiv hp a b • p - 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]
-- 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 + 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
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw₄ : b - toIcoDiv hp a b • p = b - (toIocDiv hp a b • p + 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]
-- 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 + 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
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw₅ : toIcoDiv hp a b • p = toIocDiv hp a b • p + 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]
-- 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 + 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
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw₆ : toIcoDiv hp a b • p = (toIocDiv hp a b + 1) • 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]
-- 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 + 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
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1
have rw₇ : toIcoDiv hp a b = toIocDiv hp a b + 1 ↔ 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]
-- 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 c : α
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]
have rw : (∃ (n : ℤ), b - a = n • p) ↔ a ≡ b [PMOD p]
Tactic: rw [toIcoMod_eq_toIcoMod, AddCommGroup.modEq_iff_zsmul']
-- 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 c : α
rw : (∃ (n : ℤ), b - a = n • p) ↔ a ≡ b [PMOD p]
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]
have rw₁ : (∃ (n : ℤ), b - a = n • p) ↔ ∃ (m : ℤ), b - a = m • p
Tactic: rw [toIcoMod_eq_toIcoMod, AddCommGroup.modEq_iff_zsmul']
-- 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 : α
⊢ Eq.{u_1 + 1} (α := Set α) {b : α | toIcoMod hp a b = toIocMod hp a b} (⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p))
have 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
Tactic: ext1
-- 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 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
have h : toIcoMod hp a x = toIocMod hp a 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]
-- 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 x : α
h : toIcoMod hp a x = toIocMod hp a x ↔ Membership.mem (γ := Set α) (⋃ (z : ℤ), Set.Ioo (a + z • p) (a + p + z • p)) 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
have h₁ : toIcoMod hp a x = toIocMod hp a x ↔ ∃ (i : ℤ), x ∈ Set.Ioo (a + i • p) (a + p + i • p)
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]
-- 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 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)
⊢ 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
have h₂ : toIcoMod hp a x = toIocMod hp a x ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
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]
-- 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 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)
⊢ 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
have h₃ : ¬a ≡ x [PMOD p] ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
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]
-- 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 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)
⊢ 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
have h₄ : (¬∀ (z : ℤ), x - z • p ∉ Set.Ioo a (a + p)) ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
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]
-- 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 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)
⊢ 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
have h₅ : (∃ (x_1 : ℤ), ¬x - x_1 • p ∉ Set.Ioo a (a + p)) ↔ ∃ (i : ℤ), x - i • p ∈ Set.Ioo a (a + p)
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]
-- 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 : α
this : 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
have rwa : 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]
-- 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 : α
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
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b
have rwa₁ : toIocDiv hp a b = toIcoDiv hp a b ∨ Order.succ (toIocDiv hp a b) = toIcoDiv hp a b
Tactic: rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]
-- 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 ⩿ toIcoDiv hp a b
have suffices : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = 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]
-- 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 = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
have rw : ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]
Tactic: rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ←
    modEq_iff_toIcoDiv_eq_toIocDiv_add_one]
-- 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 ≤ toIocMod hp a b
have rw : toIocDiv hp a b • p ≤ toIcoDiv hp a b • p
Tactic: rw [toIcoMod, toIocMod, sub_le_sub_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 ≤ toIcoMod hp a b + p
have rw : toIcoDiv hp a b ≤ toIocDiv hp a b + 1
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]