[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
[PROOFSTEP]
obtain rfl | hr := hr.eq_or_lt
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ log b 1 = -↑(Nat.clog b ⌈1⁻¹⌉₊)
[PROOFSTEP]
rw [log, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right, Int.ofNat_zero,
  neg_zero]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
[PROOFSTEP]
exact if_neg hr.not_le
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ log b ↑n = ↑(Nat.log b n)
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b ↑Nat.zero = ↑(Nat.log b Nat.zero)
[PROOFSTEP]
simp [log_of_right_le_one]
[GOAL]
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(Nat.succ n✝) = ↑(Nat.log b (Nat.succ n✝))
[PROOFSTEP]
rw [log_of_one_le_right, Nat.floor_coe]
[GOAL]
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ log b r = 0
[PROOFSTEP]
cases' le_total 1 r with h h
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ log b r = 0
[PROOFSTEP]
rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, Int.ofNat_zero]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0
[PROOFSTEP]
rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ log b r = 0
[PROOFSTEP]
rw [log_of_right_le_one _ (hr.trans zero_le_one),
  Nat.clog_of_right_le_one ((Nat.ceil_eq_zero.mpr <| inv_nonpos.2 hr).trans_le zero_le_one), Int.ofNat_zero, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ log b r ≤ r
[PROOFSTEP]
cases' le_total 1 r with hr1 hr1
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ log b r ≤ r
[PROOFSTEP]
rw [log_of_one_le_right _ hr1]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ ↑(Nat.log b ⌊r⌋₊) ≤ r
[PROOFSTEP]
rw [zpow_ofNat, ← Nat.cast_pow, ← Nat.le_floor_iff hr.le]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ b ^ Nat.log b ⌊r⌋₊ ≤ ⌊r⌋₊
[PROOFSTEP]
exact Nat.pow_log_le_self b (Nat.floor_pos.mpr hr1).ne'
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ ↑b ^ log b r ≤ r
[PROOFSTEP]
rw [log_of_right_le_one _ hr1, zpow_neg, zpow_ofNat, ← Nat.cast_pow]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (↑(b ^ Nat.clog b ⌈r⁻¹⌉₊))⁻¹ ≤ r
[PROOFSTEP]
exact inv_le_of_inv_le hr (Nat.ceil_le.1 <| Nat.le_pow_clog hb _)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
cases' le_or_lt r 0 with hr hr
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
rw [log_of_right_le_zero _ hr, zero_add, zpow_one]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b
[PROOFSTEP]
exact hr.trans_lt (zero_lt_one.trans_le <| by exact_mod_cast hb.le)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ 1 ≤ ↑b
[PROOFSTEP]
exact_mod_cast hb.le
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
cases' le_or_lt 1 r with hr1 hr1
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
rw [log_of_one_le_right _ hr1]
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑b ^ (↑(Nat.log b ⌊r⌋₊) + 1)
[PROOFSTEP]
rw [Int.ofNat_add_one_out, zpow_ofNat, ← Nat.cast_pow]
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ r < ↑(b ^ Nat.succ (Nat.log b ⌊r⌋₊))
[PROOFSTEP]
apply Nat.lt_of_floor_lt
[GOAL]
case inr.inl.h
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : 1 ≤ r
⊢ ⌊r⌋₊ < b ^ Nat.succ (Nat.log b ⌊r⌋₊)
[PROOFSTEP]
exact Nat.lt_pow_succ_log_self hb _
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (log b r + 1)
[PROOFSTEP]
rw [log_of_right_le_one _ hr1.le]
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
[PROOFSTEP]
have hcri : 1 < r⁻¹ := one_lt_inv hr hr1
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
[PROOFSTEP]
have : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊ :=
  Nat.succ_le_of_lt (Nat.clog_pos hb <| Nat.one_lt_cast.1 <| hcri.trans_le (Nat.le_ceil _))
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊) + 1)
[PROOFSTEP]
rw [neg_add_eq_sub, ← neg_sub, ← Int.ofNat_one, ← Int.ofNat_sub this, zpow_neg, zpow_ofNat,
  lt_inv hr (pow_pos (Nat.cast_pos.mpr <| zero_lt_one.trans hb) _), ← Nat.cast_pow]
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ ↑(b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1)) < r⁻¹
[PROOFSTEP]
refine' Nat.lt_ceil.1 _
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ b ^ (Nat.clog b ⌈r⁻¹⌉₊ - 1) < ⌈r⁻¹⌉₊
[PROOFSTEP]
exact Nat.pow_pred_clog_lt_self hb <| Nat.one_lt_cast.1 <| hcri.trans_le <| Nat.le_ceil _
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b 1 = 0
[PROOFSTEP]
rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ log b (↑b ^ z) = z
[PROOFSTEP]
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
[GOAL]
case intro.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ ↑n) = ↑n
[PROOFSTEP]
rw [log_of_one_le_right _ (one_le_zpow_of_nonneg _ <| Int.coe_nat_nonneg _), zpow_ofNat, ← Nat.cast_pow, Nat.floor_coe,
  Nat.log_pow hb]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
