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 c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ x₄ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
h₂₃₄ : btw x₂ x₄ x₃ ∧ ¬btw x₃ x₄ x₂
z : α
h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ∧ ¬btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀ (z_1 : α) (h₂₃₄ : btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p))
  (h₁₂₃ :
    btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∧
      ¬btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)),
  btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₂ using QuotientAddGroup.induction_on
Cleared hypotheses: x₂, 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
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ x₄ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 : α
h₂₃₄ : btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
h₁₂₃ :
  btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∧
    ¬btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ x₃ ∧ ¬btw x₃ x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀ (z_2 : α)
  (h₂₃₄ :
    btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
      ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p))
  (h₁₂₃ :
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
      ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
          (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
          (↑z : α ⧸ AddSubgroup.zmultiples p)),
  btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₃ using QuotientAddGroup.induction_on
Cleared hypotheses: x₃, 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
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₄ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 z_2 : α
h₂₃₄ :
  btw (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (↑z_2 : α ⧸ AddSubgroup.zmultiples p) x₄ (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀ (z_3 : α)
  (h₂₃₄ :
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
      ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
          (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
          (↑z_1 : α ⧸ AddSubgroup.zmultiples p)),
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_3 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
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_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
z_3 : α
h₂₃₄ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
      (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p)
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_3 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∧
    ¬btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_3 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀
  (h₁₂₃ :
    toIcoMod (p := p) sorry z z_1 ≤ toIocMod (p := p) sorry z z_2 ∧ ¬toIcoMod (p := p) sorry z_2 z_1 ≤ toIocMod (p := p) sorry z_2 z)
  (h₂₃₄ :
    toIcoMod (p := p) sorry z_1 z_3 ≤ toIocMod (p := p) sorry z_1 z_2 ∧
      ¬toIcoMod (p := p) sorry z_2 z_3 ≤ toIocMod (p := p) sorry z_2 z_1),
  toIcoMod (p := p) sorry z z_3 ≤ toIocMod (p := p) sorry z z_2 ∧ ¬toIcoMod (p := p) sorry z_2 z_3 ≤ toIocMod (p := p) sorry z_2 z
Tactic: simp_rw [btw_coe_iff] 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 : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
h₁₂₃ : btw x₁ x₂ x₃
h₃₂₁ : btw x₃ x₂ x₁
⊢ x₁ = x₂ ∨ x₂ = x₃ ∨ x₃ = x₁
have H : ∀ (z : α) (h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃) (h₃₂₁ : btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)),
  (↑z : α ⧸ AddSubgroup.zmultiples p) = x₂ ∨ x₂ = x₃ ∨ x₃ = (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₁ using QuotientAddGroup.induction_on
Cleared hypotheses: x₁, 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
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z : α
h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃
h₃₂₁ : btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ (↑z : α ⧸ AddSubgroup.zmultiples p) = x₂ ∨ x₂ = x₃ ∨ x₃ = (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀ (z_1 : α) (h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃)
  (h₃₂₁ : btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)),
  Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) = x₃ ∨ x₃ = (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₂ using QuotientAddGroup.induction_on
Cleared hypotheses: x₂, 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
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 : α
h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃
h₃₂₁ : btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) = x₃ ∨ 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))
  (h₃₂₁ :
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)),
  Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
      Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₃ using QuotientAddGroup.induction_on
Cleared hypotheses: x₃, 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 : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p)
h₃₂₁ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
      Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have h₃₂₂ : btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
  (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
Tactic: rw [btw_cyclic] 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 : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p)
h₃₂₁ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
      Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have h₁₂₄ : toIcoMod (p := p) sorry z z_1 ≤ toIocMod (p := p) sorry z z_2
Tactic: simp_rw [btw_coe_iff] at h₁₂₃ 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 : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p)
h₃₂₁ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
h₁₂₄ : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
      Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have h₃₂₂ : toIcoMod (p := p) sorry z z_2 ≤ toIocMod (p := p) sorry z z_1
Tactic: simp_rw [btw_coe_iff] 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 : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2
h₃₂₁ : toIcoMod (p := p) ⋯ z z_2 ≤ toIocMod (p := p) ⋯ z z_1
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
      Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : z ≡ z_1 [PMOD p] ∨ z_1 ≡ z_2 [PMOD p] ∨ z_2 ≡ z [PMOD p]
