awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).inf t)
have cons : IsRetrocompact (t i ⊓ s.inf t)
Tactic: rw [Finset.inf_cons]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)
have empty : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)), IsRetrocompact (Finset.inf ∅ t)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht
Cleared hypotheses: s, ht
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
empty : ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsRetrocompact (t i)), IsRetrocompact (Finset.inf ∅ t)
⊢ IsRetrocompact (s.inf t)
have cons : ∀ (i : ι) (s : Finset ι) (ih : i ∉ s) (hi : ∀ (ht : ∀ i ∈ s, IsRetrocompact (t i)), IsRetrocompact (s.inf t))
  (ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)), IsRetrocompact ((Finset.cons i s ih).inf t)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht
Cleared hypotheses: s, ht
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf' hs t)
have rw : IsRetrocompact (s.inf t)
Tactic: rw [Finset.inf'_eq_inf]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ IsRetrocompact s ↔ IsSpectralMap.{u_2, u_2} (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
have refine_1 : ∀ (hs : IsRetrocompact s) (t : Set X) (htopen : IsOpen[inst] t) (htcomp : IsCompact t),
  IsCompact (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
Tactic: refine ⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (hs : IsRetrocompact s) (t : Set X) (htopen : IsOpen[inst] t) (htcomp : IsCompact t),
    IsCompact (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
⊢ IsRetrocompact s ↔ IsSpectralMap.{u_2, u_2} (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))
have refine_2 : ∀ (hs : IsSpectralMap.{u_2, u_2} (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))) (t : Set X)
  (htcomp : IsCompact t) (htopen : IsOpen[inst] t), IsCompact (s ∩ t)
Tactic: refine ⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst] t
htcomp : IsCompact t
⊢ IsCompact (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
have refine_1 : IsCompact (s ∩ t)
Tactic: rw [IsEmbedding.subtypeVal.isCompact_iff, image_preimage_eq_inter_range,
      Subtype.range_coe_subtype, setOf_mem_eq, inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
⊢ IsCompact (f '' s ∩ U)
have rw : IsCompact (s ∩ f ⁻¹' U)
Tactic: rw [← image_inter_preimage, ← hfemb.isCompact_iff]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
⊢ IsCompact (s ∩ f ⁻¹' U)
have refine : IsCompact (f ⁻¹' U)
Tactic: refine hs ?_ <| hUopen.preimage hfemb.continuous
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst_1] U
⊢ IsCompact (f ⁻¹' U)
have rw : IsCompact (range f ∩ U)
Tactic: rw [hfemb.isCompact_iff, image_preimage_eq_inter_range, inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
⊢ IsCompact (f ⁻¹' s ∩ U)
have rw : IsCompact (s ∩ f '' U)
Tactic: rw [hf.isCompact_iff, image_preimage_inter]
-- Lean 4 proof step from Mathlib.Topology.Constructible (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
⊢ IsCompact (f ⁻¹' s ∩ U)
have hfUopen : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
Tactic: have hfUopen : IsOpen (f '' U ∪ (range f)ᶜ) := by
    simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
      using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Constructible (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst] U
hfUopen : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)
have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ)
Tactic: have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf'
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] 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
have mem : ∀ (U : Set X) (hU : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U} U), p U sorry
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'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] 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
mem : ∀ (U : Set X) (hU : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U} U), p U ⋯
⊢ p s hs
have bot : p ⊥ sorry
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'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] 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
mem : ∀ (U : Set X) (hU : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U} U), p U ⋯
bot : p ⊥ ⋯
⊢ p s hs
have sup : ∀ (s : Set X)
  (hs :
    Membership.mem (γ := BooleanSubalgebra (Set X))
      (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s)
  (t : Set X)
  (ht :
    Membership.mem (γ := BooleanSubalgebra (Set X))
      (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) t)
  (hs' : p s hs) (ht' : p t ht), p (s ⊔ t) sorry
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'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] 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
mem : ∀ (U : Set X) (hU : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U} U), p U ⋯
bot : p ⊥ ⋯
sup :
  ∀ (s : Set X)
    (hs :
      Membership.mem (γ := BooleanSubalgebra (Set X))
        (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s)
    (t : Set X)
    (ht :
      Membership.mem (γ := BooleanSubalgebra (Set X))
        (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) t)
    (hs' : p s hs) (ht' : p t ht), p (s ⊔ t) ⋯
⊢ p s hs
have compl₁ : ∀ (s : Set X)
  (hs :
    Membership.mem (γ := BooleanSubalgebra (Set X))
      (BooleanSubalgebra.closure {U : Set X | IsOpen[inst] U ∧ IsRetrocompact U}) s)
  (hs' : p s hs), p sᶜ sorry
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'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
t : Set Y
ht : IsConstructible t
hs' : IsConstructible (f ⁻¹' s)
ht' : IsConstructible (f ⁻¹' t)
⊢ IsConstructible (f ⁻¹' (s ∪ t))
have union : IsConstructible (f ⁻¹' s ∪ f ⁻¹' t)
Tactic: rw [preimage_union]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (f ⁻¹' sᶜ)
have compl : IsConstructible (f ⁻¹' s)ᶜ
Tactic: rw [preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
hs : IsConstructible s
⊢ IsConstructible (f ⁻¹' s)
have open_retrocompact : ∀ (U : Set Y) (hUopen : IsOpen[inst_1] U) (hUcomp : IsRetrocompact U), IsConstructible (f ⁻¹' U)
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hf _ hUopen hUcomp).isConstructible <| hUopen.preimage hfcont
  | union s hs t ht hs' ht' => rw [preimage_union]; exact hs'.union ht'
  | compl s hs hs' => rw [preimage_compl]; exact hs'.compl
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
hs : IsConstructible s
open_retrocompact : ∀ (U : Set Y) (hUopen : IsOpen[inst_1] U) (hUcomp : IsRetrocompact U), IsConstructible (f ⁻¹' U)
⊢ IsConstructible (f ⁻¹' s)
have union : ∀ (s : Set Y) (hs : IsConstructible s) (t : Set Y) (ht : IsConstructible t) (hs' : IsConstructible (f ⁻¹' s))
  (ht' : IsConstructible (f ⁻¹' t)), IsConstructible (f ⁻¹' (s ∪ t))
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hf _ hUopen hUcomp).isConstructible <| hUopen.preimage hfcont
  | union s hs t ht hs' ht' => rw [preimage_union]; exact hs'.union ht'
  | compl s hs hs' => rw [preimage_compl]; exact hs'.compl
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
hs : IsConstructible s
open_retrocompact : ∀ (U : Set Y) (hUopen : IsOpen[inst_1] U) (hUcomp : IsRetrocompact U), IsConstructible (f ⁻¹' U)
union :
  ∀ (s : Set Y) (hs : IsConstructible s) (t : Set Y) (ht : IsConstructible t) (hs' : IsConstructible (f ⁻¹' s))
    (ht' : IsConstructible (f ⁻¹' t)), IsConstructible (f ⁻¹' (s ∪ t))
⊢ IsConstructible (f ⁻¹' s)
have compl : ∀ (s : Set Y) (hs : IsConstructible s) (hs' : IsConstructible (f ⁻¹' s)), IsConstructible (f ⁻¹' sᶜ)
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hf _ hUopen hUcomp).isConstructible <| hUopen.preimage hfcont
  | union s hs t ht hs' ht' => rw [preimage_union]; exact hs'.union ht'
  | compl s hs hs' => rw [preimage_compl]; exact hs'.compl
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' (s ∪ t))
have union : IsConstructible (f '' s ∪ f '' t)
Tactic: rw [image_union]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)
have compl : IsConstructible (range f \ f '' s)
Tactic: rw [← range_diff_image hfopen.injective]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
⊢ IsConstructible (f '' s)
have open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hfopen.injective]
    exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
⊢ IsConstructible (f '' s)
have union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t) (hs' : IsConstructible (f '' s))
  (ht' : IsConstructible (f '' t)), IsConstructible (f '' (s ∪ t))
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hfopen.injective]
    exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
union :
  ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t) (hs' : IsConstructible (f '' s))
    (ht' : IsConstructible (f '' t)), IsConstructible (f '' (s ∪ t))
⊢ IsConstructible (f '' s)
have compl : ∀ (s : Set X) (hs : IsConstructible s) (hs' : IsConstructible (f '' s)), IsConstructible (f '' sᶜ)
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hfopen.injective]
    exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Constructible (hypothesis)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f '' U)
have hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
Tactic: have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
⊢ IsConstructible (f '' U)
have open_retrocompact : IsRetrocompact (f '' U ∪ (range f)ᶜ)
Tactic: suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst_1] V
⊢ IsCompact ((f '' U ∪ (range f)ᶜ) ∩ V)
have open_retrocompact : IsCompact (f '' (U ∩ f ⁻¹' V) ∪ (range f)ᶜ ∩ V)
Tactic: rw [union_inter_distrib_right, ← image_inter_preimage]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' (s ∪ t))
have union : IsConstructible (f '' s ∪ f '' t)
Tactic: rw [image_union]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)
have compl : IsConstructible (range f \ f '' s)
Tactic: rw [← range_diff_image hf.injective]
-- Lean 4 proof step from Mathlib.Topology.Constructible (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
⊢ IsConstructible (f '' s)
have open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
Tactic: induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
    suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
    rintro V hVcomp hVopen
    rw [union_inter_distrib_right, ← image_inter_preimage]
    exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hf.injective]
    exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'
Cleared hypotheses: hs