Theorem: rectangle_in_convex (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ Rectangle z w ⊆ U
Tactic:
rw [Rectangle, segment_reProdIm_segment_eq_convexHull]
State after:
z✝ w✝ : ℂ
c : ℝ
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w} ⊆ U

State before:
z✝ w✝ : ℂ
c : ℝ
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w} ⊆ U
Tactic:
exact convexHull_min (by simp_all [insert_subset_iff]) U_convex
State after:
no goals

State before:
z✝ w✝ : ℂ
c : ℝ
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w} ⊆ U
Tactic:
simp_all [insert_subset_iff]
State after:
no goals