V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
⊢ ContinuousAt (fun y => ∠ y.fst y.snd.fst y.snd.snd) x
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
⊢ ContinuousAt (fun y => ∠ y.fst y.snd.fst y.snd.snd) x
let f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
⊢ ContinuousAt (fun y => ∠ y.fst y.snd.fst y.snd.snd) x
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
⊢ ContinuousAt (fun y => ∠ y.fst y.snd.fst y.snd.snd) x
have hf1 : (f x).1 ≠ 0 := by simp [hx12]
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
hf2 : (f x).snd ≠ 0
⊢ ContinuousAt (fun y => ∠ y.fst y.snd.fst y.snd.snd) x
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
⊢ ContinuousAt (fun y => ∠ y.fst y.snd.fst y.snd.snd) x
have hf2 : (f x).2 ≠ 0 := by simp [hx32]
no goals
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
hf2 : (f x).snd ≠ 0
⊢ ContinuousAt (fun y => ∠ y.fst y.snd.fst y.snd.snd) x
exact (InnerProductGeometry.continuousAt_angle hf1 hf2).comp
  ((continuous_fst.vsub continuous_snd.fst).prod_mk
    (continuous_snd.snd.vsub continuous_snd.fst)).continuousAt
no goals
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
⊢ (f x).fst ≠ 0
simp [hx12]
no goals
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P × P × P
hx12 : x.fst ≠ x.snd.fst
hx32 : x.snd.snd ≠ x.snd.fst
f : P × P × P → V × V := fun y => (y.fst -ᵥ y.snd.fst, y.snd.snd -ᵥ y.snd.fst)
hf1 : (f x).fst ≠ 0
⊢ (f x).snd ≠ 0
simp [hx32]