awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCommRingCat (goal)
Goal:
X Y Z : TopCommRingCat
val : X.α →+* Y.α
property : Continuous (X := X.α) (Y := Y.α) (⇑val : (a : X.α) → Y.α)
val_1 : Y.α →+* Z.α
property_1 : Continuous (X := Y.α) (Y := Z.α) (⇑val_1 : (a : Y.α) → Z.α)
⊢ Continuous (X := X.α) (Y := Z.α)
    (⇑((↑(Subtype.mk (p := fun (f : Y.α →+* Z.α) ↦ Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α)) val_1
                  property_1) :
              Y.α →+* Z.α).comp
          (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                property) :
            X.α →+* Y.α)) :
      (a : X.α) → Z.α)
have mk : Continuous (X := X.α) (Y := Z.α) (Function.comp (β := Y.α) (⇑val_1 : (a : Y.α) → Z.α) (⇑val : (a : X.α) → Y.α))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Category.TopPair (goal)
Goal:
X_1 Y_1 X Y Z : TopPair
X_2 Y_2 : TopCat
f : X_2 ⟶ Y_2
⊢ 𝟙 (snd (X := ofTopCat X_2)) ≫ map = map ≫ f
have w : ∀ (x : (↑(snd (X := ofTopCat X_2)) : Type u)),
  Eq (α := (↑(fst (X := ofTopCat Y_2)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (𝟙 (snd (X := ofTopCat X_2)) ≫ map) :
          (a : (↑snd : Type u)) → (↑fst : Type u))
        x :
      (↑(fst (X := ofTopCat Y_2)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            snd (X := ofTopCat X_2)) (Y := fst (X := ofTopCat Y_2)) (map ≫ f) :
          (a : (↑snd : Type u)) → (↑fst : Type u))
        x :
      (↑(fst (X := ofTopCat Y_2)) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopPair (hypothesis)
Goal:
X Y : TopPair
f g : X ⟶ Y
H : Homotopy f g
x : (↑(TopPair.snd (X := X)) : Type u)
t : (↑unitInterval : Type)
⊢ Eq (α := (↑(TopPair.fst (X := Y)) : Type u))
    ((H.fst : (a : (↑unitInterval : Type) × (↑TopPair.fst : Type u)) → (↑TopPair.fst : Type u))
        ((t,
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  TopPair.snd (X := X)) map :
                (a : (↑TopPair.snd : Type u)) → (↑TopPair.fst : Type u))
              x) :
          (↑unitInterval : Type) × (↑(TopPair.fst (X := X)) : Type u)) :
      (↑(TopPair.fst (X := Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            TopPair.snd (X := Y)) map :
          (a : (↑TopPair.snd : Type u)) → (↑TopPair.fst : Type u))
        ((H.snd : (a : (↑unitInterval : Type) × (↑TopPair.snd : Type u)) → (↑TopPair.snd : Type u)) (t, x) :
          (↑(TopPair.snd (X := Y)) : Type u)) :
      (↑(TopPair.fst (X := Y)) : Type u))
have this : Eq (α := (↑(TopPair.fst (X := Y)) : Type u))
  ((H.fst : (a : (↑unitInterval : Type) × (↑TopPair.fst : Type u)) → (↑TopPair.fst : Type u))
      (((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type))
            (x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t).2,
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                TopPair.snd (X := X)) map :
              (a : (↑TopPair.snd : Type u)) → (↑TopPair.fst : Type u))
            ((x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t) :
                (↑(TopPair.snd (X := X)) : Type u) × (↑I : Type u)).1) :
        (↑unitInterval : Type) × (↑(TopPair.fst (X := X)) : Type u)) :
    (↑(TopPair.fst (X := Y)) : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          TopPair.snd (X := Y)) map :
        (a : (↑TopPair.snd : Type u)) → (↑TopPair.fst : Type u))
      ((H.snd : (a : (↑unitInterval : Type) × (↑TopPair.snd : Type u)) → (↑TopPair.snd : Type u))
          (((I.homeomorph : (a : (↑I : Type u)) → (↑unitInterval : Type))
                (x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t).2,
              ((x, (I.homeomorph.symm : (a : (↑unitInterval : Type)) → (↑I : Type u)) t) :
                  (↑(TopPair.snd (X := X)) : Type u) × (↑I : Type u)).1) :
            (↑unitInterval : Type) × (↑(TopPair.snd (X := X)) : Type u)) :
        (↑(TopPair.snd (X := Y)) : Type u)) :
    (↑(TopPair.fst (X := Y)) : Type u))
