Theorem: annulus_real_eq (Carleson/Theorem1_1/CarlesonOperatorReal.lean)

State before:
x r R : ℝ
r_nonneg : 0 ≤ r
⊢ {y | dist x y ∈ Set.Ioo r R} = Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)
Tactic:
ext y
State after:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo r R} ↔ y ∈ Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)

State before:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo r R} ↔ y ∈ Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)
Tactic:
simp
State after:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ r < dist x y ∧ dist x y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

State before:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ r < dist x y ∧ dist x y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
rw [Real.dist_eq, lt_abs, abs_lt]
State after:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

State before:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
constructor
State after:
case h.mp
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R → x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

State before:
case h.mp
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R → x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. rintro ⟨(h₀ | h₀), h₁, h₂⟩
  . left
    constructor <;> linarith
  . right
    constructor <;> linarith
State after:
case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

State before:
case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. rintro (⟨h₀, h₁⟩ | ⟨h₀, h₁⟩)
  . constructor
    . left
      linarith
    . constructor <;> linarith
  . constructor
    . right
      linarith
    . constructor <;> linarith
State after:
no goals

State before:
case h.mp
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R → x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
rintro ⟨(h₀ | h₀), h₁, h₂⟩
State after:
case h.mp.intro.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

State before:
case h.mp.intro.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
. left
  constructor <;> linarith
State after:
case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

State before:
case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
. right
  constructor <;> linarith
State after:
no goals

State before:
case h.mp.intro.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
left
State after:
case h.mp.intro.inl.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r

State before:
case h.mp.intro.inl.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r
Tactic:
constructor <;> linarith
State after:
no goals

State before:
case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
right
State after:
case h.mp.intro.inr.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x + r < y ∧ y < x + R

State before:
case h.mp.intro.inr.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x + r < y ∧ y < x + R
Tactic:
constructor <;> linarith
State after:
no goals

State before:
case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
rintro (⟨h₀, h₁⟩ | ⟨h₀, h₁⟩)
State after:
case h.mpr.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

State before:
case h.mpr.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. constructor
  . left
    linarith
  . constructor <;> linarith
State after:
case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

State before:
case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. constructor
  . right
    linarith
  . constructor <;> linarith
State after:
no goals

State before:
case h.mpr.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
constructor
State after:
case h.mpr.inl.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R

State before:
case h.mpr.inl.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Tactic:
. left
  linarith
State after:
case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R

State before:
case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Tactic:
. constructor <;> linarith
State after:
no goals

State before:
case h.mpr.inl.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y ∨ r < -(x - y)
Tactic:
left
State after:
case h.mpr.inl.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y

State before:
case h.mpr.inl.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y
Tactic:
linarith
State after:
no goals

State before:
case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Tactic:
constructor <;> linarith
State after:
no goals

State before:
case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
constructor
State after:
case h.mpr.inr.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R

State before:
case h.mpr.inr.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Tactic:
. right
  linarith
State after:
case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R

State before:
case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Tactic:
. constructor <;> linarith
State after:
no goals

State before:
case h.mpr.inr.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < x - y ∨ r < -(x - y)
Tactic:
right
State after:
case h.mpr.inr.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < -(x - y)

State before:
case h.mpr.inr.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < -(x - y)
Tactic:
linarith
State after:
no goals

State before:
case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Tactic:
constructor <;> linarith
State after:
no goals