awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst_5 : Fintype m
inst_6 : DecidableEq m
inst_7 : Fintype n
inst_8 : DecidableEq n
inst_9 : FiniteDimensional 𝕜 E
inst_10 : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
i : m
j : n
simp_rw :
  inner.{u_1, u_2} 𝕜 (E := E) (∑ j : n, HSMul.hSMul (β := E) (Aᴴ j i) ((v₁.toBasis : (a : n) → E) j : E) : E)
      ((v₁.toBasis : (a : n) → E) j : E) =
    inner.{u_1, u_3} 𝕜 (E := F) ((v₂.toBasis : (a : m) → F) i : F)
      (∑ j_1 : m, HSMul.hSMul (β := F) (A j_1 j) ((v₂.toBasis : (a : m) → F) j_1 : F) : F)
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((((toLin v₂.toBasis v₁.toBasis : (a : Matrix n m 𝕜) → F →ₗ[𝕜] E) Aᴴ : F →ₗ[𝕜] E) : (a : F) → E)
          ((v₂.toBasis : (a : m) → F) i : F) :
        E)
      ((v₁.toBasis : (a : n) → E) j : E) =
    inner.{u_1, u_3} 𝕜 (E := F) ((v₂.toBasis : (a : m) → F) i : F)
      ((((toLin v₁.toBasis v₂.toBasis : (a : Matrix m n 𝕜) → E →ₗ[𝕜] F) A : E →ₗ[𝕜] F) : (a : E) → F)
          ((v₁.toBasis : (a : n) → E) j : E) :
        F)

Tactic:
simp_rw [toLin_self]

Premises used: Matrix.toLin_self
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst_5 : Fintype m
inst_6 : DecidableEq m
inst_7 : Fintype n
inst_8 : DecidableEq n
inst_9 : FiniteDimensional 𝕜 E
inst_10 : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
i : m
j : n
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ j : n, HSMul.hSMul (β := E) (Aᴴ j i) ((v₁.toBasis : (a : n) → E) j : E) : E)
      ((v₁.toBasis : (a : n) → E) j : E) =
    inner.{u_1, u_3} 𝕜 (E := F) ((v₂.toBasis : (a : m) → F) i : F)
      (∑ j_1 : m, HSMul.hSMul (β := F) (A j_1 j) ((v₂.toBasis : (a : m) → F) j_1 : F) : F)

Tactic:
simp [sum_inner, inner_smul_left, inner_sum, inner_smul_right,
    orthonormal_iff_ite.mp v₁.orthonormal, orthonormal_iff_ite.mp v₂.orthonormal]

Premises used: inner_sum, sum_inner, inner_smul_right, OrthonormalBasis.orthonormal, Iff.mp, orthonormal_iff_ite, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst_5 : Fintype m
inst_6 : DecidableEq m
inst_7 : Fintype n
inst_8 : DecidableEq n
inst_9 : FiniteDimensional 𝕜 E
inst_10 : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
f : E →ₗ[𝕜] F
⊢ Eq (α := F →ₗ[𝕜] E)
    ((toLin v₂.toBasis v₁.toBasis : (a : Matrix n m 𝕜) → F →ₗ[𝕜] E)
        ((toMatrix v₂.toBasis v₁.toBasis : (a : F →ₗ[𝕜] E) → Matrix n m 𝕜)
          ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) f)) :
      F →ₗ[𝕜] E)
    ((toLin v₂.toBasis v₁.toBasis : (a : Matrix n m 𝕜) → F →ₗ[𝕜] E)
        ((toMatrix v₁.toBasis v₂.toBasis : (a : E →ₗ[𝕜] F) → Matrix m n 𝕜) f)ᴴ :
      F →ₗ[𝕜] E)

Tactic:
simp [toLin_conjTranspose]

Premises used: Matrix.toLin_conjTranspose
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : Type u_6
inst_3 : Fintype n
inst_4 : DecidableEq n
inst_5 : FiniteDimensional 𝕜 E
v₁ : OrthonormalBasis n 𝕜 E
f : E →ₗ[𝕜] E
i j : n
⊢ (toMatrixOrthonormal v₁ : (a : E →ₗ[𝕜] E) → Matrix n n 𝕜) f i j =
    inner.{u_1, u_2} 𝕜 (E := E) ((v₁ : (a : n) → E) i : E) ((f : (a : E) → E) ((v₁ : (a : n) → E) j : E) : E)

