-- Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean
theorem range_eq_top (coercive : IsCoercive B) : range B♯ = ⊤

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ w = 0

Tactic:
rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ←
  mul_assoc]

Result:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * ‖w‖ * ‖w‖ = 0

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ ∀ (x : V), x ∈ (range (continuousLinearMapOfBilin B))ᗮᗮ

Tactic:
intro v w mem_w_orthogonal

Result:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ ⟪w, v⟫_ℝ = 0

Proof state:
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖

Tactic:
positivity

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[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v : V
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
mem_w_orthogonal : 0 ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ ⟪0, v⟫_ℝ = 0

Tactic:
exact inner_zero_left _

Result:
no goals

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ (range (continuousLinearMapOfBilin B))ᗮᗮ = ⊤

Tactic:
rw [Submodule.eq_top_iff']

Result:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ ∀ (x : V), x ∈ (range (continuousLinearMapOfBilin B))ᗮᗮ

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
⊢ ⟪w, v⟫_ℝ = 0

Tactic:
rcases coercive with ⟨C, C_pos, coercivity⟩

Result:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ ⟪w, v⟫_ℝ = 0

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ range (continuousLinearMapOfBilin B) = ⊤

Tactic:
haveI := coercive.isClosed_range.completeSpace_coe

Result:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ range (continuousLinearMapOfBilin B) = ⊤

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ range (continuousLinearMapOfBilin B) = ⊤

Tactic:
rw [← (range B♯).orthogonal_orthogonal]

Result:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
⊢ (range (continuousLinearMapOfBilin B))ᗮᗮ = ⊤

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * ‖w‖ * ‖w‖ = 0

Tactic:
apply le_antisymm

Result:
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * ‖w‖ * ‖w‖ ≤ 0

case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖

Proof state:
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))
v w : V
mem_w_orthogonal : w ∈ (range (continuousLinearMapOfBilin B))ᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * ‖w‖ * ‖w‖ ≤ 0

Tactic:
calc
  C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
  _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
  _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩

Result:
no goals