Theorem: square.rp (Ray/Hartogs/FubiniBall.lean)

State before:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
⊢ x ∈ square r0 r1 → 0 < x.1
Tactic:
simp only [square, gt_iff_lt, not_lt, ge_iff_le, zero_lt_two, mul_pos_iff_of_pos_left,
  mem_prod, mem_Ioc, and_imp]
State after:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
⊢ r0 < x.1 → x.1 ≤ r1 → 0 < x.2 → x.2 ≤ 2 * π → 0 < x.1

State before:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
⊢ r0 < x.1 → x.1 ≤ r1 → 0 < x.2 → x.2 ≤ 2 * π → 0 < x.1
Tactic:
intro h _ _ _
State after:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
h : r0 < x.1
a✝² : x.1 ≤ r1
a✝¹ : 0 < x.2
a✝ : x.2 ≤ 2 * π
⊢ 0 < x.1

State before:
r0 r1 : ℝ
x : ℝ × ℝ
r0p : 0 ≤ r0
h : r0 < x.1
a✝² : x.1 ≤ r1
a✝¹ : 0 < x.2
a✝ : x.2 ≤ 2 * π
⊢ 0 < x.1
Tactic:
linarith
State after:
no goals