awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ HMul.hMul (α := E)
      (({ toFun := (⇑((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* E } :
            (a : 𝕜) → E)
          r :
        E)
      x =
    HMul.hMul (β := E) x
      (({ toFun := (⇑((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → E)
          r :
        E)
have dsimp : Eq (α := E)
  ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E) :
    E)
  ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      (x ⊗ₜ[𝕜] (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r : E ⊗[𝕜] E) :
    E)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ Eq (α := E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E) :
      E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        (x ⊗ₜ[𝕜] (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r : E ⊗[𝕜] E) :
      E)
have simp_rw : Eq.{u_2 + 1} (α := E)
  (((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
        (a : 𝕜 ⊗[𝕜] E) → E)
      (r ⊗ₜ[𝕜] x) :
    E)
  (((↑(toLinearEquiv
              (LinearIsometryEquiv.symm
                (LinearIsometryEquiv.symm (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))))) :
          E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
        (a : E ⊗[𝕜] 𝕜) → E)
      (x ⊗ₜ[𝕜] r) :
    E)
Tactic: simp_rw [← rTensor_tmul, ← lTensor_tmul, ← adjoint_lTensor, ← adjoint_rTensor,
      ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, lTensor_counit_comp_comul,
      ← toLinearMap_symm_rid, ← toLinearMap_symm_lid, ← comm_trans_lid,
      ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans,
      ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x =
    HMul.hMul (α := E)
      (({ toFun := (⇑((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → E)
          r :
        E)
      x
have dsimp : r • x =
  (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
    ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x =
    (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E)
have simp_rw : r • x =
  ((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
      (a : 𝕜 ⊗[𝕜] E) → E)
    (r ⊗ₜ[𝕜] x)
Tactic: simp_rw [← rTensor_tmul, ← adjoint_rTensor, ← comp_apply, ← adjoint_comp,
      rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry,
      ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq (α := E →+ 𝕜)
    (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) 0) :
      E →+ 𝕜)
    0
have h : ∀ (x : E),
  Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
            RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) 0) :
          (a : E) → 𝕜)
        x :
      𝕜)
    ((0 : (a : E) → 𝕜) x : 𝕜)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
      RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) (x + y)) =
    HAdd.hAdd (α := E →+ 𝕜) (β := E →+ 𝕜)
      (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
          RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
        E →+ 𝕜)
      (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) y))
have h : ∀ (z : E),
  Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
            RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) (x + y)) :
          (a : E) → 𝕜)
        z :
      𝕜)
    ((HAdd.hAdd (α := E →+ 𝕜) (β := E →+ 𝕜)
            (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
                (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
              E →+ 𝕜)
            (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
              (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) y)) :
          (a : E) → 𝕜)
        z :
      𝕜)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Completion (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
⊢ Continuous.{u_2, u_1} (X := Completion E × Completion E) (uncurry (inner 𝕜))
have this : Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2
Tactic: have : Continuous fun p : E × E => inner' p.1 p.2 := continuous_inner
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
this : Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2
⊢ Continuous.{u_2, u_1} (X := Completion E × Completion E) (uncurry (inner 𝕜))
have rw : Continuous.{u_2, u_1} (X := Completion E × Completion E) (IsDenseInducing.extend sorry (uncurry (inner 𝕜)))
Tactic: rw [Completion.toInner, inner, uncurry_curry _]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Completion (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
this : Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2
⊢ Continuous.{u_2, u_1} (X := Completion E × Completion E) (IsDenseInducing.extend ⋯ (uncurry (inner 𝕜)))
have fun : Continuous.{u_2, u_1} (X := Completion E × Completion E) (Y := 𝕜)
  (IsDenseInducing.extend (i := Prod.map (⇑toCompl : (a : E) → Completion E) (⇑toCompl : (a : E) → Completion E)) sorry
    fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2)
Tactic: change
    Continuous
      (((isDenseInducing_toCompl E).prodMap (isDenseInducing_toCompl E)).extend fun p : E × E =>
        inner' p.1 p.2)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ConformalLinearMap (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ IsConformalMap f ↔
    ∃ (c : ℝ),
      0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫
have mp : IsConformalMap f →
  ∃ (c : ℝ),
    0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ConformalLinearMap (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
mp :
  IsConformalMap f →
    ∃ (c : ℝ),
      0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫
⊢ IsConformalMap f ↔
    ∃ (c : ℝ),
      0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫
have mpr : (∃ (c : ℝ),
    0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫) →
  IsConformalMap f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ConformalLinearMap (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ ∃ (c : ℝ),
    0 < c ∧
      ∀ (u v : E),
        inner.{0, u_2} ℝ (E := F) ((c₁ • li.toContinuousLinearMap : (a : E) → F) u : F)
            ((c₁ • li.toContinuousLinearMap : (a : E) → F) v : F) =
          c * ⟪u, v⟫
have mp : ∀ (u v : E),
  inner.{0, u_2} ℝ (E := F) ((c₁ • li.toContinuousLinearMap : (a : E) → F) u : F)
      ((c₁ • li.toContinuousLinearMap : (a : E) → F) v : F) =
    c₁ * c₁ * ⟪u, v⟫
Tactic: refine ⟨c₁ * c₁, mul_self_pos.2 hc₁, fun u v => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ConformalLinearMap (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c₁ * ⟪u, v⟫
⊢ IsConformalMap f
have mpr : ∀ (c : ℝ) (hc : 0 < c) (hc₁ : 0 < c * c)
  (huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫),
  IsConformalMap f
Tactic: obtain ⟨c, hc, rfl⟩ : ∃ c : ℝ, 0 < c ∧ c₁ = c * c :=
      ⟨√c₁, Real.sqrt_pos.2 hc₁, (Real.mul_self_sqrt hc₁.le).symm⟩
Cleared hypotheses: c₁, hc₁, huv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ConformalLinearMap (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
⊢ IsConformalMap f
have mpr : ∀ (u v : E),
  inner.{0, u_2} ℝ (E := F) ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) u : F)
      ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) v : F) =
    ⟪u, v⟫
Tactic: refine ⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometryOfInner fun u v => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ConformalLinearMap (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
mpr :
  ∀ (u v : E),
    inner.{0, u_2} ℝ (E := F) ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) u : F)
        ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) v : F) =
      ⟪u, v⟫
