awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
hp : p ≠ 0
inr :
  ∀ (y : ℝ),
    y ∈
        preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ↔
      Membership.mem (γ := Set ℝ) (⋃ (z : ℤ), closedBall (x + z • p) ε) y
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
      (closedBall (↑x : ℝ ⧸ zmultiples p) ε) =
    ⋃ (z : ℤ), closedBall (x + z • p) ε

Tactic:
ext y
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
inr : |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε ↔ ∃ (i : ℤ), |y - x - (↑i : ℝ) * p| ≤ ε
⊢ y ∈
      preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ↔
    Membership.mem (γ := Set ℝ) (⋃ (z : ℤ), closedBall (x + z • p) ε) y

Tactic:
simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs,
    ← QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]

Premises used: zsmul_eq_mul, dist_eq_norm, Set.mem_iUnion, QuotientAddGroup.mk_sub, sub_sub, Metric.mem_closedBall, AddCircle.norm_eq, Real.norm_eq_abs, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε ↔ ∃ (i : ℤ), |y - x - (↑i : ℝ) * p| ≤ ε

Tactic:
⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, ?_⟩

Premises used: HMul.hMul, HSub.hSub, Inv.inv, round, Iff.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
inr : (∃ (i : ℤ), |y - x - (↑i : ℝ) * p| ≤ ε) → |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε
⊢ |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε ↔ ∃ (i : ℤ), |y - x - (↑i : ℝ) * p| ≤ ε

Tactic:
refine ⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |y - x - (↑n : ℝ) * p| ≤ ε
inr : ∀ (hn : |p⁻¹ * (y - x) - (↑n : ℝ)| ≤ |p⁻¹| * ε), |p⁻¹ * (y - x) - (↑(round (p⁻¹ * (y - x))) : ℝ)| ≤ |p⁻¹| * ε
⊢ |y - x - (↑(round (p⁻¹ * (y - x))) : ℝ) * p| ≤ ε

Tactic:
rw [← mul_le_mul_iff_right₀ (abs_pos.mpr <| inv_ne_zero hp), ← abs_mul, mul_sub, mul_comm _ p,
    inv_mul_cancel_left₀ hp] at hn ⊢

Premises used: Iff.mpr, mul_sub, inv_mul_cancel_left₀, abs_mul, abs_pos, mul_comm, inv_ne_zero, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹ * (y - x) - (↑n : ℝ)| ≤ |p⁻¹| * ε
⊢ |p⁻¹ * (y - x) - (↑(round (p⁻¹ * (y - x))) : ℝ)| ≤ |p⁻¹| * ε

Tactic:
(round_le (p⁻¹ * (y - x)) n).trans hn

Premises used: HMul.hMul, HSub.hSub, round_le, Inv.inv, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹ * (y - x) - (↑n : ℝ)| ≤ |p⁻¹| * ε
⊢ |p⁻¹ * (y - x) - (↑(round (p⁻¹ * (y - x))) : ℝ)| ≤ |p⁻¹| * ε

Tactic:
exact (round_le (p⁻¹ * (y - x)) n).trans hn

Premises used: HMul.hMul, HSub.hSub, round_le, Inv.inv, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
inl :
  ∀ (hε : |p| / 2 ≤ ε),
    preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
        s =
      if ε < |p| / 2 then closedBall x ε ∩ s else s
inr :
  ∀ (hε : ε < |p| / 2),
    preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
        s =
      if ε < |p| / 2 then closedBall x ε ∩ s else s
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
rcases le_or_gt (|p| / 2) ε with hε | hε

Premises used: abs, HDiv.hDiv, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
inl :
  ∀ (hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)) (hε : HDiv.hDiv (α := ℝ) |0| 2 ≤ ε),
    preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ∩
        s =
      if ε < HDiv.hDiv (α := ℝ) |0| 2 then closedBall x ε ∩ s else s
inl₁ :
  ∀ (hp : p ≠ 0),
    preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
          (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
        s =
      if ε < |p| / 2 then closedBall x ε ∩ s else s
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)
hε : HDiv.hDiv (α := ℝ) |0| 2 ≤ ε
⊢ 0 ≤ ε

Tactic:
simp only [abs_zero, zero_div] at hε

Premises used: zero_div, abs_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)
hε : 0 ≤ ε
inl : s ⊆ closedBall x ε
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples 0)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples 0) ε) ∩
      s =
    if ε < HDiv.hDiv (α := ℝ) |0| 2 then closedBall x ε ∩ s else s

Tactic:
simp only [not_lt.mpr hε, coe_real_preimage_closedBall_period_zero, abs_zero, zero_div,
        if_false, inter_eq_right]

