[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 : P
⊢ dist p1 (midpoint ℝ p1 p2) = dist p2 (midpoint ℝ p1 p2)
[PROOFSTEP]
rw [dist_left_midpoint (𝕜 := ℝ) p1 p2, dist_right_midpoint (𝕜 := ℝ) p1 p2]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ inner (↑(Finset.weightedVSub s₁ p₁) w₁) (↑(Finset.weightedVSub s₂ p₂) w₂) =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
[PROOFSTEP]
rw [Finset.weightedVSub_apply, Finset.weightedVSub_apply, inner_sum_smul_sum_smul_of_sum_eq_zero _ h₁ _ h₂]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ (-∑ i₁ in s₁,
          ∑ i₂ in s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ choice (_ : Nonempty P) - (p₂ i₂ -ᵥ choice (_ : Nonempty P))‖ *
                ‖p₁ i₁ -ᵥ choice (_ : Nonempty P) - (p₂ i₂ -ᵥ choice (_ : Nonempty P))‖)) /
      2 =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
[PROOFSTEP]
simp_rw [vsub_sub_vsub_cancel_right]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ (-∑ x in s₁, ∑ x_1 in s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) / 2 =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
[PROOFSTEP]
rcongr (i₁ i₂)
[GOAL]
case e_a.e_a.e_f.h.e_f.h.e_a.e_a
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
i₁ : ι₁
i₂ : ι₂
⊢ ‖p₁ i₁ -ᵥ p₂ i₂‖ = dist (p₁ i₁) (p₂ i₂)
[PROOFSTEP]
rw [dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)]
[GOAL]
case e_a.e_a.e_f.h.e_f.h.e_a.e_a
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
i₁ : ι₁
i₂ : ι₂
⊢ ‖p₁ i₁ -ᵥ p₂ i₂‖ = dist (p₁ i₁) (p₂ i₂)
[PROOFSTEP]
rw [dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
⊢ Sort ?u.15044
[PROOFSTEP]
have a₁ := s.affineCombination ℝ p w₁
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
a₁ : (fun a => P) w₁
⊢ Sort ?u.15044
[PROOFSTEP]
have a₂ := s.affineCombination ℝ p w₂
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
a₁ : (fun a => P) w₁
a₂ : (fun a => P) w₂
⊢ Sort ?u.15044
[PROOFSTEP]
exact
  dist a₁ a₂ * dist a₁ a₂ =
    (-∑ i₁ in s, ∑ i₂ in s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
⊢ let_fun a₁ := ↑(Finset.affineCombination ℝ s p) w₁;
  let_fun a₂ := ↑(Finset.affineCombination ℝ s p) w₂;
  dist a₁ a₂ * dist a₁ a₂ =
    (-∑ i₁ in s, ∑ i₂ in s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
[PROOFSTEP]
dsimp only
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
⊢ dist (↑(Finset.affineCombination ℝ s p) w₁) (↑(Finset.affineCombination ℝ s p) w₂) *
      dist (↑(Finset.affineCombination ℝ s p) w₁) (↑(Finset.affineCombination ℝ s p) w₂) =
    (-∑ i₁ in s, ∑ i₂ in s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
[PROOFSTEP]
rw [dist_eq_norm_vsub V (s.affineCombination ℝ p w₁) (s.affineCombination ℝ p w₂), ← @inner_self_eq_norm_mul_norm ℝ,
  Finset.affineCombination_vsub]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
⊢ ↑IsROrC.re (inner (↑(Finset.weightedVSub s p) (w₁ - w₂)) (↑(Finset.weightedVSub s p) (w₁ - w₂))) =
    (-∑ i₁ in s, ∑ i₂ in s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
[PROOFSTEP]
have h : (∑ i in s, (w₁ - w₂) i) = 0 := by simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
⊢ ∑ i in s, (w₁ - w₂) i = 0
[PROOFSTEP]
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i in s, w₁ i = 1
h₂ : ∑ i in s, w₂ i = 1
h : ∑ i in s, (w₁ - w₂) i = 0
⊢ ↑IsROrC.re (inner (↑(Finset.weightedVSub s p) (w₁ - w₂)) (↑(Finset.weightedVSub s p) (w₁ - w₂))) =
    (-∑ i₁ in s, ∑ i₂ in s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
[PROOFSTEP]
exact inner_weightedVSub p h p h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
r : ℝ
v : V
p₁ p₂ : P
⊢ dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ =
    inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂)
[PROOFSTEP]
rw [dist_eq_norm_vsub V _ p₂, ← real_inner_self_eq_norm_mul_norm, vadd_vsub_assoc, real_inner_add_add_self,
  real_inner_smul_left, real_inner_smul_left, real_inner_smul_right]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
r : ℝ
v : V
p₁ p₂ : P
⊢ r * (r * inner v v) + 2 * (r * inner v (p₁ -ᵥ p₂)) + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂) =
    inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂)
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
[PROOFSTEP]
conv_lhs =>
  rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, ← sub_eq_zero, add_sub_assoc,
    dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm, sub_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂
[PROOFSTEP]
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, ← sub_eq_zero, add_sub_assoc,
    dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm, sub_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂
[PROOFSTEP]
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, ← sub_eq_zero, add_sub_assoc,
    dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm, sub_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂
[PROOFSTEP]
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, ← sub_eq_zero, add_sub_assoc,
  dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm, sub_self]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
[PROOFSTEP]
have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ inner v v ≠ 0
[PROOFSTEP]
simpa using hv
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
[PROOFSTEP]
have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫) :=
  by
  rw [discrim]
  ring
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
[PROOFSTEP]
rw [discrim]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ (2 * inner v (p₁ -ᵥ p₂)) ^ 2 - 4 * inner v v * 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
hd : discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
[PROOFSTEP]
rw [quadratic_eq_zero_iff hvi hd, add_left_neg, zero_div, neg_mul_eq_neg_mul, ← mul_sub_right_distrib, sub_eq_add_neg, ←
  mul_two, mul_assoc, mul_div_assoc, mul_div_mul_left, mul_div_assoc]
[GOAL]
case hc
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
hd : discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
have ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
  inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hp₂c₁.symm) (hp₁c₂.trans hp₂c₂.symm)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 :=
  inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hpc₁.symm) (hp₁c₂.trans hpc₂.symm)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
