awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F →L[ℝ] G
h : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
⊢ Ne (α := WithTop ℕ∞) 2 (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F →L[ℝ] G
h : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
a : E
h₁a : ContDiffWithinAt ℝ 2 f s a
⊢ a ∈ s → Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) a) (((⇑l : (a : F) → G) ∘ Δ[s] f) a)

Tactic:
h₁a.laplacianWithin_CLM_comp_left hs

Premises used: ContDiffWithinAt.laplacianWithin_CLM_comp_left
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F →L[ℝ] G
h : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ContDiffWithinAt ℝ 2 f s x) x} x →
          Membership.mem (γ := Set E)
            {x : E |
              Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ x ∈ s) x} x →
                Membership.mem (γ := Set E)
                  {x : E |
                    (fun (x : E) ↦
                        Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) x) (((⇑l : (a : F) → G) ∘ Δ[s] f) x))
                      x}
                  x}
            x}
      a
h₂ h₃ :
  ∀ (a : E) (h₁a : ContDiffWithinAt ℝ 2 f s a),
    a ∈ s → Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) a) (((⇑l : (a : F) → G) ∘ Δ[s] f) a)
⊢ EventuallyEq.{u_2, u_4} (β := G) (𝓝[s] x) (Δ[s] (⇑l : (a : F) → G) ∘ f) ((⇑l : (a : F) → G) ∘ Δ[s] f)

Tactic:
filter_upwards [(h.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
    eventually_mem_nhdsWithin] with a h₁a using h₁a.laplacianWithin_CLM_comp_left hs

Premises used: Filter.Eventually.filter_mono, ContDiffWithinAt.eventually, eventually_mem_nhdsWithin, Set.subset_insert, nhdsWithin_mono
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
l : F →L[ℝ] G
h : ContDiffAt ℝ 2 f x
⊢ Ne (α := WithTop ℕ∞) 2 (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
l : F →L[ℝ] G
h : ContDiffAt ℝ 2 f x
h₁ : ∀ (a : E) (ha : ContDiffAt ℝ 2 f a), Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) a = ((⇑l : (a : F) → G) ∘ Δ f) a
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) =ᶠ[𝓝 x] (⇑l : (a : F) → G) ∘ Δ f

Tactic:
filter_upwards [h.eventually (by simp)] with a ha

Premises used: ContDiffAt.eventually
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
l : F →L[ℝ] G
h : ContDiffAt ℝ 2 f x
a : E
ha : ContDiffAt ℝ 2 f a
h₁ h₂ : Eq.{u_4 + 1} (α := G) (((⇑l : (a : F) → G) ∘ Δ f) a) (((⇑l : (a : F) → G) ∘ Δ f) a)
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) a = ((⇑l : (a : F) → G) ∘ Δ f) a

Tactic:
rw [ha.laplacian_CLM_comp_left]

Premises used: ContDiffAt.laplacian_CLM_comp_left
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F ≃L[ℝ] G
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) x) (((⇑l : (a : F) → G) ∘ Δ[s] f) x)

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    l.iteratedFDerivWithin_comp_left _ hs hx]

Premises used: InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, ContinuousLinearEquiv.iteratedFDerivWithin_comp_left
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
l : F ≃L[ℝ] G
h : ∀ (x : E), Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) x = ((⇑l : (a : F) → G) ∘ Δ f) x
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) = (⇑l : (a : F) → G) ∘ Δ f

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
l : F ≃L[ℝ] G
x : E
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) x = ((⇑l : (a : F) → G) ∘ Δ f) x

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, l.iteratedFDeriv_comp_left]

Premises used: ContinuousLinearEquiv.iteratedFDeriv_comp_left, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
rcases :
  ∀ (C : ℝ) (C_ge_0 : 0 < C)
    (coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u),
    ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)

Tactic:
rcases coercive with ⟨C, C_ge_0, coercivity⟩
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)

Tactic:
⟨C, C_ge_0, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
refine : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)

Tactic:
refine ⟨C, C_ge_0, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
pos : ∀ (h : 0 < ‖v‖), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
neg : ∀ (h : ¬0 < ‖v‖), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
⊢ C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)

Tactic:
by_cases h : 0 < ‖v‖
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)

Tactic:
(mul_le_mul_iff_left₀ h).mp ?_

Premises used: Iff.mp, mul_le_mul_iff_left₀
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : 0 < ‖v‖
pos : C * ‖v‖ * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V) * ‖v‖
⊢ C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)

Tactic:
refine (mul_le_mul_iff_left₀ h).mp ?_

Premises used: Iff.mp, mul_le_mul_iff_left₀
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ * ‖v‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) v : V →L[ℝ] ℝ) : (a : V) → ℝ) v

Tactic:
coercivity v
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : 0 < ‖v‖
⊢ (((B : (a : V) → V →L[ℝ] ℝ) v : V →L[ℝ] ℝ) : (a : V) → ℝ) v = ⟪(continuousLinearMapOfBilin B : (a : V) → V) v, v⟫

Tactic:
(continuousLinearMapOfBilin_apply B v v).symm

Premises used: InnerProductSpace.continuousLinearMapOfBilin_apply, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : 0 < ‖v‖
⊢ ⟪(continuousLinearMapOfBilin B : (a : V) → V) v, v⟫ ≤
    norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V) * ‖v‖

Tactic:
real_inner_le_norm (B♯ v) v

Premises used: real_inner_le_norm, InnerProductSpace.continuousLinearMapOfBilin, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V) * ‖v‖

Tactic:
calc
      C * ‖v‖ * ‖v‖ ≤ B v v := coercivity v
      _ = ⟪B♯ v, v⟫_ℝ := (continuousLinearMapOfBilin_apply B v v).symm
      _ ≤ ‖B♯ v‖ * ‖v‖ := real_inner_le_norm (B♯ v) v

Premises used: real_inner_le_norm, InnerProductSpace.continuousLinearMapOfBilin, InnerProductSpace.continuousLinearMapOfBilin_apply, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : ¬0 < ‖v‖
⊢ v = 0

Tactic:
simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : ¬0 < ‖v‖
⊢ v = 0

Tactic:
have : v = 0 := by simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : ¬0 < ‖v‖
this : v = 0
⊢ C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
rcases :
  ∀ (C : ℝ) (C_pos : 0 < C)
    (below_bound : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)),
    ∃ (C : ℝ≥0), 0 < C ∧ AntilipschitzWith (α := V) (β := V) C (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
⊢ ∃ (C : ℝ≥0), 0 < C ∧ AntilipschitzWith (α := V) (β := V) C (⇑(continuousLinearMapOfBilin B) : (a : V) → V)

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

Premises used: IsCoercive.bounded_below
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
⊢ ∃ (C : ℝ≥0), 0 < C ∧ AntilipschitzWith (α := V) (β := V) C (⇑(continuousLinearMapOfBilin B) : (a : V) → V)

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

Premises used: Iff.mpr, inv_pos, Real.toNNReal_pos, Inv.inv, And.intro, Exists.intro, Real.toNNReal
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
refine : AntilipschitzWith (α := V) (β := V) C⁻¹.toNNReal (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
⊢ ∃ (C : ℝ≥0), 0 < C ∧ AntilipschitzWith (α := V) (β := V) C (⇑(continuousLinearMapOfBilin B) : (a : V) → V)

Tactic:
refine ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
⊢ AntilipschitzWith (α := V) (β := V) C⁻¹.toNNReal (⇑(continuousLinearMapOfBilin B) : (a : V) → V)

Tactic:
ContinuousLinearMap.antilipschitz_of_bound B♯ ?_

Premises used: InnerProductSpace.continuousLinearMapOfBilin, ContinuousLinearMap.antilipschitz_of_bound
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
refine : ∀ (x : V), ‖x‖ ≤ (↑C⁻¹.toNNReal : ℝ) * norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) x : V)
⊢ AntilipschitzWith (α := V) (β := V) C⁻¹.toNNReal (⇑(continuousLinearMapOfBilin B) : (a : V) → V)

Tactic:
refine ContinuousLinearMap.antilipschitz_of_bound B♯ ?_

Premises used: InnerProductSpace.continuousLinearMapOfBilin, ContinuousLinearMap.antilipschitz_of_bound
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
simp_rw : ∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) x : V)
⊢ ∀ (x : V), ‖x‖ ≤ (↑C⁻¹.toNNReal : ℝ) * norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) x : V)

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)]

Premises used: Iff.mpr, Real.coe_toNNReal', inv_pos, inv_mul_le_iff₀, max_eq_left_of_lt
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
C : ℝ
C_pos : 0 < C
below_bound : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
⊢ ∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) x : V)

Tactic:
simpa using below_bound
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
rw : Function.Injective (α := V) (β := V) (⇑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V) : (a : V) → V)
⊢ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).ker = ⊥

Tactic:
rw [LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
rcases :
  ∀ (w : ℝ≥0),
    0 < w →
      ∀ (antilipschitz : AntilipschitzWith (α := V) (β := V) w (⇑(continuousLinearMapOfBilin B) : (a : V) → V)),
        Function.Injective (α := V) (β := V) (⇑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V) : (a : V) → V)
⊢ Function.Injective (α := V) (β := V) (⇑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V) : (a : V) → V)

Tactic:
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩

Premises used: IsCoercive.antilipschitz
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w : ℝ≥0
left : 0 < w
antilipschitz : AntilipschitzWith (α := V) (β := V) w (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
⊢ Function.Injective (α := V) (β := V) (⇑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V) : (a : V) → V)

Tactic:
antilipschitz.injective

Premises used: AntilipschitzWith.injective
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w : ℝ≥0
left : 0 < w
antilipschitz : AntilipschitzWith (α := V) (β := V) w (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
⊢ Function.Injective (α := V) (β := V) (⇑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V) : (a : V) → V)

Tactic:
exact antilipschitz.injective

Premises used: AntilipschitzWith.injective
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
rcases :
  ∀ (w : ℝ≥0),
    0 < w →
      ∀ (antilipschitz : AntilipschitzWith (α := V) (β := V) w (⇑(continuousLinearMapOfBilin B) : (a : V) → V)),
        IsClosed (↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V)
⊢ IsClosed (↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V)

Tactic:
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩

Premises used: IsCoercive.antilipschitz
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w : ℝ≥0
left : 0 < w
antilipschitz : AntilipschitzWith (α := V) (β := V) w (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
⊢ IsClosed (↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V)

Tactic:
antilipschitz.isClosed_range B♯.uniformContinuous

Premises used: AntilipschitzWith.isClosed_range, setOf, ContinuousLinearMap.uniformContinuous, InnerProductSpace.continuousLinearMapOfBilin, Set.range
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w : ℝ≥0
left : 0 < w
antilipschitz : AntilipschitzWith (α := V) (β := V) w (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
⊢ IsClosed (↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V)

Tactic:
exact antilipschitz.isClosed_range B♯.uniformContinuous

Premises used: AntilipschitzWith.isClosed_range, ContinuousLinearMap.uniformContinuous, InnerProductSpace.continuousLinearMapOfBilin
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ CompleteSpace.{u} (↑(↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V) : Type u)

Tactic:
haveI := coercive.isClosed_range.completeSpace_coe
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace.{u} (↑(↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V) : Type u)
rw : (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮᗮ = ⊤
⊢ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range = ⊤

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

Premises used: Submodule.orthogonal_orthogonal, LinearMap.range, ContinuousLinearMap.toLinearMap, InnerProductSpace.continuousLinearMapOfBilin
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace.{u} (↑(↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V) : Type u)
rw : ∀ (x : V), x ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮᗮ
⊢ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮᗮ = ⊤

Tactic:
rw [Submodule.eq_top_iff']

Premises used: Submodule.eq_top_iff'
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace.{u} (↑(↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V) : Type u)
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮ
rcases :
  ∀ (C : ℝ) (C_pos : 0 < C)
    (coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u), ⟪w, v⟫ = 0
⊢ ⟪w, v⟫ = 0

Tactic:
rcases coercive with ⟨C, C_pos, coercivity⟩
-- Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace.{u} (↑(↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V) : Type u)
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
rw : C * ‖w‖ * ‖w‖ = 0
⊢ w = 0

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

Premises used: norm_eq_zero, mul_self_eq_zero, mul_assoc, MulZeroClass.mul_zero, LT.lt.ne', mul_right_inj'