awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
⊢ x ∈ f ⁻¹' s → ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
have f₁ : ∀ (hx : f x ∈ s), ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
Tactic: (hx : f x ∈ s)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
hx : f x ∈ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
have obtain : ∀ (ε : ℝ≥0∞) (hε : ε > 0) (hεs : Metric.eball (f x) ε ⊆ s), ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
Tactic: obtain ⟨ε, hε, hεs⟩ := hs (f x) hx
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
have obtain : ∀ (u : Set β) (hu : IsOpen[n] u)
  (uy :
    Eq (α := Set { x_1 : β // x_1 ∈ Metric.eball (f x) ∞ })
      (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ Metric.eball (f x) ∞) ⁻¹' u)
      (Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r)),
  IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
Tactic: obtain ⟨u, hu, uy⟩ := m.topology_eq_on_restrict (f x) r
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy :
  Eq (α := Set { x_1 : β // x_1 ∈ Metric.eball (f x) ∞ })
    (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ Metric.eball (f x) ∞) ⁻¹' u) (Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r)
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
have rw : IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
Tactic: rw [(isInducing_iff f).mp hf]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
m m' : WeakEMetricSpace α
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
⊢ m = m'
have mk : ∀ [toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α] (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y)
  (h :
    Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst))
      (WeakPseudoEMetricSpace.toEDist (τ := inst))),
  { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
      WeakEMetricSpace α } =
    m'
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
m' : WeakEMetricSpace α
toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
⊢ { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
      WeakEMetricSpace α } =
    m'
have mk : ∀ [toWeakPseudoEMetricSpace_1 : WeakPseudoEMetricSpace α] (eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y)
  (h :
    Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst))
      (WeakPseudoEMetricSpace.toEDist (τ := inst))),
  { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
      WeakEMetricSpace α } =
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace_1, eq_of_edist_eq_zero := @eq_of_edist_eq_zero_1 }
Tactic: cases m'
Cleared hypotheses: m', h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
toWeakPseudoEMetricSpace_1 : WeakPseudoEMetricSpace α
eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
⊢ { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero :
      WeakEMetricSpace α } =
    { toWeakPseudoEMetricSpace := toWeakPseudoEMetricSpace_1, eq_of_edist_eq_zero := @eq_of_edist_eq_zero_1 }
have mk : toWeakPseudoEMetricSpace = toWeakPseudoEMetricSpace_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
ι : Type u_3
o : Option ι
s : ι → Set X
⊢ ediam.{u_2} (X := X) (⋃ i ∈ o, s i) = ⨆ i ∈ o, ediam (s i)
have none : ediam.{u_2} (X := X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Option ι) none i), s i) =
  ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Option ι) none i), ediam (s i)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
ι : Type u_3
o : Option ι
s : ι → Set X
none :
  ediam.{u_2} (X := X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Option ι) Option.none i), s i) =
    ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Option ι) Option.none i), ediam (s i)
⊢ ediam.{u_2} (X := X) (⋃ i ∈ o, s i) = ⨆ i ∈ o, ediam (s i)
have some : ∀ (val : ι), ediam.{u_2} (X := X) (⋃ i ∈ some val, s i) = ⨆ i ∈ some val, ediam (s i)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist a x + edist x y + edist y b ≤ ediam s + edist x y + ediam t
have h₁ : edist a x ≤ ediam s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
h₁ : edist a x ≤ ediam s
⊢ edist a x + edist x y + edist y b ≤ ediam s + edist x y + ediam t
have h₂ : edist y b ≤ ediam t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (hypothesis)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t
have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
Tactic: have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t := fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
      _ ≤ ediam s + edist x y + ediam t := by
        gcongr
        exacts [edist_le_ediam_of_mem ha xs, edist_le_ediam_of_mem yt hb]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t