let b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
have hb : LinearIndependent ℝ b :=
  by
  refine' linearIndependent_of_ne_zero_of_inner_eq_zero _ _
  · intro i
    fin_cases i <;> simp [hc.symm, hp.symm]
  · intro i j hij
    fin_cases i <;> fin_cases j <;> try exact False.elim (hij rfl)
    · exact ho
    · rw [real_inner_comm]
      exact ho
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ LinearIndependent ℝ b
[PROOFSTEP]
refine' linearIndependent_of_ne_zero_of_inner_eq_zero _ _
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ ∀ (i : Fin 2), b i ≠ 0
[PROOFSTEP]
intro i
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
i : Fin 2
⊢ b i ≠ 0
[PROOFSTEP]
fin_cases i
[GOAL]
case refine'_1.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ b { val := 0, isLt := (_ : 0 < 2) } ≠ 0
[PROOFSTEP]
simp [hc.symm, hp.symm]
[GOAL]
case refine'_1.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ b { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ 0
[PROOFSTEP]
simp [hc.symm, hp.symm]
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ ∀ (i j : Fin 2), i ≠ j → inner (b i) (b j) = 0
[PROOFSTEP]
intro i j hij
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
i j : Fin 2
hij : i ≠ j
⊢ inner (b i) (b j) = 0
[PROOFSTEP]
fin_cases i
[GOAL]
case refine'_2.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
j : Fin 2
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ j
⊢ inner (b { val := 0, isLt := (_ : 0 < 2) }) (b j) = 0
[PROOFSTEP]
fin_cases j
[GOAL]
case refine'_2.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
j : Fin 2
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ j
⊢ inner (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) (b j) = 0
[PROOFSTEP]
fin_cases j
[GOAL]
case refine'_2.head.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (b { val := 0, isLt := (_ : 0 < 2) }) (b { val := 0, isLt := (_ : 0 < 2) }) = 0
[PROOFSTEP]
try exact False.elim (hij rfl)
[GOAL]
case refine'_2.head.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (b { val := 0, isLt := (_ : 0 < 2) }) (b { val := 0, isLt := (_ : 0 < 2) }) = 0
[PROOFSTEP]
exact False.elim (hij rfl)
[GOAL]
case refine'_2.head.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (b { val := 0, isLt := (_ : 0 < 2) }) (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) = 0
[PROOFSTEP]
try exact False.elim (hij rfl)
[GOAL]
case refine'_2.head.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (b { val := 0, isLt := (_ : 0 < 2) }) (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) = 0
[PROOFSTEP]
exact False.elim (hij rfl)
[GOAL]
case refine'_2.tail.head.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) (b { val := 0, isLt := (_ : 0 < 2) }) = 0
[PROOFSTEP]
try exact False.elim (hij rfl)
[GOAL]
case refine'_2.tail.head.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) (b { val := 0, isLt := (_ : 0 < 2) }) = 0
[PROOFSTEP]
exact False.elim (hij rfl)
[GOAL]
case refine'_2.tail.head.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) = 0
[PROOFSTEP]
try exact False.elim (hij rfl)
[GOAL]
case refine'_2.tail.head.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) = 0
[PROOFSTEP]
exact False.elim (hij rfl)
[GOAL]
case refine'_2.head.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (b { val := 0, isLt := (_ : 0 < 2) }) (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) = 0
[PROOFSTEP]
exact ho
[GOAL]
case refine'_2.tail.head.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) (b { val := 0, isLt := (_ : 0 < 2) }) = 0
[PROOFSTEP]
rw [real_inner_comm]
[GOAL]
case refine'_2.tail.head.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (b { val := 0, isLt := (_ : 0 < 2) }) (b { val := 1, isLt := (_ : (fun a => a < 2) 1) }) = 0
[PROOFSTEP]
exact ho
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
have hbs : Submodule.span ℝ (Set.range b) = s.direction :=
  by
  refine' eq_of_le_of_finrank_eq _ _
  · rw [Submodule.span_le, Set.range_subset_iff]
    intro i
    fin_cases i
    · exact vsub_mem_direction hc₂s hc₁s
    · exact vsub_mem_direction hp₂s hp₁s
  · rw [finrank_span_eq_card hb, Fintype.card_fin, hd]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ Submodule.span ℝ (Set.range b) = direction s
