internlm/Lean-Github huggingface dataset:
Theorem: Square_apply
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Square p c = Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)
Tactic:
rw [Square, Rectangle, uIcc_of_le (by simp; linarith), uIcc_of_le (by simp; linarith)]
Proof state after:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Icc (-↑c - ↑c * I + p).re (↑c + ↑c * I + p).re ×ℂ Icc (-↑c - ↑c * I + p).im (↑c + ↑c * I + p).im =
    Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)
Theorem: Square_apply
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Icc (-↑c - ↑c * I + p).re (↑c + ↑c * I + p).re ×ℂ Icc (-↑c - ↑c * I + p).im (↑c + ↑c * I + p).im =
    Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)
Tactic:
simp
Proof state after:
no goals
Theorem: Square_apply
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ (-↑c - ↑c * I + p).re ≤ (↑c + ↑c * I + p).re
Tactic:
simp
Proof state after:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ 0 ≤ c
Theorem: Square_apply
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ 0 ≤ c
Tactic:
linarith
Proof state after:
no goals
Theorem: Square_apply
Proof state before:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ (-↑c - ↑c * I + p).im ≤ (↑c + ↑c * I + p).im
Tactic:
simp
Proof state after:
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ 0 ≤ c
Theorem: reProdIm_subset_iff
Proof state before:
z w : ℂ
c : ℝ
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
Tactic:
simp_rw [← preimage_equivRealProd_prod, equivRealProd.preimage_subset]
Proof state after:
no goals
Theorem: segment_reProdIm_segment_eq_convexHull
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] = (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Tactic:
simp_rw [← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm, reProdIm]
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ (convexHull ℝ) (re ⁻¹' {z.re, w.re} ∩ im ⁻¹' {z.im, w.im}) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Theorem: segment_reProdIm_segment_eq_convexHull
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ (convexHull ℝ) (re ⁻¹' {z.re, w.re} ∩ im ⁻¹' {z.im, w.im}) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Tactic:
exact congrArg _ <| Set.ext <| by simpa [Complex.ext_iff] using by tauto
Proof state after:
no goals
Theorem: segment_reProdIm_segment_eq_convexHull
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ ∀ (x : ℂ), x ∈ re ⁻¹' {z.re, w.re} ∩ im ⁻¹' {z.im, w.im} ↔ x ∈ {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Tactic:
simpa [Complex.ext_iff] using by tauto
Proof state after:
no goals
Theorem: segment_reProdIm_segment_eq_convexHull
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ ∀ (x : ℂ),
    (x.re = z.re ∨ x.re = w.re) ∧ (x.im = z.im ∨ x.im = w.im) ↔
      x.re = z.re ∧ x.im = z.im ∨ x.re = z.re ∧ x.im = w.im ∨ x.re = w.re ∧ x.im = z.im ∨ x.re = w.re ∧ x.im = w.im
Tactic:
tauto
Proof state after:
no goals
Theorem: rectangle_in_convex
Proof 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]
Proof 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
Theorem: rectangle_in_convex
Proof 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
Proof state after:
no goals
Theorem: rectangle_in_convex
Proof 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]
Proof state after:
no goals
Theorem: mem_Rect
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
p : ℂ
⊢ p ∈ Rectangle z w ↔ z.re ≤ p.re ∧ p.re ≤ w.re ∧ z.im ≤ p.im ∧ p.im ≤ w.im
Tactic:
rw [Rectangle, uIcc_of_le zRe_lt_wRe, uIcc_of_le zIm_lt_wIm]
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
p : ℂ
⊢ p ∈ Icc z.re w.re ×ℂ Icc z.im w.im ↔ z.re ≤ p.re ∧ p.re ≤ w.re ∧ z.im ≤ p.im ∧ p.im ≤ w.im
Theorem: mem_Rect
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
zRe_lt_wRe : z.re ≤ w.re
zIm_lt_wIm : z.im ≤ w.im
p : ℂ
⊢ p ∈ Icc z.re w.re ×ℂ Icc z.im w.im ↔ z.re ≤ p.re ∧ p.re ≤ w.re ∧ z.im ≤ p.im ∧ p.im ≤ w.im
Tactic:
exact and_assoc
Proof state after:
no goals
Theorem: square_neg
Proof state before:
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
⊢ Square p (-c) = Square p c
Tactic:
simpa [Square] using Rectangle.symm
Proof state after:
no goals
Theorem: uIoo_of_le
Proof state before:
z w : ℂ
c : ℝ
α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ uIoo a b = Ioo a b
Tactic:
rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
Proof state after:
no goals
Theorem: rect_subset_iff
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
⊢ Rectangle z' w' ⊆ Rectangle z w ↔ z' ∈ Rectangle z w ∧ w' ∈ Rectangle z w
Tactic:
use fun h ↦ ⟨h (left_mem_rect z' w'), h (right_mem_rect z' w')⟩
Proof state after:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
⊢ z' ∈ Rectangle z w ∧ w' ∈ Rectangle z w → Rectangle z' w' ⊆ Rectangle z w
Theorem: rect_subset_iff
Proof state before:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
⊢ z' ∈ Rectangle z w ∧ w' ∈ Rectangle z w → Rectangle z' w' ⊆ Rectangle z w
Tactic:
intro ⟨⟨⟨hz're_ge, hz're_le⟩, ⟨hz'im_ge, hz'im_le⟩⟩,
  ⟨⟨hw're_ge, hw're_le⟩, ⟨hw'im_ge, hw'im_le⟩⟩⟩ x ⟨⟨hxre_ge, hxre_le⟩, ⟨hxim_ge, hxim_le⟩⟩
