awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : C * ‖w‖ * ‖w‖ ≤ 0
a₁ : 0 ≤ C * ‖w‖ * ‖w‖
⊢ C * ‖w‖ * ‖w‖ = 0

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
⊢ C * ‖w‖ * ‖w‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) w : V →L[ℝ] ℝ) : (a : V) → ℝ) w

Tactic:
coercivity w
-- 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
⊢ (((B : (a : V) → V →L[ℝ] ℝ) w : V →L[ℝ] ℝ) : (a : V) → ℝ) w = ⟪(continuousLinearMapOfBilin B : (a : V) → V) w, w⟫

Tactic:
(continuousLinearMapOfBilin_apply B w w).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[ℝ] ℝ
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
⊢ ⟪(continuousLinearMapOfBilin B : (a : V) → V) w, w⟫ = 0

Tactic:
mem_w_orthogonal _ ⟨w, rfl⟩

Premises used: Exists.intro, rfl
-- 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
⊢ 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⟩

Premises used: InnerProductSpace.continuousLinearMapOfBilin, Exists.intro, InnerProductSpace.continuousLinearMapOfBilin_apply, Eq.symm, DFunLike.coe, rfl
-- 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
⊢ 0 ≤ C * ‖w‖ * ‖w‖

Tactic:
positivity
-- 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
obtain : ∀ (mem_w_orthogonal : 0 ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮ), ⟪0, v⟫ = 0
⊢ ⟪w, 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

Premises used: rfl
-- 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 : V
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
mem_w_orthogonal : 0 ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮ
⊢ ⟪0, v⟫ = 0

Tactic:
inner_zero_left _

Premises used: inner_zero_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[ℝ] ℝ
this : CompleteSpace.{u} (↑(↑(↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).range : Set V) : Type u)
v : V
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
mem_w_orthogonal : 0 ∈ (↑(continuousLinearMapOfBilin B) : V →ₗ[ℝ] V).rangeᗮ
⊢ ⟪0, v⟫ = 0

Tactic:
exact inner_zero_left _

Premises used: inner_zero_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[ℝ] ℝ
coercive : IsCoercive B
v w : V
⊢ ⟪(coercive.continuousLinearEquivOfBilin : (a : V) → V) v, w⟫ =
    (((B : (a : V) → V →L[ℝ] ℝ) v : V →L[ℝ] ℝ) : (a : V) → ℝ) w

Tactic:
continuousLinearMapOfBilin_apply B v w

Premises used: Classical.choose, InnerProductSpace.continuousLinearMapOfBilin_apply
-- 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
v f : V
is_lax_milgram : ∀ (w : V), ⟪f, w⟫ = (((B : (a : V) → V →L[ℝ] ℝ) v : V →L[ℝ] ℝ) : (a : V) → ℝ) w
⊢ f = (coercive.continuousLinearEquivOfBilin : (a : V) → V) v

Tactic:
unique_continuousLinearMapOfBilin B is_lax_milgram

Premises used: InnerProductSpace.unique_continuousLinearMapOfBilin, Classical.choose
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
V : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
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
⊢ ⟪(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

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]

Premises used: pow_two, map_sub, mul_sub, mul_assoc, neg_one_mul, map_add, neg_neg, inner_add_left, inner_add_right, inner_sub_left, sub_sub, inner_smul_right, inner_sub_right, Complex.I_sq, mul_add, Complex.conj_I, one_mul, mul_neg, map_smul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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, 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:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
V : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
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
⊢ ⟪(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

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]

