awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (hypothesis)
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)
have this : v = 0
Tactic: have : v = 0 := by simpa using h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ (C : ℝ≥0), 0 < C ∧ AntilipschitzWith (α := V) (β := V) C (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
have 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)
Tactic: rcases coercive.bounded_below with ⟨C, C_pos, below_bound⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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)
have refine : AntilipschitzWith (α := V) (β := V) C⁻¹.toNNReal (⇑(continuousLinearMapOfBilin B) : (a : V) → V)
Tactic: refine ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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)
have refine : ∀ (x : V), ‖x‖ ≤ (↑C⁻¹.toNNReal : ℝ) * norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) x : V)
Tactic: refine ContinuousLinearMap.antilipschitz_of_bound B♯ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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), ‖x‖ ≤ (↑C⁻¹.toNNReal : ℝ) * norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) x : V)
have simp_rw : ∀ (x : V), C⁻¹⁻¹ * ‖x‖ ≤ 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)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).ker = ⊥
have rw : Function.Injective (α := V) (β := V) (⇑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V) : (a : V) → V)
Tactic: rw [LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective (α := V) (β := V) (⇑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V) : (a : V) → V)
have 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)
Tactic: rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ IsClosed (↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V)
have rcases : ∀ (w : ℝ≥0),
  0 < w →
    ∀ (antilipschitz : AntilipschitzWith (α := V) (β := V) w (⇑(continuousLinearMapOfBilin B) : (a : V) → V)),
      IsClosed (↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V)
Tactic: rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (hypothesis)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range = ⊤
have this : CompleteSpace.{u} (↑(↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V) : Type u)
Tactic: haveI := coercive.isClosed_range.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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)
⊢ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range = ⊤
have rw : (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮᗮ = ⊤
Tactic: rw [← B♯.range.orthogonal_orthogonal]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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)
⊢ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮᗮ = ⊤
have rw : ∀ (x : V), x ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮᗮ
Tactic: rw [Submodule.eq_top_iff']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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ᗮ
⊢ ⟪w, v⟫ = 0
have 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
Tactic: rcases coercive with ⟨C, C_pos, coercivity⟩
Cleared hypotheses: coercive
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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
⊢ w = 0
have rw : C * ‖w‖ * ‖w‖ = 0
Tactic: rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ←
      mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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
⊢ C * ‖w‖ * ‖w‖ = 0
have a : C * ‖w‖ * ‖w‖ ≤ 0
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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
a : C * ‖w‖ * ‖w‖ ≤ 0
⊢ C * ‖w‖ * ‖w‖ = 0
have a₁ : 0 ≤ C * ‖w‖ * ‖w‖
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
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
⊢ ⟪w, v⟫ = 0
have obtain : ∀ (mem_w_orthogonal : 0 ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮ), ⟪0, v⟫ = 0
Tactic: obtain rfl : w = 0 := by
    rw [← norm_eq_zero, ← mul_self_eq_zero, ← mul_right_inj' C_pos.ne', mul_zero, ←
      mul_assoc]
    apply le_antisymm
    · calc
        C * ‖w‖ * ‖w‖ ≤ B w w := coercivity w
        _ = ⟪B♯ w, w⟫_ℝ := (continuousLinearMapOfBilin_apply B w w).symm
        _ = 0 := mem_w_orthogonal _ ⟨w, rfl⟩
    · positivity
Cleared hypotheses: w, mem_w_orthogonal
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪(T : (a : V) → V) y, x⟫_ℂ =
    (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ +
          Complex.I * ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
        Complex.I * ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4
have simp : ⟪(T : (a : V) → V) y, x⟫_ℂ =
  (⟪(T : (a : V) → V) x, x⟫_ℂ + ⟪(T : (a : V) → V) y, x⟫_ℂ + (⟪(T : (a : V) → V) x, y⟫_ℂ + ⟪(T : (a : V) → V) y, y⟫_ℂ) -
          (⟪(T : (a : V) → V) x, x⟫_ℂ -
            (⟪(T : (a : V) → V) y, x⟫_ℂ + (⟪(T : (a : V) → V) x, y⟫_ℂ - ⟪(T : (a : V) → V) y, y⟫_ℂ))) +
        (Complex.I * ⟪(T : (a : V) → V) x, x⟫_ℂ + ⟪(T : (a : V) → V) y, x⟫_ℂ +
          (-⟪(T : (a : V) → V) x, y⟫_ℂ + Complex.I * ⟪(T : (a : V) → V) y, y⟫_ℂ)) -
      (Complex.I * ⟪(T : (a : V) → V) x, x⟫_ℂ -
        (⟪(T : (a : V) → V) y, x⟫_ℂ + (-⟪(T : (a : V) → V) x, y⟫_ℂ - Complex.I * ⟪(T : (a : V) → V) y, y⟫_ℂ)))) /
    4
Tactic: simp only [map_add, map_sub, inner_add_left, inner_add_right, map_smul, inner_smul_left,
    inner_smul_right, Complex.conj_I, ← pow_two, Complex.I_sq, inner_sub_left, inner_sub_right,
    mul_add, ← mul_assoc, mul_neg, neg_neg, one_mul, neg_one_mul, mul_sub, sub_sub]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪(T : (a : V) → V) x, y⟫_ℂ =
    (⟪(T : (a : V) → V) (x + y), x + y⟫_ℂ - ⟪(T : (a : V) → V) (x - y), x - y⟫_ℂ -
          Complex.I * ⟪(T : (a : V) → V) (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪(T : (a : V) → V) (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4
have simp : ⟪(T : (a : V) → V) x, y⟫_ℂ =
  (⟪(T : (a : V) → V) x, x⟫_ℂ + ⟪(T : (a : V) → V) y, x⟫_ℂ + (⟪(T : (a : V) → V) x, y⟫_ℂ + ⟪(T : (a : V) → V) y, y⟫_ℂ) -
        (⟪(T : (a : V) → V) x, x⟫_ℂ -
            (⟪(T : (a : V) → V) y, x⟫_ℂ + (⟪(T : (a : V) → V) x, y⟫_ℂ - ⟪(T : (a : V) → V) y, y⟫_ℂ)) +
          (Complex.I * ⟪(T : (a : V) → V) x, x⟫_ℂ + ⟪(T : (a : V) → V) y, x⟫_ℂ +
            (-⟪(T : (a : V) → V) x, y⟫_ℂ + Complex.I * ⟪(T : (a : V) → V) y, y⟫_ℂ))) +
      (Complex.I * ⟪(T : (a : V) → V) x, x⟫_ℂ -
        (⟪(T : (a : V) → V) y, x⟫_ℂ + (-⟪(T : (a : V) → V) x, y⟫_ℂ - Complex.I * ⟪(T : (a : V) → V) y, y⟫_ℂ)))) /
    4
Tactic: simp only [map_add, map_sub, inner_add_left, inner_add_right, map_smul, inner_smul_left,
    inner_smul_right, Complex.conj_I, ← pow_two, Complex.I_sq, inner_sub_left, inner_sub_right,
    mul_add, ← mul_assoc, mul_neg, neg_neg, one_mul, neg_one_mul, mul_sub, sub_sub]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0) ↔ T = 0
have mp : (∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0) → T = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
mp : (∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0) → T = 0
⊢ (∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0) ↔ T = 0
have mpr : T = 0 → ∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0
⊢ T = 0
have mp : ∀ (x : V), Eq (α := V) ((T : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0
x : V
⊢ Eq (α := V) ((T : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)
have mp : (⟪(T : (a : V) → V) (HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) x),
            HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) x⟫_ℂ -
          ⟪(T : (a : V) → V) (HSub.hSub (α := V) ((T : (a : V) → V) x : V) x),
            HSub.hSub (α := V) ((T : (a : V) → V) x : V) x⟫_ℂ +
        Complex.I *
          ⟪(T : (a : V) → V) (HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)),
            HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)⟫_ℂ -
      Complex.I *
        ⟪(T : (a : V) → V) (HSub.hSub (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)),
          HSub.hSub (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)⟫_ℂ) /
    4 =
  0
Tactic: rw [LinearMap.zero_apply, ← @inner_self_eq_zero ℂ V, inner_map_polarization]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0
x : V
⊢ (⟪(T : (a : V) → V) (HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) x),
              HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) x⟫_ℂ -
            ⟪(T : (a : V) → V) (HSub.hSub (α := V) ((T : (a : V) → V) x : V) x),
              HSub.hSub (α := V) ((T : (a : V) → V) x : V) x⟫_ℂ +
          Complex.I *
            ⟪(T : (a : V) → V) (HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)),
              HAdd.hAdd (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)⟫_ℂ -
        Complex.I *
          ⟪(T : (a : V) → V) (HSub.hSub (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)),
            HSub.hSub (α := V) ((T : (a : V) → V) x : V) (Complex.I • x)⟫_ℂ) /
      4 =
    0