⊢ IsConformalMap f
have mpr₁ : f = HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner sorry))
Tactic: refine ⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometryOfInner fun u v => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ConformalLinearMap (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
⊢ f = HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner ⋯))
have mpr : ∀ (x : E),
  Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x : F)
    ((HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner sorry)) : (a : E) → F)
        x :
      F)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Continuous (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
x y : E
⊢ ‖⟪(x, y).1, (x, y).2⟫‖ ≤ 1 * ‖x‖ * ‖y‖
have rw : ‖⟪(x, y).1, (x, y).2⟫‖ ≤ ‖x‖ * ‖y‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Continuous (hypothesis)
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
⊢ x = 0
have hK : Dense (↑K : Set E)
Tactic: have hK : Dense (K : Set E) := hS.mono subset_span
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Continuous (hypothesis)
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense (↑K : Set E)
⊢ x = 0
have this : Eq (α := E → 𝕜) (fun (x_1 : E) ↦ ⟪x, x_1⟫) 0
Tactic: have : (⟪x, ·⟫) = 0 := (continuous_const.inner continuous_id).ext_on
    hK continuous_const fun v ↦ Submodule.span_induction h (by simp)
      (by simp +contextual [inner_add_right]) (by simp +contextual [inner_smul_right])
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Continuous (goal)
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = 0
v : E
hv : v ∈ S
⊢ ⟪x, v⟫ = 0
have rw! : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, x⟫ : 𝕜) (0 : 𝕜)
Tactic: rw! [← inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Continuous (goal)
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = ⟪y, v⟫
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Continuous (goal)
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = ⟪v, y⟫
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : F⦄, ‖x‖ = 1 → ∀ ⦃y : F⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
have refine_1 : 4 - HPow.hPow (β := ℕ) ε 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: refine
      ⟨2 - √(4 - ε ^ 2), sub_pos_of_lt <| (sqrt_lt' zero_lt_two).2 ?_, fun x hx y hy hxy => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
refine_1 : 4 - HPow.hPow (β := ℕ) ε 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : F⦄, ‖x‖ = 1 → ∀ ⦃y : F⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
have refine_2 : ∀ (x : F) (hx : ‖x‖ = 1) (y : F) (hy : ‖y‖ = 1) (hxy : ε ≤ ‖x - y‖), ‖x + y‖ ≤ 2 - (2 - √(4 - HPow.hPow (β := ℕ) ε 2))
Tactic: refine
      ⟨2 - √(4 - ε ^ 2), sub_pos_of_lt <| (sqrt_lt' zero_lt_two).2 ?_, fun x hx y hy hxy => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
⊢ 4 - HPow.hPow (β := ℕ) ε 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
have refine_1 : 0 < HPow.hPow (β := ℕ) ε 2
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 - (2 - √(4 - HPow.hPow (β := ℕ) ε 2))
have refine_2 : ‖x + y‖ ≤ √(4 - HPow.hPow (β := ℕ) ε 2)
Tactic: rw [sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ √(4 - HPow.hPow (β := ℕ) ε 2)
have refine_2 : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
Tactic: refine le_sqrt_of_sq_le ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
have refine_2 : 2 * (HMul.hMul (α := ℝ) 1 1 + HMul.hMul (α := ℝ) 1 1) - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
Tactic: rw [sq, eq_sub_iff_add_eq.2 (parallelogram_law_with_norm_mul ℝ x y), ← sq ‖x - y‖, hx, hy]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 2 * (HMul.hMul (α := ℝ) 1 1 + HMul.hMul (α := ℝ) 1 1) - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
have refine_2 : 4 - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Convex (goal)
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
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 4 - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
have refine_2 : 0 ≤ ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (inner 𝕜 x x) : ℝ)
have rw : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [← InnerProductSpace.norm_sq_eq_re_inner]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)
have rw : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [← InnerProductSpace.norm_sq_eq_re_inner]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
hx : ⟪x, x⟫_𝕜 = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = 0
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ) (0 : ℝ)
Tactic: rw [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜) x, hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
hx : ⟪x, x⟫_𝕜 = 0
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ) (0 : ℝ)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = 0
have rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜) x, hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
hx : ⟪x, x⟫_𝕜 = 0
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜) x, hx, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (0 : ℝ)
have rw : I * HSub.hSub (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, x⟫ : 𝕜) ⟪x, x⟫ / 2 = (↑0 : 𝕜)
Tactic: rw [← @ofReal_inj 𝕜, im_eq_conj_sub]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫
have rw : HAdd.hAdd (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪z, x⟫ : 𝕜) =
  ⟪x, y⟫ + ⟪x, z⟫
Tactic: rw [← inner_conj_symm, inner_add_left, map_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) = ⟪x, x⟫
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ∧
  Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
Tactic: rw [ext_iff]