-- Mathlib/Analysis/InnerProductSpace/Positive.lean
lemma isUnit_of_forall_le_norm_inner_map (f : E →L[𝕜] E) {c : ℝ≥0} (hc : 0 < c)
    (h : ∀ x, ‖x‖ ^ 2 * c ≤ ‖⟪f x, x⟫_𝕜‖) : IsUnit f

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
x : E
hx : x ∈ (LinearMap.range f)ᗮ
⊢ ‖x‖ ^ 2 * ↑c ≤ 0

Tactic:
simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
⊢ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f

Tactic:
have h_anti : AntilipschitzWith c⁻¹ f := antilipschitz_of_forall_le_inner_map f hc h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
⊢ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
⊢ (LinearMap.range f).topologicalClosure = ⊤

Tactic:
have _inst := h_anti.completeSpace_range_clm

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
⊢ (LinearMap.range f).topologicalClosure = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
x : E
hx : x ∈ (LinearMap.range f)ᗮ
⊢ 0 ≤ ‖x‖ ^ 2 * ↑c

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
⊢ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f

Tactic:
refine ⟨?_, ⟨_, h_anti⟩⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
⊢ (LinearMap.range f).topologicalClosure = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
x : E
hx : x ∈ (LinearMap.range f)ᗮ
this : ‖x‖ ^ 2 * ↑c = 0
⊢ x = 0

Tactic:
aesop

Result:
no goals

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

Tactic:
rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
⊢ (LinearMap.range f).topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
x : E
hx : x ∈ (LinearMap.range f)ᗮ
⊢ x = 0

Tactic:
have : ‖x‖ ^ 2 * c = 0 := le_antisymm (by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x)
  (by positivity)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
x : E
hx : x ∈ (LinearMap.range f)ᗮ
this : ‖x‖ ^ 2 * ↑c = 0
⊢ x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
⊢ (LinearMap.range f).topologicalClosure = ⊤

Tactic:
rw [Submodule.topologicalClosure_eq_top_iff, Submodule.eq_bot_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
⊢ ∀ x ∈ (LinearMap.range f)ᗮ, x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
⊢ ∀ x ∈ (LinearMap.range f)ᗮ, x = 0

Tactic:
intro x hx

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫_𝕜‖
h_anti : AntilipschitzWith c⁻¹ ⇑f
_inst : CompleteSpace ↥(LinearMap.range f)
x : E
hx : x ∈ (LinearMap.range f)ᗮ
⊢ x = 0