have refine : ∀ (a : X) (ha : a ∈ s ∪ t) (b : X) (hb : b ∈ s ∪ t), edist a b ≤ ediam s + edist x y + ediam t
Tactic: refine ediam_le fun a ha b hb => ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∪ t
b : X
hb : b ∈ s ∪ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
have rw : ∀ (ha : a ∈ s ∨ a ∈ t) (b : X) (hb : b ∈ s ∨ b ∈ t), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rw [mem_union] at ha hb
Cleared hypotheses: ha, b, hb
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∨ a ∈ t
b : X
hb : b ∈ s ∨ b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
have inl : ∀ (h'a : a ∈ s), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rcases ha with h'a | h'a
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∨ a ∈ t
b : X
hb : b ∈ s ∨ b ∈ t
inl : ∀ (h'a : a ∈ s), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t
have inr : ∀ (h'a : a ∈ t), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rcases ha with h'a | h'a
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t
have inl : ∀ (h'b : b ∈ s), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rcases hb with h'b | h'b
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ s
inl : ∀ (h'b : b ∈ s), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t
have inl₁ : ∀ (h'b : b ∈ t), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rcases hb with h'b | h'b
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
have inr : ∀ (h'b : b ∈ s), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rcases hb with h'b | h'b
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
hb : b ∈ s ∨ b ∈ t
h'a : a ∈ t
inr : ∀ (h'b : b ∈ s), edist a b ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t
have inr₁ : ∀ (h'b : b ∈ t), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rcases hb with h'b | h'b
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (hypothesis)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t
have Z : edist b a ≤ ediam s + edist x y + ediam t
Tactic: have Z := A b h'b a h'a
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
x y : X
inst : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
Z : edist b a ≤ ediam s + edist x y + ediam t
⊢ edist a b ≤ ediam s + edist x y + ediam t
have inr : ∀ (Z : edist a b ≤ ediam s + edist x y + ediam t), edist a b ≤ ediam s + edist x y + ediam t
Tactic: rwa [edist_comm] at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
X : Type u_2
s t : Set X
inst : PseudoEMetricSpace X
h : (s ∩ t).Nonempty
⊢ ediam (s ∪ t) ≤ ediam s + ediam t
have let : ∀ (x : X) (xs : x ∈ s) (xt : x ∈ t), ediam (s ∪ t) ≤ ediam s + ediam t
Tactic: let ⟨x, ⟨xs, xt⟩⟩ := h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
⊢ ediam (Set.pi (α := X) univ s) ≤ c
have refine : ∀ (x : (i : ι) → X i) (hx : x ∈ Set.pi (α := X) univ s) (y : (i : ι) → X i) (hy : y ∈ Set.pi (α := X) univ s) (b : ι),
  edist (x b) (y b) ≤ c
Tactic: refine ediam_le fun x hx y hy => edist_pi_le_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Diam (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : x ∈ Set.pi (α := X) univ s
y : (i : ι) → X i
hy : y ∈ Set.pi (α := X) univ s
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c
have rw : ∀ (hx : ∀ (i : ι), x i ∈ s i) (y : (i : ι) → X i) (hy : ∀ (i : ι), y i ∈ s i) (b : ι), edist (x b) (y b) ≤ c
Tactic: rw [mem_univ_pi] at hx hy
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
have obtain : ∀ (K : ℝ≥0) (u : Set α) (hu : u ∈ 𝓝[t] x) (hfu : LipschitzOnWith K f u),
  ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Tactic: obtain ⟨K, u, hu, hfu⟩ := hf (h hx)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict (π := fun (a : α) ↦ β) f)
have simp : (∀ (x : (↑s : Type u)), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
  ∀ (x : (↑s : Type u)),
    ∃ (K : ℝ≥0) (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: simp only [LocallyLipschitzOn, LocallyLipschitz, SetCoe.forall',
    lipschitzOnWith_restrict,
    nhds_subtype_eq_comap_nhdsWithin, mem_comap]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ (∀ (x : (↑s : Type u)), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
    ∀ (x : (↑s : Type u)),
      ∃ (K : ℝ≥0) (t : Set (↑s : Type u)),
        (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
          LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
have a : ∀ (x : (↑s : Type u)) (K : ℝ≥0),
  (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
    ∃ (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: congr! with x K
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
x : (↑s : Type u)
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
    ∃ (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
have a : (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) →
  ∃ (t : Set (↑s : Type u)),
    (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
      LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
x : (↑s : Type u)
K : ℝ≥0
a :
  (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) →
    ∃ (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
    ∃ (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
have a₁ : (∃ (t : Set (↑s : Type u)),
    (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
      LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)) →
  ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ edist (f x) (f y) < (↑K : ℝ≥0∞) * r
have grw : (↑K : ℝ≥0∞) * edist x y < (↑K : ℝ≥0∞) * r
Tactic: grw [h x y]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ (↑K : ℝ≥0∞) * edist x y < (↑K : ℝ≥0∞) * r
have hinf : (↑K : ℝ≥0∞) ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ (↑K : ℝ≥0∞)⁻¹ * edist (f x) (f y) ≤ edist x y
have rw : edist (f x) (f y) / (↑K : ℝ≥0∞) ≤ edist x y
Tactic: rw [mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ediam (f '' s) ≤ (↑K : ℝ≥0∞) * ediam s
have h : ∀ x ∈ f '' s, ∀ y ∈ f '' s, edist x y ≤ (↑K : ℝ≥0∞) * ediam s
Tactic: apply Metric.ediam_le
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
⊢ (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist x y) = (↑(Kf * Kg) : ℝ≥0∞) * edist x y
have rw : (↑Kf : ℝ≥0∞) * (↑Kg : ℝ≥0∞) * edist x y = (↑(Kf * Kg) : ℝ≥0∞) * edist x y
Tactic: rw [← mul_assoc, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
rw : (↑Kf : ℝ≥0∞) * (↑Kg : ℝ≥0∞) * edist x y = (↑(Kf * Kg) : ℝ≥0∞) * edist x y
⊢ (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist x y) = (↑(Kf * Kg) : ℝ≥0∞) * edist x y
have rw₁ : (↑Kf : ℝ≥0∞) * (↑Kg : ℝ≥0∞) * edist x y = (↑Kf : ℝ≥0∞) * (↑Kg : ℝ≥0∞) * edist x y
Tactic: rw [← mul_assoc, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist (α := β × γ) ((fun (x : α) ↦ (f x, g x)) x) ((fun (x : α) ↦ (f x, g x)) y) ≤ (↑(max Kf Kg) : ℝ≥0∞) * edist x y
have rw : max (edist.{v} (α := β) ((fun (x : α) ↦ (f x, g x)) x).1 ((fun (x : α) ↦ (f x, g x)) y).1)
    (edist.{w} (α := γ) ((fun (x : α) ↦ (f x, g x)) x).2 ((fun (x : α) ↦ (f x, g x)) y).2) ≤
  max ((↑Kf : ℝ≥0∞) * edist x y) ((↑Kg : ℝ≥0∞) * edist x y)
Tactic: rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith.{u, w} (β := γ) Kα fun (a : α) ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (uncurry f (a₁, b₁)) (uncurry f (a₂, b₂)) ≤ (↑(Kα + Kβ) : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)
have simp : edist (f a₁ b₁) (f a₂ b₂) ≤ (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)
Tactic: simp only [Function.uncurry, ENNReal.coe_add, add_mul]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith.{u, w} (β := γ) Kα fun (a : α) ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)
have apply : edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤
  (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)
Tactic: apply le_trans (edist_triangle _ (f a₂ b₁) _)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) f^[n + 1]
have rw : LipschitzWith (K ^ n * K) f^[n + 1]
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n
have rw : edist (f^[n] x) ((f^[n] ∘ f) x) ≤ (↑K : ℝ≥0∞) ^ n * edist x (f x)
Tactic: rw [iterate_succ, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
ι : Type x
inst : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (List.map K (i :: l)).prod (List.map f (i :: l)).prod
have simp : LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)
Tactic: simp only [List.map_cons, List.prod_cons]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) (f ^ (n + 1))
have rw : LipschitzWith (K ^ n * K) (f ^ n * f)
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (α := β × γ) ((fun (x : α) ↦ (f x, g x)) x) ((fun (x : α) ↦ (f x, g x)) y) ≤ (↑(max Kf Kg) : ℝ≥0∞) * edist x y
have rw : max (edist.{v} (α := β) ((fun (x : α) ↦ (f x, g x)) x).1 ((fun (x : α) ↦ (f x, g x)) y).1)
    (edist.{w} (α := γ) ((fun (x : α) ↦ (f x, g x)) x).2 ((fun (x : α) ↦ (f x, g x)) y).2) ≤
  max ((↑Kf : ℝ≥0∞) * edist x y) ((↑Kg : ℝ≥0∞) * edist x y)
Tactic: rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]