Proof state after:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x ∈ Rectangle z w
Theorem: rect_subset_iff
Proof state before:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x ∈ Rectangle z w
Tactic:
refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩
Proof state after:
case mpr.refine_1
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.re ⊓ w.re ≤ x.re

case mpr.refine_2
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.re ≤ z.re ⊔ w.re

case mpr.refine_3
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.im ⊓ w.im ≤ x.im

case mpr.refine_4
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.im ≤ z.im ⊔ w.im
Theorem: rect_subset_iff
Proof state before:
case mpr.refine_1
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.re ⊓ w.re ≤ x.re
Tactic:
exact (le_inf hz're_ge hw're_ge).trans hxre_ge
Proof state after:
no goals
Theorem: rect_subset_iff
Proof state before:
case mpr.refine_2
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.re ≤ z.re ⊔ w.re
Tactic:
exact (le_sup_iff.mp hxre_le).casesOn (fun h ↦ h.trans hz're_le) (fun h ↦ h.trans hw're_le)
Proof state after:
no goals
Theorem: rect_subset_iff
Proof state before:
case mpr.refine_3
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.im ⊓ w.im ≤ x.im
Tactic:
exact (le_inf hz'im_ge hw'im_ge).trans hxim_ge
Proof state after:
no goals
Theorem: rect_subset_iff
Proof state before:
case mpr.refine_4
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.im ≤ z.im ⊔ w.im
Tactic:
exact (le_sup_iff.mp hxim_le).casesOn (fun h ↦ h.trans hz'im_le) (fun h ↦ h.trans hw'im_le)
Proof state after:
no goals
Theorem: RectSubRect
Proof state before:
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ Rectangle (↑x₁ + ↑y₁ * I) (↑x₂ + ↑y₂ * I) ⊆ Rectangle (↑x₀ + ↑y₀ * I) (↑x₃ + ↑y₃ * I)
Tactic:
rw [rect_subset_iff, mem_Rect, mem_Rect]
Proof state after:
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ ((↑x₀ + ↑y₀ * I).re ≤ (↑x₁ + ↑y₁ * I).re ∧
      (↑x₁ + ↑y₁ * I).re ≤ (↑x₃ + ↑y₃ * I).re ∧
        (↑x₀ + ↑y₀ * I).im ≤ (↑x₁ + ↑y₁ * I).im ∧ (↑x₁ + ↑y₁ * I).im ≤ (↑x₃ + ↑y₃ * I).im) ∧
    (↑x₀ + ↑y₀ * I).re ≤ (↑x₂ + ↑y₂ * I).re ∧
      (↑x₂ + ↑y₂ * I).re ≤ (↑x₃ + ↑y₃ * I).re ∧
        (↑x₀ + ↑y₀ * I).im ≤ (↑x₂ + ↑y₂ * I).im ∧ (↑x₂ + ↑y₂ * I).im ≤ (↑x₃ + ↑y₃ * I).im