Premises used: Iff.mpr, if_false, zero_div, Set.inter_eq_right, abs_zero, not_lt, AddCircle.coe_real_preimage_closedBall_period_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)
hε : 0 ≤ ε
⊢ HDiv.hDiv (α := ℝ) |0| 2 ≤ ε

Tactic:
simp [hε]
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (HDiv.hDiv (α := ℝ) |0| 2)
hε : 0 ≤ ε
⊢ s ⊆ closedBall x ε

Tactic:
exact hs.trans (closedBall_subset_closedBall <| by simp [hε])

Premises used: HasSubset.Subset.trans, Metric.closedBall_subset_closedBall
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
hp : p ≠ 0
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
simp [closedBall_eq_univ_of_half_period_le p hp (↑x) hε, not_lt.mpr hε]

Premises used: Iff.mpr, QuotientAddGroup.mk, AddCircle.closedBall_eq_univ_of_half_period_le, not_lt
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
this : ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
simp [-zsmul_eq_mul, coe_real_preimage_closedBall_eq_iUnion,
        iUnion_inter, iUnion_ite, this, hε]

Premises used: zsmul_eq_mul, AddCircle.coe_real_preimage_closedBall_eq_iUnion, Set.iUnion_ite, Set.iUnion_inter
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
inr : ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
⊢ preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (zmultiples p)) QuotientAddGroup.mk
        (closedBall (↑x : ℝ ⧸ zmultiples p) ε) ∩
      s =
    if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
suffices ∀ z : ℤ, closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅ by
      simp [-zsmul_eq_mul, coe_real_preimage_closedBall_eq_iUnion,
        iUnion_inter, iUnion_ite, this, hε]
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
z : ℤ
inr :
  ∀ (hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)),
    Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅

Tactic:
simp only [Real.closedBall_eq_Icc] at hs ⊢

Premises used: Real.closedBall_eq_Icc
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
inr :
  Icc (x + HSMul.hSMul (α := ℤ) 0 p - ε) (x + HSMul.hSMul (α := ℤ) 0 p + ε) ∩ s =
    if Eq (α := ℤ) 0 0 then Icc (x - ε) (x + ε) ∩ s else ∅
inr₁ : ∀ (hz : z ≠ 0), Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅

Tactic:
rcases eq_or_ne z 0 with (rfl | hz)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
⊢ Icc (x + HSMul.hSMul (α := ℤ) 0 p - ε) (x + HSMul.hSMul (α := ℤ) 0 p + ε) ∩ s =
    if Eq (α := ℤ) 0 0 then Icc (x - ε) (x + ε) ∩ s else ∅

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
inr : ∀ (x_1 : ℝ), x_1 ∉ Icc (x + (↑z : ℝ) * p - ε) (x + (↑z : ℝ) * p + ε) ∩ s
⊢ Icc (x + z • p - ε) (x + z • p + ε) ∩ s = if z = 0 then Icc (x - ε) (x + ε) ∩ s else ∅

Tactic:
simp only [hz, zsmul_eq_mul, if_false, eq_empty_iff_forall_notMem]

Premises used: zsmul_eq_mul, if_false, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
⊢ x - |p| / 2 ≤ y

Tactic:
obtain ⟨hy₃, hy₄⟩ := hs hy₀
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
⊢ y ≤ x + |p| / 2

Tactic:
obtain ⟨hy₃, hy₄⟩ := hs hy₀
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
inr : ∀ (hp : 0 < p), False
inr₁ :
  ∀ (hε : ε < HDiv.hDiv (α := ℝ) |0| 2) (hs : s ⊆ Icc (x - HDiv.hDiv (α := ℝ) |0| 2) (x + HDiv.hDiv (α := ℝ) |0| 2))
    (hy₁ : x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 - ε ≤ y) (hy₂ : y ≤ x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 + ε)
    (hy₃ : x - HDiv.hDiv (α := ℝ) |0| 2 ≤ y) (hy₄ : y ≤ x + HDiv.hDiv (α := ℝ) |0| 2), False
inr₂ : ∀ (hp : p < 0), False
⊢ False

Tactic:
rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
inr : ∀ (hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)), False
inr₁ : ∀ (hz' : LE.le (α := ℝ) 1 (↑z : ℝ)), False
⊢ False

Tactic:
rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'

Premises used: Real, Int.cast_le_neg_one_or_one_le_cast_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)
nlinarith : -p < (↑z : ℝ) * p → 2 / 2 = 1
nlinarith₁ : -p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : -p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
nlinarith₃ : -p < (↑z : ℝ) * p → 2 / 2 = 1
nlinarith₄ : -p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : -p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
nlinarith₆ : -p < (↑z : ℝ) * p → 2 / 2 = 1
nlinarith₇ : -p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₈ : -p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
nlinarith₉ : -p < (↑z : ℝ) * p → -p - (↑z : ℝ) * p + (0 - (0 - p) * HSub.hSub (α := ℝ) (↑z : ℝ) (-1)) = 0
⊢ (↑z : ℝ) * p ≤ -p

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)
⊢ (↑z : ℝ) * p ≤ -p