[PROOFSTEP]
exact_mod_cast hb.le
[GOAL]
case intro.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n
[PROOFSTEP]
rw [log_of_right_le_one _ (zpow_le_one_of_nonpos _ <| neg_nonpos.mpr (Int.coe_nat_nonneg _)), zpow_neg, inv_inv,
  zpow_ofNat, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ 1 ≤ ↑b
[PROOFSTEP]
exact_mod_cast hb.le
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : b ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_left_le_one hb, log_of_left_le_one hb]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_total r₁ 1 with h₁ h₁
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_total r₂ 1 with h₂ h₂
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
cases' le_total r₂ 1 with h₂ h₂
[GOAL]
case inr.inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Int.ofNat_le]
[GOAL]
case inr.inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊
[PROOFSTEP]
exact Nat.clog_mono_right _ (Nat.ceil_mono <| inv_le_inv_of_le h₀ h)
[GOAL]
case inr.inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_right_le_one _ h₁, log_of_one_le_right _ h₂]
[GOAL]
case inr.inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : r₁ ≤ 1
h₂ : 1 ≤ r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ ↑(Nat.log b ⌊r₂⌋₊)
[PROOFSTEP]
exact (neg_nonpos.mpr (Int.coe_nat_nonneg _)).trans (Int.coe_nat_nonneg _)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
obtain rfl := le_antisymm h (h₂.trans h₁)
[GOAL]
case inr.inr.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ : R
h₀ : 0 < r₁
hb : 1 < b
h₁ : 1 ≤ r₁
h : r₁ ≤ r₁
h₂ : r₁ ≤ 1
⊢ log b r₁ ≤ log b r₁
[PROOFSTEP]
rfl
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
[PROOFSTEP]
rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Int.ofNat_le]
[GOAL]
case inr.inr.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
hb : 1 < b
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ Nat.log b ⌊r₁⌋₊ ≤ Nat.log b ⌊r₂⌋₊
[PROOFSTEP]
exact Nat.log_mono_right (Nat.floor_mono h)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ 0 < ↑b
[PROOFSTEP]
exact_mod_cast zero_lt_one.trans hb
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z₁ z₂ : ℤ
hz : z₁ ≤ z₂
⊢ 1 < ↑b
[PROOFSTEP]
exact_mod_cast hb
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)
[PROOFSTEP]
obtain rfl | hr := hr.eq_or_lt
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ clog b 1 = -↑(Nat.log b ⌊1⁻¹⌋₊)
[PROOFSTEP]
rw [clog, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right, Int.ofNat_zero,
  neg_zero]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)
