case tfae_1_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
⊢ chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'

α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
tfae_have 1 ↔ 3
case tfae_2_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ (∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l') ↔
    ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'

α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
tfae_2_iff_3 :
  (∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l') ↔
    ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
tfae_have 2 ↔ 3
no goals
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
tfae_2_iff_3 :
  (∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l') ↔
    ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ TFAE
    [chainHeight s ≤ chainHeight t, ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l',
      ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l']
tfae_finish
no goals
case tfae_1_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
⊢ chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
convert ← chainHeight_add_le_chainHeight_add s t 0 0 <;> apply add_zero
case tfae_2_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
l : List α
hl : l ∈ subchain s
⊢ (∃ l', l' ∈ subchain t ∧ length l = length l') ↔ ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
case tfae_2_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
⊢ (∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l = length l') ↔
    ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
refine' forall₂_congr fun l hl ↦ _
no goals
case tfae_2_iff_3
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s✝ t✝ : Set α
l✝ : List α
a : α
s : Set α
t : Set β
tfae_1_iff_3 :
  chainHeight s ≤ chainHeight t ↔ ∀ (l : List α), l ∈ subchain s → ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
l : List α
hl : l ∈ subchain s
⊢ (∃ l', l' ∈ subchain t ∧ length l = length l') ↔ ∃ l', l' ∈ subchain t ∧ length l ≤ length l'
simp_rw [← (le_chainHeight_TFAE t l.length).out 1 2, eq_comm]