Tactic:
have : ↑z * p ≤ -p := by nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)
this : (↑z : ℝ) * p ≤ -p
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 2 / 2 = 1
linarith₇ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : GT.gt (α := ℝ) 2 0
linarith₉ :
  2 * ε - 1 * |p| + 2 * (y - (x + (↑z : ℝ) * p + ε)) + (2 * x - 1 * |p| - 2 * y) + 2 * ((↑z : ℝ) * p - -p) +
      2 * (|p| - p) =
    0
linarith₁₀ linarith₁₁ linarith₁₂ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith [abs_eq_self.mpr hp.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : LE.le (α := ℝ) 1 (↑z : ℝ)
nlinarith : (↑z : ℝ) * p < p → 2 / 2 = 1
nlinarith₁ : (↑z : ℝ) * p < p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : (↑z : ℝ) * p < p → GT.gt (α := ℝ) 2 0
nlinarith₃ : (↑z : ℝ) * p < p → 2 / 2 = 1
nlinarith₄ : (↑z : ℝ) * p < p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : (↑z : ℝ) * p < p → GT.gt (α := ℝ) 2 0
nlinarith₆ : (↑z : ℝ) * p < p → 2 / 2 = 1
nlinarith₇ : (↑z : ℝ) * p < p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₈ : (↑z : ℝ) * p < p → GT.gt (α := ℝ) 2 0
nlinarith₉ : (↑z : ℝ) * p < p → (↑z : ℝ) * p - p + (0 - (0 - p) * HSub.hSub (α := ℝ) 1 (↑z : ℝ)) = 0
⊢ p ≤ (↑z : ℝ) * p

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : LE.le (α := ℝ) 1 (↑z : ℝ)
⊢ p ≤ (↑z : ℝ) * p

Tactic:
have : p ≤ ↑z * p := by nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : LE.le (α := ℝ) 1 (↑z : ℝ)
this : p ≤ (↑z : ℝ) * p
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 2 / 2 = 1
linarith₇ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : GT.gt (α := ℝ) 2 0
linarith₉ :
  2 * ε - 1 * |p| + 2 * (x + (↑z : ℝ) * p - ε - y) + (2 * y - (2 * x + 1 * |p|)) + 2 * (p - (↑z : ℝ) * p) +
      2 * (|p| - p) =
    0
linarith₁₀ linarith₁₁ linarith₁₂ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith [abs_eq_self.mpr hp.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hε : ε < HDiv.hDiv (α := ℝ) |0| 2
hs : s ⊆ Icc (x - HDiv.hDiv (α := ℝ) |0| 2) (x + HDiv.hDiv (α := ℝ) |0| 2)
hy₁ : x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 - ε ≤ y
hy₂ : y ≤ x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 + ε
hy₃ : x - HDiv.hDiv (α := ℝ) |0| 2 ≤ y
hy₄ : y ≤ x + HDiv.hDiv (α := ℝ) |0| 2
⊢ x - ε ≤ y

Tactic:
simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε

Premises used: zero_div, MulZeroClass.mul_zero, abs_zero, add_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hε : ε < HDiv.hDiv (α := ℝ) |0| 2
hs : s ⊆ Icc (x - HDiv.hDiv (α := ℝ) |0| 2) (x + HDiv.hDiv (α := ℝ) |0| 2)
hy₁ : x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 - ε ≤ y
hy₂ : y ≤ x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 + ε
hy₃ : x - HDiv.hDiv (α := ℝ) |0| 2 ≤ y
hy₄ : y ≤ x + HDiv.hDiv (α := ℝ) |0| 2
hy₅ : x - ε ≤ y
⊢ y ≤ x + ε

Tactic:
simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε

Premises used: zero_div, MulZeroClass.mul_zero, abs_zero, add_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hε : ε < HDiv.hDiv (α := ℝ) |0| 2
hs : s ⊆ Icc (x - HDiv.hDiv (α := ℝ) |0| 2) (x + HDiv.hDiv (α := ℝ) |0| 2)
hy₁ : x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 - ε ≤ y
hy₂ : y ≤ x + HMul.hMul (α := ℝ) (↑z : ℝ) 0 + ε
hy₃ : x - HDiv.hDiv (α := ℝ) |0| 2 ≤ y
hy₄ : y ≤ x + HDiv.hDiv (α := ℝ) |0| 2
hy₅ : x - ε ≤ y
hy₆ : y ≤ x + ε
⊢ ε < 0

Tactic:
simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε

Premises used: zero_div, MulZeroClass.mul_zero, abs_zero, add_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
x ε : ℝ
s : Set ℝ
z : ℤ
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hs : s ⊆ Icc (x - HDiv.hDiv (α := ℝ) |0| 2) (x + HDiv.hDiv (α := ℝ) |0| 2)
hy₃ : x - HDiv.hDiv (α := ℝ) |0| 2 ≤ y
hy₄ : y ≤ x + HDiv.hDiv (α := ℝ) |0| 2
hy₁ : x - ε ≤ y
hy₂ : y ≤ x + ε
hε : ε < 0
linarith : 1 * y - (1 * x + HMul.hMul (α := ℝ) 1 0) + (x - ε - y) + (ε - 0) = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
inr : ∀ (hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)), False
inr₁ : ∀ (hz' : LE.le (α := ℝ) 1 (↑z : ℝ)), False
⊢ False

Tactic:
rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'

Premises used: Real, Int.cast_le_neg_one_or_one_le_cast_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)
nlinarith : (↑z : ℝ) * p < -p → 2 / 2 = 1
nlinarith₁ : (↑z : ℝ) * p < -p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : (↑z : ℝ) * p < -p → GT.gt (α := ℝ) 2 0
nlinarith₃ : (↑z : ℝ) * p < -p → 2 / 2 = 1
nlinarith₄ : (↑z : ℝ) * p < -p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : (↑z : ℝ) * p < -p → GT.gt (α := ℝ) 2 0
nlinarith₆ : (↑z : ℝ) * p < -p → 2 / 2 = 1
nlinarith₇ : (↑z : ℝ) * p < -p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₈ : (↑z : ℝ) * p < -p → GT.gt (α := ℝ) 2 0
nlinarith₉ : (↑z : ℝ) * p < -p → (↑z : ℝ) * p - -p + (0 - (p - 0) * HSub.hSub (α := ℝ) (↑z : ℝ) (-1)) = 0
⊢ -p ≤ (↑z : ℝ) * p

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)
⊢ -p ≤ (↑z : ℝ) * p

