awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have inr : ∀ (hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)), False
Tactic: rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have inr₁ : ∀ (hz' : LE.le (α := ℝ) 1 (↑z : ℝ)), False
Tactic: rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
have nlinarith : -p < (↑z : ℝ) * p → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ (↑z : ℝ) * p ≤ -p
have nlinarith₁ : -p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ (↑z : ℝ) * p ≤ -p
have nlinarith₂ : -p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ (↑z : ℝ) * p ≤ -p
have nlinarith₉ : -p < (↑z : ℝ) * p → -p - (↑z : ℝ) * p + (0 - (0 - p) * HSub.hSub (α := ℝ) (↑z : ℝ) (-1)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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)
⊢ False
have this : (↑z : ℝ) * p ≤ -p
Tactic: have : ↑z * p ≤ -p := by nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₉ : 2 * ε - 1 * |p| + 2 * (y - (x + (↑z : ℝ) * p + ε)) + (2 * x - 1 * |p| - 2 * y) + 2 * ((↑z : ℝ) * p - -p) +
    2 * (|p| - p) =
  0
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
have nlinarith : (↑z : ℝ) * p < p → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p ≤ (↑z : ℝ) * p
have nlinarith₁ : (↑z : ℝ) * p < p → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p ≤ (↑z : ℝ) * p
have nlinarith₂ : (↑z : ℝ) * p < p → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ p ≤ (↑z : ℝ) * p
have nlinarith₉ : (↑z : ℝ) * p < p → (↑z : ℝ) * p - p + (0 - (0 - p) * HSub.hSub (α := ℝ) 1 (↑z : ℝ)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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 : ℝ)
⊢ False
have this : p ≤ (↑z : ℝ) * p
Tactic: have : p ≤ ↑z * p := by nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₉ : 2 * ε - 1 * |p| + 2 * (x + (↑z : ℝ) * p - ε - y) + (2 * y - (2 * x + 1 * |p|)) + 2 * (p - (↑z : ℝ) * p) +
    2 * (|p| - p) =
  0
Tactic: linarith [abs_eq_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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
⊢ False
have hy₅ : x - ε ≤ y
Tactic: simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε
Cleared hypotheses: hε, hy₁, hy₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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
⊢ False
have hy₆ : y ≤ x + ε
Tactic: simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε
Cleared hypotheses: hε, hy₁, hy₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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 + ε
⊢ False
have hε₁ : ε < 0
Tactic: simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε
Cleared hypotheses: hε, hy₁, hy₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith : 1 * y - (1 * x + HMul.hMul (α := ℝ) 1 0) + (x - ε - y) + (ε - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have inr : ∀ (hz' : LE.le (α := ℝ) (↑z : ℝ) (-1)), False
Tactic: rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have inr₁ : ∀ (hz' : LE.le (α := ℝ) 1 (↑z : ℝ)), False
Tactic: rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
have nlinarith : (↑z : ℝ) * p < -p → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ -p ≤ (↑z : ℝ) * p
have nlinarith₁ : (↑z : ℝ) * p < -p → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ -p ≤ (↑z : ℝ) * p
have nlinarith₂ : (↑z : ℝ) * p < -p → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ -p ≤ (↑z : ℝ) * p
have nlinarith₉ : (↑z : ℝ) * p < -p → (↑z : ℝ) * p - -p + (0 - (p - 0) * HSub.hSub (α := ℝ) (↑z : ℝ) (-1)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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)
⊢ False
have this : -p ≤ (↑z : ℝ) * p
Tactic: have : -p ≤ ↑z * p := by nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith [abs_eq_neg_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [abs_eq_neg_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith [abs_eq_neg_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₉ : 2 * ε - 1 * |p| + 2 * (x + (↑z : ℝ) * p - ε - y) + (2 * y - (2 * x + 1 * |p|)) + 2 * (-p - (↑z : ℝ) * p) +
    2 * (|p| - -p) =
  0
Tactic: linarith [abs_eq_neg_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
have nlinarith : p < (↑z : ℝ) * p → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ (↑z : ℝ) * p ≤ p
have nlinarith₁ : p < (↑z : ℝ) * p → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ (↑z : ℝ) * p ≤ p
have nlinarith₂ : p < (↑z : ℝ) * p → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ (↑z : ℝ) * p ≤ p
have nlinarith₉ : p < (↑z : ℝ) * p → p - (↑z : ℝ) * p + (0 - (p - 0) * HSub.hSub (α := ℝ) 1 (↑z : ℝ)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (hypothesis)
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 : ℝ)
⊢ False
have this : (↑z : ℝ) * p ≤ p
Tactic: have : ↑z * p ≤ p := by nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith [abs_eq_neg_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [abs_eq_neg_self.mpr hp.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.AddCircle (goal)
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
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith [abs_eq_neg_self.mpr hp.le]