awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
x : α
hx : x ∈ U
mpr : ∀ (Us : Set (Opens α)) (hUs : Us ⊆ B) (hx : x ∈ sSup Us), ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
rcases h U with ⟨Us, hUs, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us : Set (Opens α)
hUs : Us ⊆ B
hx : x ∈ sSup Us
mpr : ∀ (U : Opens α) (Us_1 : U ∈ Us) (xU : x ∈ U), ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us

Tactic:
rcases mem_sSup.1 hx with ⟨U, Us, xU⟩

Premises used: TopologicalSpace.Opens.mem_sSup, Iff.mp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us_1 : Set (Opens α)
hUs : Us_1 ⊆ B
hx : x ∈ sSup Us_1
U : Opens α
Us : U ∈ Us_1
xU : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us_1

Tactic:
⟨U, hUs Us, xU, le_sSup Us⟩

Premises used: And.intro, Exists.intro, le_sSup
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
x : α
Us_1 : Set (Opens α)
hUs : Us_1 ⊆ B
hx : x ∈ sSup Us_1
U : Opens α
Us : U ∈ Us_1
xU : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ sSup Us_1

Tactic:
exact ⟨U, hUs Us, xU, le_sSup Us⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
hb₁ : IsTopologicalBasis.{u_2} (α := α) (range fun (i : ι) ↦ (b i).carrier)
hb'₁ : ∀ (i : ι), IsCompact (b i).carrier
⊢ IsCompact U ∧ IsOpen[inst] U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, (↑(b i) : Set α)

Tactic:
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1

Premises used: TopologicalSpace.Opens.carrier, isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
⊢ IsBasis (range b)

Tactic:
hb
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
h : (range fun (i : ι) ↦ (b i).carrier) = SetLike.coe '' range b
⊢ IsTopologicalBasis.{u_2} (α := α) (range fun (i : ι) ↦ (b i).carrier)

Tactic:
convert! (config := { transparency := .default }) hb
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
h : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) (range fun (i : ι) ↦ (b i).carrier) x ↔ x ∈ SetLike.coe '' range b
⊢ (range fun (i : ι) ↦ (b i).carrier) = SetLike.coe '' range b

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U x : Set α
⊢ Membership.mem (γ := Set (Set α)) (range fun (i : ι) ↦ (b i).carrier) x ↔ x ∈ SetLike.coe '' range b

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier

Tactic:
hb'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact (↑(b i) : Set α)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier

Tactic:
exact hb'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
obtain : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us'), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

Tactic:
obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U

Premises used: Iff.mp, TopologicalSpace.Opens.isBasis_iff_cover
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
⊢ U.carrier ⊆ ⋃ (i : (↑Us' : Type u_2)), (fun (s : (↑Us' : Type u_2)) ↦ (↑(↑s : Opens α) : Set α)) i

Tactic:
simp [hsup]
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
obtain :
  ∀ (t : Finset (↑Us' : Type u_2)) (ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)),
    ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

Tactic:
obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])

