-- Mathlib/Order/Height.lean
theorem chainHeight_le_chainHeight_TFAE (s : Set α) (t : Set β) :
    TFAE [s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l = length l',
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l ≤ length l']

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
tfae_1_iff_3 : s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
⊢ [s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length,
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length].TFAE

Tactic:
tfae_have 2 ↔ 3 := by
  refine forall₂_congr fun l _ ↦ ?_
  simp_rw [← (le_chainHeight_TFAE t l.length).out 1 2, eq_comm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
tfae_1_iff_3 : s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
tfae_2_iff_3 :
  (∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length) ↔
    ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
⊢ [s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length,
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length].TFAE

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
tfae_1_iff_3 : s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
tfae_2_iff_3 :
  (∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length) ↔
    ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
⊢ [s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length,
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
⊢ [s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length,
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length].TFAE

Tactic:
tfae_have 1 ↔ 3 := by
  convert ← chainHeight_add_le_chainHeight_add s t 0 0 <;> apply add_zero

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
tfae_1_iff_3 : s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
⊢ [s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length,
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length].TFAE

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
tfae_1_iff_3 : s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
⊢ (∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length) ↔
    ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length

Tactic:
refine forall₂_congr fun l _ ↦ ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
tfae_1_iff_3 : s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
l : List α
x✝ : l ∈ s.subchain
⊢ (∃ l' ∈ t.subchain, l.length = l'.length) ↔ ∃ l' ∈ t.subchain, l.length ≤ l'.length

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
tfae_1_iff_3 : s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
l : List α
x✝ : l ∈ s.subchain
⊢ (∃ l' ∈ t.subchain, l.length = l'.length) ↔ ∃ l' ∈ t.subchain, l.length ≤ l'.length

Tactic:
simp_rw [← (le_chainHeight_TFAE t l.length).out 1 2, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
⊢ s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length

Tactic:
convert ← chainHeight_add_le_chainHeight_add s t 0 0 <;> apply add_zero

Result:
no goals