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
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₂'
⊢ x₃' ≤ toIocMod hp x₂' x₁
have inl : ∀ (h₃₁ : x₃' ≤ x₁ + p), x₃' ≤ toIocMod hp x₂' x₁
Tactic: rcases le_or_gt x₃' (x₁ + p) with h₃₁ | 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
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₁
⊢ x₃' ≤ toIocMod hp x₂' x₁
have inr : ∀ (h₁₃ : x₁ + p < x₃'), x₃' ≤ toIocMod hp x₂' x₁
Tactic: rcases le_or_gt x₃' (x₁ + p) with h₃₁ | 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
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₃' ≤ toIocMod hp x₂' x₁
have inl : toIocMod hp x₂' x₁ = x₁ + p
Tactic: suffices hIoc₂₁ : toIocMod hp x₂' x₁ = x₁ + p from hIoc₂₁.trans_ge 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
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
⊢ toIocMod hp x₂' x₁ = x₁ + p
have inl : x₁ + p ∈ Set.Ioc x₂' (x₂' + p) ∧ ∃ (z : ℤ), x₁ = x₁ + p + z • p
Tactic: apply (toIocMod_eq_iff hp).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₂'
h₁₃ : x₁ + p < x₃'
⊢ toIocMod hp x₁ x₃' = x₃' - p
have apply : x₃' - p ∈ Set.Ioc x₁ (x₁ + p) ∧ ∃ (z : ℤ), x₃' = x₃' - p + z • p
Tactic: apply (toIocMod_eq_iff hp).2
-- 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
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
⊢ x₃' ≤ toIocMod hp x₂' x₁
have hIoc₁₃ : 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⟩
-- 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
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p
⊢ x₃' ≤ toIocMod hp x₂' x₁
have not_h₃₂ : ¬x₃' - p < x₂'
Tactic: have not_h₃₂ := (h.trans hIoc₁₃.le).not_gt
-- 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 : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
⊢ b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p]
have by_contra! : ∀ (h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]), False
Tactic: by_contra! 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 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]
⊢ False
have h₁ : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
Tactic: rw [modEq_comm] at h
Cleared hypotheses: 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 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]
⊢ False
have h₁₂₄ : toIcoMod hp a b ≤ toIcoMod hp a c
Tactic: rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.2.2] at h₁₂₃
Cleared hypotheses: h₁₂₃, h₁₃₂, 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 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]
⊢ False
have h₁₃₃ : toIcoMod hp a c ≤ toIcoMod hp a b
Tactic: rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.1] at h₁₃₂
Cleared hypotheses: h₁₃₂, 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 c : α
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
have 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)
Tactic: have := congr_arg₂ (· + ·) (toIcoMod_add_toIocMod_zero hp a b) (toIcoMod_add_toIocMod_zero hp c 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 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 b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
have this₁ : 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
Cleared hypotheses: this
-- 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 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 b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
have 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
Tactic: rw [_root_.add_comm (toIocMod _ _ _), add_add_add_comm, ← two_nsmul] at this
Cleared hypotheses: this
-- 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 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
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
have this₁ : 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
Cleared hypotheses: this
-- 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 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 b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
have this₁ : 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
Cleared hypotheses: this
-- 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 : α
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 b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
have rw : toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
Tactic: rw [toIxxMod_iff, toIxxMod_iff]
-- 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₃ 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₂
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁
have left : toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃
Tactic: constructor
-- 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₃ 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₃
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁
have right : ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁
Tactic: constructor
-- 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₃ 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₃
have h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
Tactic: have h₁₂₃' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₁₂₃.1)
-- 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₃ 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₃
have h₂₃₄' : toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
Tactic: have h₂₃₄' := toIxxMod_cyclic_left _ (toIxxMod_cyclic_left _ h₂₃₄.1)
-- 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₃ 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₄
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃
have h₂₃₄'₁ : toIocMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
Tactic: rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'
Cleared hypotheses: 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
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₂
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃
have left : ¬x₃ ≡ x₂ [PMOD p]
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₂₃₄')
-- 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₃ 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]
⊢ False
have h₁₂₄ : 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₁₂₃
Cleared hypotheses: h₁₂₃, h₂₃₄, 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
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₂
⊢ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁
have 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₄
Tactic: rw [not_le] at h₁₂₃ h₂₃₄ ⊢
Cleared hypotheses: h₁₂₃, 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' : 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) ⋯ x₁ x₂ ≤ toIocMod (p := p) ⋯ x₁ x₃
have rw : toIcoMod (p := p) sorry 0 (x₂ - x₁) ≤ toIocMod (p := p) sorry 0 (x₃ - x₁) ↔
  toIcoMod (p := p) sorry x₁ x₂ ≤ toIocMod (p := p) sorry x₁ x₃
Tactic: rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_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' : 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₃
⊢ 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₃
have rw₁ : toIcoMod (p := p) sorry 0 (x₂ - x₁) ≤ toIocMod (p := p) sorry (0 + x₁) x₃ - x₁ ↔
  toIcoMod (p := p) sorry x₁ x₂ ≤ toIocMod (p := p) sorry x₁ x₃
Tactic: rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_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' : 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₃
⊢ 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₃
have rw₂ : toIcoMod (p := p) sorry (0 + x₁) x₂ - x₁ ≤ toIocMod (p := p) sorry (0 + x₁) x₃ - x₁ ↔
  toIcoMod (p := p) sorry x₁ x₂ ≤ toIocMod (p := p) sorry x₁ x₃
Tactic: rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_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' : 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₃
⊢ 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₃
have rw₃ : toIcoMod (p := p) sorry x₁ x₂ - x₁ ≤ toIocMod (p := p) sorry x₁ x₃ - x₁ ↔ toIcoMod (p := p) sorry x₁ x₂ ≤ toIocMod (p := p) sorry x₁ x₃
Tactic: rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_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' : 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₃
⊢ 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₃
have rw₄ : toIcoMod (p := p) sorry x₁ x₂ ≤ toIocMod (p := p) sorry x₁ x₃ ↔ toIcoMod (p := p) sorry x₁ x₂ ≤ toIocMod (p := p) sorry x₁ x₃
Tactic: rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_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
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₁
have H : ∀ (z : α) (h : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃), btw x₂ x₃ (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₁ using QuotientAddGroup.induction_on
Cleared hypotheses: x₁, 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 c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z : α
h : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃
⊢ btw x₂ x₃ (↑z : α ⧸ AddSubgroup.zmultiples p)
have 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)
Tactic: induction x₂ using QuotientAddGroup.induction_on
Cleared hypotheses: x₂, 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 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₃
⊢ btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ (↑z : α ⧸ AddSubgroup.zmultiples p)
have 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)
Tactic: induction x₃ using QuotientAddGroup.induction_on
Cleared hypotheses: x₃, 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 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_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀ (h : toIcoMod (p := p) sorry z z_1 ≤ toIocMod (p := p) sorry z z_2), toIcoMod (p := p) sorry z_1 z_2 ≤ toIocMod (p := p) sorry z_1 z
Tactic: simp_rw [btw_coe_iff] at h ⊢
Cleared hypotheses: 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 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₂
⊢ btw x₁ x₄ x₃ ∧ ¬btw x₃ x₄ x₁
have 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)
Tactic: induction x₁ using QuotientAddGroup.induction_on
Cleared hypotheses: x₁, h₁₂₃