Premises used: pow_two, map_sub, mul_sub, mul_assoc, neg_one_mul, map_add, neg_neg, inner_add_left, inner_add_right, inner_sub_left, sub_sub, inner_smul_right, inner_sub_right, Complex.I_sq, mul_add, Complex.conj_I, one_mul, mul_neg, map_smul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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, 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:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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
mpr : T = 0 → ∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0
⊢ (∀ (x : V), ⟪(T : (a : V) → V) x, x⟫_ℂ = 0) ↔ T = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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
mp : ∀ (x : V), Eq (α := V) ((T : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)
⊢ T = 0

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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
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
⊢ Eq (α := V) ((T : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)

Tactic:
rw [LinearMap.zero_apply, ← @inner_self_eq_zero ℂ V, inner_map_polarization]

Premises used: LinearMap.zero_apply, inner_self_eq_zero, inner_map_polarization
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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
mp : (HSub.hSub (α := ℂ) 0 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0
⊢ (⟪(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:
simp only [hT]
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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
⊢ (HSub.hSub (α := ℂ) 0 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
x : V
⊢ ⟪(0 : (a : V) → V) x, x⟫_ℂ = 0

Tactic:
simp only [LinearMap.zero_apply, inner_zero_left]

Premises used: LinearMap.zero_apply, inner_zero_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
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
⊢ (∀ (x : V), ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ) ↔ S = T

Tactic:
rw [← sub_eq_zero, ← inner_map_self_eq_zero]

Premises used: sub_eq_zero, inner_map_self_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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

Tactic:
forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
V : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
refine : ∀ (x : V), ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0
⊢ (∀ (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:
refine forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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
rw₂ 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⟫_ℂ
⊢ ⟪(S : (a : V) → V) x, x⟫_ℂ = ⟪(T : (a : V) → V) x, x⟫_ℂ ↔ ⟪(S - T : (a : V) → V) x, x⟫_ℂ = 0

Tactic:
rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]

Premises used: sub_eq_zero, inner_sub_left, LinearMap.sub_apply
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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 y : E
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫

Tactic:
simp [inner_eq_sum_norm_sq_div_four, ← f.norm_map]

Premises used: LinearIsometry.norm_map, inner_eq_sum_norm_sq_div_four
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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 y : E
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫

Tactic:
f.toLinearIsometry.inner_map_map x y

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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'
rw : ⟪x, (f.symm : (a : E') → E) y⟫
| ⟪(f : (a : E) → E') x, y⟫

Tactic:
rw [← f.apply_symm_apply y, f.inner_map_map]

Premises used: LinearIsometryEquiv.apply_symm_apply, LinearIsometryEquiv.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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⟫
conv_lhs₁ : ⟪x, (f.symm : (a : E') → E) y⟫ = ⟪x, (f.symm : (a : E') → E) y⟫
⊢ ⟪(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]

Premises used: LinearIsometryEquiv.apply_symm_apply, LinearIsometryEquiv.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
f : E →ₗ[𝕜] E'
h : ∀ (x y : E), inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
x : E
⊢ Norm.norm.{u_7} (E := E') ((f : (a : E) → E') x : E') = ‖x‖

Tactic:
simp only [@norm_eq_sqrt_re_inner 𝕜, h]

Premises used: norm_eq_sqrt_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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'
h : ∀ (x y : E), inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
⊢ Eq (α := (a : E) → E') (⇑(f.isometryOfInner h) : (a : E) → E') (⇑f : (a : E) → E')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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'
h : ∀ (x y : E), inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
⊢ (f.isometryOfInner h).toLinearMap = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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'
h : ∀ (x y : E), inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
⊢ Eq (α := (a : E) → E') (⇑(f.isometryOfInner h) : (a : E) → E') (⇑f : (a : E) → E')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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'
h : ∀ (x y : E), inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
⊢ (f.isometryOfInner h).toLinearEquiv = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
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 : Type u_9
inst_5 : FunLike F E E'
inst_6 : LinearMapClass F 𝕜 E E'
f : F
⊢ (∀ (x : E), Norm.norm.{u_7} (E := E') ((f : (a : E) → E') x : E') = ‖x‖) ↔
    ∀ (x y : E), inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫

Tactic:
⟨({ toLinearMap := LinearMapClass.linearMap f, norm_map' := · : E →ₗᵢ[𝕜] E' }.inner_map_map),
    (LinearMapClass.linearMap f |>.isometryOfInner · |>.norm_map)⟩

Premises used: LinearIsometry.norm_map, LinearIsometry.mk, LinearIsometry.inner_map_map, LinearMapClass.linearMap, LinearMap.isometryOfInner, Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
x y : E
⊢ Norm.norm.{u_1} (E := 𝕜) ((((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜) ≤ 1 * ‖x‖ * ‖y‖

Tactic:
simp only [norm_inner_le_norm, one_mul, innerₛₗ_apply_apply]

Premises used: innerₛₗ_apply_apply, one_mul, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
⊢ Eq (α := (a : E) → 𝕜) (⇑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) fun (w : E) ↦ ⟪v, w⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w = ⟪v, w⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
⊢ Eq (α := E →ₗ[𝕜] 𝕜) (↑((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) v) : E →ₗ[𝕜] 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) v)

Tactic:
rfl

Premises used: rfl