awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
x : (↑s : Type u_1)
hf : ContinuousOn f s
rw :
  ({ toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ :
          ContinuousMap.{u_1, u_2} (↑s : Type u_1) β } :
        (a : (↑s : Type u_1)) → β)
      x =
    f (↑x : α)
⊢ (mkD (s.restrict (π := fun (a : α) ↦ β) f) g : (a : (↑s : Type u_1)) → β) x = f (↑x : α)
have rw₁ : s.restrict (π := fun (a : α) ↦ β) f x = f (↑x : α)
Tactic: rw [mkD_of_continuousOn hf, coe_mk, Set.restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
x : (↑s : Type u_1)
hf : ContinuousOn f s
rw :
  ({ toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ :
          ContinuousMap.{u_1, u_2} (↑s : Type u_1) β } :
        (a : (↑s : Type u_1)) → β)
      x =
    f (↑x : α)
rw₁ : s.restrict (π := fun (a : α) ↦ β) f x = f (↑x : α)
⊢ (mkD (s.restrict (π := fun (a : α) ↦ β) f) g : (a : (↑s : Type u_1)) → β) x = f (↑x : α)
have rw₂ : f (↑x : α) = f (↑x : α)
Tactic: rw [mkD_of_continuousOn hf, coe_mk, Set.restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
H : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), S i) Set.univ
i : ι
⊢ ContinuousOn (Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ H) (S i)
have rw : Continuous[instTopologicalSpaceSubtype, inst_1]
  ((S i).restrict (π := fun (a : α) ↦ β)
    (Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ H))
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
i : ι
x : (↑(S i) : Type u_1)
⊢ Eq.{u_2 + 1} (α := β) ((liftCover S φ hφ hS : (a : α) → β) (↑x : α) : β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
have rw : Eq.{u_2 + 1} (α := β)
  (({ toFun := Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ sorry, continuous_toFun := sorry :
          C(α, β) } :
        (a : α) → β)
      (↑x : α) :
    β)
  ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
Tactic: rw [liftCover, coe_mk, Set.liftCover_coe _]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
i : ι
x : (↑(S i) : Type u_1)
rw :
  Eq.{u_2 + 1} (α := β)
    (({ toFun := Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ ⋯, continuous_toFun := ⋯ :
            C(α, β) } :
          (a : α) → β)
        (↑x : α) :
      β)
    ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
⊢ Eq.{u_2 + 1} (α := β) ((liftCover S φ hφ hS : (a : α) → β) (↑x : α) : β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
have rw₁ : Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ sorry (↑x : α) =
  (φ i : (a : (↑(S i) : Type u_1)) → β) x
Tactic: rw [liftCover, coe_mk, Set.liftCover_coe _]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
i : ι
x : (↑(S i) : Type u_1)
rw :
  Eq.{u_2 + 1} (α := β)
    (({ toFun := Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ ⋯, continuous_toFun := ⋯ :
            C(α, β) } :
          (a : α) → β)
        (↑x : α) :
      β)
    ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
rw₁ :
  Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ ⋯ (↑x : α) =
    (φ i : (a : (↑(S i) : Type u_1)) → β) x
⊢ Eq.{u_2 + 1} (α := β) ((liftCover S φ hφ hS : (a : α) → β) (↑x : α) : β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
have rw₂ : Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
Tactic: rw [liftCover, coe_mk, Set.liftCover_coe _]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
i : ι
⊢ restrict (S i) (liftCover S φ hφ hS) = φ i
have h : ∀ (a : (↑(S i) : Type u_1)),
  Eq.{u_2 + 1} (α := β) ((restrict (S i) (liftCover S φ hφ hS) : (a : (↑(S i) : Type u_1)) → β) a : β)
    ((φ i : (a : (↑(S i) : Type u_1)) → β) a : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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} (α := β) ((liftCover' A F hF hA : (a : α) → β) (↑x : α) : β) ((F s hs : (a : (↑s : Type u_1)) → β) x : β)
have delta : 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 α) sorry;
        liftCover (Subtype.val (p := fun (x : Set α) ↦ x ∈ A)) F_1 sorry sorry :
        (a : α) → β)
      (↑x : α) :
    β)
  ((F s hs : (a : (↑s : Type u_1)) → β) x : β)
Tactic: delta liftCover'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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_1, instTopologicalSpaceQuotient] (Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun
have rw : Continuous[inst, instTopologicalSpaceQuotient]
  ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) sorry).invFun ∘ (⇑f : (a : X) → Y))
Tactic: rw [hf.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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]
    ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y))