case zRe_lt_wRe
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im

case zRe_lt_wRe
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im
Theorem: RectSubRect
Proof state before:
case refine_1
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₁ + ↑y₁ * I).re

case refine_2
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₁ + ↑y₁ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case refine_3
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₁ + ↑y₁ * I).im

case refine_4
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₁ + ↑y₁ * I).im ≤ (↑x₃ + ↑y₃ * I).im

case refine_5
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₂ + ↑y₂ * I).re

case refine_6
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₂ + ↑y₂ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case refine_7
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₂ + ↑y₂ * I).im

case refine_8
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₂ + ↑y₂ * I).im ≤ (↑x₃ + ↑y₃ * I).im

case zRe_lt_wRe
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im

case zRe_lt_wRe
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im
Tactic:
all_goals simpa using by linarith
Proof state after:
no goals
Theorem: RectSubRect
Proof state before:
case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im
Tactic:
simpa using by linarith
Proof state after:
no goals
Theorem: RectSubRect
Proof state before:
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ y₀ ≤ y₃
Tactic:
linarith
Proof state after:
no goals
Theorem: RectSubRect'
Proof state before:
z w : ℂ
c : ℝ
z₀ z₁ z₂ z₃ : ℂ
x₀_le_x₁ : z₀.re ≤ z₁.re
x₁_le_x₂ : z₁.re ≤ z₂.re
x₂_le_x₃ : z₂.re ≤ z₃.re
y₀_le_y₁ : z₀.im ≤ z₁.im
y₁_le_y₂ : z₁.im ≤ z₂.im
y₂_le_y₃ : z₂.im ≤ z₃.im
⊢ Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃
Tactic:
rw [← re_add_im z₀, ← re_add_im z₁, ← re_add_im z₂, ← re_add_im z₃]
Proof state after:
z w : ℂ
c : ℝ
z₀ z₁ z₂ z₃ : ℂ
x₀_le_x₁ : z₀.re ≤ z₁.re
x₁_le_x₂ : z₁.re ≤ z₂.re
x₂_le_x₃ : z₂.re ≤ z₃.re
y₀_le_y₁ : z₀.im ≤ z₁.im
y₁_le_y₂ : z₁.im ≤ z₂.im
y₂_le_y₃ : z₂.im ≤ z₃.im
⊢ Rectangle (↑z₁.re + ↑z₁.im * I) (↑z₂.re + ↑z₂.im * I) ⊆ Rectangle (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₃.im * I)
Theorem: RectSubRect'
Proof state before:
z w : ℂ
c : ℝ
z₀ z₁ z₂ z₃ : ℂ
x₀_le_x₁ : z₀.re ≤ z₁.re
x₁_le_x₂ : z₁.re ≤ z₂.re
x₂_le_x₃ : z₂.re ≤ z₃.re
y₀_le_y₁ : z₀.im ≤ z₁.im
y₁_le_y₂ : z₁.im ≤ z₂.im
y₂_le_y₃ : z₂.im ≤ z₃.im
⊢ Rectangle (↑z₁.re + ↑z₁.im * I) (↑z₂.re + ↑z₂.im * I) ⊆ Rectangle (↑z₀.re + ↑z₀.im * I) (↑z₃.re + ↑z₃.im * I)
Tactic:
exact RectSubRect x₀_le_x₁ x₁_le_x₂ x₂_le_x₃ y₀_le_y₁ y₁_le_y₂ y₂_le_y₃
Proof state after:
no goals
Theorem: rectangleBorder_subset_rectangle
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ RectangleBorder z w ⊆ Rectangle z w
Tactic:
intro x hx
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
hx : x ∈ RectangleBorder z w
⊢ x ∈ Rectangle z w
Theorem: rectangleBorder_subset_rectangle
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
hx : x ∈ RectangleBorder z w
⊢ x ∈ Rectangle z w
Tactic:
obtain ⟨⟨h | h⟩ | h⟩ | h := hx
Proof state after:
case inl.inl.inl
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {z.im}
⊢ x ∈ Rectangle z w

