-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem le_TFAE : List.TFAE [I ≤ J, (I : Set (ι → ℝ)) ⊆ J,
    Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]

Proof state:
ι : Type u_1
I J : Box ι
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl

Result:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Proof state:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_have 3 ↔ 4 := Icc_subset_Icc_iff I.lower_le_upper

Result:
ι : Type u_1
I J : Box ι
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
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Proof state:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
x✝ : ↑I ⊆ ↑J
h : ↑I ⊆ ↑J := x✝
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper

Tactic:
simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_have 2 → 3
| h => by simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h

Result:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Proof state:
ι : Type u_1
I J : Box ι
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
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
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
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_have 4 → 2
| h, x, hx, i => Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)

Result:
ι : Type u_1
I J : Box ι
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
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE