awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    Eq.{u_2 + 1} (α := β) ((F s hs : (a : (↑s : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxi) : β)
      ((F t ht : (a : (↑t : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxj) : β)
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
x : (↑s : Type u_1)
x' : (↑(↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ A) s hs) : Set α) : Type u_1) := x
⊢ Eq.{u_2 + 1} (α := β)
    ((let F_1 : (i : (↑A : Type u_1)) → ContinuousMap.{u_1, u_2} (↑(↑i : Set α) : Type u_1) β :=
            fun (i : (↑A : Type u_1)) ↦ F (↑i : Set α) ⋯;
          liftCover (Subtype.val (p := fun (x : Set α) ↦ x ∈ A)) F_1 ⋯ ⋯ :
          (a : α) → β)
        (↑x : α) :
      β)
    ((F s hs : (a : (↑s : Type u_1)) → β) x : β)

Tactic:
ContinuousMap.liftCover_coe x'

Premises used: ContinuousMap.liftCover_coe
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    Eq.{u_2 + 1} (α := β) ((F s hs : (a : (↑s : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxi) : β)
      ((F t ht : (a : (↑t : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxj) : β)
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
x : (↑s : Type u_1)
x' : (↑(↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ A) s hs) : Set α) : Type u_1) := x
⊢ Eq.{u_2 + 1} (α := β)
    ((let F_1 : (i : (↑A : Type u_1)) → ContinuousMap.{u_1, u_2} (↑(↑i : Set α) : Type u_1) β :=
            fun (i : (↑A : Type u_1)) ↦ F (↑i : Set α) ⋯;
          liftCover (Subtype.val (p := fun (x : Set α) ↦ x ∈ A)) F_1 ⋯ ⋯ :
          (a : α) → β)
        (↑x : α) :
      β)
    ((F s hs : (a : (↑s : Type u_1)) → β) x : β)

Tactic:
exact ContinuousMap.liftCover_coe x'

Premises used: ContinuousMap.liftCover_coe
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    Eq.{u_2 + 1} (α := β) ((F s hs : (a : (↑s : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxi) : β)
      ((F t ht : (a : (↑t : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxj) : β)
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
⊢ restrict s (liftCover' A F hF hA) = F s hs

Tactic:
ext <| liftCover_coe' (hF := hF) (hA := hA)

Premises used: ContinuousMap.ext, ContinuousMap.liftCover_coe'
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
rw :
  Continuous[inst, instTopologicalSpaceQuotient]
    ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y))
⊢ Continuous[inst_1, instTopologicalSpaceQuotient] (Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun

Tactic:
rw [hf.continuous_iff]

Premises used: Topology.IsQuotientMap.continuous_iff
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
⊢ Continuous[inst, instTopologicalSpaceQuotient] Quotient.mk'

Tactic:
continuous_quotient_mk'

Premises used: continuous_quotient_mk'
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
h : (Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y) = Quotient.mk'
⊢ Continuous[inst, instTopologicalSpaceQuotient]
    ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y))

Tactic:
convert! continuous_quotient_mk'

Premises used: continuous_quotient_mk'
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
h :
  ∀ (x : X), ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y)) x = Quotient.mk' x
⊢ (Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y) = Quotient.mk'

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
x : X
h :
  Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y)
    ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯ : (a : Quotient (Setoid.ker (⇑f : (a : X) → Y))) → Y)
        (Quotient.mk' x) :
      Y)
⊢ ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y)) x = Quotient.mk' x

Tactic:
simp only [Equiv.invFun_as_coe, Function.comp_apply,
      (Setoid.quotientKerEquivOfSurjective f hf.surjective).symm_apply_eq]

Premises used: Equiv.invFun_as_coe, Topology.IsQuotientMap.surjective, Equiv.symm_apply_eq, Function.comp_apply, Setoid.quotientKerEquivOfSurjective, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y)
    ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯ : (a : Quotient (Setoid.ker (⇑f : (a : X) → Y))) → Y)
        (Quotient.mk' x) :
      Y)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
g : C(X, Z)
h : FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z) (⇑f : (a : X) → Y)
h₁ : ∀ (a : X), Eq.{u_3 + 1} (α := Z) (((hf.lift g h).comp f : (a : X) → Z) a : Z) ((g : (a : X) → Z) a : Z)
⊢ (hf.lift g h).comp f = g

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
g : C(X, Z)
h : FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z) (⇑f : (a : X) → Y)
a : X
⊢ Eq.{u_3 + 1} (α := Z) (((hf.lift g h).comp f : (a : X) → Z) a : Z) ((g : (a : X) → Z) a : Z)