Tactic:
calc
    _ = v₁.repr (f (v₁ j)) i := f.toMatrix_apply ..
    _ = ⟪v₁ i, f (v₁ j)⟫_𝕜 := v₁.repr_apply_apply ..

Premises used: Trans.trans, OrthonormalBasis.repr_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m : Type u_5
n : Type u_6
inst_3 : Fintype m
inst_4 : DecidableEq m
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : FiniteDimensional 𝕜 E
v₁ : OrthonormalBasis n 𝕜 E
e : n ≃ m
f : E →ₗ[𝕜] E
i j : m
⊢ Eq.{u_1 + 1} (α := (fun (x : m) ↦ 𝕜) i)
    (WithLp.ofLp (p := 2)
      ((OrthonormalBasis.repr (v₁.reindex e) : (a : E) → EuclideanSpace 𝕜 m)
        ((f : (a : E) → E) ((v₁.reindex e : (a : m) → E) j : E)))
      i)
    (WithLp.ofLp (p := 2)
      ((v₁.repr : (a : E) → EuclideanSpace 𝕜 n)
        ((f : (a : E) → E) ((v₁ : (a : n) → E) ((e.symm : (a : m) → n) j : n) : E)))
      ((e.symm : (a : m) → n) i))

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
m : Type u_5
n : Type u_6
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
A : Matrix m n 𝕜
⊢ Eq (α := EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
    ((toEuclideanLin : (a : Matrix n m 𝕜) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n) Aᴴ :
      EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
    ((adjoint : (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) A) :
      EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)

Tactic:
A.toLin_conjTranspose (EuclideanSpace.basisFun n 𝕜) (EuclideanSpace.basisFun m 𝕜)

Premises used: Multiset.sum, Multiset.foldr, dotProduct, EuclideanSpace.basisFun, Matrix.toLin_conjTranspose, Matrix.mulVec, Finset.sum
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_5
E' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
inst_4 : NormedAddCommGroup E'
inst_5 : InnerProductSpace 𝕜 E'
inst_6 : CompleteSpace E'
f : E →ₗᵢ[𝕜] E'
⊢ Eq (α := E →L[𝕜] E)
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
      ((ContinuousLinearMap.adjoint : (a : E →L[𝕜] E') → E' →L[𝕜] E) f.toContinuousLinearMap) f.toContinuousLinearMap)
    1

Tactic:
f.toContinuousLinearMap.isometry_iff_adjoint_comp_self.mp f.isometry

Premises used: ContinuousLinearMap.isometry_iff_adjoint_comp_self, LinearIsometry.isometry, Iff.mp, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_5
E' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : NormedAddCommGroup E'
inst_5 : InnerProductSpace 𝕜 E'
inst_6 : FiniteDimensional 𝕜 E'
f : E →ₗᵢ[𝕜] E'
⊢ CompleteSpace E

Tactic:
haveI := FiniteDimensional.complete 𝕜 E
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_5
E' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : NormedAddCommGroup E'
inst_5 : InnerProductSpace 𝕜 E'
inst_6 : FiniteDimensional 𝕜 E'
f : E →ₗᵢ[𝕜] E'
this : CompleteSpace E
⊢ CompleteSpace E'

Tactic:
haveI := FiniteDimensional.complete 𝕜 E'
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_5
E' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : NormedAddCommGroup E'
inst_5 : InnerProductSpace 𝕜 E'
inst_6 : FiniteDimensional 𝕜 E'
f : E →ₗᵢ[𝕜] E'
this_1 : CompleteSpace E
this : CompleteSpace E'
h :
  ∀ (x : E),
    Eq (α := E)
      (((LinearMap.adjoint : (a : E →ₗ[𝕜] E') → E' →ₗ[𝕜] E) f.toLinearMap ∘ₗ f.toLinearMap : (a : E) → E) x : E)
      ((LinearMap.id : (a : E) → E) x : E)
⊢ (LinearMap.adjoint : (a : E →ₗ[𝕜] E') → E' →ₗ[𝕜] E) f.toLinearMap ∘ₗ f.toLinearMap = LinearMap.id

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_5
E' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : NormedAddCommGroup E'
inst_5 : InnerProductSpace 𝕜 E'
inst_6 : FiniteDimensional 𝕜 E'
f : E →ₗᵢ[𝕜] E'
this_1 : CompleteSpace E
this : CompleteSpace E'
x : E
⊢ Eq (α := E) (((LinearMap.adjoint : (a : E →ₗ[𝕜] E') → E' →ₗ[𝕜] E) f.toLinearMap ∘ₗ f.toLinearMap : (a : E) → E) x : E)
    ((LinearMap.id : (a : E) → E) x : E)

Tactic:
congr($(f.adjoint_comp_self) x)

Premises used: congrArg, id, DFunLike.coe, LinearIsometry.adjoint_comp_self
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_5
E' : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : NormedAddCommGroup E'
inst_5 : InnerProductSpace 𝕜 E'
inst_6 : FiniteDimensional 𝕜 E'
f : E →ₗᵢ[𝕜] E'
this_1 : CompleteSpace E
this : CompleteSpace E'
x : E
⊢ Eq (α := E) (((LinearMap.adjoint : (a : E →ₗ[𝕜] E') → E' →ₗ[𝕜] E) f.toLinearMap ∘ₗ f.toLinearMap : (a : E) → E) x : E)
    ((LinearMap.id : (a : E) → E) x : E)

Tactic:
exact congr($(f.adjoint_comp_self) x)
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_5
E : Type u_6
E' : Type u_7
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι 𝕜 E'
⊢ FiniteDimensional 𝕜 E

Tactic:
have : FiniteDimensional 𝕜 E := Module.Basis.finiteDimensional_of_finite b.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_5
E : Type u_6
E' : Type u_7
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι 𝕜 E'
this : FiniteDimensional 𝕜 E
⊢ FiniteDimensional 𝕜 E'

Tactic:
have : FiniteDimensional 𝕜 E' := Module.Basis.finiteDimensional_of_finite b'.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
ι : Type u_5
E : Type u_6
E' : Type u_7
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
inst_5 : NormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι 𝕜 E'
this_1 : FiniteDimensional 𝕜 E
this : FiniteDimensional 𝕜 E'
⊢ Membership.mem (α := Matrix ι ι 𝕜) (γ := Submonoid (Matrix ι ι 𝕜)) (Matrix.unitaryGroup ι 𝕜)
    ((LinearMap.toMatrix b.toBasis b'.toBasis : (a : E →ₗ[𝕜] E') → Matrix ι ι 𝕜) (↑f.toLinearEquiv : E →ₗ[𝕜] E') :
      Matrix ι ι 𝕜)

Tactic:
simp [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose, ← LinearMap.toMatrix_adjoint,
    ← LinearMap.toMatrix_comp, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm,
    -OrthonormalBasis.coe_toBasis]

Premises used: Matrix.star_eq_conjTranspose, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, Matrix.mem_unitaryGroup_iff, OrthonormalBasis.coe_toBasis, LinearMap.toMatrix_comp, LinearMap.toMatrix_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
a b : P
v : V
rw : ⟪-(b -ᵥ a), v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
rw₁ : -⟪b -ᵥ a, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
rw₂ rw₃ : ⟪b -ᵥ a, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
⊢ ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0

Tactic:
rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]

Premises used: neg_eq_zero, neg_vsub_eq_vsub_rev, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
v : V
a b : P
rw : ⟪v, -(b -ᵥ a)⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
rw₁ : -⟪v, b -ᵥ a⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
rw₂ rw₃ : ⟪v, b -ᵥ a⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
⊢ ⟪v, a -ᵥ b⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0

Tactic:
rw [← neg_vsub_eq_vsub_rev, inner_neg_right, neg_eq_zero]

Premises used: inner_neg_right, neg_eq_zero, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
rw : ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) ‖a -ᵥ b‖ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
rw₁ : ⟪a -ᵥ b, a -ᵥ b - (a -ᵥ c)⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
rw₂ : ⟪a -ᵥ b, c -ᵥ b⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
rw₃ rw₄ : ⟪a -ᵥ b, b -ᵥ c⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a b) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0

Tactic:
rw [dist_eq_norm_vsub V, inner_eq_norm_sq_left_iff, vsub_sub_vsub_cancel_left,
    inner_vsub_right_eq_zero_symm]

Premises used: inner_vsub_right_eq_zero_symm, inner_eq_norm_sq_left_iff, vsub_sub_vsub_cancel_left, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
rw : ⟪a -ᵥ c, a -ᵥ b⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
rw₁ : ⟪a -ᵥ c, c -ᵥ b⟫ = 0 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
rw₂ rw₃ : ⟪c -ᵥ b, a -ᵥ c⟫ = 0 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0

Tactic:
rw [real_inner_comm, inner_vsub_vsub_left_eq_dist_sq_left_iff, real_inner_comm]

Premises used: inner_vsub_vsub_left_eq_dist_sq_left_iff, real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
rw : ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) ‖a -ᵥ c‖ 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
rw₁ : ⟪a -ᵥ c, a -ᵥ c - (b -ᵥ c)⟫ = 0 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
rw₂ : ⟪a -ᵥ c, a -ᵥ b⟫ = 0 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
rw₃ rw₄ : ⟪a -ᵥ c, b -ᵥ a⟫ = 0 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0

Tactic:
rw [dist_eq_norm_vsub V, inner_eq_norm_sq_left_iff, vsub_sub_vsub_cancel_right,
    inner_vsub_right_eq_zero_symm]

Premises used: inner_vsub_right_eq_zero_symm, inner_eq_norm_sq_left_iff, vsub_sub_vsub_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
rw : ⟪b -ᵥ c, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist b c) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
rw₁ : ⟪b -ᵥ c, a -ᵥ b⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
rw₂ rw₃ : ⟪a -ᵥ b, b -ᵥ c⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist b c) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0

