-- Mathlib/Analysis/InnerProductSpace/Positive.lean
lemma antilipschitz_of_forall_le_inner_map {H : Type*} [NormedAddCommGroup H]
    [InnerProductSpace 𝕜 H] (f : H →L[𝕜] H) {c : ℝ≥0} (hc : 0 < c)
    (h : ∀ x, ‖x‖ ^ 2 * c ≤ ‖⟪f x, x⟫_𝕜‖) : AntilipschitzWith c⁻¹ f

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
x : H
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
simp_rw [sq, mul_assoc] at h

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
by_cases hx0 : x = 0

Result:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
hx0 : x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
hx0 : ¬x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
hx0 : ¬x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
apply (map_le_map_iff <| OrderIso.mulLeft₀ ‖x‖ (norm_pos_iff.mpr hx0)).mp

Result:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
hx0 : ¬x = 0
⊢ (OrderIso.mulLeft₀ ‖x‖ ⋯) (‖x‖ * ↑c) ≤ (OrderIso.mulLeft₀ ‖x‖ ⋯) ‖f x‖

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
x : H
⊢ 0 < ↑c

Tactic:
exact_mod_cast hc

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
⊢ AntilipschitzWith c⁻¹ ⇑f

Tactic:
refine f.antilipschitz_of_bound (K := c⁻¹) fun x ↦ ?_

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
x : H
⊢ ‖x‖ ≤ ↑c⁻¹ * ‖f x‖

Proof state:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
hx0 : x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
simp [hx0]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
x : H
⊢ ‖x‖ ≤ ↑c⁻¹ * ‖f x‖

Tactic:
rw [NNReal.coe_inv, inv_mul_eq_div, le_div_iff₀ (by exact_mod_cast hc)]

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
x : H
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫_𝕜‖
hx0 : ¬x = 0
⊢ (OrderIso.mulLeft₀ ‖x‖ ⋯) (‖x‖ * ↑c) ≤ (OrderIso.mulLeft₀ ‖x‖ ⋯) ‖f x‖

Tactic:
exact (h x).trans <| (norm_inner_le_norm _ _).trans <| (mul_comm _ _).le

Result:
no goals