awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_8
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := F →L[𝕜] E)
    ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E)
    (0 : F →L[𝕜] E)

Tactic:
grind [rankOne_eq_zero]

Premises used: InnerProductSpace.rankOne_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ IsIdempotentElem (M := F →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) ↔
    ‖x‖ = 1

Tactic:
⟨?_, isIdempotentElem_rankOne_self⟩

Premises used: InnerProductSpace.isIdempotentElem_rankOne_self, Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
refine :
  IsIdempotentElem (M := F →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
    ‖x‖ = 1
⊢ IsIdempotentElem (M := F →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) ↔
    ‖x‖ = 1

Tactic:
refine ⟨?_, isIdempotentElem_rankOne_self⟩
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
simp :
  HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      (((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x →
    ‖x‖ = 1
⊢ IsIdempotentElem (M := F →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
    ‖x‖ = 1

Tactic:
simp only [IsIdempotentElem, mul_def, comp_rankOne, rankOne_apply, inner_self_eq_norm_sq_to_K,
    map_smul, coe_smul', Pi.smul_apply]

Premises used: ContinuousLinearMap.coe_smul', InnerProductSpace.rankOne_apply, inner_self_eq_norm_sq_to_K, InnerProductSpace.comp_rankOne, IsIdempotentElem, ContinuousLinearMap.mul_def, map_smul, Pi.smul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
nth_rw :
  HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      HSMul.hSMul.{u_4, u_8, u_8} (α := 𝕜) (β := F →L[𝕜] F) 1
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
    ‖x‖ = 1
⊢ HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      (((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x →
    ‖x‖ = 1

Tactic:
nth_rw 2 [← one_smul 𝕜 (rankOne 𝕜 x x)]

Premises used: InnerProductSpace.rankOne, one_smul, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
rw :
  HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 - 1)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      0 →
    ‖x‖ = 1
⊢ HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      HSMul.hSMul.{u_4, u_8, u_8} (α := 𝕜) (β := F →L[𝕜] F) 1
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
    ‖x‖ = 1

Tactic:
rw [← sub_eq_zero, ← sub_smul]

Premises used: sub_eq_zero, sub_smul
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ Eq.{u_4 + 1} (α := 𝕜) (↑(-1) : 𝕜) (-1)

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
simp : ‖x‖ = 1 ∨ ‖x‖ = -1 → ‖x‖ = 1
⊢ HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 - 1)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      0 →
    ‖x‖ = 1

Tactic:
simp only [smul_eq_zero, rankOne_eq_zero, hx, or_self, or_false, sub_eq_zero, sq_eq_one_iff,
    FaithfulSMul.algebraMap_eq_one_iff, ← show ((-(1 : ℝ) : ℝ) : 𝕜) = -1 by grind, ofReal_inj]

Premises used: sq_eq_one_iff, RCLike.ofReal_inj, sub_eq_zero, InnerProductSpace.rankOne_eq_zero, FaithfulSMul.algebraMap_eq_one_iff, or_self, or_false, smul_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ ‖x‖ = 1 ∨ ‖x‖ = -1 → ‖x‖ = 1

Tactic:
grind [norm_nonneg]

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
simp_rw :
  (∀ (x : H) (v : F),
      ⟪v,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F) :
              (a : H) → F)
            x⟫_𝕜 =
        ⟪v,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) :
              (a : H) → F)
            x⟫_𝕜) ↔
    ∀ (x : F) (v : H),
      ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜 =
        ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜
⊢ Eq (α := H →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) ↔
    Eq (α := F →L[𝕜] H)
      ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
      ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)

Tactic:
simp_rw [ContinuousLinearMap.ext_iff, ext_iff_inner_left 𝕜 (E := F),
    ext_iff_inner_right 𝕜 (E := H)]

Premises used: ext_iff_inner_left, ContinuousLinearMap.ext_iff, ext_iff_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
rw :
  (∀ (b_1 : F) (a_1 : H),
      ⟪b_1,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F) :
              (a : H) → F)
            a_1⟫_𝕜 =
        ⟪b_1,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) :
              (a : H) → F)
            a_1⟫_𝕜) ↔
    ∀ (x : F) (v : H),
      ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜 =
        ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜
⊢ (∀ (x : H) (v : F),
      ⟪v,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F) :
              (a : H) → F)
            x⟫_𝕜 =
        ⟪v,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) :
              (a : H) → F)
            x⟫_𝕜) ↔
    ∀ (x : F) (v : H),
      ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜 =
        ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜

Tactic:
rw [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
⊢ (∀ (b_1 : F) (a_1 : H),
      ⟪b_1,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F) :
              (a : H) → F)
            a_1⟫_𝕜 =
        ⟪b_1,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) :
              (a : H) → F)
            a_1⟫_𝕜) ↔
    ∀ (x : F) (v : H),
      ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜 =
        ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜

Tactic:
simp [inner_smul_left, inner_smul_right, mul_comm]

Premises used: inner_smul_right, mul_comm, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h :
  Eq (α := H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F)
⊢ Eq (α := F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)

Tactic:
have h₂ := rankOne_eq_rankOne_iff_comm.mp h
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h :
  Eq (α := H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F)
h₂ :
  Eq (α := F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)
⊢ ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c

Tactic:
simp only [ContinuousLinearMap.ext_iff, rankOne_apply] at h h₂

Premises used: InnerProductSpace.rankOne_apply, ContinuousLinearMap.ext_iff
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h :
  Eq (α := H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F)
h₂ :
  Eq (α := F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)
h₁ : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
⊢ ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d

Tactic:
simp only [ContinuousLinearMap.ext_iff, rankOne_apply] at h h₂

Premises used: InnerProductSpace.rankOne_apply, ContinuousLinearMap.ext_iff
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
⊢ a = (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
simp : (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a = (1 / ⟪b, b⟫_𝕜 * ⟪b, b⟫_𝕜) • a
⊢ (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a = (1 / ⟪b, b⟫_𝕜) • ⟪b, b⟫_𝕜 • a

Tactic:
simp only [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
⊢ (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a = (1 / ⟪b, b⟫_𝕜 * ⟪b, b⟫_𝕜) • a

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
simp : (1 / ⟪b, b⟫_𝕜 * ⟪d, b⟫_𝕜) • c = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
⊢ (1 / ⟪b, b⟫_𝕜) • ⟪b, b⟫_𝕜 • a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c

Tactic:
simp only [h, smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
⊢ (1 / ⟪b, b⟫_𝕜 * ⟪d, b⟫_𝕜) • c = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
⊢ a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c

Tactic:
have h₃ := calc
    a = (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a := by simp_all
    _ = (1 / ⟪b, b⟫_𝕜) • (⟪b, b⟫_𝕜 • a) := by simp only [smul_smul]; ring_nf
    _ = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c := by simp only [h, smul_smul]; ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
⊢ b = (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
simp : (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b = (1 / ⟪a, a⟫_𝕜 * ⟪a, a⟫_𝕜) • b
⊢ (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b = (1 / ⟪a, a⟫_𝕜) • ⟪a, a⟫_𝕜 • b

Tactic:
simp only [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
⊢ (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b = (1 / ⟪a, a⟫_𝕜 * ⟪a, a⟫_𝕜) • b

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
simp_rw :
  (1 / (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪(⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c, c⟫_𝕜) * (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪c, c⟫_𝕜)) • d =
    (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪(⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c, c⟫_𝕜))) • d
⊢ (1 / ⟪a, a⟫_𝕜) • ⟪a, a⟫_𝕜 • b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d

Tactic:
simp_rw [h₂, h₃, inner_smul_right, smul_smul]

Premises used: smul_smul, inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
⊢ (1 / (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪(⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c, c⟫_𝕜) * (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪c, c⟫_𝕜)) • d =
    (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪(⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c, c⟫_𝕜))) • d

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
⊢ b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d

Tactic:
have h₄ := calc
    b = (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b := by simp_all
    _ = (1 / ⟪a, a⟫_𝕜) • (⟪a, a⟫_𝕜 • b) := by simp only [smul_smul]; ring_nf
    _ = ((⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d := by
      simp_rw [h₂, h₃, inner_smul_right, smul_smul]; ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h_1 : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h : ⟪d, b⟫_𝕜 = 0
⊢ False

Tactic:
simp [h, hb] at h₄
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
⊢ ⟪d, b⟫_𝕜 ≠ 0

Tactic:
have h₅ : ⟪d, b⟫_𝕜 ≠ 0 := fun h ↦ by simp [h, hb] at h₄
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h_1 : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h : c = 0
⊢ False

Tactic:
simp [h, ha] at h₃
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
⊢ c ≠ 0

Tactic:
have h₆ : c ≠ 0 := fun h ↦ by simp [h, ha] at h₃
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ ⟪b, b⟫_𝕜 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖c‖ : 𝕜) 2 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖a‖ : 𝕜) 2)) • d

Tactic:
simpa using h₄
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
refine : 0 < HPow.hPow (α := 𝕜) (β := ℕ) (↑‖c‖ : 𝕜) 2 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖a‖ : 𝕜) 2
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d

Tactic:
refine ⟨_, ‖c‖ ^ 2 / ‖a‖ ^ 2, div_ne_zero h₅ <| by simpa, ?_, h₃, by simpa using h₄⟩