Tactic:
rw [real_inner_comm, inner_vsub_vsub_right_eq_dist_sq_left_iff, real_inner_comm]

Premises used: inner_vsub_vsub_right_eq_dist_sq_left_iff, real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
rw : (t₁ • (b -ᵥ a) +ᵥ a) -ᵥ (AffineMap.lineMap a c : (a : ℝ) → P) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
rw₁ : (t₁ • (b -ᵥ a) +ᵥ a) -ᵥ (t₂ • (c -ᵥ a) +ᵥ a) = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
rw₂ rw₃ : t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a) = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ VSub.vsub.{u_2, u_3} (P := P) ((AffineMap.lineMap a b : (a : ℝ) → P) t₁ : P)
      ((AffineMap.lineMap a c : (a : ℝ) → P) t₂ : P) =
    t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)

Tactic:
rw [AffineMap.lineMap_apply, AffineMap.lineMap_apply, vadd_vsub_vadd_cancel_right]

Premises used: vadd_vsub_vadd_cancel_right, AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
⊢ VSub.vsub.{u_2, u_3} (P := P) ((AffineMap.lineMap a b : (a : ℝ) → P) t₁ : P)
      ((AffineMap.lineMap a c : (a : ℝ) → P) t₂ : P) =
    t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)

Tactic:
have hvec : AffineMap.lineMap a b t₁ -ᵥ AffineMap.lineMap a c t₂ =
              t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a) := by
    rw [AffineMap.lineMap_apply, AffineMap.lineMap_apply, vadd_vsub_vadd_cancel_right]
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec :
  VSub.vsub.{u_2, u_3} (P := P) ((AffineMap.lineMap a b : (a : ℝ) → P) t₁ : P)
      ((AffineMap.lineMap a c : (a : ℝ) → P) t₂ : P) =
    t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