Premises used: IsCompact.elim_finite_subcover, SetLike.coe, TopologicalSpace.Opens.is_open', Subtype.val
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset (↑Us' : Type u_2)
ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)
⊢ (↑(Finset.image (Subtype.val (p := fun (x : Opens α) ↦ x ∈ Us')) t) : Set (Opens α)) ⊆ Us'

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset (↑Us' : Type u_2)
ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)
refine : U = sSup (↑(Finset.image (Subtype.val (p := fun (x : Opens α) ↦ x ∈ Us')) t) : Set (Opens α))
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

Tactic:
refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset (↑Us' : Type u_2)
ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)
⊢ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α) ⊆
    (↑(sSup (↑(Finset.image (Subtype.val (p := fun (x : Opens α) ↦ x ∈ Us')) t) : Set (Opens α))) : Set α)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
Us' : Set (Opens α)
hsub : Us' ⊆ B
hsup : U = sSup Us'
t : Finset (↑Us' : Type u_2)
ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)
⊢ U = sSup (↑(Finset.image (Subtype.val (p := fun (x : Opens α) ↦ x ∈ Us')) t) : Set (Opens α))

Tactic:
exact le_antisymm (subset_trans ht (by simp)) (le_trans (sSup_le_sSup (by simp)) hsup.ge)

Premises used: Eq.ge, subset_trans, le_antisymm, sSup_le_sSup, le_trans
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
obtain : ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us'), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
obtain₁ :
  ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us') (t : Finset (↑Us' : Type u_2))
    (ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)), ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
obtain₂ :
  ∀ (Us' : Set (Opens α)) (hsub : Us' ⊆ B) (hsup : U = sSup Us') (t : Finset (↑Us' : Type u_2))
    (ht : U.carrier ⊆ ⋃ i ∈ t, (↑(↑i : Opens α) : Set α)),
    U = sSup (↑(Finset.image (Subtype.val (p := fun (x : Opens α) ↦ x ∈ Us')) t) : Set (Opens α))
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

Tactic:
classical
  obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U
  obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])
  refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
  exact le_antisymm (subset_trans ht (by simp)) (le_trans (sSup_le_sSup (by simp)) hsup.ge)

Premises used: Iff.mp, TopologicalSpace.Opens.isBasis_iff_cover
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
rw : t₁ ≤ generateFrom (SetLike.coe '' Us)
| t₁ ≤ t₂

Tactic:
rw [hUs.eq_generateFrom]

Premises used: TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
conv_lhs : t₁ ≤ generateFrom (SetLike.coe '' Us) ↔ ∀ U ∈ Us, IsOpen[t₁] (↑U : Set α)
⊢ t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen[t₁] (↑U : Set α)

Tactic:
conv_lhs => rw [hUs.eq_generateFrom]

Premises used: TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
⊢ t₁ ≤ generateFrom (SetLike.coe '' Us) ↔ ∀ U ∈ Us, IsOpen[t₁] (↑U : Set α)

Tactic:
simp [Set.subset_def, le_generateFrom_iff_subset_isOpen]

Premises used: Set.subset_def, TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsTopologicalBasis (α := (i : ι) × α i)
    (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) '' SetLike.coe '' B i)

Tactic:
TopologicalSpace.IsTopologicalBasis.sigma hB

Premises used: TopologicalSpace.IsTopologicalBasis.sigma
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
a :
  IsBasis (α := Sigma α)
      (⋃ (i : ι), (fun (U : Opens (α i)) ↦ { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := ⋯ }) '' B i) ↔
    IsTopologicalBasis (α := (i : ι) × α i)
      (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) '' SetLike.coe '' B i)
⊢ IsBasis (α := Sigma α)
    (⋃ (i : ι), (fun (U : Opens (α i)) ↦ { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := ⋯ }) '' B i)

Tactic:
convert! TopologicalSpace.IsTopologicalBasis.sigma hB

Premises used: TopologicalSpace.IsTopologicalBasis.sigma
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
a :
  IsTopologicalBasis (α := Sigma α)
      (⋃ (i : ι),
        (comp (β := Opens (Sigma α)) SetLike.coe fun (U : Opens (α i)) ↦
            { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := ⋯ }) ''
          B i) ↔
    IsTopologicalBasis (α := (i : ι) × α i)
      (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) ∘ SetLike.coe '' B i)
⊢ IsBasis (α := Sigma α)
      (⋃ (i : ι), (fun (U : Opens (α i)) ↦ { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := ⋯ }) '' B i) ↔
    IsTopologicalBasis (α := (i : ι) × α i)
      (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) '' SetLike.coe '' B i)

Tactic:
simp only [IsBasis, Set.image_iUnion, ← Set.image_comp]

Premises used: Set.image_iUnion, TopologicalSpace.Opens.IsBasis, Set.image_comp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsTopologicalBasis (α := Sigma α)
      (⋃ (i : ι),
        (comp (β := Opens (Sigma α)) SetLike.coe fun (U : Opens (α i)) ↦
            { carrier := Sigma.mk (β := α) i '' U.carrier, is_open' := ⋯ }) ''
          B i) ↔
    IsTopologicalBasis (α := (i : ι) × α i)
      (⋃ (i : ι), (fun (u : Set (α i)) ↦ Sigma.mk (β := fun (i : ι) ↦ α i) i '' u) ∘ SetLike.coe '' B i)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
⊢ IsTopologicalBasis (preimage f '' SetLike.coe '' B)

Tactic:
H.isInducing h

Premises used: TopologicalSpace.IsTopologicalBasis.isInducing
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
h₁ :
  image (α := Opens α) SetLike.coe
      {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := ⋯ : Opens α } = x} =
    preimage f '' SetLike.coe '' B
⊢ IsTopologicalBasis
    (image (α := Opens α) SetLike.coe
      {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := ⋯ : Opens α } = x})

Tactic:
convert! H.isInducing h

Premises used: TopologicalSpace.IsTopologicalBasis.isInducing
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
h₁ :
  ∀ (x : Set α),
    x ∈
        image (α := Opens α) SetLike.coe
          {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := ⋯ : Opens α } = x} ↔
      x ∈ preimage f '' SetLike.coe '' B
⊢ image (α := Opens α) SetLike.coe
      {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := ⋯ : Opens α } = x} =
    preimage f '' SetLike.coe '' B

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
x : Set α
⊢ x ∈
      image (α := Opens α) SetLike.coe
        {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' (↑U : Set β), is_open' := ⋯ : Opens α } = x} ↔
    x ∈ preimage f '' SetLike.coe '' B

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
rw :
  (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
⊢ IsCompactElement s ↔ IsCompact (↑s : Set α)

Tactic:
rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup]

Premises used: isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i

Tactic:
⟨?_, fun H ι U hU => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
refine_1 :
  (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
refine_2 :
  ∀
    (H :
      ∀ {ι : Type u_2} (U : ι → Set α),
        (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i)
    (ι : Type u_2) (U : ι → Opens α) (hU : s ≤ iSup U), ∃ (t : Finset ι), s ≤ t.sup U
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α),
      (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨?_, fun H ι U hU => ?_⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
⊢ s ≤ ⨆ (i : ι), { carrier := U i, is_open' := ⋯ }

Tactic:
simpa
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
refine_1 :
  ∀ (t : Finset ι) (ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }),
    ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)

Premises used: TopologicalSpace.Opens.mk
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }
⊢ ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i

Tactic:
⟨t, Set.Subset.trans ht ?_⟩

Premises used: Set.Subset.trans, Exists.intro
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }
refine_1 : (↑(t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ : Opens α }) : Set α) ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨t, Set.Subset.trans ht ?_⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }
refine_1 :
  Subset.{u_2} (α := Set α)
    (⨆ a ∈ t, comp (β := Opens α) SetLike.coe (fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }) a)
    (⨆ a ∈ t, comp (β := Opens α) SetLike.coe (fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }) a)
⊢ (↑(t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ : Opens α }) : Set α) ⊆ ⋃ i ∈ t, U i

Tactic:
rw [coe_finset_sup, Finset.sup_eq_iSup]

Premises used: TopologicalSpace.Opens.coe_finset_sup, Finset.sup_eq_iSup
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ (t : Finset ι), s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
hU' : (↑s : Set α) ⊆ ⋃ (i : ι), U i
t : Finset ι
ht : s ≤ t.sup fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }
⊢ Subset.{u_2} (α := Set α)
    (⨆ a ∈ t, comp (β := Opens α) SetLike.coe (fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }) a)
    (⨆ a ∈ t, comp (β := Opens α) SetLike.coe (fun (i : ι) ↦ { carrier := U i, is_open' := ⋯ }) a)

Tactic:
rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ (↑s : Set α) ⊆ ⋃ (i : ι), (fun (i : ι) ↦ (↑(U i) : Set α)) i

Tactic:
simpa using show (s : Set α) ⊆ ↑(iSup U) from hU
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
refine_2 : ∀ (t : Finset ι) (ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)), ∃ (t : Finset ι), s ≤ t.sup U
⊢ ∃ (t : Finset ι), s ≤ t.sup U

Tactic:
obtain ⟨t, ht⟩ :=
      H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)

Premises used: SetLike.coe, TopologicalSpace.Opens.isOpen
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
⊢ ∃ (t : Finset ι), s ≤ t.sup U

Tactic:
⟨t, Set.Subset.trans ht ?_⟩

Premises used: Set.Subset.trans, Exists.intro
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
refine_2 : ⋃ i ∈ t, (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)
⊢ ∃ (t : Finset ι), s ≤ t.sup U

Tactic:
refine ⟨t, Set.Subset.trans ht ?_⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
refine_2 : ∀ (i : ι) (i_1 : i ∈ t), (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)
⊢ ⋃ i ∈ t, (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)

Tactic:
simp only [Set.iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
refine_2 : ∀ i ∈ t, U i ≤ t.sup U
⊢ ∀ (i : ι) (i_1 : i ∈ t), (↑(U i) : Set α) ⊆ (↑(t.sup U) : Set α)

Tactic:
change ∀ i ∈ t, U i ≤ t.sup U

Premises used: Finset.sup
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
⊢ ∀ i ∈ t, U i ≤ t.sup U

Tactic:
fun i => Finset.le_sup

Premises used: Finset.le_sup
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
H :
  ∀ {ι : Type u_2} (U : ι → Set α),
    (∀ (i : ι), IsOpen[inst] (U i)) → (↑s : Set α) ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), (↑s : Set α) ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : (↑s : Set α) ⊆ ⋃ i ∈ t, (↑(U i) : Set α)
⊢ ∀ i ∈ t, U i ≤ t.sup U

Tactic:
exact fun i => Finset.le_sup

Premises used: Finset.le_sup
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(α, β)
s : Set (Opens β)
⊢ (↑{ carrier := (⇑f : (a : α) → β) ⁻¹' (↑(sSup s) : Set β), is_open' := ⋯ : Opens α } : Set α) =
    (↑(sSup ((fun (s : Opens β) ↦ { carrier := (⇑f : (a : α) → β) ⁻¹' (↑s : Set β), is_open' := ⋯ }) '' s)) : Set α)

Tactic:
simp only [coe_sSup, preimage_iUnion, biUnion_image, coe_mk]

Premises used: TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.coe_sSup, Set.preimage_iUnion, Set.biUnion_image
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Eq (α := FrameHom (Opens α) (Opens α)) (comap (ContinuousMap.id α)) (FrameHom.id (Opens α))

Tactic:
FrameHom.ext fun _ => ext rfl

Premises used: FrameHom.ext, TopologicalSpace.Opens.ext, rfl