awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (hypothesis)
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
t : ℝ
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
h :
  HPow.hPow (β := ℕ)
      (dist.{u_3} (α := P) ((AffineMap.lineMap a p : (a : ℝ) → P) 1 : P) ((AffineMap.lineMap a b : (a : ℝ) → P) t : P))
      2 =
    HPow.hPow (α := ℝ) (β := ℕ) 1 2 * HPow.hPow (β := ℕ) (dist a p) 2 +
      HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a b) 2
⊢ HPow.hPow (β := ℕ) (dist p ((AffineMap.lineMap a b : (a : ℝ) → P) t)) 2 =
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a b) 2
have h₁ : HPow.hPow (β := ℕ) (dist p ((AffineMap.lineMap a b : (a : ℝ) → P) t)) 2 =
  HPow.hPow (β := ℕ) (dist a p) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a b) 2
Tactic: simp only [AffineMap.lineMap_apply_one, one_pow, one_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (goal)
Goal:
V : Type u_2
P : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p : P
t : ℝ
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
h :
  HPow.hPow (β := ℕ) (dist p ((AffineMap.lineMap a b : (a : ℝ) → P) t)) 2 =
    HPow.hPow (β := ℕ) (dist a p) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a b) 2
⊢ HPow.hPow (β := ℕ) (dist p ((AffineMap.lineMap a b : (a : ℝ) → P) t)) 2 =
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a b) 2
have rwa : ∀
  (h :
    HPow.hPow (β := ℕ) (dist p ((AffineMap.lineMap a b : (a : ℝ) → P) t)) 2 =
      HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a b) 2),
  HPow.hPow (β := ℕ) (dist p ((AffineMap.lineMap a b : (a : ℝ) → P) t)) 2 =
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a b) 2
Tactic: rwa [dist_comm a p] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0
have rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) (0 : 𝕜) ↔ ⟪y, x⟫ = 0
Tactic: rw [← inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ 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.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y z : E
⊢ ⟪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.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_im]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw₁ : Eq (α := ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_im]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
have rw : ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
  HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
Tactic: rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw :
  ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
have rw₁ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) : 𝕜) ⟪x, y⟫ =
  HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
Tactic: rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw :
  ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₁ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
have rw₂ : HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ =
  HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
Tactic: rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw :
  ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₁ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₂ :
  HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
have rw₃ : HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
Tactic: rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw :
  ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₁ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₂ :
  HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₃ : HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
have rw₄ : HMul.hMul (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) (star r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
Tactic: rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw :
  ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₁ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₂ :
  HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₃ : HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
rw₄ : HMul.hMul (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) (star r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
have rw₅ : HSMul.hSMul (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) (star r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
Tactic: rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw :
  ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₁ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₂ :
  HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₃ : HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
rw₄ : HMul.hMul (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) (star r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
rw₅ : HSMul.hSMul (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) (star r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
have rw₆ : star r • ⟪x, y⟫ = star r • ⟪x, y⟫
Tactic: rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
inst_9 : TrivialStar 𝕝
x y : E
r : 𝕝
⊢ ⟪r • x, y⟫ = r • ⟪x, y⟫
have rw : HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫ = r • ⟪x, y⟫
Tactic: rw [inner_smul_left_eq_star_smul, starRingEnd_apply, star_trivial]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
inst_9 : TrivialStar 𝕝
x y : E
r : 𝕝
rw : HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫ = r • ⟪x, y⟫
⊢ ⟪r • x, y⟫ = r • ⟪x, y⟫
have rw₁ : star r • ⟪x, y⟫ = r • ⟪x, y⟫
Tactic: rw [inner_smul_left_eq_star_smul, starRingEnd_apply, star_trivial]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
inst_9 : TrivialStar 𝕝
x y : E
r : 𝕝
rw : HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫ = r • ⟪x, y⟫
rw₁ : star r • ⟪x, y⟫ = r • ⟪x, y⟫
⊢ ⟪r • x, y⟫ = r • ⟪x, y⟫
have rw₂ : r • ⟪x, y⟫ = r • ⟪x, y⟫
Tactic: rw [inner_smul_left_eq_star_smul, starRingEnd_apply, star_trivial]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw₂ : star (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₂ : star (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw₃ : star (star r • ⟪y, x⟫) = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₂ : star (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₃ : star (star r • ⟪y, x⟫) = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw₄ : star (star r) • star ⟪y, x⟫ = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₂ : star (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₃ : star (star r • ⟪y, x⟫) = r • ⟪x, y⟫
rw₄ : star (star r) • star ⟪y, x⟫ = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw₅ : r • star ⟪y, x⟫ = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₂ : star (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₃ : star (star r • ⟪y, x⟫) = r • ⟪x, y⟫
rw₄ : star (star r) • star ⟪y, x⟫ = r • ⟪x, y⟫
rw₅ : r • star ⟪y, x⟫ = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw₆ : HSMul.hSMul (β := 𝕜) r ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₂ : star (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₃ : star (star r • ⟪y, x⟫) = r • ⟪x, y⟫
rw₄ : star (star r) • star ⟪y, x⟫ = r • ⟪x, y⟫
rw₅ : r • star ⟪y, x⟫ = r • ⟪x, y⟫
rw₆ : HSMul.hSMul (β := 𝕜) r ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫
have rw₇ : r • ⟪x, y⟫ = r • ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x, y⟫ = r • ⟪x, y⟫
have rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) ⟪x, y⟫ = r • ⟪x, y⟫
Tactic: rw [inner_smul_left, conj_ofReal, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) ⟪x, y⟫ = r • ⟪x, y⟫
⊢ ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x, y⟫ = r • ⟪x, y⟫
have rw₁ : (↑r : 𝕜) * ⟪x, y⟫ = r • ⟪x, y⟫
Tactic: rw [inner_smul_left, conj_ofReal, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) ⟪x, y⟫ = r • ⟪x, y⟫
rw₁ : (↑r : 𝕜) * ⟪x, y⟫ = r • ⟪x, y⟫
⊢ ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x, y⟫ = r • ⟪x, y⟫
have rw₂ : (↑r : 𝕜) * ⟪x, y⟫ = HMul.hMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) r : 𝕜) ⟪x, y⟫
Tactic: rw [inner_smul_left, conj_ofReal, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ ⟪x, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) y⟫ = r • ⟪x, y⟫
have rw : (↑r : 𝕜) * ⟪x, y⟫ = r • ⟪x, y⟫
Tactic: rw [inner_smul_right, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
rw : (↑r : 𝕜) * ⟪x, y⟫ = r • ⟪x, y⟫
⊢ ⟪x, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) y⟫ = r • ⟪x, y⟫
have rw₁ : (↑r : 𝕜) * ⟪x, y⟫ = HMul.hMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) r : 𝕜) ⟪x, y⟫
Tactic: rw [inner_smul_right, Algebra.smul_def]