rw :
  HPow.hPow (β := ℕ) (|t₁| * ‖b -ᵥ a‖) 2 - 2 * HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) t₁ : ℝ) (t₂ * 0) +
      HPow.hPow (β := ℕ) (|t₂| * ‖c -ᵥ a‖) 2 =
    HPow.hPow (β := ℕ) t₁ 2 * HPow.hPow (β := ℕ) (dist a b) 2 +
      HPow.hPow (β := ℕ) t₂ 2 * HPow.hPow (β := ℕ) (dist a c) 2
⊢ HPow.hPow (β := ℕ)
      (dist.{u_3} (α := P) ((AffineMap.lineMap a b : (a : ℝ) → P) t₁ : P)
        ((AffineMap.lineMap a c : (a : ℝ) → P) t₂ : P))
      2 =
    HPow.hPow (β := ℕ) t₁ 2 * HPow.hPow (β := ℕ) (dist a b) 2 +
      HPow.hPow (β := ℕ) t₂ 2 * HPow.hPow (β := ℕ) (dist a c) 2

Tactic:
rw [dist_eq_norm_vsub V, hvec, norm_sub_sq_real, norm_smul, norm_smul,
      Real.norm_eq_abs, Real.norm_eq_abs, inner_smul_left, inner_smul_right, h_inner]

