-- Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean
theorem antilipschitz (coercive : IsCoercive B) : ∃ C : ℝ≥0, 0 < C ∧ AntilipschitzWith C B♯

Proof state:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ AntilipschitzWith C⁻¹.toNNReal ⇑(continuousLinearMapOfBilin B)

Tactic:
refine ContinuousLinearMap.antilipschitz_of_bound B♯ ?_

Result:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), ‖x‖ ≤ ↑C⁻¹.toNNReal * ‖(continuousLinearMapOfBilin B) x‖

Proof state:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ⇑(continuousLinearMapOfBilin B)

Tactic:
refine ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), ?_⟩

Result:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ AntilipschitzWith C⁻¹.toNNReal ⇑(continuousLinearMapOfBilin B)

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ⇑(continuousLinearMapOfBilin B)

Tactic:
rcases coercive.bounded_below with ⟨C, C_pos, below_bound⟩

Result:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∃ C, 0 < C ∧ AntilipschitzWith C ⇑(continuousLinearMapOfBilin B)

Proof state:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ ‖(continuousLinearMapOfBilin B) x‖

Tactic:
simpa using below_bound

Result:
no goals

Proof state:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), ‖x‖ ≤ ↑C⁻¹.toNNReal * ‖(continuousLinearMapOfBilin B) x‖

Tactic:
simp_rw [Real.coe_toNNReal', max_eq_left_of_lt (inv_pos.mpr C_pos), ←
  inv_mul_le_iff₀ (inv_pos.mpr C_pos)]

Result:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
⊢ ∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ ‖(continuousLinearMapOfBilin B) x‖