Theorem: test_with_context (Ray/Tactic/BoundTests.lean)

State before:
s : Set ℂ
o : IsOpen s
z : ℂ
h : z ∈ s
⊢ ∃ r, r > 0
Tactic:
rw [Metric.isOpen_iff] at o
State after:
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
⊢ ∃ r, r > 0

State before:
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
⊢ ∃ r, r > 0
Tactic:
rcases o z h with ⟨t, tp, bs⟩
State after:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ ∃ r, r > 0

State before:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ ∃ r, r > 0
Tactic:
exists t/2
State after:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ t / 2 > 0

State before:
case intro.intro
s : Set ℂ
o : ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
z : ℂ
h : z ∈ s
t : ℝ
tp : t > 0
bs : Metric.ball z t ⊆ s
⊢ t / 2 > 0
Tactic:
clear o h bs z s
State after:
case intro.intro
t : ℝ
tp : t > 0
⊢ t / 2 > 0

State before:
case intro.intro
t : ℝ
tp : t > 0
⊢ t / 2 > 0
Tactic:
bound
State after:
no goals