Tactic:
simpa using h (Function.rightInverse_surjInv _ _)

Premises used: Function.rightInverse_surjInv
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
g_1 : C(X, Z)
h_1 : FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g_1 : (a : X) → Z) (⇑f : (a : X) → Y)
g : C(Y, Z)
x x_1 : X
h : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x_1 : Y)
simp :
  Eq.{u_3 + 1} (α := Z) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)
    ((g : (a : Y) → Z) ((f : (a : X) → Y) x_1 : Y) : Z)
⊢ Eq.{u_3 + 1} (α := Z) ((g.comp f : (a : X) → Z) x : Z) ((g.comp f : (a : X) → Z) x_1 : Z)

Tactic:
simp only [ContinuousMap.comp_apply]

Premises used: ContinuousMap.comp_apply
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
g_1 : C(X, Z)
h_1 : FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g_1 : (a : X) → Z) (⇑f : (a : X) → Y)
g : C(Y, Z)
x x_1 : X
h : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x_1 : Y)
rw rw₁ :
  Eq.{u_3 + 1} (α := Z) ((g : (a : Y) → Z) ((f : (a : X) → Y) x_1 : Y) : Z)
    ((g : (a : Y) → Z) ((f : (a : X) → Y) x_1 : Y) : Z)
⊢ Eq.{u_3 + 1} (α := Z) ((g : (a : Y) → Z) ((f : (a : X) → Y) x : Y) : Z)
    ((g : (a : Y) → Z) ((f : (a : X) → Y) x_1 : Y) : Z)

Tactic:
rw [h]
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
g : C(X, Z)
h : FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z) (⇑f : (a : X) → Y)
x :
  { g : C(X, Z) //
    FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z) (⇑f : (a : X) → Y) }
⊢ (fun (g : C(Y, Z)) ↦
        (Subtype.mk (p := fun (g : C(X, Z)) ↦
            FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z) (⇑f : (a : X) → Y))
            (g.comp f) ⋯ :
          { g : C(X, Z) //
            FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
              (⇑f : (a : X) → Y) }))
      ((fun
            (g :
              { g : C(X, Z) //
                FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                  (⇑f : (a : X) → Y) }) ↦
          hf.lift (↑g : C(X, Z)) ⋯)
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
g_1 : C(X, Z)
h : FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g_1 : (a : X) → Z) (⇑f : (a : X) → Y)
g : C(Y, Z)
h₁ :
  ∀ (a : Y),
    Eq.{u_3 + 1} (α := Z)
      (((fun
                  (g :
                    { g : C(X, Z) //
                      FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                        (⇑f : (a : X) → Y) }) ↦
                hf.lift (↑g : C(X, Z)) ⋯)
              ((fun (g : C(Y, Z)) ↦
                  (Subtype.mk (p := fun (g : C(X, Z)) ↦
                      FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                        (⇑f : (a : X) → Y))
                      (g.comp f) ⋯ :
                    { g : C(X, Z) //
                      FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                        (⇑f : (a : X) → Y) }))
                g) :
            (a : Y) → Z)
          a :
        Z)
      ((g : (a : Y) → Z) a : Z)
