awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this_1 : Inhabited α
this : ∃ (s : Set α), s.Countable ∧ Dense s
inr : ∀ (S : Set α) (S_countable : S.Countable) (S_dense : Dense S), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
inr : ∀ (x : ℕ → α) (x_range : S ⊆ range x), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
rcases Set.countable_iff_exists_subset_range.1 S_countable with ⟨x, x_range⟩

Premises used: Set.countable_iff_exists_subset_range, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩

Premises used: Dense.mono, KuratowskiEmbedding.embeddingOfSubset_isometry, Exists.intro, KuratowskiEmbedding.embeddingOfSubset
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
exact ⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
⊢ Isometry (kuratowskiEmbedding α)

Tactic:
Classical.choose_spec (exists_isometric_embedding α)

Premises used: Classical.choose_spec, kuratowskiEmbedding, KuratowskiEmbedding.exists_isometric_embedding
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl : LipschitzOnWith K f s
⊢ ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s

Tactic:
rw [LipschitzOnWith.coordinate] at hfl

Premises used: LipschitzOnWith.coordinate
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
⊢ ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) g s

Tactic:
have (i : ι) : ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s :=
    LipschitzOnWith.extend_real (hfl i)
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
this : ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) g s
choose :
  ∀ (g : (i : ι) → α → ℝ) (hgl : ∀ (i : ι), LipschitzWith K (g i))
    (hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s),
    ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s

Tactic:
choose g hgl hgeq using this
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
inl :
  ∀
    (hfl :
      ∀ (i : ι),
        LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ∅)
    (hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) ∅),
    ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g ∅
inr : ∀ (a₀ : α) (ha₀_in_s : a₀ ∈ s), ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ∅
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) ∅
⊢ EqOn f 0 ∅

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ∅
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) ∅
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g ∅

Tactic:
exact ⟨0, LipschitzWith.const' 0, by simp⟩
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
apply : Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀) ∞
⊢ ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞

Tactic:
apply LipschitzWith.uniformly_bounded (swap g) hgl a₀

Premises used: Function.swap, LipschitzWith.uniformly_bounded
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
h :
  Membership.mem (γ := Set ℝ) (upperBounds (range fun (i : ι) ↦ ‖swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀ i‖)) ‖f a₀‖
⊢ Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀) ∞

Tactic:
use ‖f a₀‖
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
h : ‖(↑(f a₀) : (i : ι) → ℝ) i‖ ≤ ‖f a₀‖
⊢ (fun (i : ι) ↦ ‖swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀ i‖) i ≤ ‖f a₀‖

Tactic:
simp_rw [← hgeq i ha₀_in_s]
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖(↑(f a₀) : (i : ι) → ℝ) i‖ ≤ ‖f a₀‖

Tactic:
lp.norm_apply_le_norm top_ne_zero (f a₀) i

Premises used: lp.norm_apply_le_norm, ENNReal.top_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖(↑(f a₀) : (i : ι) → ℝ) i‖ ≤ ‖f a₀‖

Tactic:
exact lp.norm_apply_le_norm top_ne_zero (f a₀) i

Premises used: lp.norm_apply_le_norm, ENNReal.top_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞

Tactic:
have hf_extb : ∀ a : α, Memℓp (swap g a) ∞ := by
      apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
      use ‖f a₀‖
      rintro - ⟨i, rfl⟩
      simp_rw [← hgeq i ha₀_in_s]
      exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s

Tactic:
⟨f_ext', ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
inr : LipschitzWith K f_ext'
inr₁ : EqOn f f_ext' s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s