Tactic: have := w_apply H (x, I.homeomorph.symm t)
-- Lean 4 proof step from Mathlib.Topology.Category.TopPair (goal)
Goal:
X_1 Y_1 X Y Z : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ map ▷ I ≫ Homotopy.h (F.fst.trans G.fst) = Homotopy.h (F.snd.trans G.snd) ≫ map
have w : ∀ (fst : (↑(TopPair.snd (X := X)) : Type u)) (snd : (↑I : Type u)),
  Eq (α := (↑(TopPair.fst (X := Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (map ▷ I ≫ Homotopy.h (F.fst.trans G.fst)) :
          (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑TopPair.fst : Type u))
        (fst, snd) :
      (↑(TopPair.fst (X := Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (Homotopy.h (F.snd.trans G.snd) ≫ map) :
          (a : (↑(TopPair.snd ⊗ I) : Type u)) → (↑TopPair.fst : Type u))
        (fst, snd) :
      (↑(TopPair.fst (X := Y)) : Type u))
Tactic: ext ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopPair (goal)
Goal:
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm = G.symm.trans F.symm
have fst : (F.trans G).symm.fst = (G.symm.trans F.symm).fst
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.Category.TopPair (goal)
Goal:
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
fst : (F.trans G).symm.fst = (G.symm.trans F.symm).fst
⊢ (F.trans G).symm = G.symm.trans F.symm
have snd : (F.trans G).symm.snd = (G.symm.trans F.symm).snd
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.Category.UniformSpace (goal)
Goal:
X Y : UniformSpaceCat
f : X.Hom Y
⊢ {
      hom' :=
        Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
          ((↑f.hom' : X.carrier → Y.carrier) ∘
            (↑(Hom.hom'
                  { hom' := Subtype.mk (p := fun (f : X.carrier → X.carrier) ↦ UniformContinuous f) id ⋯ : X.Hom X }) :
              X.carrier → X.carrier))
          ⋯ :
      X.Hom Y } =
    f
have hom' : {
      hom' :=
        Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
          ((↑f.hom' : X.carrier → Y.carrier) ∘
            (↑(Hom.hom'
                  { hom' := Subtype.mk (p := fun (f : X.carrier → X.carrier) ↦ UniformContinuous f) id sorry : X.Hom X }) :
              X.carrier → X.carrier))
          sorry :
      X.Hom Y }.hom' =
  f.hom'
Tactic: apply Hom.ext
-- Lean 4 proof step from Mathlib.Topology.Category.UniformSpace (goal)
Goal:
X Y : UniformSpaceCat
f : X.Hom Y
⊢ {
      hom' :=
        Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
          ((↑(Hom.hom'
                  { hom' := Subtype.mk (p := fun (f : Y.carrier → Y.carrier) ↦ UniformContinuous f) id ⋯ : Y.Hom Y }) :
              Y.carrier → Y.carrier) ∘
            (↑f.hom' : X.carrier → Y.carrier))
          ⋯ :
      X.Hom Y } =
    f
have hom' : {
      hom' :=
        Subtype.mk (p := fun (f : X.carrier → Y.carrier) ↦ UniformContinuous f)
          ((↑(Hom.hom'
                  { hom' := Subtype.mk (p := fun (f : Y.carrier → Y.carrier) ↦ UniformContinuous f) id sorry : Y.Hom Y }) :
              Y.carrier → Y.carrier) ∘
            (↑f.hom' : X.carrier → Y.carrier))
          sorry :
      X.Hom Y }.hom' =
  f.hom'
Tactic: apply Hom.ext
-- Lean 4 proof step from Mathlib.Topology.Category.UniformSpace (goal)
Goal:
W X Y Z : UniformSpaceCat
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ {
      hom' :=
        Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
          ((↑h.hom' : Y.carrier → Z.carrier) ∘
            (↑{
                    hom' :=
                      Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                        ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) ⋯ :
                    W.Hom Y }.hom' :
              W.carrier → Y.carrier))
          ⋯ :
      W.Hom Z } =
    {
      hom' :=
        Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
          ((↑{
                    hom' :=
                      Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                        ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) ⋯ :
                    X.Hom Z }.hom' :
              X.carrier → Z.carrier) ∘
            (↑f.hom' : W.carrier → X.carrier))
          ⋯ }
have hom' : {
      hom' :=
        Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
          ((↑h.hom' : Y.carrier → Z.carrier) ∘
            (↑{
                    hom' :=
                      Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                        ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) sorry :
                    W.Hom Y }.hom' :
              W.carrier → Y.carrier))
          sorry }.hom' =
  {
      hom' :=
        Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
          ((↑{
                    hom' :=
                      Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                        ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) sorry :
                    X.Hom Z }.hom' :
              X.carrier → Z.carrier) ∘
            (↑f.hom' : W.carrier → X.carrier))
          sorry :
      W.Hom Z }.hom'
Tactic: apply Hom.ext
-- Lean 4 proof step from Mathlib.Topology.Category.UniformSpace (goal)
Goal:
W X Y Z : UniformSpaceCat
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ {
        hom' :=
          Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
            ((↑h.hom' : Y.carrier → Z.carrier) ∘
              (↑{
                      hom' :=
                        Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                          ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) ⋯ :
                      W.Hom Y }.hom' :
                W.carrier → Y.carrier))
            ⋯ }.hom' =
    {
        hom' :=
          Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
            ((↑{
                      hom' :=
                        Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                          ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) ⋯ :
                      X.Hom Z }.hom' :
                X.carrier → Z.carrier) ∘
              (↑f.hom' : W.carrier → X.carrier))
            ⋯ :
        W.Hom Z }.hom'
have hom' : ∀ (x : W.carrier),
  (↑{
              hom' :=
                Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
                  ((↑h.hom' : Y.carrier → Z.carrier) ∘
                    (↑{
                            hom' :=
                              Subtype.mk (p := fun (f : W.carrier → Y.carrier) ↦ UniformContinuous f)
                                ((↑g.hom' : X.carrier → Y.carrier) ∘ (↑f.hom' : W.carrier → X.carrier)) sorry :
                            W.Hom Y }.hom' :
                      W.carrier → Y.carrier))
                  sorry :
              W.Hom Z }.hom' :
        W.carrier → Z.carrier)
      x =
    (↑{
              hom' :=
                Subtype.mk (p := fun (f : W.carrier → Z.carrier) ↦ UniformContinuous f)
                  ((↑{
                            hom' :=
                              Subtype.mk (p := fun (f : X.carrier → Z.carrier) ↦ UniformContinuous f)
                                ((↑h.hom' : Y.carrier → Z.carrier) ∘ (↑g.hom' : X.carrier → Y.carrier)) sorry :
                            X.Hom Z }.hom' :
                      X.carrier → Z.carrier) ∘
                    (↑f.hom' : W.carrier → X.carrier))
                  sorry :
              W.Hom Z }.hom' :
        W.carrier → Z.carrier)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.UniformSpace (goal)
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
⊢ (extensionHom (X.completionHom ≫ f)).hom = f
have h : ∀ (x : (completionFunctor.obj X).toUniformSpace.carrier),
  Eq (α := Y.toUniformSpace.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier)
            (extensionHom (X.completionHom ≫ f)).hom :
          (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
        x :
      Y.toUniformSpace.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f :
          (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
        x :
      Y.toUniformSpace.carrier)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.UniformSpace (goal)
Goal:
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
        { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
        fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
      Y
x : (completionFunctor.obj X').α
⊢ (↑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
            (CC := α) (extensionHom (f ≫ g))) :
        (completionFunctor.obj X').α → Y.α)
      x =
    Function.comp (β := (completionFunctor.obj X).α)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) (extensionHom g)) :
        (a : (completionFunctor.obj X).α) → Y.α)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) (X := completionFunctor.obj X') (Y :=
            completionFunctor.obj X)
            (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
              { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
              (Subtype.mk (p := fun (f : Completion X'.carrier → Completion X.carrier) ↦ UniformContinuous f)
                (Completion.map (⇑f.hom' : (a : X'.carrier) → X.carrier)) ⋯))) :
        (a : (completionFunctor.obj X').α) → (completionFunctor.obj X).α)
      x
have h : (↑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
          (CC := α) (extensionHom (f ≫ g))) :
      (completionFunctor.obj X').α → Y.α)
    x =
  Completion.extension
    ((↑(Hom.hom g) : X.carrier → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y).carrier) ∘
      (↑(Hom.hom f) : X'.carrier → X.carrier))
    x
Tactic: erw [Completion.extension_map (γ := Y) g.hom.2 f.hom.2]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClopen s ↔ frontier s = ∅
have rw : closure[inst] s = s ∧ interior s = s ↔ closure[inst] s ⊆ interior s
Tactic: rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, diff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s = s ∧ interior s = s ↔ closure[inst] s ⊆ interior s
have refine : ∀ (h : closure[inst] s ⊆ interior s), closure[inst] s = s ∧ interior s = s
Tactic: refine ⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
⊢ IsClopen (s ∩ a)
have refine : IsClosed[inst] (s ∩ a)
Tactic: refine ⟨?_, IsOpen.inter h.2 ha⟩
-- Lean 4 proof step from Mathlib.Topology.Clopen (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
⊢ IsClosed[inst] (s ∩ a)
have this : IsClosed[inst] (s ∩ bᶜ)
Tactic: have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
⊢ IsClosed[inst] (s ∩ a)
have h₁ : s ∩ a = s ∩ bᶜ
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
⊢ s ∩ a = s ∩ bᶜ
have h₁ : s ∩ bᶜ ⊆ s ∩ a
Tactic: refine (inter_subset_inter_right s hab.subset_compl_right).antisymm ?_
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ IsClopen (s ∩ a)
have rw : IsClopen (s ∩ (s ∩ a))
Tactic: rw [show s ∩ a = s ∩ (s ∩ a) by simp]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ IsClopen (s ∩ (s ∩ a))
have refine_1 : s ⊆ s ∩ a ∪ s ∩ b
Tactic: refine isClopen_inter_of_disjoint_cover_clopen h ?_ (h.2.inter ha) (h.2.inter hb) ?_
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_1 : s ⊆ s ∩ a ∪ s ∩ b
⊢ IsClopen (s ∩ (s ∩ a))
have refine_2 : Disjoint (s ∩ a) (s ∩ b)
Tactic: refine isClopen_inter_of_disjoint_cover_clopen h ?_ (h.2.inter ha) (h.2.inter hb) ?_
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ s ⊆ s ∩ a ∪ s ∩ b
have refine_1 : s ⊆ s ∩ (a ∪ b)
Tactic: rw [← inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)
have refine_2 : s ∩ a ∩ (s ∩ b) = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, inter_comm s b, ← inter_assoc, hab, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_2 : s ∩ a ∩ (s ∩ b) = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)
have refine_2₁ : s ∩ a ∩ (b ∩ s) = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, inter_comm s b, ← inter_assoc, hab, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_2 : s ∩ a ∩ (s ∩ b) = ∅
refine_2₁ : s ∩ a ∩ (b ∩ s) = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)
have refine_2₂ : s ∩ a ∩ b ∩ s = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, inter_comm s b, ← inter_assoc, hab, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_2 : s ∩ a ∩ (s ∩ b) = ∅
refine_2₁ : s ∩ a ∩ (b ∩ s) = ∅
refine_2₂ : s ∩ a ∩ b ∩ s = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)
have refine_2₃ : ∅ ∩ s = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, inter_comm s b, ← inter_assoc, hab, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_2 : s ∩ a ∩ (s ∩ b) = ∅
refine_2₁ : s ∩ a ∩ (b ∩ s) = ∅
refine_2₂ : s ∩ a ∩ b ∩ s = ∅
refine_2₃ : ∅ ∩ s = ∅
⊢ Disjoint (s ∩ a) (s ∩ b)
have refine_2₄ : Eq.{u + 1} (α := Set X) ∅ ∅
Tactic: rw [disjoint_iff_inter_eq_empty, inter_comm s b, ← inter_assoc, hab, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
U : Set X
⊢ Continuous[inst, _] U.boolIndicator ↔ IsClopen U
have rw : IsClopen (U.boolIndicator ⁻¹' {true}) ↔ IsClopen U
Tactic: rw [continuous_bool_rng true, preimage_boolIndicator_true]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
U : Set X
rw : IsClopen (U.boolIndicator ⁻¹' {true}) ↔ IsClopen U
⊢ Continuous[inst, _] U.boolIndicator ↔ IsClopen U
have rw₁ : IsClopen U ↔ IsClopen U
Tactic: rw [continuous_bool_rng true, preimage_boolIndicator_true]
-- Lean 4 proof step from Mathlib.Topology.Clopen (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s U : Set X
⊢ ContinuousOn U.boolIndicator s ↔ IsClopen (X := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U)
have rw : Continuous[instTopologicalSpaceSubtype, _] (s.restrict (π := fun (a : X) ↦ Bool) U.boolIndicator) ↔
  Continuous[instTopologicalSpaceSubtype, _] (boolIndicator (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' U))
Tactic: rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_isClopen]
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
⊢ ∃ (U : Clopens X), a.1 ∈ U ∧ ∃ (V : Clopens Y), a.2 ∈ V ∧ U ×ˢ V ≤ W
have hp : Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)
Tactic: have hp : Continuous (fun y : Y ↦ (a.1, y)) := .prodMk_right _
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)
V : Set Y := {y : Y | (a.1, y) ∈ W}
⊢ ∃ (U : Clopens X), a.1 ∈ U ∧ ∃ (V : Clopens Y), a.2 ∈ V ∧ U ×ˢ V ≤ W
have hV : IsCompact V
Tactic: have hV : IsCompact V := (W.2.1.preimage hp).isCompact
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous[inst_1, instTopologicalSpaceProd] fun (y : Y) ↦ (a.1, y)
V : Set Y := {y : Y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x : X | MapsTo (Prod.mk x) V (↑W : Set (X × Y))}
⊢ ∃ (U : Clopens X), a.1 ∈ U ∧ ∃ (V : Clopens Y), a.2 ∈ V ∧ U ×ˢ V ≤ W
have hUV : U ×ˢ V ⊆ (↑W : Set (X × Y))
Tactic: have hUV : U ×ˢ V ⊆ W := fun ⟨_, _⟩ hw ↦ hw.1 hw.2
-- Lean 4 proof step from Mathlib.Topology.ClopenBox (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
inst_3 : CompactSpace X
W : Clopens (X × Y)
⊢ ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
have choose! : ∀ (U : (x : X × Y) → Clopens X) (hxU : ∀ (x : X × Y) (h : x ∈ W), x.1 ∈ U x) (V : (x : X × Y) → Clopens Y)
  (hxV : ∀ (x : X × Y) (h : x ∈ W), x.2 ∈ V x) (hUV : ∀ (x : X × Y) (h : x ∈ W), U x ×ˢ V x ≤ W),
  ∃ (I : Finset (Prod.{u_1, u_2} (Clopens X) (Clopens Y))),
    W = I.sup fun (i : Prod.{u_1, u_2} (Clopens X) (Clopens Y)) ↦ i.1 ×ˢ i.2
Tactic: choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)