case inl.inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {z.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w

case inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {w.im}
⊢ x ∈ Rectangle z w

case inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {w.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w
Theorem: rectangleBorder_subset_rectangle
Proof state before:
case inl.inl.inl
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {z.im}
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1, h.2 ▸ left_mem_uIcc⟩
Proof state after:
no goals
Theorem: rectangleBorder_subset_rectangle
Proof state before:
case inl.inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {z.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1 ▸ left_mem_uIcc, h.2⟩
Proof state after:
no goals
Theorem: rectangleBorder_subset_rectangle
Proof state before:
case inl.inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ [[z.re, w.re]] ×ℂ {w.im}
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1, h.2 ▸ right_mem_uIcc⟩
Proof state after:
no goals
Theorem: rectangleBorder_subset_rectangle
Proof state before:
case inr
z✝ w✝ : ℂ
c : ℝ
z w x : ℂ
h : x ∈ {w.re} ×ℂ [[z.im, w.im]]
⊢ x ∈ Rectangle z w
Tactic:
exact ⟨h.1 ▸ right_mem_uIcc, h.2⟩
Proof state after:
no goals
Theorem: rectangle_disjoint_singleton
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re < z.re ∧ p.re < w.re ∨ p.im < z.im ∧ p.im < w.im ∨ z.re < p.re ∧ w.re < p.re ∨ z.im < p.im ∧ w.im < p.im
⊢ Disjoint (Rectangle z w) {p}
Tactic:
refine disjoint_singleton_right.mpr (not_and_or.mpr ?_)
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re < z.re ∧ p.re < w.re ∨ p.im < z.im ∧ p.im < w.im ∨ z.re < p.re ∧ w.re < p.re ∨ z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Theorem: rectangle_disjoint_singleton
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re < z.re ∧ p.re < w.re ∨ p.im < z.im ∧ p.im < w.im ∨ z.re < p.re ∧ w.re < p.re ∨ z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
obtain h | h | h | h := h
Proof state after:
case inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re < z.re ∧ p.re < w.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]

case inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.im < z.im ∧ p.im < w.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]

case inr.inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.re < p.re ∧ w.re < p.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]

case inr.inr.inr
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Theorem: rectangle_disjoint_singleton
Proof state before:
case inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re < z.re ∧ p.re < w.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inl (not_mem_uIcc_of_lt h.1 h.2)
Proof state after:
no goals
Theorem: rectangle_disjoint_singleton
Proof state before:
case inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.im < z.im ∧ p.im < w.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inr (not_mem_uIcc_of_lt h.1 h.2)
Proof state after:
no goals
Theorem: rectangle_disjoint_singleton
Proof state before:
case inr.inr.inl
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.re < p.re ∧ w.re < p.re
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inl (not_mem_uIcc_of_gt h.1 h.2)
Proof state after:
no goals
Theorem: rectangle_disjoint_singleton
Proof state before:
case inr.inr.inr
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : z.im < p.im ∧ w.im < p.im
⊢ p ∉ re ⁻¹' [[z.re, w.re]] ∨ p ∉ im ⁻¹' [[z.im, w.im]]
Tactic:
exact Or.inr (not_mem_uIcc_of_gt h.1 h.2)
Proof state after:
no goals
Theorem: rectangleBorder_disjoint_singleton
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ Disjoint (RectangleBorder z w) {p}
Tactic:
refine disjoint_singleton_right.mpr ?_
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ p ∉ RectangleBorder z w
Theorem: rectangleBorder_disjoint_singleton
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ p ∉ RectangleBorder z w
Tactic:
simp_rw [RectangleBorder, Set.mem_union, not_or]
Proof state after:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ ((p ∉ [[z.re, w.re]] ×ℂ {z.im} ∧ p ∉ {z.re} ×ℂ [[z.im, w.im]]) ∧ p ∉ [[z.re, w.re]] ×ℂ {w.im}) ∧
    p ∉ {w.re} ×ℂ [[z.im, w.im]]
Theorem: rectangleBorder_disjoint_singleton
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ ((p ∉ [[z.re, w.re]] ×ℂ {z.im} ∧ p ∉ {z.re} ×ℂ [[z.im, w.im]]) ∧ p ∉ [[z.re, w.re]] ×ℂ {w.im}) ∧
    p ∉ {w.re} ×ℂ [[z.im, w.im]]
