awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
t : Set (ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
h : IsOpen t
s : Set (↑(Metric.closedBall 0 1) : Type)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs :
  Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
      r =
    s
hst : ULift.down ⁻¹' s = t
rw :
  ∃ (t : Set (↑(Metric.sphere 0 1) : Type)),
    IsOpen t ∧
      ULift.down ⁻¹' t =
        Set.preimage (β := ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
          (fun (x : ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type)) ↦
            match (motive :=
              ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
            | { down := ⟨p, hp⟩ } =>
              {
                down :=
                  Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                    Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ })
          (ULift.down ⁻¹'
            Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
              r)
⊢ IsOpen (X := ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type))
    ((fun (x : ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type)) ↦
        match (motive :=
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
        | { down := ⟨p, hp⟩ } =>
          {
            down :=
              Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ }) ⁻¹'
      t)

Tactic:
rw [isOpen_induced_iff, ← hst, ← hrs]

Premises used: isOpen_induced_iff
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
t : Set (ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
h : IsOpen t
s : Set (↑(Metric.closedBall 0 1) : Type)
r : Set (EuclideanSpace ℝ (Fin n))
hro : IsOpen r
hrs :
  Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
        Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
      r =
    s
hst : ULift.down ⁻¹' s = t
rw :
  ∃ (t : Set (↑(Metric.ball 0 1) : Type)),
    IsOpen t ∧
      ULift.down ⁻¹' t =
        Set.preimage (β := ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
          (fun (x : ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)) ↦
            match (motive :=
              ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type)) x with
            | { down := ⟨p, hp⟩ } =>
              {
                down :=
                  Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                    Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ })
          (ULift.down ⁻¹'
            Subtype.val (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) ⁻¹'
              r)
⊢ IsOpen (X := ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type))
    ((fun (x : ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type)) ↦
        match (motive := ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) → ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))
          x with
        | { down := ⟨p, hp⟩ } =>
          {
            down :=
              Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.closedBall 0 1) x) p ⋯ }) ⁻¹'
      t)

Tactic:
rw [isOpen_induced_iff, ← hst, ← hrs]

