awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
⊢ LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))

Tactic:
have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
⊢ IsCompact A

Tactic:
IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
      fun f hf => ?_

Premises used: IsCompact.of_isClosed_subset, IsCompact.image, BoundedContinuousFunction.continuous_comp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
refine_1 : IsCompact (F ⁻¹' A)
refine_2 :
  ∀ (f : α →ᵇ β) (hf : f ∈ A),
    Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) f
⊢ IsCompact A

Tactic:
refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
      fun f hf => ?_

Premises used: IsCompact.of_isClosed_subset, IsCompact.image, BoundedContinuousFunction.continuous_comp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
⊢ CompactSpace.{v} (↑s : Type v)

Tactic:
haveI : CompactSpace s := isCompact_iff_compactSpace.1 hs
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
this : CompactSpace.{v} (↑s : Type v)
⊢ IsCompact (F ⁻¹' A)

Tactic:
arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_

Premises used: BoundedContinuousFunction.arzela_ascoli₁, continuous_iff_isClosed, Iff.mp, BoundedContinuousFunction.continuous_comp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
this : CompactSpace.{v} (↑s : Type v)
refine_1 :
  Equicontinuous (X := α) (α := (↑s : Type v)) fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦
    (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v))
⊢ IsCompact (F ⁻¹' A)

Tactic:
refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_

Premises used: BoundedContinuousFunction.arzela_ascoli₁, continuous_iff_isClosed, Iff.mp, BoundedContinuousFunction.continuous_comp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
this : CompactSpace.{v} (↑s : Type v)
refine_1 :
  Equicontinuous (ι := (↑(F ⁻¹' A) : Type (max u v))) (X := α) (α := β)
    ((fun (x : α → { x : β // x ∈ s }) ↦ Subtype.val (p := fun (x : β) ↦ x ∈ s) ∘ x) ∘
      fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦ (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v)))
⊢ Equicontinuous (X := α) (α := (↑s : Type v)) fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦
    (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v))

Tactic:
rw [isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff]

Premises used: IsUniformEmbedding.isUniformInducing, isUniformEmbedding_subtype_val, IsUniformInducing.equicontinuous_iff
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
this : CompactSpace.{v} (↑s : Type v)
⊢ Equicontinuous (ι := (↑(F ⁻¹' A) : Type (max u v))) (X := α) (α := β)
    ((fun (x : α → { x : β // x ∈ s }) ↦ Subtype.val (p := fun (x : β) ↦ x ∈ s) ∘ x) ∘
      fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦ (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v)))

Tactic:
H.comp (A.restrictPreimage F)

Premises used: Set.restrictPreimage, Equicontinuous.comp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
this : CompactSpace.{v} (↑s : Type v)
⊢ Equicontinuous (ι := (↑(F ⁻¹' A) : Type (max u v))) (X := α) (α := β)
    ((fun (x : α → { x : β // x ∈ s }) ↦ Subtype.val (p := fun (x : β) ↦ x ∈ s) ∘ x) ∘
      fun (x : (↑(F ⁻¹' A) : Type (max u v))) ↦ (⇑(↑x : α →ᵇ (↑s : Type v)) : (a : α) → (↑s : Type v)))

Tactic:
exact H.comp (A.restrictPreimage F)

Premises used: Set.restrictPreimage, Equicontinuous.comp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
h : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((F g : (a : α) → β) x : β)
⊢ f = F g

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
x : α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((F g : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf_1 : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
hf : F g ∈ A
h : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((F g : (a : α) → β) x : β)
⊢ f = F g

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf_1 : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
hf : F g ∈ A
x : α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((F g : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
refine_2 :
  ∀ (hf : F g ∈ A),
    Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) (F g)
⊢ Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) f

Tactic:
rw [show f = F g by ext; rfl] at hf ⊢
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf_1 : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
hf : F g ∈ A
⊢ Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) (F g)

Tactic:
⟨g, hf, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
M : LipschitzWith.{v, v} (α := { x : β // x ∈ s }) 1 (Subtype.val (p := fun (x : β) ↦ x ∈ s))
F : BoundedContinuousFunction.{u, v} α (↑s : Type v) → α →ᵇ β := comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M
f : α →ᵇ β
hf_1 : f ∈ A
g : BoundedContinuousFunction.{u, v} α (↑s : Type v) := codRestrict s f ⋯
hf : F g ∈ A
⊢ Membership.mem (γ := Set (α →ᵇ β)) (comp (Subtype.val (p := fun (x : β) ↦ x ∈ s)) M '' F ⁻¹' A) (F g)

Tactic:
exact ⟨g, hf, rfl⟩
-- Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : T2Space β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → Membership.mem (α := β) s ((f : (a : α) → β) x : β)
H : Equicontinuous (X := α) (α := β) fun (x : (↑A : Type (max u v))) ↦ (⇑(↑x : α →ᵇ β) : (a : α) → β)
⊢ IsCompact (closure A)

Tactic:
arzela_ascoli₂ s hs (closure A) isClosed_closure
    (fun _ x hf =>
      (mem_of_closed' hs.isClosed).2 fun ε ε0 =>
        let ⟨g, gA, dist_fg⟩ := Metric.mem_closure_iff.1 hf ε ε0
        ⟨g x, in_s g x gA, lt_of_le_of_lt (dist_coe_le_dist _) dist_fg⟩)
    (H.closure' continuous_coe)

Premises used: Iff.mpr, Equicontinuous.closure', lt_of_le_of_lt, Membership.mem, Exists, Metric.mem_closure_iff, BoundedContinuousFunction.dist_coe_le_dist, BoundedContinuousFunction.continuous_coe, _private.0.BoundedContinuousFunction.arzela_ascoli.match_1, Metric.mem_of_closed', And, closure, And.intro, LT.lt, Exists.intro, Iff.mp, Dist.dist, isClosed_closure, DFunLike.coe, IsCompact.isClosed, BoundedContinuousFunction.arzela_ascoli₂
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f_1 g_1 : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
h : Eq (α := (a : α) → β) ((fun (f : α →ᵇ β) ↦ f.toFun) f) ((fun (f : α →ᵇ β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (continuous_toFun : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun)
    (map_bounded' :
      ∃ (C : ℝ),
        ∀ (x y : α),
          dist ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun x)
              ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun y) ≤
            C)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →ᵇ β) ↦ f.toFun)
          { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' })
        ((fun (f : α →ᵇ β) ↦ f.toFun) g)),
    { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' : α →ᵇ β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g_1 : α →ᵇ β
x : α
C : ℝ
g : α →ᵇ β
toFun : α → β
continuous_toFun : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun
map_bounded' :
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun x)
          ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun y) ≤
        C
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ᵇ β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' })
    ((fun (f : α →ᵇ β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β)
    (continuous_toFun_1 : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun_1)
    (map_bounded'_1 :
      ∃ (C : ℝ),
        ∀ (x y : α),
          dist ({ toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun x)
              ({ toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun y) ≤
            C)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →ᵇ β) ↦ f.toFun)
          { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' })
        ((fun (f : α →ᵇ β) ↦ f.toFun)
          { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_bounded' := map_bounded'_1 })),
    { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' : α →ᵇ β } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_bounded' := map_bounded'_1 }
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' : α →ᵇ β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
toFun : α → β
continuous_toFun : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun
map_bounded' :
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun x)
          ({ toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun y) ≤
        C
toFun_1 : α → β
continuous_toFun_1 : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toFun_1
map_bounded'_1 :
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist ({ toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun x)
          ({ toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun y) ≤
        C
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →ᵇ β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' })
    ((fun (f : α →ᵇ β) ↦ f.toFun)
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_bounded' := map_bounded'_1 })
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, map_bounded' := map_bounded' : α →ᵇ β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, map_bounded' := map_bounded'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑f.toContinuousMap : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
f.map_bounded'

Premises used: BoundedContinuousFunction.map_bounded'
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : α) → β)

Tactic:
f.toContinuousMap.continuous

Premises used: ContinuousMap.continuous, BoundedContinuousFunction.toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
h : ∀ (x : α), Eq.{v + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h' :
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist ({ toFun := f, continuous_toFun := h : C(α, β) }.toFun x)
          ({ toFun := f, continuous_toFun := h : C(α, β) }.toFun y) ≤
        C
⊢ (⇑{ toFun := f, continuous_toFun := h, map_bounded' := h' : α →ᵇ β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
⊢ Bornology.IsBounded.{v} (α := β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
isBounded_range_iff.2 f.bounded

Premises used: Iff.mpr, BoundedContinuousFunction.bounded, Metric.isBounded_range_iff
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵇ β
s : Set α
⊢ Bornology.IsBounded.{v} (α := β) ((⇑f : (a : α) → β) '' s)

Tactic:
f.isBounded_range.subset <| image_subset_range _ _

Premises used: BoundedContinuousFunction.isBounded_range, Set.image_subset_range, Bornology.IsBounded.subset
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
h : IsEmpty α
f g : α →ᵇ β
⊢ f = g

Tactic:
ext <| h.elim

Premises used: BoundedContinuousFunction.ext, IsEmpty.elim
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : C(α, β)
C : ℝ
h : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
⊢ Eq (α := (a : α) → β) (⇑(mkOfBound f C h) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : CompactSpace α
f : C(α, β)
a : α
⊢ Eq.{v + 1} (α := β) ((mkOfCompact f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f g : α →ᵇ β
⊢ dist f g = sInf {C : ℝ | 0 ≤ C ∧ ∀ (x : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) ≤ C}

Tactic:
rfl

Premises used: rfl