awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
H : Type u_5
inst_7 : NormedAddCommGroup H
inst_8 : InnerProductSpace 𝕜 H
inst_9 : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
⊢ (let __src := (↑(u * v) : H →L[𝕜] H);
    { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star (u * v)) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
      left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) =
    HMul.hMul (α := H ≃ₗᵢ[𝕜] H)
      (let __src := (↑u : H →L[𝕜] H);
      { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star u) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
        left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H })
      (let __src := (↑v : H →L[𝕜] H);
      { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star v) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
        left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ : H ≃ₗᵢ[𝕜] H })
have h : ∀ (x : H),
  Eq (α := H)
    ((let __src := (↑(u * v) : H →L[𝕜] H);
          { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star (u * v)) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
            left_inv := sorry, right_inv := sorry, norm_map' := sorry } :
          (a : H) → H)
        x :
      H)
    ((HMul.hMul (α := H ≃ₗᵢ[𝕜] H)
            (let __src := (↑u : H →L[𝕜] H);
            { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star u) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
              left_inv := sorry, right_inv := sorry, norm_map' := sorry : H ≃ₗᵢ[𝕜] H })
            (let __src := (↑v : H →L[𝕜] H);
            { toLinearMap := (↑__src : H →ₗ[𝕜] H), invFun := (⇑(↑(↑(star v) : H →L[𝕜] H) : H →ₜ+ H) : (a : H) → H),
              left_inv := sorry, right_inv := sorry, norm_map' := sorry : H ≃ₗᵢ[𝕜] H }) :
          (a : H) → H)
        x :
      H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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 𝕜
⊢ Eq (α := F →ₗ[𝕜] E) ((toLin v₂.toBasis v₁.toBasis : (a : Matrix n m 𝕜) → F →ₗ[𝕜] E) Aᴴ : F →ₗ[𝕜] E)
    ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((toLin v₁.toBasis v₂.toBasis : (a : Matrix m n 𝕜) → E →ₗ[𝕜] F) A) :
      F →ₗ[𝕜] E)
have refine : ∀ (i : m) (j : n),
  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: refine eq_adjoint_iff_basis v₂.toBasis v₁.toBasis _ _ |>.mpr fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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)
      ((((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)
have 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)
Tactic: simp_rw [toLin_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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'
⊢ (LinearMap.adjoint : (a : E →ₗ[𝕜] E') → E' →ₗ[𝕜] E) f.toLinearMap ∘ₗ f.toLinearMap = LinearMap.id
have this : CompleteSpace E
Tactic: haveI := FiniteDimensional.complete 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
⊢ (LinearMap.adjoint : (a : E →ₗ[𝕜] E') → E' →ₗ[𝕜] E) f.toLinearMap ∘ₗ f.toLinearMap = LinearMap.id
have this₁ : CompleteSpace E'
Tactic: haveI := FiniteDimensional.complete 𝕜 E'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
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'
⊢ (LinearMap.adjoint : (a : E →ₗ[𝕜] E') → E' →ₗ[𝕜] E) f.toLinearMap ∘ₗ f.toLinearMap = LinearMap.id
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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'
⊢ Membership.mem (α := Matrix ι ι 𝕜) (γ := Submonoid (Matrix ι ι 𝕜)) (Matrix.unitaryGroup ι 𝕜)
    ((LinearMap.toMatrix b.toBasis b'.toBasis : (a : E →ₗ[𝕜] E') → Matrix ι ι 𝕜) (↑f.toLinearEquiv : E →ₗ[𝕜] E') :
      Matrix ι ι 𝕜)
have this : FiniteDimensional 𝕜 E
Tactic: have : FiniteDimensional 𝕜 E := Module.Basis.finiteDimensional_of_finite b.toBasis
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
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
⊢ Membership.mem (α := Matrix ι ι 𝕜) (γ := Submonoid (Matrix ι ι 𝕜)) (Matrix.unitaryGroup ι 𝕜)
    ((LinearMap.toMatrix b.toBasis b'.toBasis : (a : E →ₗ[𝕜] E') → Matrix ι ι 𝕜) (↑f.toLinearEquiv : E →ₗ[𝕜] E') :
      Matrix ι ι 𝕜)
have this₁ : FiniteDimensional 𝕜 E'
Tactic: have : FiniteDimensional 𝕜 E' := Module.Basis.finiteDimensional_of_finite b'.toBasis
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (goal)
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
⊢ ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
have rw : ⟪-(b -ᵥ a), v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
Tactic: rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (goal)
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
⊢ ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
have rw₁ : -⟪b -ᵥ a, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
Tactic: rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (goal)
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
⊢ ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
have rw₂ : ⟪b -ᵥ a, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
Tactic: rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (goal)
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
⊢ ⟪v, a -ᵥ b⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
have rw : ⟪v, -(b -ᵥ a)⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
Tactic: rw [← neg_vsub_eq_vsub_rev, inner_neg_right, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (goal)
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
⊢ ⟪v, a -ᵥ b⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
have rw₁ : -⟪v, b -ᵥ a⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
Tactic: rw [← neg_vsub_eq_vsub_rev, inner_neg_right, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Affine (goal)
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
⊢ ⟪v, a -ᵥ b⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
have rw₂ : ⟪v, b -ᵥ a⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
Tactic: rw [← neg_vsub_eq_vsub_rev, inner_neg_right, neg_eq_zero]
-- 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 c : P
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a b) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
have rw : ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) ‖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]
-- 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 c : P
rw : ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) ‖a -ᵥ b‖ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a b) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
have rw₁ : ⟪a -ᵥ b, a -ᵥ b - (a -ᵥ c)⟫ = 0 ↔ ⟪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]
-- 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 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
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a b) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
have rw₂ : ⟪a -ᵥ b, c -ᵥ b⟫ = 0 ↔ ⟪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]
-- 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 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
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a b) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
have rw₃ : ⟪a -ᵥ b, b -ᵥ c⟫ = 0 ↔ ⟪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]
-- 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 c : P
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
have rw : ⟪a -ᵥ c, a -ᵥ b⟫ = 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]
-- 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 c : P
rw : ⟪a -ᵥ c, a -ᵥ b⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
have rw₁ : ⟪a -ᵥ c, c -ᵥ b⟫ = 0 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
Tactic: rw [real_inner_comm, inner_vsub_vsub_left_eq_dist_sq_left_iff, real_inner_comm]
-- 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 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
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
have rw₂ : ⟪c -ᵥ b, a -ᵥ c⟫ = 0 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0
Tactic: rw [real_inner_comm, inner_vsub_vsub_left_eq_dist_sq_left_iff, real_inner_comm]
-- 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 c : P
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
have rw : ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) ‖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]
-- 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 c : P
rw : ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) ‖a -ᵥ c‖ 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
have rw₁ : ⟪a -ᵥ c, a -ᵥ c - (b -ᵥ c)⟫ = 0 ↔ ⟪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]
-- 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 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
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
have rw₂ : ⟪a -ᵥ c, a -ᵥ b⟫ = 0 ↔ ⟪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]
-- 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 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
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist a c) 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0
have rw₃ : ⟪a -ᵥ c, b -ᵥ a⟫ = 0 ↔ ⟪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]
-- 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 c : P
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist b c) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
have rw : ⟪b -ᵥ c, a -ᵥ 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]
-- 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 c : P
rw : ⟪b -ᵥ c, a -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist b c) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist b c) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
have rw₁ : ⟪b -ᵥ c, a -ᵥ b⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
Tactic: rw [real_inner_comm, inner_vsub_vsub_right_eq_dist_sq_left_iff, real_inner_comm]
-- 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 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
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = HPow.hPow (β := ℕ) (dist b c) 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
have rw₂ : ⟪a -ᵥ b, b -ᵥ c⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
Tactic: rw [real_inner_comm, inner_vsub_vsub_right_eq_dist_sq_left_iff, real_inner_comm]
-- 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 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)
have rw : (t₁ • (b -ᵥ a) +ᵥ a) -ᵥ (AffineMap.lineMap a c : (a : ℝ) → P) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
Tactic: rw [AffineMap.lineMap_apply, AffineMap.lineMap_apply, vadd_vsub_vadd_cancel_right]
-- 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 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)
⊢ 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)
have rw₁ : (t₁ • (b -ᵥ a) +ᵥ a) -ᵥ (t₂ • (c -ᵥ a) +ᵥ a) = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
Tactic: rw [AffineMap.lineMap_apply, AffineMap.lineMap_apply, vadd_vsub_vadd_cancel_right]
-- 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 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)
⊢ 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)
have rw₂ : t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a) = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
Tactic: rw [AffineMap.lineMap_apply, AffineMap.lineMap_apply, vadd_vsub_vadd_cancel_right]
-- 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 c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
⊢ 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
have 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)
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]
-- 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 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 (β := ℕ)
      (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
have 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
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]
-- 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
⊢ 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.{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