⊢ (fun
          (g :
            { g : C(X, Z) //
              FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                (⇑f : (a : X) → Y) }) ↦
        hf.lift (↑g : C(X, Z)) ⋯)
      ((fun (g : C(Y, Z)) ↦
          (Subtype.mk (p := fun (g : C(X, Z)) ↦
              FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                (⇑f : (a : X) → Y))
              (g.comp f) ⋯ :
            { g : C(X, Z) //
              FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                (⇑f : (a : X) → Y) }))
        g) =
    g

Tactic:
ext a
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y)
g_1 : C(X, Z)
h : FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g_1 : (a : X) → Z) (⇑f : (a : X) → Y)
g : C(Y, Z)
a : Y
⊢ Eq.{u_3 + 1} (α := Z)
    (((fun
                (g :
                  { g : C(X, Z) //
                    FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                      (⇑f : (a : X) → Y) }) ↦
              hf.lift (↑g : C(X, Z)) ⋯)
            ((fun (g : C(Y, Z)) ↦
                (Subtype.mk (p := fun (g : C(X, Z)) ↦
                    FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                      (⇑f : (a : X) → Y))
                    (g.comp f) ⋯ :
                  { g : C(X, Z) //
                    FactorsThrough.{u_1 + 1, u_2 + 1, u_3 + 1} (α := X) (β := Y) (γ := Z) (⇑g : (a : X) → Z)
                      (⇑f : (a : X) → Y) }))
              g) :
          (a : Y) → Z)
        a :
      Z)
    ((g : (a : Y) → Z) a : Z)

Tactic:
simpa using congrArg g (Function.rightInverse_surjInv hf.surjective a)

Premises used: congrArg, Topology.IsQuotientMap.surjective, Function.rightInverse_surjInv, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq (α := C(α, α)) (↑(Homeomorph.refl α) : C(α, α)) (ContinuousMap.id α)

Tactic:
rfl

Premises used: toContinuousMap, ContinuousMap.id, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
g : β ≃ₜ γ
⊢ Eq (α := C(α, γ)) (↑(f.trans g) : C(α, γ)) (ContinuousMap.comp (↑g : C(β, γ)) (↑f : C(α, β)))

Tactic:
rfl

Premises used: ContinuousMap.comp, toContinuousMap, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
rw : Eq (α := C(α, α)) (↑(f.trans f.symm) : C(α, α)) (ContinuousMap.id α)
rw₁ : Eq (α := C(α, α)) (↑(Homeomorph.refl α) : C(α, α)) (ContinuousMap.id α)
rw₂ rw₃ : Eq (α := C(α, α)) (ContinuousMap.id α) (ContinuousMap.id α)
⊢ Eq (α := C(α, α)) (ContinuousMap.comp (↑f.symm : C(β, α)) (↑f : C(α, β))) (ContinuousMap.id α)

Tactic:
rw [← coe_trans, self_trans_symm, coe_refl]

Premises used: Homeomorph.self_trans_symm, Homeomorph.coe_refl, Homeomorph.coe_trans
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
rw : Eq (α := C(β, β)) (↑(f.symm.trans f) : C(β, β)) (ContinuousMap.id β)
rw₁ : Eq (α := C(β, β)) (↑(Homeomorph.refl β) : C(β, β)) (ContinuousMap.id β)
rw₂ rw₃ : Eq (α := C(β, β)) (ContinuousMap.id β) (ContinuousMap.id β)
⊢ Eq (α := C(β, β)) (ContinuousMap.comp (↑f : C(α, β)) (↑f.symm : C(β, α))) (ContinuousMap.id β)

Tactic:
rw [← coe_trans, symm_trans_self, coe_refl]

Premises used: Homeomorph.coe_refl, Homeomorph.coe_trans, Homeomorph.symm_trans_self
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
⊢ ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε

Tactic:
simp_rw [Equicontinuous, Metric.equicontinuousAt_iff_pair] at H

Premises used: Equicontinuous, Metric.equicontinuousAt_iff_pair
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
⊢ IsCompact A

Tactic:
TotallyBounded.isCompact_of_isClosed ?_ closed

Premises used: TotallyBounded.isCompact_of_isClosed
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
refine : TotallyBounded A
⊢ IsCompact A