have mp : (HSub.hSub (α := ℂ) 0 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0
Tactic: simp only [hT]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ) ↔ S = T
have rw : (∀ (x : V), ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ) ↔ ∀ (x : V), ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0
Tactic: rw [← sub_eq_zero, ← inner_map_self_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ) ↔ ∀ (x : V), ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0
have refine : ∀ (x : V), ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0
Tactic: refine forall_congr' fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0
have rw : ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔
  ⟪HSub.hSub (α := V) (β := V) ((S : (a : V) → V) x : V) ((T : (a : V) → V) x : V), x⟫_ℂ = 0
Tactic: rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
rw :
  ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔
    ⟪HSub.hSub (α := V) (β := V) ((S : (a : V) → V) x : V) ((T : (a : V) → V) x : V), x⟫_ℂ = 0
⊢ ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0
have rw₁ : ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S : (a : V) → V) x, x⟫_ℂ - ⟪(T : (a : V) → V) x, x⟫_ℂ = 0
Tactic: rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
rw :
  ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔
    ⟪HSub.hSub (α := V) (β := V) ((S : (a : V) → V) x : V) ((T : (a : V) → V) x : V), x⟫_ℂ = 0
rw₁ :
  ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S : (a : V) → V) x, x⟫_ℂ - ⟪(T : (a : V) → V) x, x⟫_ℂ = 0
⊢ ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0
have rw₂ : ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ
Tactic: rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
x : E
y : E'
| ⟪(f : (a : E) → E') x, y⟫
have rw : ⟪x, (f.symm : (a : E') → E) y⟫
Tactic: rw [← f.apply_symm_apply y, f.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
x : E
y : E'
⊢ ⟪(f : (a : E) → E') x, y⟫ = ⟪x, (f.symm : (a : E') → E) y⟫
have conv_lhs : ⟪(f : (a : E) → E') x, y⟫ = ⟪x, (f.symm : (a : E') → E) y⟫
Tactic: conv_lhs => rw [← f.apply_symm_apply y, f.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
x : E
y : E'
conv_lhs : ⟪(f : (a : E) → E') x, y⟫ = ⟪x, (f.symm : (a : E') → E) y⟫
⊢ ⟪(f : (a : E) → E') x, y⟫ = ⟪x, (f.symm : (a : E') → E) y⟫
have conv_lhs₁ : ⟪x, (f.symm : (a : E') → E) y⟫ = ⟪x, (f.symm : (a : E') → E) y⟫
Tactic: conv_lhs => rw [← f.apply_symm_apply y, f.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F →L⋆[ℝ] ℝ) (ContinuousLinearMap.flip (innerSL ℝ)) (innerSL ℝ)
have h : ∀ (v w : F),
  Eq (α := ℝ) ((((ContinuousLinearMap.flip (innerSL ℝ) : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
    ((((innerSL ℝ : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
⊢ Norm.norm (E := E →L[𝕜] 𝕜)
      ((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
        E →L[𝕜] 𝕜) ≤
    ‖f‖ * ‖v‖
have refine : ∀ (x : E),
  Norm.norm.{u_1} (E := 𝕜)
      ((((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          x :
        𝕜) ≤
    ‖f‖ * ‖v‖ * ‖x‖
Tactic: refine opNorm_le_bound _ (by positivity) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
⊢ Norm.norm.{u_1} (E := 𝕜)
      ((((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          x :
        𝕜) ≤
    ‖f‖ * ‖v‖ * ‖x‖
have h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
Tactic: have h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
⊢ Norm.norm.{u_1} (E := 𝕜)
      ((((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          x :
        𝕜) ≤
    ‖f‖ * ‖v‖ * ‖x‖
have h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
Tactic: have h₂ := @norm_inner_le_norm 𝕜 E' _ _ _ v (f x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
⊢ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖v‖ * (‖f‖ * ‖x‖)
have ha : 0 ≤ ‖v‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
⊢ Norm.norm.{u_1} (E := 𝕜)
      ((((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          x :
        𝕜) ≤
    ‖f‖ * ‖v‖ * ‖x‖
have f₁ : ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖v‖ * (‖f‖ * ‖x‖)
Tactic: calc
    ‖⟪v, f x⟫‖ ≤ ‖v‖ * ‖f x‖ := h₂
    _ ≤ ‖v‖ * (‖f‖ * ‖x‖) := by gcongr
    _ = ‖f‖ * ‖v‖ * ‖x‖ := by ring