Tactic:
exact ⟨⟨⟨fun hc ↦ h.2.2.1 hc.2, fun hc ↦ h.1 hc.1⟩, fun hc ↦ h.2.2.2 hc.2⟩, fun hc ↦ h.2.1 hc.1⟩
Proof state after:
no goals
Theorem: rectangle_subset_punctured_rect
Proof state before:
z w : ℂ
c : ℝ
z₀ z₁ z₂ z₃ p : ℂ
hz : z₀.re ≤ z₁.re ∧ z₁.re ≤ z₂.re ∧ z₂.re ≤ z₃.re ∧ z₀.im ≤ z₁.im ∧ z₁.im ≤ z₂.im ∧ z₂.im ≤ z₃.im
hp :
  p.re < z₁.re ∧ p.re < z₂.re ∨ p.im < z₁.im ∧ p.im < z₂.im ∨ z₁.re < p.re ∧ z₂.re < p.re ∨ z₁.im < p.im ∧ z₂.im < p.im
⊢ Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃
Tactic:
apply RectSubRect' <;> tauto
Proof state after:
no goals
Theorem: rectangleBorder_subset_punctured_rect
Proof state before:
z w : ℂ
c : ℝ
z₀ z₁ z₂ z₃ p : ℂ
hz : z₀.re ≤ z₁.re ∧ z₁.re ≤ z₂.re ∧ z₂.re ≤ z₃.re ∧ z₀.im ≤ z₁.im ∧ z₁.im ≤ z₂.im ∧ z₂.im ≤ z₃.im
hp : p.re ≠ z₁.re ∧ p.re ≠ z₂.re ∧ p.im ≠ z₁.im ∧ p.im ≠ z₂.im
⊢ Rectangle z₁ z₂ ⊆ Rectangle z₀ z₃
Tactic:
apply RectSubRect' <;> tauto
Proof state after:
no goals
Theorem: rectangle_mem_nhds_iff
Proof state before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
⊢ Rectangle z w ∈ 𝓝 p ↔ p ∈ uIoo z.re w.re ×ℂ uIoo z.im w.im
Tactic:
simp_rw [← mem_interior_iff_mem_nhds, Rectangle, Complex.interior_reProdIm, uIoo, uIcc, interior_Icc]
Proof state after:
no goals
Theorem: horizontalSegment_eq
Proof state before:
z w : ℂ
c a₁ a₂ b : ℝ
x✝² : ℂ
hx✝ : x✝² ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[a₁, a₂]] ∧ (fun x => ↑x + ↑b * I) x✝¹ = x✝²
left✝ : x✝¹ ∈ [[a₁, a₂]]
hx : (fun x => ↑x + ↑b * I) x✝¹ = x✝²
⊢ x✝² ∈ [[a₁, a₂]] ×ℂ {b}
Tactic:
simpa [← hx, reProdIm]
Proof state after:
no goals
Theorem: horizontalSegment_eq
Proof state before:
z w : ℂ
c a₁ a₂ b : ℝ
x✝ : ℂ
hx : x✝ ∈ [[a₁, a₂]] ×ℂ {b}
⊢ x✝ ∈ re ⁻¹' [[a₁, a₂]] → x✝ ∈ im ⁻¹' {b} → x✝ ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]
Tactic:
simp_all [Complex.ext_iff]
Proof state after:
no goals
Theorem: verticalSegment_eq
Proof state before:
z w : ℂ
c a b₁ b₂ : ℝ
x✝² : ℂ
hx✝ : x✝² ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]] ∧ (fun y => ↑a + ↑y * I) x✝¹ = x✝²
left✝ : x✝¹ ∈ [[b₁, b₂]]
hx : (fun y => ↑a + ↑y * I) x✝¹ = x✝²
⊢ x✝² ∈ {a} ×ℂ [[b₁, b₂]]
Tactic:
simpa [← hx, reProdIm]
Proof state after:
no goals
Theorem: verticalSegment_eq
Proof state before:
z w : ℂ
c a b₁ b₂ : ℝ
x✝ : ℂ
hx : x✝ ∈ {a} ×ℂ [[b₁, b₂]]
⊢ x✝ ∈ re ⁻¹' {a} → x✝ ∈ im ⁻¹' [[b₁, b₂]] → x✝ ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]
Tactic:
simp_all [Complex.ext_iff]
Proof state after:
no goals