Tactic:
refine TotallyBounded.isCompact_of_isClosed ?_ closed

Premises used: TotallyBounded.isCompact_of_isClosed
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
⊢ TotallyBounded A

Tactic:
totallyBounded_of_finite_discretization fun ε ε0 => ?_

Premises used: Metric.totallyBounded_of_finite_discretization
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
refine :
  ∀ (ε : ℝ) (ε0 : ε > 0),
    ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
      ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε
⊢ TotallyBounded A

Tactic:
refine totallyBounded_of_finite_discretization fun ε ε0 => ?_

Premises used: Metric.totallyBounded_of_finite_discretization
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
rcases :
  ∀ (ε₁ : ℝ) (ε₁0 : 0 < ε₁) (εε₁ : ε₁ < ε),
    ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
      ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε
⊢ ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
    ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε

Tactic:
rcases exists_between ε0 with ⟨ε₁, ε₁0, εε₁⟩

Premises used: exists_between
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
⊢ ε₂ > 0

Tactic:
have ε₂0 : ε₂ > 0 := half_pos (half_pos ε₁0)
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
⊢ ∀ (x : α),
    ∃ (U : Set α),
      x ∈ U ∧
        IsOpen U ∧
          ∀ y ∈ U,
            ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂

Tactic:
have : ∀ x : α, ∃ U, x ∈ U ∧ IsOpen U ∧
      ∀ y ∈ U, ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂ := fun x =>
    let ⟨U, nhdsU, hU⟩ := H x _ ε₂0
    let ⟨V, VU, openV, xV⟩ := _root_.mem_nhds_iff.1 nhdsU
    ⟨V, xV, openV, fun y hy z hz f hf => hU y (VU hy) z (VU hz) ⟨f, hf⟩⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
this :
  ∀ (x : α),
    ∃ (U : Set α),
      x ∈ U ∧
        IsOpen U ∧
          ∀ y ∈ U,
            ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
choose :
  ∀ (U : (x : α) → Set α)
    (hU :
      ∀ (x : α),
        x ∈ U x ∧
          IsOpen (U x) ∧
            ∀ y ∈ U x,
              ∀ z ∈ U x,
                ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂),
    ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
      ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε
⊢ ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
    ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε

Tactic:
choose U hU using this
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H :
  ∀ (x₀ : α),
    ∀ ε > 0,
      ∃ U ∈ nhds x₀,
        ∀ x ∈ U,
          ∀ x' ∈ U,
            ∀ (i : (↑A : Type (max u v))),
              dist.{v} (α := β) (((↑i : α →ᵇ β) : (a : α) → β) x : β) (((↑i : α →ᵇ β) : (a : α) → β) x' : β) < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : (x : α) → Set α
hU :
  ∀ (x : α),
    x ∈ U x ∧
      IsOpen (U x) ∧
        ∀ y ∈ U x,
          ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist.{v} (α := β) ((f : (a : α) → β) y : β) ((f : (a : α) → β) z : β) < ε₂
obtain :
  ∀ tα ⊆ univ,
    ∀ (hfin : tα.Finite) (htα : Subset.{u} (α := Set α) univ (⋃ x ∈ tα, U x)),
      ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
        ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε
⊢ ∃ (β_1 : Type (max u v)) (x : Fintype β_1) (F : (↑A : Type (max u v)) → β_1),
    ∀ (x y : (↑A : Type (max u v))), F x = F y → dist (↑x : α →ᵇ β) (↑y : α →ᵇ β) < ε

Tactic:
obtain ⟨tα : Set α, _, hfin, htα : univ ⊆ ⋃ x ∈ tα, U x⟩ :=
    isCompact_univ.elim_finite_subcover_image (fun x _ => (hU x).2.1) fun x _ =>
      mem_biUnion (mem_univ _) (hU x).1

Premises used: Set.univ, Set.mem_biUnion, And.right, isCompact_univ, And.left, IsCompact.elim_finite_subcover_image, Set.mem_univ, Set