Tactic:
refine ⟨f_ext', ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
inr :
  ∀ (i : ι), LipschitzWith (β := (fun (x : ι) ↦ ℝ) i) K fun (a : α) ↦ (↑(f_ext' a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i
⊢ LipschitzWith K f_ext'

Tactic:
rw [LipschitzWith.coordinate]

Premises used: LipschitzWith.coordinate
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
⊢ ∀ (i : ι), LipschitzWith (β := (fun (x : ι) ↦ ℝ) i) K fun (a : α) ↦ (↑(f_ext' a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i

Tactic:
hgl
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
⊢ ∀ (i : ι), LipschitzWith (β := (fun (x : ι) ↦ ℝ) i) K fun (a : α) ↦ (↑(f_ext' a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i

Tactic:
exact hgl
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
a : α
hyp : a ∈ s
inr : ∀ (i : ι), (↑(f a) : (i : ι) → ℝ) i = (↑(f_ext' a) : (i : ι) → ℝ) i
⊢ f a = f_ext' a

Tactic:
ext i
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
a : α
hyp : a ∈ s
i : ι
⊢ (↑(f a) : (i : ι) → ℝ) i = (↑(f_ext' a) : (i : ι) → ℝ) i

Tactic:
(hgeq i) hyp
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
a : α
hyp : a ∈ s
i : ι
⊢ (↑(f a) : (i : ι) → ℝ) i = (↑(f_ext' a) : (i : ι) → ℝ) i

Tactic:
exact (hgeq i) hyp
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
simp :
  (∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
    ∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)
⊢ LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ (↑K : ℝ) * dist x y

Tactic:
simp only [LipschitzWith, edist_nndist, dist_nndist]

Premises used: LipschitzWith, dist_nndist, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (∀ (x y : α), nndist (f x) (f y) ≤ K * nndist x y) ↔ ∀ (x y : α), nndist (f x) (f y) ≤ K * nndist x y
⊢ (∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
    ∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
simp :
  (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
    ∀ x ∈ s, ∀ y ∈ s, (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)
⊢ LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y

Tactic:
simp only [LipschitzOnWith, edist_nndist, dist_nndist]

Premises used: dist_nndist, LipschitzOnWith, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist (f x) (f y) ≤ K * nndist x y) ↔
    ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist (f x) (f y) ≤ K * nndist x y
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
    ∀ x ∈ s, ∀ y ∈ s, (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
hbc : K ≤ (↑K.toNNReal : ℝ)
⊢ K * dist x y ≤ (↑K.toNNReal : ℝ) * dist x y

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ (↑K.toNNReal : ℝ)

Tactic:
apply Real.le_coe_toNNReal

Premises used: Real.le_coe_toNNReal
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : ∀ (x y : α), dist (f x) (f y) ≤ dist x y
⊢ ∀ (x y : α), dist (f x) (f y) ≤ (↑1 : ℝ) * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul] using h

Premises used: NNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
K : ℝ
h : ∀ (x y : α), f x ≤ f y + K * dist x y
⊢ LipschitzWith K.toNNReal f

Tactic:
have I : ∀ x y, f x - f y ≤ K * dist x y := fun x y => sub_le_iff_le_add'.2 (h x y)
  LipschitzWith.of_dist_le' fun x y => abs_sub_le_iff.2 ⟨I x y, dist_comm y x ▸ I y x⟩

Premises used: Iff.mpr, abs_sub_le_iff, Eq.rec, dist_comm, sub_le_iff_le_add', And.intro, LipschitzWith.of_dist_le'
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
K : ℝ≥0
h : ∀ (x y : α), f x ≤ f y + (↑K : ℝ) * dist x y
⊢ LipschitzWith K f

Tactic:
simpa only [Real.toNNReal_coe] using LipschitzWith.of_le_add_mul' K h

Premises used: Real.toNNReal_coe, NNReal.toReal, LipschitzWith.of_le_add_mul'
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
h : ∀ (x y : α), f x ≤ f y + dist x y
⊢ ∀ (x y : α), f x ≤ f y + (↑1 : ℝ) * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul]

Premises used: NNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
K : ℝ≥0
h : LipschitzWith K f
x y : α
⊢ f x ≤ f y + (↑K : ℝ) * dist x y

Tactic:
sub_le_iff_le_add'.1 <| le_trans (le_abs_self _) <| h.dist_le_mul x y

Premises used: LipschitzWith.dist_le_mul, le_abs_self, sub_le_iff_le_add', Iff.mp, le_trans
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
K : ℝ≥0
⊢ LipschitzWith K f ↔ ∀ (x y : α), f x ≤ f y + (↑K : ℝ) * dist x y

Tactic:
⟨LipschitzWith.le_add_mul, LipschitzWith.of_le_add_mul K⟩

Premises used: LipschitzWith.le_add_mul, LipschitzWith.of_le_add_mul, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
x y : α
⊢ nndist (f x) (f y) ≤ K * nndist x y

Tactic:
hf.dist_le_mul x y

Premises used: LipschitzWith.dist_le_mul, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hr : dist x y ≤ r
ha : 0 ≤ (↑K : ℝ)
⊢ (↑K : ℝ) * dist x y ≤ (↑K : ℝ) * r

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
x : α
r : ℝ
⊢ MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) ((↑K : ℝ) * r))

Tactic:
fun _y hy =>
  hf.dist_le_mul_of_le hy

Premises used: LipschitzWith.dist_le_mul_of_le, Set.Mem, setOf, Set.MapsTo, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hK : K ≠ 0
hr : dist x y < r
ha : 0 < (↑K : ℝ)
⊢ (↑K : ℝ) * dist x y < (↑K : ℝ) * r

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
hK : K ≠ 0
x : α
r : ℝ
⊢ MapsTo f (Metric.ball x r) (Metric.ball (f x) ((↑K : ℝ) * r))

Tactic:
fun _y hy =>
  hf.dist_lt_mul_of_lt hK hy

Premises used: Set.Mem, setOf, Metric.ball, LipschitzWith.dist_lt_mul_of_lt, Set.MapsTo