[PROOFSTEP]
refine' eq_of_le_of_finrank_eq _ _
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ Submodule.span ℝ (Set.range b) ≤ direction s
[PROOFSTEP]
rw [Submodule.span_le, Set.range_subset_iff]
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ ∀ (y : Fin 2), b y ∈ ↑(direction s)
[PROOFSTEP]
intro i
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
i : Fin 2
⊢ b i ∈ ↑(direction s)
[PROOFSTEP]
fin_cases i
[GOAL]
case refine'_1.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ b { val := 0, isLt := (_ : 0 < 2) } ∈ ↑(direction s)
[PROOFSTEP]
exact vsub_mem_direction hc₂s hc₁s
[GOAL]
case refine'_1.tail.head
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ b { val := 1, isLt := (_ : (fun a => a < 2) 1) } ∈ ↑(direction s)
[PROOFSTEP]
exact vsub_mem_direction hp₂s hp₁s
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ finrank ℝ { x // x ∈ Submodule.span ℝ (Set.range b) } = finrank ℝ { x // x ∈ direction s }
[PROOFSTEP]
rw [finrank_span_eq_card hb, Fintype.card_fin, hd]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
have hv : ∀ v ∈ s.direction, ∃ t₁ t₂ : ℝ, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁) :=
  by
  intro v hv
  have hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁} :=
    by
    have hu : (Finset.univ : Finset (Fin 2)) = {0, 1} := by decide
    rw [← Fintype.coe_image_univ, hu]
    simp
  rw [← hbs, hr, Submodule.mem_span_insert] at hv 
  rcases hv with ⟨t₁, v', hv', hv⟩
  rw [Submodule.mem_span_singleton] at hv' 
  rcases hv' with ⟨t₂, rfl⟩
  exact ⟨t₁, t₂, hv⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
⊢ ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
[PROOFSTEP]
intro v hv
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hv : v ∈ direction s
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
[PROOFSTEP]
have hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁} :=
  by
  have hu : (Finset.univ : Finset (Fin 2)) = {0, 1} := by decide
  rw [← Fintype.coe_image_univ, hu]
  simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hv : v ∈ direction s