[PROOFSTEP]
exact if_neg hr.not_le
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ clog b r = 0
[PROOFSTEP]
rw [clog, if_neg (hr.trans_lt zero_lt_one).not_le, neg_eq_zero, Int.coe_nat_eq_zero, Nat.log_eq_zero_iff]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
[PROOFSTEP]
exact Or.inr hb
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
[PROOFSTEP]
refine' Or.inl (lt_of_le_of_lt _ hb)
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1
[PROOFSTEP]
exact Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
cases' lt_or_le 0 r with hrp hrp
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
obtain hr | hr := le_total 1 r
[GOAL]
case inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
rw [clog_of_right_le_one _ (inv_le_one hr), log_of_one_le_right _ hr, inv_inv]
[GOAL]
case inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
rw [clog_of_one_le_right _ (one_le_inv hrp hr), log_of_right_le_one _ hr, neg_neg]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r
[PROOFSTEP]
rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ log b r⁻¹ = -clog b r
[PROOFSTEP]
rw [← inv_inv r, clog_inv, neg_neg, inv_inv]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ -log b r⁻¹ = clog b r
[PROOFSTEP]
rw [log_inv, neg_neg]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ -clog b r⁻¹ = log b r
[PROOFSTEP]
rw [clog_inv, neg_neg]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑n = ↑(Nat.clog b n)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b ↑Nat.zero = ↑(Nat.clog b Nat.zero)
[PROOFSTEP]
simp [clog_of_right_le_one]
[GOAL]
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑(Nat.succ n) = ↑(Nat.clog b (Nat.succ n))
[PROOFSTEP]
rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr]
[GOAL]
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ ↑(Nat.succ n - 1) < ↑(Nat.succ n) ∧ ↑(Nat.succ n) ≤ ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ 1 ≤ ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ clog b r = 0
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, neg_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
⊢ r ≤ ↑b ^ clog b r
[PROOFSTEP]
cases' le_or_lt r 0 with hr hr
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ ↑b ^ clog b r
[PROOFSTEP]
rw [clog_of_right_le_zero _ hr, zpow_zero]
[GOAL]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ 1
[PROOFSTEP]
exact hr.trans zero_le_one
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r ≤ ↑b ^ clog b r
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, zpow_neg, le_inv hr (zpow_pos_of_pos _ _)]
[GOAL]
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ ↑b ^ log b r⁻¹ ≤ r⁻¹
[PROOFSTEP]
exact zpow_log_le_self hb (inv_pos.mpr hr)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ 0 < ↑b
[PROOFSTEP]
exact Nat.cast_pos.mpr (zero_le_one.trans_lt hb)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ (clog b r - 1) < r
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt _ hr]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < ↑b ^ (log b r⁻¹ + 1)
[PROOFSTEP]
exact lt_zpow_succ_log_self hb _
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)
[PROOFSTEP]
exact zpow_pos_of_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b 1 = 0
[PROOFSTEP]
rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_one_right, Int.ofNat_zero]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ clog b (↑b ^ z) = z
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ clog b r₁ ≤ clog b r₂
[PROOFSTEP]
rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹
[PROOFSTEP]
exact log_mono_right (inv_pos.mpr <| h₀.trans_le h) (inv_le_inv_of_le h₀ h)
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ 0 < ↑b
[PROOFSTEP]
exact_mod_cast zero_lt_one.trans hb
[GOAL]
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z₁ z₂ : ℤ
hz : z₁ ≤ z₂
⊢ 1 < ↑b
[PROOFSTEP]
exact_mod_cast hb


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a < x ∧ x < b)
⊢ Decidable (x ∈ Ioo a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a ≤ x ∧ x < b)
⊢ Decidable (x ∈ Ico a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (x < b)
⊢ Decidable (x ∈ Iio b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a ≤ x ∧ x ≤ b)
⊢ Decidable (x ∈ Icc a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (x ≤ b)
⊢ Decidable (x ∈ Iic b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a < x ∧ x ≤ b)
⊢ Decidable (x ∈ Ioc a b)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a ≤ x)
⊢ Decidable (x ∈ Ici a)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : Decidable (a < x)
⊢ Decidable (x ∈ Ioi a)
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ioo a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ico a b ↔ a < b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ioc a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ici a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ioo a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ico a b ↔ False
[PROOFSTEP]
simp [lt_irrefl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Icc a b ↔ a ≤ b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ioc a b ↔ a < b
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Iic a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Icc a b = ∅ ↔ ¬a ≤ b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Icc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ico a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ico]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ioc a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioo]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a✝ b c a : α
⊢ ∀ (x : α), x ∈ Icc a a ↔ x ∈ {a}
[PROOFSTEP]
simp [Icc, le_antisymm_iff, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c
[PROOFSTEP]
have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c
[PROOFSTEP]
exact ⟨eq_of_mem_singleton <| h.subst <| left_mem_Icc.2 hab, eq_of_mem_singleton <| h.subst <| right_mem_Icc.2 hab⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case refine'_2.intro
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}
[PROOFSTEP]
exact Icc_self _
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
⊢ Set.Subsingleton (Icc a b) ↔ b ≤ a
[PROOFSTEP]
refine' ⟨fun h ↦ _, subsingleton_Icc_of_ge⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : Set.Subsingleton (Icc a b)
⊢ b ≤ a
[PROOFSTEP]
contrapose! h
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ¬Set.Subsingleton (Icc a b)
[PROOFSTEP]
simp only [ge_iff_le, gt_iff_lt, not_subsingleton_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α✝
a✝ b✝ c : α✝
α : Type u_3
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ Set.Nontrivial (Icc a b)
[PROOFSTEP]
exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Icc a b \ {a} ↔ x ∈ Ioc a b
[PROOFSTEP]
simp [lt_iff_le_and_ne, eq_comm, and_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Icc a b \ {b} ↔ x ∈ Ico a b
[PROOFSTEP]
simp [lt_iff_le_and_ne, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ico a b \ {a} ↔ x ∈ Ioo a b
[PROOFSTEP]
simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ioc a b \ {b} ↔ x ∈ Ioo a b
[PROOFSTEP]
simp [and_assoc, ← lt_iff_le_and_ne]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Icc a b \ {a, b} = Ioo a b
[PROOFSTEP]
rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ici a \ {a} ↔ x ∈ Ioi a
[PROOFSTEP]
simp [lt_iff_le_and_ne, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Iic a \ {a} ↔ x ∈ Iio a
[PROOFSTEP]
simp [lt_iff_le_and_ne]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ Ico a b \ Ioo a b = {a}
[PROOFSTEP]
rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}
[PROOFSTEP]
rw [← Ioc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Ioc.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}
[PROOFSTEP]
rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ Icc a b \ Ioc a b = {a}
[PROOFSTEP]
rw [← Icc_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Icc.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}
[PROOFSTEP]
rw [← Icc_diff_both, diff_diff_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b
[PROOFSTEP]
simp [insert_subset_iff, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Ici a \ Ioi a = {a}
[PROOFSTEP]
rw [← Ici_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 left_mem_Ici)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ Iic a \ Iio a = {a}
[PROOFSTEP]
rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 right_mem_Iic)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c x : α
⊢ x ∈ Ioi a ∪ {a} ↔ x ∈ Ici a
[PROOFSTEP]
simp [eq_comm, le_iff_eq_or_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a < b
⊢ Ioo a b ∪ {a} = Ico a b
[PROOFSTEP]
rw [← Ico_diff_left, diff_union_self, union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a < b
⊢ Ioo a b ∪ {b} = Ioc a b
[PROOFSTEP]
simpa only [dual_Ioo, dual_Ico] using Ioo_union_left hab.dual
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
⊢ Ioc a b ∪ {a} = Icc a b
[PROOFSTEP]
rw [← Icc_diff_left, diff_union_self, union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
⊢ Ico a b ∪ {b} = Icc a b
[PROOFSTEP]
simpa only [dual_Ioc, dual_Icc] using Ioc_union_left hab.dual
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ico_union_right h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ioc_union_left h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ insert a (Ioo a b) = Ico a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ioo_union_left h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b
[PROOFSTEP]
rw [insert_eq, union_comm, Ioo_union_right h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioi a ⊆ s
hc : s ⊆ Ici a
h : a ∈ s
⊢ Ici a ⊆ s
[PROOFSTEP]
rw [← Ioi_union_left, union_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioi a ⊆ s
hc : s ⊆ Ici a
h : a ∈ s
⊢ Ioi a ⊆ s ∧ {a} ⊆ s
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
classical
by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
· refine' Or.inl (Subset.antisymm hc _)
  rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right, diff_singleton_subset_iff,
    insert_eq_of_mem hb] at ho
· refine' Or.inr <| Or.inl <| Subset.antisymm _ _
  · rw [← Icc_diff_right]
    exact subset_diff_singleton hc hb
  · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
· refine' Or.inr <| Or.inr <| Or.inl <| Subset.antisymm _ _
  · rw [← Icc_diff_left]
    exact subset_diff_singleton hc ha
  · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
· refine' Or.inr <| Or.inr <| Or.inr <| Subset.antisymm _ ho
  rw [← Ico_diff_left, ← Icc_diff_right]
  apply_rules [subset_diff_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
by_cases ha : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
by_cases hb : b ∈ s
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
by_cases hb : b ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inl (Subset.antisymm hc _)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
[PROOFSTEP]
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right, diff_singleton_subset_iff,
  insert_eq_of_mem hb] at ho
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inr <| Or.inl <| Subset.antisymm _ _
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b
[PROOFSTEP]
rw [← Icc_diff_right]
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}
[PROOFSTEP]
exact subset_diff_singleton hc hb
[GOAL]
case neg.refine'_2
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
[PROOFSTEP]
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inr <| Or.inr <| Or.inl <| Subset.antisymm _ _
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Ioc a b
[PROOFSTEP]
rw [← Icc_diff_left]
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}
[PROOFSTEP]
exact subset_diff_singleton hc ha
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
[PROOFSTEP]
rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
[PROOFSTEP]
refine' Or.inr <| Or.inr <| Or.inr <| Subset.antisymm _ ho
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ioo a b
[PROOFSTEP]
rw [← Ico_diff_left, ← Icc_diff_right]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}
[PROOFSTEP]
apply_rules [subset_diff_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Icc a ⊤ = Ici a
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Ioc a ⊤ = Ioi a
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : α
⊢ Icc ⊥ a = Iic a
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : α
⊢ Ico ⊥ a = Iio a
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ Icc ⊥ ⊤ = univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ici a \ Ici b = Ico a b
[PROOFSTEP]
rw [diff_eq, compl_Ici, Ici_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ici a \ Ioi b = Icc a b
[PROOFSTEP]
rw [diff_eq, compl_Ioi, Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a \ Ioi b = Ioc a b
[PROOFSTEP]
rw [diff_eq, compl_Ioi, Ioi_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a \ Ici b = Ioo a b
[PROOFSTEP]
rw [diff_eq, compl_Ici, Ioi_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iic b \ Iic a = Ioc a b
[PROOFSTEP]
rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iio b \ Iic a = Ioo a b
[PROOFSTEP]
rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iic b \ Iio a = Icc a b
[PROOFSTEP]
rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iio b \ Iio a = Ico a b
[PROOFSTEP]
rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : a₁ < b₁
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁
[PROOFSTEP]
convert @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2
[GOAL]
case h.e'_1.h.e'_3.h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₁ b₁ = Ico b₁ a₁
[PROOFSTEP]
exact (@dual_Ico α _ _ _).symm
[GOAL]
case h.e'_1.h.e'_4.h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₂ b₂ = Ico b₂ a₂
[PROOFSTEP]
exact (@dual_Ico α _ _ _).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
rcases exists_between h₁ with ⟨x, xa, xb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁
[PROOFSTEP]
refine' le_of_not_lt fun h' => _
[GOAL]
case intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ b₁ ≤ b₂
[PROOFSTEP]
refine' le_of_not_lt fun h' => _
[GOAL]
case intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False
[PROOFSTEP]
have ab := (h ⟨xa, xb⟩).1.trans xb
[GOAL]
case intro.intro.left
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
ab : a₂ < b₁
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h ⟨h', ab⟩).1
[GOAL]
case intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False
[PROOFSTEP]
have ab := xa.trans (h ⟨xa, xb⟩).2
[GOAL]
case intro.intro.right
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
ab : a₁ < b₂
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h ⟨ab, h'⟩).2
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ = Ico a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp [Subset.antisymm_iff] at e
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ a₁ = a₂ ∧ b₁ = b₂
[PROOFSTEP]
simp [le_antisymm_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
cases' h with h h <;> simp [Ico_subset_Ico_iff h] at e  <;> [rcases e with ⟨⟨h₁, h₂⟩, e'⟩;
      rcases e with ⟨e', ⟨h₁, h₂⟩⟩] <;>
    -- Porting note: restore `tauto`have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e' <;>
  [exact ⟨⟨hab.left, h₁⟩, ⟨h₂, hab.right⟩⟩; exact ⟨⟨h₁, hab.left⟩, ⟨hab.right, h₂⟩⟩]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
cases' h with h h <;> simp [Ico_subset_Ico_iff h] at e  <;> [rcases e with ⟨⟨h₁, h₂⟩, e'⟩; rcases e with ⟨e', ⟨h₁, h₂⟩⟩]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
cases' h with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
h : a₁ < b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
simp [Ico_subset_Ico_iff h] at e
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
h : a₂ < b₂
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
simp [Ico_subset_Ico_iff h] at e
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁
e : (a₂ ≤ a₁ ∧ b₁ ≤ b₂) ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
rcases e with ⟨⟨h₁, h₂⟩, e'⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ a₁ ≤ a₂ ∧ b₂ ≤ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
rcases e with ⟨e', ⟨h₁, h₂⟩⟩
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁
e' : Ico a₂ b₂ ⊆ Ico a₁ b₁
h₁ : a₂ ≤ a₁
h₂ : b₁ ≤ b₂
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e'
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₂ < b₂
e' : Ico a₁ b₁ ⊆ Ico a₂ b₂
h₁ : a₁ ≤ a₂
h₂ : b₂ ≤ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e'
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁
e' : Ico a₂ b₂ ⊆ Ico a₁ b₁
h₁ : a₂ ≤ a₁
h₂ : b₁ ≤ b₂
hab : a₁ ≤ a₂ ∧ b₂ ≤ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
exact ⟨⟨hab.left, h₁⟩, ⟨h₂, hab.right⟩⟩
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₂ < b₂
e' : Ico a₁ b₁ ⊆ Ico a₂ b₂
h₁ : a₁ ≤ a₂
h₂ : b₂ ≤ b₁
hab : a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
[PROOFSTEP]
exact ⟨⟨h₁, hab.left⟩, ⟨hab.right, h₂⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : a₁ < b₁ ∨ a₂ < b₂
x✝ : a₁ = a₂ ∧ b₁ = b₂
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ Ico a₁ b₁ = Ico a₂ b₂
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Ioi_subset_Ioi h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b
[PROOFSTEP]
by_contra ba
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h (not_le.mp ba))
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
⊢ Ioi b ⊆ Ici a ↔ a ≤ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Ioi_subset_Ici h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
⊢ a ≤ b
[PROOFSTEP]
by_contra ba
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ False
[PROOFSTEP]
obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c✝ d : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (ca.trans_le (h bc))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Iio a ⊆ Iio b ↔ a ≤ b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Iio_subset_Iio h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Iio a ⊆ Iio b
⊢ a ≤ b
[PROOFSTEP]
by_contra ab
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Iio a ⊆ Iio b
ab : ¬a ≤ b
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (h (not_le.mp ab))
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
inst✝ : DenselyOrdered α
⊢ Iio a ⊆ Iic b ↔ a ≤ b
[PROOFSTEP]
rw [← diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff, not_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Ioo a b ∪ Ioi c ↔ x ∈ Ioi (min a c)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioo, mem_Ioi, min_lt_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : c < x
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
have hxb : x < b := (le_of_not_gt hc).trans_lt h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x < b
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c < max a b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c < max a b
hab : a ≤ b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c < max a b
hab : b ≤ a
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
exact Ioo_union_Ioi' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
rw [min_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (min c a)
[PROOFSTEP]
simp [*, min_eq_left_of_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ico a b ∪ Ici c ↔ x ∈ Ici (min a c)
[PROOFSTEP]
simp_rw [mem_union, mem_Ico, mem_Ici, min_le_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x < b
⊢ a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : a ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : b ≤ a
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
exact Ico_union_Ici' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c ≤ a
⊢ Ico a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ioc a b ∪ Ioi c ↔ x ∈ Ioi (min a c)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioc, mem_Ioi, min_lt_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : c < x
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c < x
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : a ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : b ≤ a
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
exact Ioc_union_Ioi' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
h : c ≤ a
⊢ Ioc a b ∪ Ioi c = Ioi (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Icc a b ∪ Ici c ↔ x ∈ Ici (min a c)
[PROOFSTEP]
simp_rw [mem_union, mem_Icc, mem_Ici, min_le_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
simp only [hc, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x ≤ b
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
[PROOFSTEP]
simp only [hxb, and_true]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : a ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : c ≤ max a b
hab : b < a
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [hab] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
exact Icc_union_Ici' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ a ∨ c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
cases' h with h h
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
have hca : c ≤ a := h.trans hab.le
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
h : c ≤ b
hca : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (min a c)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iio b ∪ Ico c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Iio, mem_Ico, lt_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d
[PROOFSTEP]
simp only [hc, true_and]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d
[PROOFSTEP]
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x < b
⊢ x < b ∨ c ≤ x ∧ x < d ↔ x < b ∨ x < d
[PROOFSTEP]
simp only [hxb, true_or]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : c ≤ d
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : d ≤ c
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
exact Iio_union_Ico' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d ≤ b
⊢ Iio b ∪ Ico c d = Iio (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Iic b ∪ Ioc c d ↔ x ∈ Iic (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Iic, mem_Ioc, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
simp only [hc, true_and]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁.le
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
simp only [hxb, true_or]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : c ≤ d
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : d ≤ c
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
exact Iic_union_Ioc' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (max b d)
[PROOFSTEP]
rw [max_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (max d b)
[PROOFSTEP]
simp [*, max_eq_right_of_lt h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
cases' lt_or_le x b with hba hba
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : x < b
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
simp [hba, h₁]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
[PROOFSTEP]
simp only [mem_Iio, mem_union, mem_Ioo, lt_max_iff]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < b ∨ c < x ∧ x < d ↔ x < b ∨ x < d
[PROOFSTEP]
refine' or_congr Iff.rfl ⟨And.right, _⟩
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < d → c < x ∧ x < d
[PROOFSTEP]
exact fun h₂ => ⟨h₁.trans_le hba, h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : c ≤ d
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d < b
hcd : d ≤ c
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
exact Iio_union_Ioo' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max b d)
[PROOFSTEP]
rw [max_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d ≤ c
h : d < b
⊢ Iio b ∪ Ioo c d = Iio (max d b)
[PROOFSTEP]
simp [*, max_eq_right_of_lt h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ∈ Iic b ∪ Icc c d ↔ x ∈ Iic (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Iic, mem_Icc, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
simp only [hc, true_and]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x ≤ b
⊢ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d
[PROOFSTEP]
simp only [hxb, true_or]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
cases' le_or_lt c d with hcd hcd
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : c ≤ d
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : min c d ≤ b
hcd : d < c
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
simp [hcd] at h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : c ≤ d
h : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
exact Iic_union_Icc' h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d < c
h : c ≤ b ∨ d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
cases' h with h h
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d < c
h : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
have hdb : d ≤ b := hcd.le.trans h
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d < c
h : c ≤ b
hdb : d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hcd : d < c
h : d ≤ b
⊢ Iic b ∪ Icc c d = Iic (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ x ∈ Ico a b ∪ Ico c d ↔ x ∈ Ico (min a c) (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Ico, min_le_iff, lt_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
have hax : a ≤ x := h₂.trans (le_of_not_gt hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x < d
hax : a ≤ x
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x < d
hxb : x < b
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : ¬x < d
⊢ a ≤ x ∧ x < b ∨ c ≤ x ∧ x < d ↔ (a ≤ x ∨ c ≤ x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : d ≤ c
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : c ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : d ≤ c
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
exact Ico_union_Ico' h₂ h₁
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
all_goals simp [*]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ x ∈ Ioc a b ∪ Ioc c d ↔ x ∈ Ioc (min a c) (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioc, min_lt_iff, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c < x
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c < x
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c < x
hd : x ≤ d
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c < x
hd : ¬x ≤ d
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
have hax : a < x := h₂.trans_lt (lt_of_not_ge hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c < x
hd : ¬x ≤ d
hax : a < x
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c < x
hd : x ≤ d
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c < x
hd : x ≤ d
hxb : x ≤ b
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c < x
hd : ¬x ≤ d
⊢ a < x ∧ x ≤ b ∨ c < x ∧ x ≤ d ↔ (a < x ∨ c < x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : a ≤ b
hcd : d ≤ c
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : c ≤ d
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
hab : b ≤ a
hcd : d ≤ c
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [hab, hcd] at h₁ h₂
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
exact Ioc_union_Ioc' h₂ h₁
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
all_goals simp [*]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ x ∈ Icc a b ∪ Icc c d ↔ x ∈ Icc (min a c) (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Icc, min_le_iff, le_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hc : c ≤ x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
by_cases hd : x ≤ d
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : x ≤ d
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x ≤ d
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
have hax : a ≤ x := h₂.trans (le_of_not_ge hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : c ≤ x
hd : ¬x ≤ d
hax : a ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x ≤ d
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : x ≤ d
hxb : x ≤ b
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c ≤ b
h₂ : a ≤ d
x : α
hc : ¬c ≤ x
hd : ¬x ≤ d
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ∧ x ≤ d ↔ (a ≤ x ∨ c ≤ x) ∧ (x ≤ b ∨ x ≤ d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
cases' le_or_lt c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
cases' le_or_lt c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : d < c
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b < a
hcd : c ≤ d
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b < a
hcd : d < c
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt, min_eq_right_of_lt,
  max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
exact Icc_union_Icc' h₂.le h₁.le
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d < c
h₁ : a < c
h₂ : d < b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : d < c
h₁ : b < c
h₂ : d < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
all_goals simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d < c
h₁ : a < c
h₂ : d < b
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b < a
hcd : d < c
h₁ : b < c
h₂ : d < a
⊢ Icc a b ∪ Icc c d = Icc (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
⊢ x ∈ Ioo a b ∪ Ioo c d ↔ x ∈ Ioo (min a c) (max b d)
[PROOFSTEP]
simp_rw [mem_union, mem_Ioo, min_lt_iff, lt_max_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hc : c < x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : c < x
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : ¬c < x
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
by_cases hd : x < d
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : c < x
hd : x < d
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_true]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : c < x
hd : ¬x < d
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
have hax : a < x := h₂.trans_le (le_of_not_lt hd)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : c < x
hd : ¬x < d
hax : a < x
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hax, true_and, hc, or_self]
  -- Porting note: restore `tauto`
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : ¬c < x
hd : x < d
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
have hxb : x < b := (le_of_not_lt hc).trans_lt h₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : ¬c < x
hd : x < d
hxb : x < b
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hxb, and_true, hc, false_and, or_false, true_or]
  -- Porting note: restore `tauto`
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : c < b
h₂ : a < d
x : α
hc : ¬c < x
hd : ¬x < d
⊢ a < x ∧ x < b ∨ c < x ∧ x < d ↔ (a < x ∨ c < x) ∧ (x < b ∨ x < d)
[PROOFSTEP]
simp only [hc, hd, and_self, or_false]
  -- Porting note: restore `tauto`
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b ≤ a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
cases' le_total c d with hcd hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : c ≤ d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : a ≤ b
hcd : d ≤ c
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b ≤ a
hcd : c ≤ d
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
hab : b ≤ a
hcd : d ≤ c
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
exact Ioo_union_Ioo' h₂ h₁
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a < c
h₂ : d < b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b < c
h₂ : d < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
all_goals
  simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a < c
h₂ : d < b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b < c
h₂ : d < a
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
[PROOFSTEP]
simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, le_of_lt h₂, le_of_lt h₁]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
[PROOFSTEP]
simp [Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a b : α
⊢ Ici a ∩ Ici b = Ici (a ⊔ b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a b x : α
⊢ x ∈ Ici a ∩ Ici b ↔ x ∈ Ici (a ⊔ b)
[PROOFSTEP]
simp [Ici]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ Ico a b ∩ Ici c = Ico (a ⊔ c) b
[PROOFSTEP]
rw [← Ici_inter_Iio, ← Ici_inter_Iio, ← Ici_inter_Ici, inter_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Lattice α
a b c a₁ a₂ b₁ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Lattice α
a b c a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Lattice α
a b c a₁ a₂ b₁ b₂ : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}
[PROOFSTEP]
rw [Icc_inter_Icc, sup_of_le_right hab, inf_of_le_left hbc, Icc_self]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ici_inter_Iio.symm, Ici_inter_Ici.symm, Iio_inter_Iio.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ici a₁ ∩ Iio b₁ ∩ (Ici a₂ ∩ Iio b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iio b₁ ∩ Iio b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ioi_inter_Iic.symm, Ioi_inter_Ioi.symm, Iic_inter_Iic.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a₁ ∩ Iic b₁ ∩ (Ioi a₂ ∩ Iic b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iic b₁ ∩ Iic b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)
[PROOFSTEP]
simp only [Ioi_inter_Iio.symm, Ioi_inter_Ioi.symm, Iio_inter_Iio.symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a₁ ∩ Iio b₁ ∩ (Ioi a₂ ∩ Iio b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iio b₁ ∩ Iio b₂)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₁ < b₂
x : α
⊢ x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioc (max a₁ a₂) b₁
[PROOFSTEP]
simp [and_assoc, @and_left_comm (x ≤ _), and_iff_left_iff_imp.2 fun h' => lt_of_le_of_lt h' h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₂ ≤ b₁
x : α
⊢ x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioo (max a₁ a₂) b₂
[PROOFSTEP]
simp [and_assoc, @and_left_comm (x ≤ _), and_iff_right_iff_imp.2 fun h' => (le_of_lt h').trans h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁
[PROOFSTEP]
rw [inter_comm, Ioc_inter_Ioo_of_right_le h, max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₂ < b₁
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂
[PROOFSTEP]
rw [inter_comm, Ioc_inter_Ioo_of_left_lt h, max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ico a b \ Iio c = Ico (max a c) b
[PROOFSTEP]
rw [diff_eq, compl_Iio, Ico_inter_Ici, sup_eq_max]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ ∀ (x : α), x ∈ Ioc a b \ Ioi c ↔ x ∈ Ioc a (min b c)
[PROOFSTEP]
simp (config := { contextual := true }) [iff_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b
[PROOFSTEP]
rw [← Ioi_inter_Iic, inter_assoc, inter_comm, inter_assoc, Ioi_inter_Ioi, inter_comm, Ioi_inter_Iic, sup_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ ∀ (x : α), x ∈ Ico a b ∩ Iio c ↔ x ∈ Ico a (min b c)
[PROOFSTEP]
simp (config := { contextual := true }) [iff_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b \ Iic c = Ioc (max a c) b
[PROOFSTEP]
rw [diff_eq, compl_Iic, Ioc_inter_Ioi, sup_eq_max]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc a c = Ioc a (max b c)
[PROOFSTEP]
rw [Ioc_union_Ioc, min_self]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max a c
[PROOFSTEP]
exact (min_le_left _ _).trans (le_max_left _ _)
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a c ≤ max a b
[PROOFSTEP]
exact (min_le_left _ _).trans (le_max_left _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a c ∪ Ioc b c = Ioc (min a b) c
[PROOFSTEP]
rw [Ioc_union_Ioc, max_self]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a c ≤ max b c
[PROOFSTEP]
exact (min_le_right _ _).trans (le_max_right _ _)
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b c ≤ max a c
[PROOFSTEP]
exact (min_le_right _ _).trans (le_max_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)
[PROOFSTEP]
rw [max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max b a)
[PROOFSTEP]
apply Ioc_union_Ioc
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max b a
[PROOFSTEP]
rw [max_comm]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b a ≤ max a b
[PROOFSTEP]
rw [max_comm]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max a b
[PROOFSTEP]
exact min_le_max
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b a ≤ max b a
[PROOFSTEP]
exact min_le_max
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c))
[PROOFSTEP]
rw [Ioc_union_Ioc, Ioc_union_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc (min (min a b) c) (max (max b c) a) = Ioc (min a (min b c)) (max a (max b c))
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min (min a b) (max b c) ≤ max c a
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min c a ≤ max (min a b) (max b c)
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min a b ≤ max b c
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ min b c ≤ max a b
[PROOFSTEP]
simp [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right, le_refl, min_assoc, max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
x : α
y : β
⊢ (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
simp [and_assoc, and_comm, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α × β
⊢ Icc a b = Icc a.fst b.fst ×ˢ Icc a.snd b.snd
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a < y) }
[PROOFSTEP]
rcases exists_between ha₁ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a < y) }
[PROOFSTEP]
exact ⟨⟨b, hb₁, hb₂.trans ha₂⟩, hb₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioc x y)
a : α
ha₁ : x < a
ha₂ : a ≤ y
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a ≤ y) }
[PROOFSTEP]
rcases exists_between ha₁ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioc x y)
a : α
ha₁ : x < a
ha₂ : a ≤ y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < { val := a, property := (_ : x < a ∧ a ≤ y) }
[PROOFSTEP]
exact ⟨⟨b, hb₁, hb₂.le.trans ha₂⟩, hb₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioi x)
a : α
ha : a ∈ Set.Ioi x
⊢ ∃ b, b < { val := a, property := ha }
[PROOFSTEP]
rcases exists_between ha with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioi x)
a : α
ha : a ∈ Set.Ioi x
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < { val := a, property := ha }
[PROOFSTEP]
exact ⟨⟨b, hb₁⟩, hb₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
⊢ ∃ b, { val := a, property := (_ : x < a ∧ a < y) } < b
[PROOFSTEP]
rcases exists_between ha₂ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ioo x y)
a : α
ha₁ : x < a
ha₂ : a < y
b : α
hb₁ : a < b
hb₂ : b < y
⊢ ∃ b, { val := a, property := (_ : x < a ∧ a < y) } < b
[PROOFSTEP]
exact ⟨⟨b, ha₁.trans hb₁, hb₂⟩, hb₁⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ico x y)
a : α
ha₁ : x ≤ a
ha₂ : a < y
⊢ ∃ b, { val := a, property := (_ : x ≤ a ∧ a < y) } < b
[PROOFSTEP]
rcases exists_between ha₂ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Ico x y)
a : α
ha₁ : x ≤ a
ha₂ : a < y
b : α
hb₁ : a < b
hb₂ : b < y
⊢ ∃ b, { val := a, property := (_ : x ≤ a ∧ a < y) } < b
[PROOFSTEP]
exact ⟨⟨b, ha₁.trans hb₁.le, hb₂⟩, hb₁⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Iio x)
a : α
ha : a ∈ Set.Iio x
⊢ ∃ b, { val := a, property := ha } < b
[PROOFSTEP]
rcases exists_between ha with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Set.Iio x)
a : α
ha : a ∈ Set.Iio x
b : α
hb₁ : a < b
hb₂ : b < x
⊢ ∃ b, { val := a, property := ha } < b
[PROOFSTEP]
exact ⟨⟨b, hb₂⟩, hb₁⟩