Premises used: norm_sub_sq_real, norm_smul, inner_smul_right, dist_eq_norm_vsub, Real.norm_eq_abs, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec :
  VSub.vsub.{u_2, u_3} (P := P) ((AffineMap.lineMap a b : (a : ℝ) → P) t₁ : P)
      ((AffineMap.lineMap a c : (a : ℝ) → P) t₂ : P) =
    t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ HPow.hPow (β := ℕ) (|t₁| * ‖b -ᵥ a‖) 2 - 2 * HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) t₁ : ℝ) (t₂ * 0) +
      HPow.hPow (β := ℕ) (|t₂| * ‖c -ᵥ a‖) 2 =
    HPow.hPow (β := ℕ) t₁ 2 * HPow.hPow (β := ℕ) (dist a b) 2 +
      HPow.hPow (β := ℕ) t₂ 2 * HPow.hPow (β := ℕ) (dist a c) 2

Tactic:
simp only [mul_zero, sub_zero, mul_pow, sq_abs, ← dist_eq_norm_vsub' V]

Premises used: sub_zero, dist_eq_norm_vsub', MulZeroClass.mul_zero, sq_abs, mul_pow
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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
⊢ 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

Tactic:
have h := dist_sq_lineMap_lineMap_of_inner_eq_zero (t₁ := 1) (t₂ := t) h_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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 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

Premises used: one_pow, AffineMap.lineMap_apply_one, one_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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
rwa rwa₁ rwa₂ 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
⊢ 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

Premises used: dist_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Affine
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
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
⊢ HPow.hPow (β := ℕ) (dist p b) 2 = HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a b) 2

Tactic:
simpa using dist_sq_lineMap_of_inner_eq_zero 1 h_inner

Premises used: OfNat.ofNat, dist_sq_lineMap_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ = ⟪x, y⟫

Tactic:
InnerProductSpace.conj_inner_symm _ _

Premises used: InnerProductSpace.conj_inner_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
@inner_conj_symm ℝ _ _ _ _ x y

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) (0 : 𝕜) ↔ ⟪y, x⟫ = 0
⊢ ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0

Tactic:
rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) (0 : 𝕜) ↔ ⟪y, x⟫ = 0

Tactic:
star_eq_zero

Premises used: star_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) (0 : 𝕜) ↔ ⟪y, x⟫ = 0

Tactic:
exact star_eq_zero

Premises used: star_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : I * HSub.hSub (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, x⟫ : 𝕜) ⟪x, x⟫ / 2 = (↑0 : 𝕜)
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (0 : ℝ)

Tactic:
rw [← @ofReal_inj 𝕜, im_eq_conj_sub]

Premises used: RCLike.ofReal_inj, RCLike.im_eq_conj_sub
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ I * HSub.hSub (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, x⟫ : 𝕜) ⟪x, x⟫ / 2 = (↑0 : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
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, z⟫ + ⟪y, z⟫

Tactic:
InnerProductSpace.add_left _ _ _

Premises used: InnerProductSpace.add_left