awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ (u : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        (preimage toCompacts ''
          (fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        u →
      ∀ x ∈ u,
        ∃ (v : Set (NonemptyCompacts α)),
          Membership.mem (γ := Set (Set (NonemptyCompacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
              v ∧
            x ∈ v ∧ v ⊆ u
have refine_2 : ∀ ⦃x : Set (Set α)⦄,
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} x →
    ∀ (x_1 : NonemptyCompacts α),
      Membership.mem (γ := Set (NonemptyCompacts α))
          (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}) x_1 →
        ∃ (v : Set (NonemptyCompacts α)),
          Membership.mem (γ := Set (Set (NonemptyCompacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
              v ∧
            x_1 ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
Tactic: simp_rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen.{u_1} (X := NonemptyCompacts α)
    {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_1 : IsOpen.{u_1} (X := NonemptyCompacts α)
  ({a : NonemptyCompacts α | (↑a : Set α) ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : NonemptyCompacts α | ((↑x : Set α) ∩ i).Nonempty})
Tactic: simp_rw [setOf_and, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
⊢ Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} u →
    ∀ (x : NonemptyCompacts α),
      Membership.mem (γ := Set (NonemptyCompacts α))
          (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) x →
        ∃ (v : Set (NonemptyCompacts α)),
          Membership.mem (γ := Set (Set (NonemptyCompacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
              v ∧
            x ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_2 : ∀ (hu : u.Finite) (huB : u ⊆ B) (x : NonemptyCompacts α),
  Membership.mem (γ := Set (NonemptyCompacts α))
      (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) x →
    ∃ (v : Set (NonemptyCompacts α)),
      Membership.mem (γ := Set (Set (NonemptyCompacts α)))
          ((fun (u : Set (Set α)) ↦
              {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
          v ∧
        x ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
Tactic: ⟨hu, huB⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
⊢ Membership.mem (γ := Set (NonemptyCompacts α))
      (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) K →
    ∃ (v : Set (NonemptyCompacts α)),
      Membership.mem (γ := Set (Set (NonemptyCompacts α)))
          ((fun (u : Set (Set α)) ↦
              {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_2 : ∀ (hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u) (hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty),
  ∃ (v : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
Tactic: ⟨hK₁, hK₂⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty
⊢ ∃ (v : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_2 : ∀ (hu : Set.Finite.{u_1} (α := Set α) ∅) (huB : ∅ ⊆ B) (hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ ∅)
  (hK₂ : ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K.toCompacts : Set α) ∩ U).Nonempty),
  ∃ (v : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        v ∧
      K ∈ v ∧
        v ⊆
          toCompacts ⁻¹'
            {K : Compacts α |
              (↑K : Set α) ⊆ ⋃₀ ∅ ∧ ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K : Set α) ∩ U).Nonempty}
Tactic: rcases eq_empty_or_nonempty u with rfl | hu'
Cleared hypotheses: u, hu, huB, hK₁, hK₂
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty
refine_2 :
  ∀ (hu : Set.Finite.{u_1} (α := Set α) ∅) (huB : ∅ ⊆ B) (hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ ∅)
    (hK₂ : ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K.toCompacts : Set α) ∩ U).Nonempty),
    ∃ (v : Set (NonemptyCompacts α)),
      Membership.mem (γ := Set (Set (NonemptyCompacts α)))
          ((fun (u : Set (Set α)) ↦
              {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
          v ∧
        K ∈ v ∧
          v ⊆
            toCompacts ⁻¹'
              {K : Compacts α |
                (↑K : Set α) ⊆ ⋃₀ ∅ ∧
                  ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K : Set α) ∩ U).Nonempty}
⊢ ∃ (v : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_2₁ : ∀ (hu' : u.Nonempty),
  ∃ (v : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
Tactic: rcases eq_empty_or_nonempty u with rfl | hu'
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
K : NonemptyCompacts α
hu : Set.Finite.{u_1} (α := Set α) ∅
huB : ∅ ⊆ B
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ ∅
hK₂ : ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K.toCompacts : Set α) ∩ U).Nonempty
⊢ ∃ (v : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        v ∧
      K ∈ v ∧
        v ⊆
          toCompacts ⁻¹'
            {K : Compacts α |
              (↑K : Set α) ⊆ ⋃₀ ∅ ∧ ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K : Set α) ∩ U).Nonempty}
have refine_2 : ¬Set.Nonempty.{u_1} (α := α) (⋃₀ ∅)
Tactic: absurd K.nonempty.mono hK₁
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty
hu' : u.Nonempty
⊢ ∃ (v : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_2 : ∃ (x : Set (Set α)),
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} x ∧
    Membership.mem (γ := Set (NonemptyCompacts α))
        {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
      Subset.{u_1} (α := Set (NonemptyCompacts α))
        {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
        (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty})
Tactic: rw [exists_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty
hu' : u.Nonempty
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} x ∧
      Membership.mem (γ := Set (NonemptyCompacts α))
          {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
        Subset.{u_1} (α := Set (NonemptyCompacts α))
          {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
          (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty})
have refine_2 : Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} u ∧
  Membership.mem (γ := Set (NonemptyCompacts α))
      {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} K ∧
    Subset.{u_1} (α := Set (NonemptyCompacts α))
      {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
      (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty})
Tactic: exists u
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ ContinuousSup.{u_1} (NonemptyCompacts α)
have continuous_sup : Continuous (Y := NonemptyCompacts α) fun (p : NonemptyCompacts α × NonemptyCompacts α) ↦ p.1 ⊔ p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ Continuous (Y := NonemptyCompacts α) fun (p : NonemptyCompacts α × NonemptyCompacts α) ↦ p.1 ⊔ p.2
have continuous_sup : Continuous (Y := Compacts α) fun (x : NonemptyCompacts α × NonemptyCompacts α) ↦ x.1.toCompacts ⊔ x.2.toCompacts
Tactic: simp_rw [isEmbedding_toCompacts.continuous_iff, Function.comp_def, toCompacts_sup]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Continuous (Y := NonemptyCompacts (α × β)) fun (p : Prod.{u_1, u_2} (NonemptyCompacts α) (NonemptyCompacts β)) ↦
    p.1 ×ˢ p.2
have simp_rw : Continuous (Y := Compacts (α × β)) fun (x : Prod.{u_1, u_2} (NonemptyCompacts α) (NonemptyCompacts β)) ↦
  x.1.toCompacts ×ˢ x.2.toCompacts
Tactic: simp_rw [isEmbedding_toCompacts.continuous_iff, Function.comp_def, toCompacts_prod]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (NonemptyCompacts α)
hs : IsCompact S
⊢ IsCompact.{u_1} (X := α) (⋃ K ∈ S, (↑K : Set α))
have h : Eq.{u_1 + 1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ K ∈ toCompacts '' S, (↑K : Set α))
Tactic: convert! Compacts.isCompact_biUnion_coe_of_isCompact (hs.image continuous_toCompacts)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (NonemptyCompacts α)
hs : IsCompact S
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ K ∈ toCompacts '' S, (↑K : Set α))
have h : Eq.{u_1 + 1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ y ∈ S, (↑y.toCompacts : Set α))
Tactic: simp_rw [biUnion_image, coe_toCompacts]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ CompactSpace.{u_1} (NonemptyCompacts α) ↔ CompactSpace α
have refine : ∀ (h : CompactSpace.{u_1} (NonemptyCompacts α)), IsCompact.{u_1} (X := α) univ
Tactic: refine ⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
⊢ IsCompact.{u_1} (X := α) univ
have h₁ : Eq.{u_1 + 1} (α := Set α) univ
  (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α))
Tactic: convert! isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
⊢ Eq.{u_1 + 1} (α := Set α) univ
    (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α))
have h₁ : Eq.{u_1 + 1} (α := Set α)
  (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α)) univ
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α)) univ
have h₁ : ∀ (x : α), ∃ (i : NonemptyCompacts α), x ∈ (↑i : Set α)
Tactic: simp_rw [biUnion_univ, eq_univ_iff_forall, mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoncompactSpace.{u_1} (NonemptyCompacts α) ↔ NoncompactSpace α
have simp_rw : ¬CompactSpace.{u_1} (NonemptyCompacts α) ↔ ¬CompactSpace α
Tactic: simp_rw [← not_compactSpace_iff, compactSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ LocallyCompactSpace.{u_1} (NonemptyCompacts α) ↔ LocallyCompactSpace α
have refine : LocallyCompactSpace.{u_1} (NonemptyCompacts α) → ∀ (x : α) (U : Set α) (hU : U ∈ 𝓝 x), ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
Tactic: refine ⟨fun _ => ⟨fun x U hU => ?_⟩, fun _ => inferInstance⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
have hU₁ : (↑{x} : Set α) ⊆ interior U
Tactic: rw [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, ← coe_singleton] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
have obtain : ∀ (K : Set (NonemptyCompacts α)) (hK : IsCompact K) (hxK : {x} ∈ interior K)
  (hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}), ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
Tactic: obtain ⟨K, hK, hxK, hKU⟩ := exists_compact_subset (isOpen_subsets_of_isOpen isOpen_interior) hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
have refine : ⋃ L ∈ K, (↑L : Set α) ∈ 𝓝 x
Tactic: refine ⟨⋃ L ∈ K, L, ?_, iUnion₂_subset <| by grind [interior_subset],
    isCompact_biUnion_coe_of_isCompact hK⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : {x} ∈ interior K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
⊢ ⋃ L ∈ K, (↑L : Set α) ∈ 𝓝 x
have hxK₁ : Membership.mem (γ := Filter (NonemptyCompacts α)) (𝓝 {x}) K
Tactic: rw [mem_interior_iff_mem_nhds] at hxK
Cleared hypotheses: hxK, hKU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : Membership.mem (γ := Filter (NonemptyCompacts α)) (𝓝 {x}) K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
⊢ ⋃ L ∈ K, (↑L : Set α) ∈ 𝓝 x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) ((fun (x : α) ↦ {x}) ⁻¹' K) x → Membership.mem (γ := Set α) (⋃ L ∈ K, (↑L : Set α)) x}
    a
Tactic: filter_upwards [continuous_singleton.tendsto x hxK] with y hy using mem_iUnion₂_of_mem hy rfl
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h_1 : LocallyCompactSpace.{u_1} (NonemptyCompacts α)
x : α
U : Set α
hU : (↑{x} : Set α) ⊆ interior U
K : Set (NonemptyCompacts α)
hK : IsCompact K
hxK : Membership.mem (γ := Filter (NonemptyCompacts α)) (𝓝 {x}) K
hKU : K ⊆ {K : NonemptyCompacts α | (↑K : Set α) ⊆ interior U}
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) ((fun (x : α) ↦ {x}) ⁻¹' K) x →
          Membership.mem (γ := Set α) (⋃ L ∈ K, (↑L : Set α)) x}
      a
⊢ ⋃ L ∈ K, (↑L : Set α) ∈ 𝓝 x
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α) ((fun (x : α) ↦ {x}) ⁻¹' K) a → Membership.mem (γ := Set α) (⋃ L ∈ K, (↑L : Set α)) a
Tactic: filter_upwards [continuous_singleton.tendsto x hxK] with y hy using mem_iUnion₂_of_mem hy rfl
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (hypothesis)
Goal:
X : TopCat
p₀ : (↑X : Type u)
C : Type v
inst : Category.{u, v} C
inst_1 : Abelian.{u, v} C
inst_2 : HasColimits.{u, v} C
⊢ Functor.Additive (C := Presheaf C X)
    (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op ⋙ colim)
have this : Functor.Additive (C := CategoryTheory.Functor.{u, u, u, v} (Opens (↑X : Type u))ᵒᵖ C)
  (Functor.obj (Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens (↑X : Type u))ᵒᵖ C) (OpenNhds.inclusion p₀).op)
Tactic: have : ((Functor.whiskeringLeft _ _ C).obj (OpenNhds.inclusion p₀).op).Additive := ⟨by cat_disch⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (hypothesis)
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
⊢ ShortComplex.ShortExact (S.map (forget C X ⋙ stalkFunctor C p₀))
have this : ∀ (S : ShortComplex (Sheaf C X)),
  S.ShortExact →
    ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
      Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
        (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
Tactic: have := ((forget C X ⋙ stalkFunctor C p₀).preservesFiniteColimits_tfae.out 3 0).mp
      (inferInstance : (PreservesFiniteColimits _))
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (goal)
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
⊢ ShortComplex.ShortExact (S.map (forget C X ⋙ stalkFunctor C p₀))
have refine : Mono (X := ShortComplex.X₁ (S.map (forget C X ⋙ stalkFunctor C p₀)))
  (ShortComplex.f (S.map (forget C X ⋙ stalkFunctor C p₀)))
Tactic: refine ShortComplex.ShortExact.mk' (this S h).left ?_ (this S h).right
-- Lean 4 proof step from Mathlib.Topology.Sheaves.Abelian (hypothesis)
Goal:
X_1 : TopCat
C : Type v
inst : Category.{u, v} C
inst_1 : HasColimits.{u, v} C
inst_2 : HasLimits.{u, v} C
FC : C → C → Type u_1
CC : C → Type u
inst_3 : (X Y : C) → FunLike.{u_1 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : Abelian.{u, v} C
X : TopCat
p₀ : (↑X : Type u)
S : ShortComplex (Sheaf C X)
h : S.ShortExact
this :
  ∀ (S : ShortComplex (Sheaf C X)),
    S.ShortExact →
      ShortComplex.Exact (S.map (forget C X ⋙ stalkFunctor C p₀)) ∧
        Epi (X := Functor.obj (forget C X ⋙ stalkFunctor C p₀) S.X₂)
          (CategoryTheory.Functor.map (forget C X ⋙ stalkFunctor C p₀) S.g)
⊢ Mono (X := ShortComplex.X₁ (S.map (forget C X ⋙ stalkFunctor C p₀)))
    (ShortComplex.f (S.map (forget C X ⋙ stalkFunctor C p₀)))
have this₁ : Mono S.f
Tactic: have := h.2