⊢ Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
[PROOFSTEP]
have hu : (Finset.univ : Finset (Fin 2)) = {0, 1} := by decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hv : v ∈ direction s
⊢ Finset.univ = {0, 1}
[PROOFSTEP]
decide
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hv : v ∈ direction s
hu : Finset.univ = {0, 1}
⊢ Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
[PROOFSTEP]
rw [← Fintype.coe_image_univ, hu]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hv : v ∈ direction s
hu : Finset.univ = {0, 1}
⊢ ↑(Finset.image b {0, 1}) = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hv : v ∈ direction s
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
[PROOFSTEP]
rw [← hbs, hr, Submodule.mem_span_insert] at hv 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hv : ∃ a z, z ∈ Submodule.span ℝ {p₂ -ᵥ p₁} ∧ v = a • (c₂ -ᵥ c₁) + z
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
[PROOFSTEP]
rcases hv with ⟨t₁, v', hv', hv⟩
[GOAL]
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
t₁ : ℝ
v' : V
hv' : v' ∈ Submodule.span ℝ {p₂ -ᵥ p₁}
hv : v = t₁ • (c₂ -ᵥ c₁) + v'
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
[PROOFSTEP]
rw [Submodule.mem_span_singleton] at hv' 
[GOAL]
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
t₁ : ℝ
v' : V
hv' : ∃ a, a • (p₂ -ᵥ p₁) = v'
hv : v = t₁ • (c₂ -ᵥ c₁) + v'
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
[PROOFSTEP]
rcases hv' with ⟨t₂, rfl⟩
[GOAL]
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
v : V
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
t₁ t₂ : ℝ
hv : v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
[PROOFSTEP]
exact ⟨t₁, t₂, hv⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
rcases hv (p -ᵥ p₁) (vsub_mem_direction hps hp₁s) with ⟨t₁, t₂, hpt⟩
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hpt : p -ᵥ p₁ = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
simp only [hpt, inner_add_right, inner_smul_right, ho, mul_zero, add_zero, mul_eq_zero, inner_self_eq_zero,
  vsub_eq_zero_iff_eq, hc.symm, or_false_iff] at hop 
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hpt : p -ᵥ p₁ = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
hop : t₁ = 0
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
rw [hop, zero_smul, zero_add, ← eq_vadd_iff_vsub_eq] at hpt 
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hpt : p = t₂ • (p₂ -ᵥ p₁) +ᵥ p₁
hop : t₁ = 0
⊢ p = p₁ ∨ p = p₂
[PROOFSTEP]
subst hpt
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
have hp' : (p₂ -ᵥ p₁ : V) ≠ 0 := by simp [hp.symm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
⊢ p₂ -ᵥ p₁ ≠ 0
[PROOFSTEP]
simp [hp.symm]
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
have hp₂ : dist ((1 : ℝ) • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁ := by simp [hp₂c₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
⊢ dist (1 • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
[PROOFSTEP]
simp [hp₂c₁]
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : dist (1 • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
rw [← hp₁c₁, dist_smul_vadd_eq_dist _ _ hp'] at hpc₁ hp₂ 
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : t₂ = 0 ∨ t₂ = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = 0 ∨ 1 = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
simp only [one_ne_zero, false_or_iff] at hp₂ 
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : t₂ = 0 ∨ t₂ = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
rw [hp₂.symm] at hpc₁ 
[GOAL]
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : t₂ = 0 ∨ t₂ = 1
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
cases' hpc₁ with hpc₁ hpc₁
[GOAL]
case intro.intro.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
hpc₁ : t₂ = 0
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
simp [hpc₁]
[GOAL]
case intro.intro.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ { x // x ∈ direction s }
hd : finrank ℝ { x // x ∈ direction s } = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = direction s
hv : ∀ (v : V), v ∈ direction s → ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
hpc₁ : t₂ = 1
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
[PROOFSTEP]
simp [hpc₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = 2
c₁ c₂ p₁ p₂ p : P
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ finrank ℝ { x // x ∈ direction ⊤ } = 2
[PROOFSTEP]
rw [direction_top, finrank_top]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = 2
c₁ c₂ p₁ p₂ p : P
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ finrank ℝ V = 2
[PROOFSTEP]
exact hd
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ IsCompl (direction s) (direction (mk' p (direction s)ᗮ))
[PROOFSTEP]
rw [direction_mk' p s.directionᗮ]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ IsCompl (direction s) (direction s)ᗮ
[PROOFSTEP]
exact Submodule.isCompl_orthogonal_of_completeSpace
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ IsCompl (direction s) (direction (mk' p (direction s)ᗮ))
[PROOFSTEP]
rw [direction_mk' p s.directionᗮ]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ IsCompl (direction s) (direction s)ᗮ
[PROOFSTEP]
exact Submodule.isCompl_orthogonal_of_completeSpace
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ orthogonalProjectionFn s p ∈ s
[PROOFSTEP]
rw [← mem_coe, ← Set.singleton_subset_iff, ← inter_eq_singleton_orthogonalProjectionFn]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑s ∩ ↑(mk' p (direction s)ᗮ) ⊆ ↑s
[PROOFSTEP]
exact Set.inter_subset_left _ _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ orthogonalProjectionFn s p ∈ mk' p (direction s)ᗮ
[PROOFSTEP]
rw [← mem_coe, ← Set.singleton_subset_iff, ← inter_eq_singleton_orthogonalProjectionFn]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑s ∩ ↑(mk' p (direction s)ᗮ) ⊆ ↑(mk' p (direction s)ᗮ)
[PROOFSTEP]
exact Set.inter_subset_right _ _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
⊢ (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) (v +ᵥ p) =
    ↑↑(_root_.orthogonalProjection (direction s)) v +ᵥ
      (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) p
[PROOFSTEP]
have hs : ((orthogonalProjection s.direction) v : V) +ᵥ orthogonalProjectionFn s p ∈ s :=
  vadd_mem_of_mem_direction (orthogonalProjection s.direction v).2 (orthogonalProjectionFn_mem p)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
⊢ (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) (v +ᵥ p) =
    ↑↑(_root_.orthogonalProjection (direction s)) v +ᵥ
      (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) p
[PROOFSTEP]
have ho : ((orthogonalProjection s.direction) v : V) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) s.directionᗮ :=
  by
  rw [← vsub_right_mem_direction_iff_mem (self_mem_mk' _ _) _, direction_mk', vsub_vadd_eq_vsub_sub, vadd_vsub_assoc,
    add_comm, add_sub_assoc]
  refine' Submodule.add_mem _ (orthogonalProjectionFn_vsub_mem_direction_orthogonal p) _
  rw [Submodule.mem_orthogonal']
  intro w hw
  rw [← neg_sub, inner_neg_left, orthogonalProjection_inner_eq_zero _ w hw, neg_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
⊢ ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) (direction s)ᗮ
[PROOFSTEP]
rw [← vsub_right_mem_direction_iff_mem (self_mem_mk' _ _) _, direction_mk', vsub_vadd_eq_vsub_sub, vadd_vsub_assoc,
  add_comm, add_sub_assoc]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
⊢ orthogonalProjectionFn s p -ᵥ p + (↑(↑(_root_.orthogonalProjection (direction s)) v) - v) ∈ (direction s)ᗮ
[PROOFSTEP]
refine' Submodule.add_mem _ (orthogonalProjectionFn_vsub_mem_direction_orthogonal p) _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
⊢ ↑(↑(_root_.orthogonalProjection (direction s)) v) - v ∈ (direction s)ᗮ
[PROOFSTEP]
rw [Submodule.mem_orthogonal']
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
⊢ ∀ (u : V), u ∈ direction s → inner (↑(↑(_root_.orthogonalProjection (direction s)) v) - v) u = 0
[PROOFSTEP]
intro w hw
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
w : V
hw : w ∈ direction s
⊢ inner (↑(↑(_root_.orthogonalProjection (direction s)) v) - v) w = 0
[PROOFSTEP]
rw [← neg_sub, inner_neg_left, orthogonalProjection_inner_eq_zero _ w hw, neg_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
ho : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) (direction s)ᗮ
⊢ (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) (v +ᵥ p) =
    ↑↑(_root_.orthogonalProjection (direction s)) v +ᵥ
      (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) p
[PROOFSTEP]
have hm :
  ((orthogonalProjection s.direction) v : V) +ᵥ orthogonalProjectionFn s p ∈
    ({orthogonalProjectionFn s (v +ᵥ p)} : Set P) :=
  by
  rw [← inter_eq_singleton_orthogonalProjectionFn (v +ᵥ p)]
  exact Set.mem_inter hs ho
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
ho : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) (direction s)ᗮ
⊢ ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ {orthogonalProjectionFn s (v +ᵥ p)}
[PROOFSTEP]
rw [← inter_eq_singleton_orthogonalProjectionFn (v +ᵥ p)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
ho : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) (direction s)ᗮ
⊢ ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ ↑s ∩ ↑(mk' (v +ᵥ p) (direction s)ᗮ)
[PROOFSTEP]
exact Set.mem_inter hs ho
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
ho : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) (direction s)ᗮ
hm :
  ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ {orthogonalProjectionFn s (v +ᵥ p)}
⊢ (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) (v +ᵥ p) =
    ↑↑(_root_.orthogonalProjection (direction s)) v +ᵥ
      (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) p
[PROOFSTEP]
rw [Set.mem_singleton_iff] at hm 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
ho : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) (direction s)ᗮ
hm : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p = orthogonalProjectionFn s (v +ᵥ p)
⊢ (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) (v +ᵥ p) =
    ↑↑(_root_.orthogonalProjection (direction s)) v +ᵥ
      (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) p
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V
hs : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ s
ho : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p ∈ mk' (v +ᵥ p) (direction s)ᗮ
hm : ↑(↑(_root_.orthogonalProjection (direction s)) v) +ᵥ orthogonalProjectionFn s p = orthogonalProjectionFn s (v +ᵥ p)
⊢ ↑((fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) (v +ᵥ p)) =
    ↑(↑↑(_root_.orthogonalProjection (direction s)) v +ᵥ
        (fun p => { val := orthogonalProjectionFn s p, property := (_ : orthogonalProjectionFn s p ∈ s) }) p)
[PROOFSTEP]
exact hm.symm
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑s ∩ ↑(mk' p (direction s)ᗮ) = {↑(↑(orthogonalProjection s) p)}
[PROOFSTEP]
rw [← orthogonalProjectionFn_eq]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑s ∩ ↑(mk' p (direction s)ᗮ) = {orthogonalProjectionFn s p}
[PROOFSTEP]
exact inter_eq_singleton_orthogonalProjectionFn p
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(↑(orthogonalProjection s) p) = p ↔ p ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(↑(orthogonalProjection s) p) = p → p ∈ s
[PROOFSTEP]
exact fun h => h ▸ orthogonalProjection_mem p
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ p ∈ s → ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
intro h
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : p ∈ s
⊢ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
have hp : p ∈ (s : Set P) ∩ mk' p s.directionᗮ := ⟨h, self_mem_mk' p _⟩
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : p ∈ s
hp : p ∈ ↑s ∩ ↑(mk' p (direction s)ᗮ)
⊢ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
rw [inter_eq_singleton_orthogonalProjection p] at hp 
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : p ∈ s
hp✝ : p ∈ ↑s ∩ ↑(mk' p (direction s)ᗮ)
hp : p ∈ {↑(↑(orthogonalProjection s) p)}
⊢ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
symm
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : p ∈ s
hp✝ : p ∈ ↑s ∩ ↑(mk' p (direction s)ᗮ)
hp : p ∈ {↑(↑(orthogonalProjection s) p)}
⊢ p = ↑(↑(orthogonalProjection s) p)
[PROOFSTEP]
exact hp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : { x // x ∈ s }
⊢ ↑(orthogonalProjection s) ↑p = p
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : { x // x ∈ s }
⊢ ↑(↑(orthogonalProjection s) ↑p) = ↑p
[PROOFSTEP]
rw [orthogonalProjection_eq_self_iff]
[GOAL]
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : { x // x ∈ s }
⊢ ↑p ∈ s
[PROOFSTEP]
exact p.2
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(orthogonalProjection s) ↑(↑(orthogonalProjection s) p) = ↑(orthogonalProjection s) p
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(↑(orthogonalProjection s) ↑(↑(orthogonalProjection s) p)) = ↑(↑(orthogonalProjection s) p)
[PROOFSTEP]
rw [orthogonalProjection_eq_self_iff]
[GOAL]
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(↑(orthogonalProjection s) p) ∈ s
[PROOFSTEP]
exact orthogonalProjection_mem p
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s s' : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s }
inst✝² : Nonempty { x // x ∈ s' }
inst✝¹ : HasOrthogonalProjection (direction s)
inst✝ : HasOrthogonalProjection (direction s')
h : s = s'
p : P
⊢ ↑(↑(orthogonalProjection s) p) = ↑(↑(orthogonalProjection s') p)
[PROOFSTEP]
subst h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s }
inst✝² : HasOrthogonalProjection (direction s)
p : P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
⊢ ↑(↑(orthogonalProjection s) p) = ↑(↑(orthogonalProjection s) p)
[PROOFSTEP]
rfl
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ dist p ↑(↑(orthogonalProjection s) p) = 0 ↔ p ∈ s
[PROOFSTEP]
rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_iff]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(_root_.orthogonalProjection (direction s)) (p -ᵥ ↑(↑(orthogonalProjection s) p)) = 0
[PROOFSTEP]
apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
[GOAL]
case hv
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ p -ᵥ ↑(↑(orthogonalProjection s) p) ∈ (direction s)ᗮ
[PROOFSTEP]
intro c hc
[GOAL]
case hv
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
c : V
hc : c ∈ direction s
⊢ inner c (p -ᵥ ↑(↑(orthogonalProjection s) p)) = 0
[PROOFSTEP]
rw [← neg_vsub_eq_vsub_rev, inner_neg_right, orthogonalProjection_vsub_mem_direction_orthogonal s p c hc, neg_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
[PROOFSTEP]
have h := vsub_orthogonalProjection_mem_direction_orthogonal s (v +ᵥ p)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
h : v +ᵥ p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
[PROOFSTEP]
rw [vadd_vsub_assoc, Submodule.add_mem_iff_right _ hv] at h 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑(orthogonalProjection s) (v +ᵥ p) = { val := p, property := hp }
[PROOFSTEP]
refine' (eq_of_vsub_eq_zero _).symm
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ { val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p) = 0
[PROOFSTEP]
ext
[GOAL]
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑({ val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p)) = ↑0
[PROOFSTEP]
refine' Submodule.disjoint_def.1 s.direction.orthogonal_disjoint _ _ h
[GOAL]
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
h : p -ᵥ ↑(↑(orthogonalProjection s) (v +ᵥ p)) ∈ (direction s)ᗮ
⊢ ↑({ val := p, property := hp } -ᵥ ↑(orthogonalProjection s) (v +ᵥ p)) ∈ direction s
[PROOFSTEP]
exact (_ : s.direction).2
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p1 p2 : P
hp1 : p1 ∈ s
⊢ dist p1 p2 * dist p1 p2 =
    dist p1 ↑(↑(orthogonalProjection s) p2) * dist p1 ↑(↑(orthogonalProjection s) p2) +
      dist p2 ↑(↑(orthogonalProjection s) p2) * dist p2 ↑(↑(orthogonalProjection s) p2)
[PROOFSTEP]
rw [dist_comm p2 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V _ p2, ←
  vsub_add_vsub_cancel p1 (orthogonalProjection s p2) p2, norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p1 p2 : P
hp1 : p1 ∈ s
⊢ inner (p1 -ᵥ ↑(↑(orthogonalProjection s) p2)) (↑(↑(orthogonalProjection s) p2) -ᵥ p2) = 0
[PROOFSTEP]
exact
  Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p2 hp1)
    (orthogonalProjection_vsub_mem_direction_orthogonal s p2)
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) =
    ‖p1 -ᵥ p2 + (r1 - r2) • v‖ * ‖p1 -ᵥ p2 + (r1 - r2) • v‖
[PROOFSTEP]
rw [dist_eq_norm_vsub V (r1 • v +ᵥ p1), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul, add_comm, add_sub_assoc]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + ‖(r1 - r2) • v‖ * ‖(r1 - r2) • v‖ =
    ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * |r1 - r2| * ‖v‖ * ‖v‖
[PROOFSTEP]
rw [norm_smul, Real.norm_eq_abs]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * ‖v‖ * (|r1 - r2| * ‖v‖) =
    ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * |r1 - r2| * ‖v‖ * ‖v‖
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
r1 r2 : ℝ
v : V
hv : v ∈ (direction s)ᗮ
⊢ ‖p1 -ᵥ p2‖ * ‖p1 -ᵥ p2‖ + |r1 - r2| * |r1 - r2| * ‖v‖ * ‖v‖ =
    dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (‖v‖ * ‖v‖)
[PROOFSTEP]
rw [dist_eq_norm_vsub V p1, abs_mul_abs_self, mul_assoc]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
⊢ ∀ (p' : P),
    (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p)) p' =
      ↑(_root_.reflection (direction s)) (p' -ᵥ ↑(Classical.arbitrary { x // x ∈ s })) +ᵥ
        (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p))
          ↑(Classical.arbitrary { x // x ∈ s })
[PROOFSTEP]
intro p
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p)) p =
    ↑(_root_.reflection (direction s)) (p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })) +ᵥ
      (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p))
        ↑(Classical.arbitrary { x // x ∈ s })
[PROOFSTEP]
let v := p -ᵥ ↑(Classical.arbitrary s)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
⊢ (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p)) p =
    ↑(_root_.reflection (direction s)) (p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })) +ᵥ
      (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p))
        ↑(Classical.arbitrary { x // x ∈ s })
[PROOFSTEP]
let a : V := _root_.orthogonalProjection s.direction v
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
⊢ (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p)) p =
    ↑(_root_.reflection (direction s)) (p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })) +ᵥ
      (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p))
        ↑(Classical.arbitrary { x // x ∈ s })
[PROOFSTEP]
let b : P := ↑(Classical.arbitrary s)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
b : P := ↑(Classical.arbitrary { x // x ∈ s })
⊢ (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p)) p =
    ↑(_root_.reflection (direction s)) (p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })) +ᵥ
      (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p))
        ↑(Classical.arbitrary { x // x ∈ s })
[PROOFSTEP]
have key : a +ᵥ b -ᵥ (v +ᵥ b) +ᵥ (a +ᵥ b) = a + a - v +ᵥ (b -ᵥ b +ᵥ b) :=
  by
  rw [← add_vadd, vsub_vadd_eq_vsub_sub, vsub_vadd, vadd_vsub]
  congr 1
  abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
b : P := ↑(Classical.arbitrary { x // x ∈ s })
⊢ a +ᵥ b -ᵥ (v +ᵥ b) +ᵥ (a +ᵥ b) = a + a - v +ᵥ (b -ᵥ b +ᵥ b)
[PROOFSTEP]
rw [← add_vadd, vsub_vadd_eq_vsub_sub, vsub_vadd, vadd_vsub]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
b : P := ↑(Classical.arbitrary { x // x ∈ s })
⊢ a - v + a +ᵥ b = a + a - v +ᵥ b
[PROOFSTEP]
congr 1
[GOAL]
case e_a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
b : P := ↑(Classical.arbitrary { x // x ∈ s })
⊢ a - v + a = a + a - v
[PROOFSTEP]
abel
[GOAL]
case e_a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
b : P := ↑(Classical.arbitrary { x // x ∈ s })
⊢ a - v + a = a + a - v
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
b : P := ↑(Classical.arbitrary { x // x ∈ s })
key : a +ᵥ b -ᵥ (v +ᵥ b) +ᵥ (a +ᵥ b) = a + a - v +ᵥ (b -ᵥ b +ᵥ b)
⊢ (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p)) p =
    ↑(_root_.reflection (direction s)) (p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })) +ᵥ
      (fun p => ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p))
        ↑(Classical.arbitrary { x // x ∈ s })
[PROOFSTEP]
dsimp only
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
v : V := p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })
a : V := ↑(↑(_root_.orthogonalProjection (direction s)) v)
b : P := ↑(Classical.arbitrary { x // x ∈ s })
key : a +ᵥ b -ᵥ (v +ᵥ b) +ᵥ (a +ᵥ b) = a + a - v +ᵥ (b -ᵥ b +ᵥ b)
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) =
    ↑(_root_.reflection (direction s)) (p -ᵥ ↑(Classical.arbitrary { x // x ∈ s })) +ᵥ
      (↑(↑(orthogonalProjection s) ↑(Classical.arbitrary { x // x ∈ s })) -ᵥ ↑(Classical.arbitrary { x // x ∈ s }) +ᵥ
        ↑(↑(orthogonalProjection s) ↑(Classical.arbitrary { x // x ∈ s })))
[PROOFSTEP]
rwa [reflection_apply, (vsub_vadd p b).symm, AffineMap.map_vadd, orthogonalProjection_linear, vadd_vsub,
  orthogonalProjection_mem_subspace_eq_self, two_smul]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s s' : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s }
inst✝² : Nonempty { x // x ∈ s' }
inst✝¹ : HasOrthogonalProjection (direction s)
inst✝ : HasOrthogonalProjection (direction s')
h : s = s'
p : P
⊢ ↑(reflection s) p = ↑(reflection s') p
[PROOFSTEP]
subst h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s }
inst✝² : HasOrthogonalProjection (direction s)
p : P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
⊢ ↑(reflection s) p = ↑(reflection s) p
[PROOFSTEP]
rfl
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(reflection s) (↑(reflection s) p) = p
[PROOFSTEP]
have :
  ∀ a : s,
    ∀ b : V,
      (_root_.orthogonalProjection s.direction) b = 0 → reflection s (reflection s (b +ᵥ (a : P))) = b +ᵥ (a : P) :=
  by
  intro _ _ h
  simp [reflection, h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
[PROOFSTEP]
intro _ _ h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
a✝ : { x // x ∈ s }
b✝ : V
h : ↑(_root_.orthogonalProjection (direction s)) b✝ = 0
⊢ ↑(reflection s) (↑(reflection s) (b✝ +ᵥ ↑a✝)) = b✝ +ᵥ ↑a✝
[PROOFSTEP]
simp [reflection, h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
this :
  ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ ↑(reflection s) (↑(reflection s) p) = p
[PROOFSTEP]
rw [← vsub_vadd p (orthogonalProjection s p)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
this :
  ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ ↑(reflection s) (↑(reflection s) (p -ᵥ ↑(↑(orthogonalProjection s) p) +ᵥ ↑(↑(orthogonalProjection s) p))) =
    p -ᵥ ↑(↑(orthogonalProjection s) p) +ᵥ ↑(↑(orthogonalProjection s) p)
[PROOFSTEP]
exact this (orthogonalProjection s p) _ (orthogonalProjection_vsub_orthogonalProjection s p)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
⊢ AffineIsometryEquiv.symm (reflection s) = reflection s
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
x✝ : P
⊢ ↑(AffineIsometryEquiv.symm (reflection s)) x✝ = ↑(reflection s) x✝
[PROOFSTEP]
rw [← (reflection s).injective.eq_iff]
[GOAL]
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
x✝ : P
⊢ ↑(reflection s) (↑(AffineIsometryEquiv.symm (reflection s)) x✝) = ↑(reflection s) (↑(reflection s) x✝)
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(reflection s) p = p ↔ p ∈ s
[PROOFSTEP]
rw [← orthogonalProjection_eq_self_iff, reflection_apply]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p ↔ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p → ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
intro h
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
rw [← @vsub_eq_zero_iff_eq V, vadd_vsub_assoc, ← two_smul ℝ (↑(orthogonalProjection s p) -ᵥ p), smul_eq_zero] at h 
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : 2 = 0 ∨ ↑(↑(orthogonalProjection s) p) -ᵥ p = 0
⊢ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
norm_num at h 
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
exact h
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
⊢ ↑(↑(orthogonalProjection s) p) = p → ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
intro h
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
h : ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
⊢ ↑(reflection s₁) p = ↑(reflection s₂) p ↔ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
rw [reflection_apply, reflection_apply]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p) ↔
    ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p) →
    ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
intro h
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
h :
  ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
    ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
rw [← @vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
  vsub_sub_vsub_cancel_right, ← two_smul ℝ ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p),
  smul_eq_zero] at h 
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
h : 2 = 0 ∨ ↑(↑(orthogonalProjection s₁) p) -ᵥ ↑(↑(orthogonalProjection s₂) p) = 0
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
norm_num at h 
[GOAL]
case mp
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
h : ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
exact h
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p) →
    ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
intro h
[GOAL]
case mpr
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : HasOrthogonalProjection (direction s₁)
inst✝ : HasOrthogonalProjection (direction s₂)
p : P
h : ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
    ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p)
[PROOFSTEP]
rw [h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ p₂ : P
⊢ dist p₁ (↑(reflection s) p₂) = dist (↑(reflection s) p₁) p₂
[PROOFSTEP]
conv_lhs => rw [← reflection_reflection s p₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ p₂ : P
| dist p₁ (↑(reflection s) p₂)
[PROOFSTEP]
rw [← reflection_reflection s p₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ p₂ : P
| dist p₁ (↑(reflection s) p₂)
[PROOFSTEP]
rw [← reflection_reflection s p₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ p₂ : P
| dist p₁ (↑(reflection s) p₂)
[PROOFSTEP]
rw [← reflection_reflection s p₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ p₂ : P
⊢ dist (↑(reflection s) (↑(reflection s) p₁)) (↑(reflection s) p₂) = dist (↑(reflection s) p₁) p₂
[PROOFSTEP]
exact (reflection s).dist_map _ _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
⊢ dist p₁ (↑(reflection s) p₂) = dist p₁ p₂
[PROOFSTEP]
rw [← reflection_eq_self_iff p₁] at hp₁ 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ : P
hp₁✝ : p₁ ∈ s
hp₁ : ↑(reflection s) p₁ = p₁
p₂ : P
⊢ dist p₁ (↑(reflection s) p₂) = dist p₁ p₂
[PROOFSTEP]
convert (reflection s).dist_map p₁ p₂
[GOAL]
case h.e'_2.h.e'_3
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p₁ : P
hp₁✝ : p₁ ∈ s
hp₁ : ↑(reflection s) p₁ = p₁
p₂ : P
⊢ p₁ = ↑(reflection s) p₁
[PROOFSTEP]
rw [hp₁]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : HasOrthogonalProjection (direction s₁)
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ ↑(reflection s₁) p ∈ s₂
[PROOFSTEP]
rw [reflection_apply]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : HasOrthogonalProjection (direction s₁)
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) ∈ s₂
[PROOFSTEP]
have ho : ↑(orthogonalProjection s₁ p) ∈ s₂ := hle (orthogonalProjection_mem p)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s₁ }
inst✝ : HasOrthogonalProjection (direction s₁)
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
ho : ↑(↑(orthogonalProjection s₁) p) ∈ s₂
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) ∈ s₂
[PROOFSTEP]
exact vadd_mem_of_mem_direction (vsub_mem_direction ho hp) ho
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
⊢ ↑(reflection s) (v +ᵥ p) = -v +ᵥ p
[PROOFSTEP]
rw [reflection_apply, orthogonalProjection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : HasOrthogonalProjection (direction s)
p : P
hp : p ∈ s
v : V
hv : v ∈ (direction s)ᗮ
⊢ ↑{ val := p, property := hp } -ᵥ p - v +ᵥ ↑{ val := p, property := hp } = -v +ᵥ p
[PROOFSTEP]
simp
