awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
refine_1 :
  ∀ (x : δ),
    dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) x : β) ((extend f g₂ h₂ : (a : δ) → β) x : β) ≤
      max (dist g₁ g₂)
        (dist (α :=
          BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
          (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
          (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
refine_2 : dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) =
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_3 : dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
    (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
    (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ) ≤
  dist (extend f g₁ h₁) (extend f g₂ h₂)
Tactic: refine le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
⊢ dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) x : β) ((extend f g₂ h₂ : (a : δ) → β) x : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_1 : ∀ (x : α),
  dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
      ((extend f g₂ h₂ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
Tactic: rcases em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
refine_1 :
  ∀ (x : α),
    dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
        ((extend f g₂ h₂ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ≤
      max (dist g₁ g₂)
        (dist (α :=
          BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
          (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
          (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
⊢ dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) x : β) ((extend f g₂ h₂ : (a : δ) → β) x : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_1₁ : ∀ (hx : ¬∃ (y : α), (f : (a : α) → δ) y = x),
  dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) x : β) ((extend f g₂ h₂ : (a : δ) → β) x : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
Tactic: rcases em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
      ((extend f g₂ h₂ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_1 : dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (a : α) → β) x : β) ≤
  max (dist g₁ g₂)
    (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
      (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
      (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
Tactic: simp only [extend_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ (y : α), (f : (a : α) → δ) y = x
⊢ dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) x : β) ((extend f g₂ h₂ : (a : δ) → β) x : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_1 : dist.{v} (α := β) ((h₁ : (a : δ) → β) x : β) ((h₂ : (a : δ) → β) x : β) ≤
  max (dist g₁ g₂)
    (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
      (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
      (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
Tactic: simp only [extend_apply' hx]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : δ
hx : ¬∃ (y : α), (f : (a : α) → δ) y = x
⊢ dist.{v} (α := β) ((h₁ : (a : δ) → β) x : β) ((h₂ : (a : δ) → β) x : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
have refine_1 : ∀ (x : { x : δ // Membership.mem (γ := Set δ) (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ x }),
  dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) ≤
    max (dist g₁ g₂)
      (dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
        (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
        (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ))
Tactic: lift x to ((range f)ᶜ : Set δ) using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
have refine_2 : ∀ (x : α),
  dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (a : α) → β) x : β) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
Tactic: refine (dist_le dist_nonneg).2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist.{v} (α := β) ((g₁ : (a : α) → β) x : β) ((g₂ : (a : α) → β) x : β) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
have refine_2 : dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β)
    ((extend f g₂ h₂ : (a : δ) → β) ((f : (a : α) → δ) x : δ) : β) ≤
  dist (extend f g₁ h₁) (extend f g₂ h₂)
Tactic: rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (α := BoundedContinuousFunction.{u_2, v} (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2) β)
      (h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ)
      (h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ) ≤
    dist (extend f g₁ h₁) (extend f g₂ h₂)
have refine_3 : ∀ (x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)),
  dist.{v} (α := β)
      ((h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β)
      ((h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β) ≤
    dist (extend f g₁ h₁) (extend f g₂ h₂)
Tactic: refine (dist_le dist_nonneg).2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)
⊢ dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)
have rw : dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
  dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)
Tactic: rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)
rw :
  dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)
⊢ dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
    dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)
have rw₁ : dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
  dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β)
Tactic: rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
δ : Type u_2
inst_2 : TopologicalSpace δ
inst_3 : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : (↑(range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ : Type u_2)
⊢ dist.{v} (α := β)
      ((h₁.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β)
      ((h₂.restrict (range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → δ))ᶜ :
            (a : (↑(range (⇑f : (a : α) → δ))ᶜ : Type u_2)) → β)
          x :
        β) ≤
    dist (extend f g₁ h₁) (extend f g₂ h₂)
have dist : dist.{v} (α := β) ((h₁ : (a : δ) → β) (↑x : δ) : β) ((h₂ : (a : δ) → β) (↑x : δ) : β) =
  dist.{v} (α := β) ((extend f g₁ h₁ : (a : δ) → β) (↑x : δ) : β) ((extend f g₂ h₂ : (a : δ) → β) (↑x : δ) : β)
Tactic: calc
      dist (h₁ x) (h₂ x) = dist (extend f g₁ h₁ x) (extend f g₂ h₂ x) := by
        rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
      _ ≤ _ := dist_coe_le_dist _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
have pos : ∀ (hx : x ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
pos : ∀ (hx : x ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
have neg : ∀ (hx : x ∉ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
have pos : ∀ (hy : y ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Tactic: by_cases hy : y ∈ s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
pos : ∀ (hy : y ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
have neg : ∀ (hy : y ∉ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Tactic: by_cases hy : y ∈ s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
have pos : ∀ (hy : y ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Tactic: by_cases hy : y ∈ s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f g : α →ᵇ β
x_1 : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
pos : ∀ (hy : y ∈ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
⊢ dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
have neg : ∀ (hy : y ∉ s), dist (α := ℝ) (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Tactic: by_cases hy : y ∈ s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
⊢ (⇑(nsmulRec 0 f) : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)
have rw : (⇑0 : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)
Tactic: rw [nsmulRec, zero_smul, coe_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
rw : (⇑0 : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)
⊢ (⇑(nsmulRec 0 f) : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)
have rw₁ : Eq (α := (a : α) → β) (⇑0 : (a : α) → β) 0
Tactic: rw [nsmulRec, zero_smul, coe_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
rw : (⇑0 : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑0 : (a : α) → β) 0
⊢ (⇑(nsmulRec 0 f) : (a : α) → β) = HSMul.hSMul (α := ℕ) (β := (a : α) → β) 0 (⇑f : (a : α) → β)
have rw₂ : Eq (α := (a : α) → β) 0 0
Tactic: rw [nsmulRec, zero_smul, coe_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
n : ℕ
⊢ (⇑(nsmulRec (n + 1) f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
have rw : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
Tactic: rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec _ n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
n : ℕ
rw : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
⊢ (⇑(nsmulRec (n + 1) f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
have rw₁ : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
Tactic: rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec _ n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
n : ℕ
rw : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
rw₁ : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
⊢ (⇑(nsmulRec (n + 1) f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
have rw₂ : HAdd.hAdd (α := (a : α) → β) (⇑(nsmulRec n f) : (a : α) → β) (⇑f : (a : α) → β) =
  HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
Tactic: rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec _ n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : BoundedAdd β
inst_4 : ContinuousAdd β
f : α →ᵇ β
n : ℕ
rw : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
rw₁ : (⇑(nsmulRec n f + f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
rw₂ :
  HAdd.hAdd (α := (a : α) → β) (⇑(nsmulRec n f) : (a : α) → β) (⇑f : (a : α) → β) =
    HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
⊢ (⇑(nsmulRec (n + 1) f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) (n + 1) (⇑f : (a : α) → β)
have rw₃ : HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β) =
  HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) + (⇑f : (a : α) → β)
Tactic: rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec _ n]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
f : α →ᵇ R
n : ℕ
⊢ ∃ (C : ℝ),
    ∀ (x y : α),
      dist (HPow.hPow (α := R) ((f : (a : α) → R) x : R) n) (HPow.hPow (α := R) ((f : (a : α) → R) y : R) n) ≤ C
have obtain : ∀ (C : ℝ)
  (hC :
    ∀ ⦃x : R⦄,
      Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) x →
        ∀ ⦃y : R⦄,
          Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' range.{u_2, u + 1} (ι := α) (⇑f : (a : α) → R)) y →
            dist x y ≤ C),
  ∃ (C : ℝ),
    ∀ (x y : α),
      dist (HPow.hPow (α := R) ((f : (a : α) → R) x : R) n) (HPow.hPow (α := R) ((f : (a : α) → R) y : R) n) ≤ C
Tactic: obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <| isBounded_pow (isBounded_range f) n
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace R
inst_2 : Monoid R
inst_3 : BoundedMul R
inst_4 : ContinuousMul R
x y : α →ᵇ R
⊢ (x * y).toContinuousMap = x.toContinuousMap * y.toContinuousMap
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := R) (((x * y).toContinuousMap : (a : α) → R) a : R)
    ((x.toContinuousMap * y.toContinuousMap : (a : α) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (hypothesis)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
⊢ LipschitzWith (β := α →ᵇ β) (LipschitzAdd.C β) fun (p : (α →ᵇ β) × (α →ᵇ β)) ↦ p.1 + p.2
have C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
Tactic: have C_nonneg := (LipschitzAdd.C β).coe_nonneg
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
⊢ LipschitzWith (β := α →ᵇ β) (LipschitzAdd.C β) fun (p : (α →ᵇ β) × (α →ᵇ β)) ↦ p.1 + p.2
have rw : ∀ (x y : (α →ᵇ β) × (α →ᵇ β)), dist (x.1 + x.2) (y.1 + y.2) ≤ (↑(LipschitzAdd.C β) : ℝ) * dist x y
Tactic: rw [lipschitzWith_iff_dist_le_mul]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
f₁ g₁ f₂ g₂ : α →ᵇ β
⊢ dist ((f₁, g₁).1 + (f₁, g₁).2) ((f₂, g₂).1 + (f₂, g₂).2) ≤ (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)
have rw : ∀ (x : α),
  dist.{v} (α := β) (((f₁, g₁).1 + (f₁, g₁).2 : (a : α) → β) x : β) (((f₂, g₂).1 + (f₂, g₂).2 : (a : α) → β) x : β) ≤
    (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)
Tactic: rw [dist_le (mul_nonneg C_nonneg dist_nonneg)]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Basic (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
inst_2 : AddMonoid β
inst_3 : LipschitzAdd β
f g : α →ᵇ β
x_1 : α
C : ℝ
C_nonneg : 0 ≤ (↑(LipschitzAdd.C β) : ℝ)
f₁ g₁ f₂ g₂ : α →ᵇ β
x : α
⊢ dist.{v} (α := β) (((f₁, g₁).1 + (f₁, g₁).2 : (a : α) → β) x : β) (((f₂, g₂).1 + (f₂, g₂).2 : (a : α) → β) x : β) ≤
    (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)
have refine : (↑(LipschitzAdd.C β) : ℝ) *
    dist.{v} (α := β × β) (((f₁ : (a : α) → β) x, (g₁ : (a : α) → β) x) : β × β)
      (((f₂ : (a : α) → β) x, (g₂ : (a : α) → β) x) : β × β) ≤
  (↑(LipschitzAdd.C β) : ℝ) * dist (f₁, g₁) (f₂, g₂)
Tactic: refine le_trans (lipschitz_with_lipschitz_const_add ⟨f₁ x, g₁ x⟩ ⟨f₂ x, g₂ x⟩) ?_