ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>p : β → β → Prop<VAR>a b : α<VAR>f : α → β<VAR>h : ∀ (a b : α), r a b → Relation.TransGen p (f a) (f b)<VAR>hab : Relation.TransGen r a b<GOAL>Relation.TransGen p (f a) (f b)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → α → Prop<GOAL>(∀ (a b : α), r a b → Relation.TransGen p a b) → Relation.TransGen r a b → Relation.TransGen p a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>P : α → Prop<VAR>dc : ∀ {a b : α}, r a b → P b → P a<VAR>a b : α<VAR>h : Relation.TransGen r a b<GOAL>P b → P a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → α → Prop<GOAL>(∀ (a b : α), r a b → p a b) → Relation.TransGen r a b → Relation.TransGen p a b
<VAR>α : Type u_1<VAR>r r' : α → α → Prop<VAR>hr' : Transitive r'<VAR>h : ∀ (x y : α), r x y → r' x y<VAR>x y : α<VAR>hxy : Relation.TransGen r x y<GOAL>r' x y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Relation.TransGen r b a<GOAL>Relation.TransGen (Function.swap r) a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>Relation.TransGen (Function.swap r) a b ↔ Relation.TransGen r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : ∀ (b : α), ¬r a b<GOAL>Relation.ReflTransGen r a b ↔ b = a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>Relation.ReflTransGen r a b ↔ b = a ∨ Relation.TransGen r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>p : β → β → Prop<VAR>a b : α<VAR>f : α → β<VAR>h : ∀ (a b : α), r a b → p (f a) (f b)<VAR>hab : Relation.ReflTransGen r a b<GOAL>Relation.ReflTransGen p (f a) (f b)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → α → Prop<GOAL>(∀ (a b : α), r a b → p a b) → Relation.ReflTransGen r a b → Relation.ReflTransGen p a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>refl : Reflexive r<VAR>trans : Transitive r<GOAL>Relation.ReflTransGen r = r
<VAR>α : Type u_1<VAR>r r' : α → α → Prop<VAR>hr₁ : Reflexive r'<VAR>hr₂ : Transitive r'<VAR>h : ∀ (x y : α), r x y → r' x y<VAR>x y : α<VAR>hxy : Relation.ReflTransGen r x y<GOAL>r' x y
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Reflexive (Relation.ReflTransGen r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Transitive (Relation.ReflTransGen r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Relation.ReflTransGen (Relation.ReflTransGen r) = Relation.ReflTransGen r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>p : β → β → Prop<VAR>a b : α<VAR>f : α → β<VAR>h : ∀ (a b : α), r a b → Relation.ReflTransGen p (f a) (f b)<VAR>hab : Relation.ReflTransGen r a b<GOAL>Relation.ReflTransGen p (f a) (f b)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → α → Prop<GOAL>(∀ (a b : α), r a b → Relation.ReflTransGen p a b) → Relation.ReflTransGen r a b → Relation.ReflTransGen p a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Relation.ReflTransGen r b a<GOAL>Relation.ReflTransGen (Function.swap r) a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>Relation.ReflTransGen (Function.swap r) a b ↔ Relation.ReflTransGen r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Relation.ReflGen (Relation.TransGen r) = Relation.ReflTransGen r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Relation.TransGen (Relation.ReflGen r) = Relation.ReflTransGen r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Relation.ReflTransGen (Relation.ReflGen r) = Relation.ReflTransGen r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Relation.ReflTransGen (Relation.TransGen r) = Relation.ReflTransGen r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hr : Reflexive r<GOAL>Relation.ReflTransGen r = Relation.TransGen r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hr : Transitive r<GOAL>Relation.ReflTransGen r = Relation.ReflGen r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>h : ∀ (a b c : α), r a b → r a c → ∃ d, Relation.ReflGen r b d ∧ Relation.ReflTransGen r c d<VAR>hab : Relation.ReflTransGen r a b<VAR>hac : Relation.ReflTransGen r a c<GOAL>Relation.Join (Relation.ReflTransGen r) b c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Reflexive r<VAR>hab : r a b<GOAL>Relation.Join r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Symmetric (Relation.Join r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Reflexive r<GOAL>Reflexive (Relation.Join r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ht : Transitive r<VAR>h : ∀ (a b c : α), r a b → r a c → Relation.Join r b c<GOAL>Transitive (Relation.Join r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hr : Reflexive r<VAR>ht : Transitive r<VAR>h : ∀ (a b c : α), r a b → r a c → Relation.Join r b c<GOAL>Equivalence (Relation.Join r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : ∀ (a b c : α), r a b → r a c → ∃ d, Relation.ReflGen r b d ∧ Relation.ReflTransGen r c d<GOAL>Equivalence (Relation.Join (Relation.ReflTransGen r))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>r' : α → α → Prop<VAR>hr : Equivalence r<VAR>h : ∀ (a b : α), r' a b → r a b<GOAL>Relation.Join r' a b → r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>r' : α → α → Prop<VAR>hr : Reflexive r<VAR>ht : Transitive r<VAR>h : ∀ (a b : α), r' a b → r a b<VAR>h' : Relation.ReflTransGen r' a b<GOAL>r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>r' : α → α → Prop<VAR>hr : Equivalence r<GOAL>(∀ (a b : α), r' a b → r a b) → Relation.ReflTransGen r' a b → r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Equivalence r<GOAL>EqvGen r a b ↔ r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Equivalence r<GOAL>EqvGen r = r
<VAR>α : Type u_1<VAR>a b : α<VAR>r p : α → α → Prop<VAR>hrp : ∀ (a b : α), r a b → p a b<VAR>h : EqvGen r a b<GOAL>EqvGen p a b
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x + y) y = ↑(Real.arccos (‖y‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x + y) y = ↑(Real.arcsin (‖x‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x + y) y = ↑(Real.arctan (‖x‖ / ‖y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).cos = ‖y‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).tan = ‖x‖ / ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).cos * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).tan * ‖y‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle (x + y) y).cos = ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle (x + y) y).sin = ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle (x + y) y).tan = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x - y) x = ↑(Real.arccos (‖x‖ / ‖x - y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x - y) x = ↑(Real.arcsin (‖y‖ / ‖x - y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x - y) x = ↑(Real.arctan (‖y‖ / ‖x‖))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).cos = ‖x‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).tan = ‖x‖ / ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).tan = ‖y‖ / ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).cos * ‖x - y‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).tan * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle (x - y) x).tan = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>(o.oangle x (x + r • (o.rotation ↑(π / 2)) x)).tan = r
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>(o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x)).tan = r⁻¹
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