-- Mathlib/Topology/Constructible.lean
/-- An induction principle for constructible sets. If `p` holds for all open retrocompact
sets, and is preserved under union and complement, then `p` holds for all constructible sets. -/
@[elab_as_elim]
lemma IsConstructible.empty_union_induction {p : ∀ s : Set X, IsConstructible s → Prop}
    (open_retrocompact : ∀ U (hUopen : IsOpen U) (hUcomp : IsRetrocompact U),
      p U (BooleanSubalgebra.subset_closure ⟨hUopen, hUcomp⟩))
    (union : ∀ s hs t ht, p s hs → p t ht → p (s ∪ t) (hs.union ht))
    (compl : ∀ s hs, p s hs → p sᶜ hs.compl) {s} (hs : IsConstructible s) : p s hs

Proof state:
case compl
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s✝ s : Set X
hs : s ∈ BooleanSubalgebra.closure {U | IsOpen U ∧ IsRetrocompact U}
hs' : p s hs
⊢ p sᶜ ⋯

Tactic:
exact compl _ _ hs'

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s : Set X
hs : IsConstructible s
⊢ p s hs

Tactic:
induction hs using BooleanSubalgebra.closure_bot_sup_induction with
| mem U hU => exact open_retrocompact _ hU.1 hU.2
| bot => exact open_retrocompact _ isOpen_empty .empty
| sup s hs t ht hs' ht' => exact union _ _ _ _ hs' ht'
| compl s hs hs' => exact compl _ _ hs'

Result:
no goals

Proof state:
case mem
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s U : Set X
hU : U ∈ {U | IsOpen U ∧ IsRetrocompact U}
⊢ p U ⋯

Tactic:
exact open_retrocompact _ hU.1 hU.2

Result:
no goals

Proof state:
case sup
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s✝ s : Set X
hs : s ∈ BooleanSubalgebra.closure {U | IsOpen U ∧ IsRetrocompact U}
t : Set X
ht : t ∈ BooleanSubalgebra.closure {U | IsOpen U ∧ IsRetrocompact U}
hs' : p s hs
ht' : p t ht
⊢ p (s ⊔ t) ⋯

Tactic:
exact union _ _ _ _ hs' ht'

Result:
no goals

Proof state:
case bot
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s : Set X
⊢ p ⊥ ⋯

Tactic:
exact open_retrocompact _ isOpen_empty .empty

Result:
no goals