Tactic:
have : -p ≤ ↑z * p := by nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)
this : -p ≤ (↑z : ℝ) * p
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 2 / 2 = 1
linarith₇ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : GT.gt (α := ℝ) 2 0
linarith₉ :
  2 * ε - 1 * |p| + 2 * (x + (↑z : ℝ) * p - ε - y) + (2 * y - (2 * x + 1 * |p|)) + 2 * (-p - (↑z : ℝ) * p) +
      2 * (|p| - -p) =
    0
linarith₁₀ linarith₁₁ linarith₁₂ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith [abs_eq_neg_self.mpr hp.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_neg_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : LE.le (α := ℝ) 1 (↑z : ℝ)
nlinarith : p < (↑z : ℝ) * p → 2 / 2 = 1
nlinarith₁ : p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
nlinarith₃ : p < (↑z : ℝ) * p → 2 / 2 = 1
nlinarith₄ : p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
nlinarith₆ : p < (↑z : ℝ) * p → 2 / 2 = 1
nlinarith₇ : p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₈ : p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
nlinarith₉ : p < (↑z : ℝ) * p → p - (↑z : ℝ) * p + (0 - (p - 0) * HSub.hSub (α := ℝ) 1 (↑z : ℝ)) = 0
⊢ (↑z : ℝ) * p ≤ p

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : LE.le (α := ℝ) 1 (↑z : ℝ)
⊢ (↑z : ℝ) * p ≤ p

Tactic:
have : ↑z * p ≤ p := by nlinarith
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + (↑z : ℝ) * p - ε ≤ y
hy₂ : y ≤ x + (↑z : ℝ) * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : LE.le (α := ℝ) 1 (↑z : ℝ)
this : (↑z : ℝ) * p ≤ p
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 2 / 2 = 1
linarith₇ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : GT.gt (α := ℝ) 2 0
linarith₉ :
  2 * ε - 1 * |p| + 2 * (y - (x + (↑z : ℝ) * p + ε)) + (2 * x - 1 * |p| - 2 * y) + 2 * ((↑z : ℝ) * p - p) +
      2 * (|p| - -p) =
    0
linarith₁₀ linarith₁₁ linarith₁₂ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith [abs_eq_neg_self.mpr hp.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_neg_self
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
rw : p⁻¹ * (p * HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
rw₁ rw₂ : HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
⊢ p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]

Premises used: inv_mul_cancel_left₀, Ne.symm, mul_comm, Fact.out, LT.lt.ne
-- Module: Mathlib.Analysis.Normed.Group.AddCircle
Goal:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ p⁻¹ * (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * p) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n := by rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]