case tfae_1_iff_2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ I ≤ J ↔ ↑I ⊆ ↑J

ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
tfae_have 1 ↔ 2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
case tfae_1_iff_2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ I ≤ J ↔ ↑I ⊆ ↑J

ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
exact Iff.rfl
case tfae_2_to_3
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper

ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
tfae_have 2 → 3
case tfae_3_iff_4
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
tfae_have 3 ↔ 4
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
case tfae_3_iff_4
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper

ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
exact Icc_subset_Icc_iff I.lower_le_upper
case tfae_4_to_2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J

ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
tfae_4_to_2 : J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
tfae_have 4 → 2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
tfae_4_to_2 : J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
case tfae_4_to_2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J

ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
tfae_4_to_2 : J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
exact fun h x hx i ↦ Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)
no goals
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
tfae_4_to_2 : J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
tfae_finish
case tfae_2_to_3
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
h : ↑I ⊆ ↑J
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper
case tfae_2_to_3
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
intro h
no goals
case tfae_2_to_3
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
h : ↑I ⊆ ↑J
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper
simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h