-- Mathlib/Topology/Bornology/BoundedOperation.lean
lemma boundedSub_of_lipschitzWith_sub [PseudoMetricSpace R] [Sub R] {K : NNReal}
    (lip : LipschitzWith K (fun (p : R × R) ↦ p.1 - p.2)) :
    BoundedSub R where
  isBounded_sub {s t} s_bdd t_bdd

Proof state:
case h.e'_3.h
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ p ∈ s - t ↔ p ∈ (fun p => p.1 - p.2) '' s ×ˢ t

Tactic:
simp only [Set.mem_image, Set.mem_prod, Prod.exists]

Result:
case h.e'_3.h
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ p ∈ s - t ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p

Proof state:
case h.e'_3
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
⊢ s - t = (fun p => p.1 - p.2) '' s ×ˢ t

Tactic:
ext p

Result:
case h.e'_3.h
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ p ∈ s - t ↔ p ∈ (fun p => p.1 - p.2) '' s ×ˢ t

Proof state:
case h.e'_3.h.mpr
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p) → p ∈ s - t

Tactic:
intro ⟨a, b, ⟨a_in_s, b_in_t⟩, eq_p⟩

Result:
case h.e'_3.h.mpr
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p a b : R
a_in_s : a ∈ s
b_in_t : b ∈ t
eq_p : a - b = p
⊢ p ∈ s - t

Proof state:
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
⊢ Bornology.IsBounded (s - t)

Tactic:
convert lip.isBounded_image bdd

Result:
case h.e'_3
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
⊢ s - t = (fun p => p.1 - p.2) '' s ×ˢ t

Proof state:
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
⊢ Bornology.IsBounded (s - t)

Tactic:
have bdd : Bornology.IsBounded (s ×ˢ t) := Bornology.IsBounded.prod s_bdd t_bdd

Result:
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
⊢ Bornology.IsBounded (s - t)

Proof state:
case h.e'_3.h
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ p ∈ s - t ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p

Tactic:
constructor

Result:
case h.e'_3.h.mp
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ p ∈ s - t → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p

case h.e'_3.h.mpr
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p) → p ∈ s - t

Proof state:
case h.e'_3.h.mpr
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p a b : R
a_in_s : a ∈ s
b_in_t : b ∈ t
eq_p : a - b = p
⊢ p ∈ s - t

Tactic:
simpa [← eq_p] using Set.sub_mem_sub a_in_s b_in_t

Result:
no goals

Proof state:
case h.e'_3.h.mp
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p a : R
a_in_s : a ∈ s
b : R
b_in_t : b ∈ t
eq_p : (fun x1 x2 => x1 - x2) a b = p
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p

Tactic:
exact ⟨a, b, ⟨a_in_s, b_in_t⟩, eq_p⟩

Result:
no goals

Proof state:
case h.e'_3.h.mp
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p : R
⊢ p ∈ s - t → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p

Tactic:
intro ⟨a, a_in_s, b, b_in_t, eq_p⟩

Result:
case h.e'_3.h.mp
R : Type u_1
inst✝¹ : PseudoMetricSpace R
inst✝ : Sub R
K : ℝ≥0
lip : LipschitzWith K fun p => p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
p a : R
a_in_s : a ∈ s
b : R
b_in_t : b ∈ t
eq_p : (fun x1 x2 => x1 - x2) a b = p
⊢ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a - b = p