have h : (Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) sorry).invFun ∘ (⇑f : (a : X) → Y) = Quotient.mk'
Tactic: convert! continuous_quotient_mk'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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)
⊢ (Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y) = Quotient.mk'
have h : ∀ (x : X), ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) sorry).invFun ∘ (⇑f : (a : X) → Y)) x = Quotient.mk' x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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
⊢ ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) ⋯).invFun ∘ (⇑f : (a : X) → Y)) x = Quotient.mk' x
have h : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y)
  ((Setoid.quotientKerEquivOfSurjective (⇑f : (a : X) → Y) sorry : (a : Quotient (Setoid.ker (⇑f : (a : X) → Y))) → Y)
      (Quotient.mk' x) :
    Y)
Tactic: simp only [Equiv.invFun_as_coe, Function.comp_apply,
      (Setoid.quotientKerEquivOfSurjective f hf.surjective).symm_apply_eq]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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)
⊢ (hf.lift g h).comp f = g
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := Z) ((g.comp f : (a : X) → Z) x : Z) ((g.comp f : (a : X) → Z) x_1 : Z)
have 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)
Tactic: simp only [ContinuousMap.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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)
⊢ (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
have 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)) sorry)
            ((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) sorry :
                  { 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: ext a
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ Eq (α := C(α, α)) (ContinuousMap.comp (↑f.symm : C(β, α)) (↑f : C(α, β))) (ContinuousMap.id α)
have rw : Eq (α := C(α, α)) (↑(f.trans f.symm) : C(α, α)) (ContinuousMap.id α)
Tactic: rw [← coe_trans, self_trans_symm, coe_refl]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
rw : Eq (α := C(α, α)) (↑(f.trans f.symm) : C(α, α)) (ContinuousMap.id α)
⊢ Eq (α := C(α, α)) (ContinuousMap.comp (↑f.symm : C(β, α)) (↑f : C(α, β))) (ContinuousMap.id α)
have rw₁ : Eq (α := C(α, α)) (↑(Homeomorph.refl α) : C(α, α)) (ContinuousMap.id α)
Tactic: rw [← coe_trans, self_trans_symm, coe_refl]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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 α)
⊢ Eq (α := C(α, α)) (ContinuousMap.comp (↑f.symm : C(β, α)) (↑f : C(α, β))) (ContinuousMap.id α)
have rw₂ : Eq (α := C(α, α)) (ContinuousMap.id α) (ContinuousMap.id α)
Tactic: rw [← coe_trans, self_trans_symm, coe_refl]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ Eq (α := C(β, β)) (ContinuousMap.comp (↑f : C(α, β)) (↑f.symm : C(β, α))) (ContinuousMap.id β)
have rw : Eq (α := C(β, β)) (↑(f.symm.trans f) : C(β, β)) (ContinuousMap.id β)
Tactic: rw [← coe_trans, symm_trans_self, coe_refl]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
rw : Eq (α := C(β, β)) (↑(f.symm.trans f) : C(β, β)) (ContinuousMap.id β)
⊢ Eq (α := C(β, β)) (ContinuousMap.comp (↑f : C(α, β)) (↑f.symm : C(β, α))) (ContinuousMap.id β)
have rw₁ : Eq (α := C(β, β)) (↑(Homeomorph.refl β) : C(β, β)) (ContinuousMap.id β)
Tactic: rw [← coe_trans, symm_trans_self, coe_refl]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Basic (goal)
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 β)
⊢ Eq (α := C(β, β)) (ContinuousMap.comp (↑f : C(α, β)) (↑f.symm : C(β, α))) (ContinuousMap.id β)
have rw₂ : Eq (α := C(β, β)) (ContinuousMap.id β) (ContinuousMap.id β)
Tactic: rw [← coe_trans, symm_trans_self, coe_refl]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (hypothesis)
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 : α) → β)
⊢ IsCompact A
have H₁ : ∀ (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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
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
have refine : TotallyBounded A
Tactic: refine TotallyBounded.isCompact_of_isClosed ?_ closed
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
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
have 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 : α →ᵇ β) < ε
Tactic: refine totallyBounded_of_finite_discretization fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
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
⊢ ∃ (β_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 : α →ᵇ β) < ε
have 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 : α →ᵇ β) < ε
Tactic: rcases exists_between ε0 with ⟨ε₁, ε₁0, εε₁⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (hypothesis)
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
⊢ ∃ (β_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 : α →ᵇ β) < ε
have ε₂0 : ε₂ > 0
Tactic: have ε₂0 : ε₂ > 0 := half_pos (half_pos ε₁0)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (hypothesis)
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
⊢ ∃ (β_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 : α →ᵇ β) < ε
have this : ∀ (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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli (goal)
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 : β) < ε₂
⊢ ∃ (β_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 : α →ᵇ β) < ε
have 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 : α →ᵇ β) < ε
Tactic: choose U hU using this
Cleared hypotheses: this