ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<VAR>x y : α<GOAL>f x = y ↔ x = f y
<VAR>α : Sort u_1<VAR>f : α → α<GOAL>(Symmetric fun x x_1 => f x = x_1) ↔ Function.Involutive f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β → γ<VAR>hf : Function.Injective2 f<VAR>b : β<GOAL>Function.Injective fun a => f a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β → γ<VAR>hf : Function.Injective2 f<VAR>a : α<GOAL>Function.Injective (f a)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>γ : Type u_6<VAR>f : α → β → γ<VAR>hf : Function.Injective2 f<GOAL>Function.Injective (Function.uncurry f)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β → γ<VAR>hf : Function.Injective2 f<VAR>Nonempty β<GOAL>Function.Injective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β → γ<VAR>hf : Function.Injective2 f<VAR>Nonempty α<GOAL>Function.Injective fun b a => f a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β → γ<VAR>hf : Function.Injective2 f<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>f a₁ b₁ = f a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>p : Prop<VAR>α : Sort u_1<VAR>Nonempty α<VAR>f : p → α<VAR>a : p<GOAL>Function.sometimes f = f a
<VAR>p : Prop<VAR>α : Sort u_1<VAR>Nonempty α<VAR>P : α → Prop<VAR>f : p → α<VAR>a : p<VAR>h : P (f a)<GOAL>P (Function.sometimes f)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>r : α → β → Prop<GOAL>(∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>hr : Symmetric r<GOAL>(∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ r = fun x x_1 => f x = x_1
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>hr : Symmetric r<GOAL>(∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b
<VAR>α : Sort u_1<VAR>C : α → Sort u_3<VAR>a a' : α<VAR>h : a = a'<GOAL>Function.Bijective fun x => h ▸ x
<VAR>α β : Sort u_3<VAR>h : α = β<GOAL>Function.Bijective h.mp
<VAR>α β : Sort u_3<VAR>h : α = β<GOAL>Function.Bijective h.mpr
<VAR>α β : Sort u_3<VAR>h : α = β<GOAL>Function.Bijective (cast h)
<VAR>α : Sort u_1<VAR>a a' : α<VAR>h : a = a'<VAR>C : α → Type u_3<VAR>x y : C a<GOAL>h ▸ x = h ▸ y ↔ x = y
<VAR>α β : Type u<VAR>h : α = β<VAR>x y : α<GOAL>cast h x = cast h y ↔ x = y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : β → Sort v<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<VAR>C : (a : α) → γ (f a)<VAR>a : α<GOAL>⋯ ▸ C (g (f a)) = C a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : β → Sort v<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<VAR>C : (a : α) → γ (f a)<VAR>a : α<GOAL>Eq.recOn ⋯ (C (g (f a))) = C a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : β → Sort v<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<VAR>C : (a : α) → γ (f a)<VAR>a : α<GOAL>cast ⋯ (C (g (f a))) = C a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>op : α → α → β<VAR>IsSymmOp α β op<GOAL>flip op = op
<VAR>α : Sort u<VAR>β : Sort v<VAR>r : β → β → Prop<VAR>f : α → β<VAR>h : Equivalence r<GOAL>Equivalence (InvImage r f)
<VAR>α : Type v<VAR>s t : Set α<VAR>hts : t ⊆ s<VAR>Small.{u, v} ↑s<GOAL>Small.{u, v} ↑t
<VAR>α : Type w<VAR>hα : Small.{u, w} α<VAR>h : UnivLE.{u, v}<GOAL>Small.{v, w} α
<VAR>UnivLE.{u, v}<VAR>UnivLE.{v, w}<GOAL>UnivLE.{u, w}
<VAR>α : Type u_1<VAR>Zero α<VAR>Small.{u_2, u_1} α<GOAL>(equivShrink α).symm 0 = 0
<VAR>α : Type u_1<VAR>One α<VAR>Small.{u_2, u_1} α<GOAL>(equivShrink α).symm 1 = 1
<VAR>α : Type u_1<VAR>Add α<VAR>Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (x + y) = (equivShrink α).symm x + (equivShrink α).symm y
<VAR>α : Type u_1<VAR>Add α<VAR>Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x + y) = (equivShrink α) x + (equivShrink α) y
<VAR>α : Type u_1<VAR>Mul α<VAR>Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (x * y) = (equivShrink α).symm x * (equivShrink α).symm y
<VAR>α : Type u_1<VAR>Mul α<VAR>Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x * y) = (equivShrink α) x * (equivShrink α) y
<VAR>α : Type u_1<VAR>Sub α<VAR>Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (x - y) = (equivShrink α).symm x - (equivShrink α).symm y
<VAR>α : Type u_1<VAR>Sub α<VAR>Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x - y) = (equivShrink α) x - (equivShrink α) y
<VAR>α : Type u_1<VAR>Div α<VAR>Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y
<VAR>α : Type u_1<VAR>Div α<VAR>Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x / y) = (equivShrink α) x / (equivShrink α) y
<VAR>α : Type u_1<VAR>Neg α<VAR>Small.{u_2, u_1} α<VAR>x : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (-x) = -(equivShrink α).symm x
<VAR>α : Type u_1<VAR>Neg α<VAR>Small.{u_2, u_1} α<VAR>x : α<GOAL>(equivShrink α) (-x) = -(equivShrink α) x
<VAR>α : Type u_1<VAR>Inv α<VAR>Small.{u_2, u_1} α<VAR>x : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹
<VAR>α : Type u_1<VAR>Inv α<VAR>Small.{u_2, u_1} α<VAR>x : α<GOAL>(equivShrink α) x⁻¹ = ((equivShrink α) x)⁻¹
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V × V<VAR>hx1 : x.1 ≠ 0<VAR>hx2 : x.2 ≠ 0<GOAL>ContinuousAt (fun y => o.oangle y.1 y.2) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>o.oangle 0 x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>o.oangle x 0 = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>o.oangle x x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y ≠ 0<GOAL>x ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y ≠ 0<GOAL>y ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y ≠ 0<GOAL>x ≠ y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑π<GOAL>x ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑π<GOAL>y ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑π<GOAL>x ≠ y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>x ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>y ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>x ≠ y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(-π / 2)<GOAL>x ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(-π / 2)<GOAL>y ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(-π / 2)<GOAL>x ≠ y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign ≠ 0<GOAL>x ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign ≠ 0<GOAL>y ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign ≠ 0<GOAL>x ≠ y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = 1<GOAL>x ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = 1<GOAL>y ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = 1<GOAL>x ≠ y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = -1<GOAL>x ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = -1<GOAL>y ≠ 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = -1<GOAL>x ≠ y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle y x = -o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y + o.oangle y x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>o.oangle (-x) y = o.oangle x y + ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>o.oangle x (-y) = o.oangle x y + ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>2 • o.oangle (-x) y = 2 • o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>2 • o.oangle x (-y) = 2 • o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle (-x) (-y) = o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle (-x) y = o.oangle x (-y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<GOAL>o.oangle (-x) x = ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<GOAL>o.oangle x (-x) = ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>2 • o.oangle (-x) x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>2 • o.oangle x (-x) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle (-x) y + o.oangle (-y) x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x (-y) + o.oangle y (-x) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>o.oangle (r • x) y = o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>o.oangle x (r • y) = o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : r < 0<GOAL>o.oangle (r • x) y = o.oangle (-x) y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : r < 0<GOAL>o.oangle x (r • y) = o.oangle x (-y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>o.oangle (r • x) x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>o.oangle x (r • x) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r₁ r₂ : ℝ<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : 0 ≤ r₂<GOAL>o.oangle (r₁ • x) (r₂ • x) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>2 • o.oangle (r • x) y = 2 • o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>2 • o.oangle x (r • y) = 2 • o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>2 • o.oangle (r • x) x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>2 • o.oangle x (r • x) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r₁ r₂ : ℝ<GOAL>2 • o.oangle (r₁ • x) (r₂ • x) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>z : V<VAR>h : Submodule.span ℝ {x} = Submodule.span ℝ {y}<GOAL>2 • o.oangle x z = 2 • o.oangle y z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>y z : V<VAR>h : Submodule.span ℝ {y} = Submodule.span ℝ {z}<GOAL>2 • o.oangle x y = 2 • o.oangle x z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>w x y z : V<VAR>hwx : Submodule.span ℝ {w} = Submodule.span ℝ {x}<VAR>hyz : Submodule.span ℝ {y} = Submodule.span ℝ {z}<GOAL>2 • o.oangle w y = 2 • o.oangle x z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ↔ o.oangle y x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ↔ SameRay ℝ x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = ↑π ↔ o.oangle y x = ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ∨ o.oangle x y = ↑π ↔ ¬LinearIndependent ℝ ![x, y]
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ∨ o.oangle x y = ↑π ↔ x = 0 ∨ ∃ r, y = r • x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y ≠ 0 ∧ o.oangle x y ≠ ↑π ↔ LinearIndependent ℝ ![x, y]
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<GOAL>x = y ↔ o.oangle x y = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = 0<GOAL>x = y ↔ ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x y + o.oangle y z = o.oangle x z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle y z + o.oangle x y = o.oangle x z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x z - o.oangle x y = o.oangle y z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x z - o.oangle y z = o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x y + o.oangle y z + o.oangle z x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = ↑π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : ‖x‖ = ‖y‖<GOAL>o.oangle x (x - y) = o.oangle (y - x) y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hn : x ≠ y<VAR>h : ‖x‖ = ‖y‖<GOAL>o.oangle y x = ↑π - 2 • o.oangle (y - x) y
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup V'<VAR>InnerProductSpace ℝ V<VAR>InnerProductSpace ℝ V'<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Fact (FiniteDimensional.finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V'<VAR>f : V ≃ₗᵢ[ℝ] V'<GOAL>((Orientation.map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)
<VAR>w z : ℂ<GOAL>Complex.orientation.oangle w z = ↑((starRingEnd ℂ) w * z).arg
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>f : V ≃ₗᵢ[ℝ] ℂ<VAR>hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : V<GOAL>o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(-o).oangle x y = -o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.oangle x y).cos = ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.oangle x y).cos = Real.cos (InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>o.oangle x y = ↑(InnerProductGeometry.angle x y) ∨ o.oangle x y = -↑(InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = 0<GOAL>x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>w x y z : V<VAR>h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z<VAR>hs : (o.oangle w x).sign = (o.oangle y z).sign<GOAL>o.oangle w x = o.oangle y z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>w x y z : V<VAR>hw : w ≠ 0<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<VAR>hs : (o.oangle w x).sign = (o.oangle y z).sign<GOAL>InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = 1<GOAL>o.oangle x y = ↑(InnerProductGeometry.angle x y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (o.oangle x y).sign = -1<GOAL>o.oangle x y = -↑(InnerProductGeometry.angle x y)