Tactic: simp_rw [← modEq_iff_eq_mod_zmultiples]
-- 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)
⊢ btw x₁ x₂ x₃ ∨ btw x₃ x₂ x₁
have H : ∀ (z : α), btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ∨ btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₁ using QuotientAddGroup.induction_on
Cleared hypotheses: x₁
-- 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 : α
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ∨ btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀ (z_1 : α),
  btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∨
    btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₂ using QuotientAddGroup.induction_on
Cleared hypotheses: x₂
-- 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 : α
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∨
    btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : ∀ (z_2 : α),
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
Tactic: induction x₃ using QuotientAddGroup.induction_on
Cleared hypotheses: x₃
-- 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 : α
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
have H : toIcoMod (p := p) sorry z z_1 ≤ toIocMod (p := p) sorry z z_2 ∨ toIcoMod (p := p) sorry z_2 z_1 ≤ toIocMod (p := p) sorry z_2 z
Tactic: simp_rw [btw_coe_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ (↑(toIcoDiv hp a b) : R) * p + toIcoMod hp a b = b
have rw : toIcoMod hp a b + (↑(toIcoDiv hp a b) : R) * p = b
Tactic: rw [add_comm, toIcoMod_add_toIcoDiv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
rw : toIcoMod hp a b + (↑(toIcoDiv hp a b) : R) * p = b
⊢ (↑(toIcoDiv hp a b) : R) * p + toIcoMod hp a b = b
have rw₁ : b = b
Tactic: rw [add_comm, toIcoMod_add_toIcoDiv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ (↑(toIocDiv hp a b) : R) * p + toIocMod hp a b = b
have rw : toIocMod hp a b + (↑(toIocDiv hp a b) : R) * p = b
Tactic: rw [add_comm, toIocMod_add_toIocDiv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
rw : toIocMod hp a b + (↑(toIocDiv hp a b) : R) * p = b
⊢ (↑(toIocDiv hp a b) : R) * p + toIocMod hp a b = b
have rw₁ : b = b
Tactic: rw [add_comm, toIocMod_add_toIocDiv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIcoMod hp a b
have rw : toIcoMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_intCast_mul', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIcoMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIcoMod hp a b
⊢ toIcoMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIcoMod hp a b
have rw₁ : toIcoMod hp a b + (↑m : R) * p = (↑m : R) * p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_intCast_mul', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIcoMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIcoMod hp a b
rw₁ : toIcoMod hp a b + (↑m : R) * p = (↑m : R) * p + toIcoMod hp a b
⊢ toIcoMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIcoMod hp a b
have rw₂ : (↑m : R) * p + toIcoMod hp a b = (↑m : R) * p + toIcoMod hp a b
Tactic: rw [add_comm, toIcoMod_add_intCast_mul', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp a ((↑m : R) * p + b) = toIocMod hp a b
have rw : toIocMod hp a (b + (↑m : R) * p) = toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_intCast_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIocMod hp a (b + (↑m : R) * p) = toIocMod hp a b
⊢ toIocMod hp a ((↑m : R) * p + b) = toIocMod hp a b
have rw₁ : toIocMod hp a b = toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_intCast_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIocMod hp a b
have rw : toIocMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_intCast_mul', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIocMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIocMod hp a b
⊢ toIocMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIocMod hp a b
have rw₁ : toIocMod hp a b + (↑m : R) * p = (↑m : R) * p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_intCast_mul', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIocMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIocMod hp a b
rw₁ : toIocMod hp a b + (↑m : R) * p = (↑m : R) * p + toIocMod hp a b
⊢ toIocMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIocMod hp a b
have rw₂ : (↑m : R) * p + toIocMod hp a b = (↑m : R) * p + toIocMod hp a b
Tactic: rw [add_comm, toIocMod_add_intCast_mul', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv (p := p) hp a b = ⌊(b - a) / p⌋
have refine : b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)
Tactic: refine toIcoDiv_eq_of_sub_zsmul_mem_Ico hp ?_