Premises used: isOpen_induced_iff
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x
this :
  ∀ (y : EuclideanSpace ℝ (Fin n)) (hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) y),
    Eq (α := (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (diskBoundaryInclusion n) :
              (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
              ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
          (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (diskBoundaryInclusion n) :
              (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) y hy :
              ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
          (↑(𝔻 n) : Type u_1)) →
      {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } =
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) y hy }
⊢ ∀ ⦃a₂ : (↑(∂𝔻 n) : Type u_1)⦄,
    Eq (α := (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (diskBoundaryInclusion n) :
              (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
              ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
          (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (diskBoundaryInclusion n) :
              (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            a₂ :
          (↑(𝔻 n) : Type u_1)) →
      {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } =
        a₂

Tactic:
⟨y, hy⟩
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x
y : EuclideanSpace ℝ (Fin n)
hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) y
h :
  Eq (α := (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (diskBoundaryInclusion n) :
          (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (diskBoundaryInclusion n) :
          (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) y hy :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
⊢ x = y

Tactic:
simpa [diskBoundaryInclusion, disk] using h

Premises used: TopCat.disk, TopCat.diskBoundaryInclusion
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x
h :
  Eq (α := (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (diskBoundaryInclusion n) :
          (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (diskBoundaryInclusion n) :
          (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hy :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
⊢ {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
      ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } =
    {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hy }

Tactic:
congr
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x
this :
  ∀ (y : EuclideanSpace ℝ (Fin n)) (hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) y),
    Eq (α := (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (ballInclusion n) :
              (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hx :
              ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } :
          (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (ballInclusion n) :
              (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) y hy :
              ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } :
          (↑(𝔻 n) : Type u_1)) →
      {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } =
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) y hy }
⊢ ∀ ⦃a₂ : (↑(𝔹 n) : Type u_1)⦄,
    Eq (α := (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (ballInclusion n) :
              (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            {
              down :=
                Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                  Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hx :
              ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } :
          (↑(𝔻 n) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (ballInclusion n) :
              (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
            a₂ :
          (↑(𝔻 n) : Type u_1)) →
      {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } =
        a₂

Tactic:
⟨y, hy⟩
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x
y : EuclideanSpace ℝ (Fin n)
hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) y
h :
  Eq (α := (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (ballInclusion n) :
          (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (ballInclusion n) :
          (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) y hy :
          ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
⊢ x = y

Tactic:
simpa [ballInclusion, disk] using h

Premises used: TopCat.disk, TopCat.ballInclusion
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x
h :
  Eq (α := (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (ballInclusion n) :
          (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (ballInclusion n) :
          (a : (↑(𝔹 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hy :
          ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
⊢ {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hx :
      ULift.{u_1, 0} (↑(Metric.ball 0 1) : Type) } =
    {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.ball 0 1) x) x hy }

Tactic:
congr
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
⊢ CompactSpace.{u_1} (ULift.{u_1, 0} (↑(Metric.closedBall 0 1) : Type))

Tactic:
Homeomorph.compactSpace Homeomorph.ulift.symm

Premises used: Homeomorph.ulift, Homeomorph.compactSpace, Homeomorph.symm
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
convert_1 : CompactSpace (↑(Metric.closedBall 0 1) : Type)
⊢ CompactSpace.{u_1} (↑(𝔻 n) : Type u_1)

Tactic:
convert! Homeomorph.compactSpace Homeomorph.ulift.symm

Premises used: Homeomorph.ulift, Homeomorph.compactSpace, Homeomorph.symm
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
⊢ CompactSpace (↑(Metric.closedBall 0 1) : Type)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
⊢ CompactSpace.{u_1} (ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type))

Tactic:
Homeomorph.compactSpace Homeomorph.ulift.symm

Premises used: Homeomorph.ulift, Homeomorph.compactSpace, Homeomorph.symm
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
convert_1 : CompactSpace (↑(Metric.sphere 0 1) : Type)
⊢ CompactSpace.{u_1} (↑(∂𝔻 n) : Type u_1)

Tactic:
convert! Homeomorph.compactSpace Homeomorph.ulift.symm

Premises used: Homeomorph.ulift, Homeomorph.compactSpace, Homeomorph.symm
-- Module: Mathlib.Topology.Category.TopCat.Sphere
Goal:
n : ℕ
⊢ CompactSpace (↑(Metric.sphere 0 1) : Type)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ Continuous (X := ULift.{v, u} (↑X : Type u)) (Y := ULift.{v, u} (↑Y : Type u))
    (ULift.map
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
X Y : TopCat
f : X ⟶ Y
x : (↑X : Type u)
⊢ Eq (α := (↑(uliftFunctor.obj Y) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (uliftFunctor.map f) :
          (a : (↑(uliftFunctor.obj X) : Type (max u v))) → (↑(uliftFunctor.obj Y) : Type (max u v)))
        ((X.uliftFunctorObjHomeo : (a : (↑X : Type u)) → (↑(uliftFunctor.obj X) : Type (max u v))) x) :
      (↑(uliftFunctor.obj Y) : Type (max u v)))
    ((Y.uliftFunctorObjHomeo : (a : (↑Y : Type u)) → (↑(uliftFunctor.obj Y) : Type (max u v)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑X : Type u)) → (↑Y : Type u))
          x) :
      (↑(uliftFunctor.obj Y) : Type (max u v)))

Tactic:
rfl

Premises used: ULift.map, rfl
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
X Y : TopCat
f : X ⟶ Y
x : (↑(uliftFunctor.obj X) : Type (max u v))
⊢ Eq (α := (↑Y : Type u))
    ((Y.uliftFunctorObjHomeo.symm : (a : (↑(uliftFunctor.obj Y) : Type (max u v))) → (↑Y : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (uliftFunctor.map f) :
            (a : (↑(uliftFunctor.obj X) : Type (max u v))) → (↑(uliftFunctor.obj Y) : Type (max u v)))
          x) :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Y : Type u))
        ((X.uliftFunctorObjHomeo.symm : (a : (↑(uliftFunctor.obj X) : Type (max u v))) → (↑X : Type u)) x :
          (↑X : Type u)) :
      (↑Y : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
X Y : TopCat
f : uliftFunctor.obj X ⟶ uliftFunctor.obj Y
⊢ Continuous.{u, u} (X := (↑X : Type u)) (Y := (↑Y : Type u))
    (ULift.down ∘
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) f) :
          (a : (↑(uliftFunctor.obj X) : Type (max u v))) → (↑(uliftFunctor.obj Y) : Type (max u v))) ∘
        ULift.up)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
⊢ uliftFunctor.Full

Tactic:
uliftFunctorFullyFaithful.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, TopCat.uliftFunctorFullyFaithful
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
⊢ uliftFunctor.Faithful

Tactic:
uliftFunctorFullyFaithful.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, TopCat.uliftFunctorFullyFaithful
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
⊢ PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.mk, CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.PreservesLimit.mk
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
refine :
  ∀ {J : Type w} [inst : Category.{w', w} J] {K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat} {c : Cone K}
    (hc : IsLimit c), Nonempty (IsLimit (uliftFunctor.mapCone c))
⊢ PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor

Tactic:
refine ⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
rw :
  Eq (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
hc₁ :
  IsLimit (F :=
    (K ⋙ uliftFunctor) ⋙
      forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
    (Functor.mapCone
      (forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
      (uliftFunctor.mapCone c))
⊢ Nonempty (IsLimit (uliftFunctor.mapCone c))

Tactic:
rw [nonempty_isLimit_iff_eq_induced]

Premises used: TopCat.nonempty_isLimit_iff_eq_induced
-- Module: Mathlib.Topology.Category.TopCat.ULift
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
⊢ Eq (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm