Theorem: LipschitzWith.le (Ray/Hartogs/Duals.lean)

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f x ≤ f y + ↑k * dist x y
Tactic:
calc f x
  _ = f y + (f x - f y) := by ring_nf
  _ ≤ f y + |f x - f y| := by bound
  _ = f y + dist (f x) (f y) := by rw [Real.dist_eq]
  _ ≤ f y + k * dist x y := by linarith [fk.dist_le_mul x y]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f x = f y + (f x - f y)
Tactic:
ring_nf
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f y + (f x - f y) ≤ f y + |f x - f y|
Tactic:
bound
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f y + |f x - f y| = f y + dist (f x) (f y)
Tactic:
rw [Real.dist_eq]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f y + dist (f x) (f y) ≤ f y + ↑k * dist x y
Tactic:
linarith [fk.dist_le_mul x y]
State after:
no goals