-- Mathlib/Topology/NoetherianSpace.lean
theorem noetherianSpace_TFAE :
    TFAE [NoetherianSpace α,
      WellFoundedLT (Closeds α),
      ∀ s : Set α, IsCompact s,
      ∀ s : Opens α, IsCompact (s : Set α)]

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 1 ↔ 2 := by
  simp_rw [isWellFounded_iff]
  exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm

Result:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 1 ↔ 4 := noetherianSpace_iff_opens α

Result:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 1 → 3 := @NoetherianSpace.isCompact α _

Result:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 3 → 4 := fun h s => h s

Result:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
tfae_3_to_4 : (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ WellFoundedLT (Closeds α)

Tactic:
simp_rw [isWellFounded_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (WellFounded fun x1 x2 => x1 > x2) ↔ WellFounded fun x1 x2 => x1 < x2

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
tfae_3_to_4 : (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (WellFounded fun x1 x2 => x1 > x2) ↔ WellFounded fun x1 x2 => x1 < x2

Tactic:
exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm

Result:
no goals