ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b c : α<GOAL>(a = if P then b else c) ↔ P ∧ a = b ∨ ¬P ∧ a = c
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>dite P A B = c ↔ (∀ (h : P), A h = c) ∧ ∀ (h : ¬P), B h = c
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b c : α<GOAL>(if P then a else b) = c ↔ (P → a = c) ∧ (¬P → b = c)
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a : α<VAR>B : ¬P → α<GOAL>dite P (fun x => a) B ≠ a ↔ ∃ h, a ≠ B h
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>b : α<VAR>A : P → α<GOAL>(dite P A fun x => b) ≠ b ↔ ∃ h, A h ≠ b
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<GOAL>(if P then a else b) ≠ a ↔ ¬P ∧ a ≠ b
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<GOAL>(if P then a else b) ≠ b ↔ P ∧ a ≠ b
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a : α<VAR>B : ¬P → α<VAR>h : ∀ (h : ¬P), a ≠ B h<GOAL>dite P (fun x => a) B = a ↔ P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>b : α<VAR>A : P → α<VAR>h : ∀ (h : P), A h ≠ b<GOAL>(dite P A fun x => b) = b ↔ ¬P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<VAR>h : a ≠ b<GOAL>(if P then a else b) = a ↔ P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<VAR>h : a ≠ b<GOAL>(if P then a else b) = b ↔ ¬P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a : α<VAR>B : ¬P → α<VAR>h : ∀ (h : ¬P), a ≠ B h<GOAL>dite P (fun x => a) B ≠ a ↔ ¬P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>b : α<VAR>A : P → α<VAR>h : ∀ (h : P), A h ≠ b<GOAL>(dite P A fun x => b) ≠ b ↔ P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<VAR>h : a ≠ b<GOAL>(if P then a else b) ≠ a ↔ ¬P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<VAR>h : a ≠ b<GOAL>(if P then a else b) ≠ b ↔ P
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>A : P → α<VAR>B : ¬P → α<GOAL>(∃ h, dite P A B = A h) ∨ ∃ h, dite P A B = B h
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<GOAL>(if P then a else b) = a ∨ (if P then a else b) = b
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>f : α → β → γ<VAR>P : Prop<VAR>Decidable P<VAR>a : P → α<VAR>b : ¬P → α<VAR>c : P → β<VAR>d : ¬P → β<GOAL>f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>f : α → β → γ<VAR>P : Prop<VAR>Decidable P<VAR>a b : α<VAR>c d : β<GOAL>f (if P then a else b) (if P then c else d) = if P then f a c else f b d
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P : Prop<VAR>Decidable P<VAR>f : P → (a : α) → σ a<VAR>g : ¬P → (a : α) → σ a<VAR>a : α<GOAL>dite P f g a = if h : P then f h a else g h a
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P : Prop<VAR>Decidable P<VAR>f g : (a : α) → σ a<VAR>a : α<GOAL>(if P then f else g) a = if P then f a else g a
<VAR>α : Sort u_1<VAR>P Q : Prop<VAR>Decidable P<VAR>Decidable Q<VAR>a b : α<GOAL>(if P ∧ Q then a else b) = if P then if Q then a else b else b
<VAR>α : Sort u_1<VAR>P Q : Prop<VAR>Decidable P<VAR>Decidable Q<VAR>A : P → α<VAR>B : Q → α<VAR>C : ¬P → ¬Q → α<VAR>h : P → ¬Q<GOAL>(if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q
<VAR>α : Sort u_1<VAR>P Q : Prop<VAR>Decidable P<VAR>Decidable Q<VAR>a b : α<VAR>c : α<VAR>h : P → ¬Q<GOAL>(if P then a else if Q then b else c) = if Q then b else if P then a else c
<VAR>P Q R : Prop<VAR>Decidable P<GOAL>(if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
<VAR>P : Prop<VAR>Q : P → Prop<VAR>R : ¬P → Prop<VAR>Decidable P<GOAL>dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p
<VAR>P Q R : Prop<VAR>Decidable P<GOAL>(if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
<VAR>P : Prop<VAR>Q : P → Prop<VAR>R : ¬P → Prop<VAR>Decidable P<GOAL>dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>ne : a ≠ b<GOAL>¬(a == b) = true
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<GOAL>(a == b) = decide (a = b)
<VAR>α : Type u_1<VAR>inst1 inst2 : BEq α<VAR>h : ∀ (x y : α), (x == y) = (x == y)<GOAL>inst1 = inst2
<VAR>α : Type u_1<VAR>inst1 inst2 : BEq α<VAR>LawfulBEq α<VAR>LawfulBEq α<GOAL>inst1 = inst2
<VAR>n m a : ℕ<VAR>h : n ≤ m<VAR>ha : m - n ∣ a<GOAL>(n * a + 1).Coprime (m * a + 1)
<VAR>m : ℕ<VAR>a : Fin m → ℕ<GOAL>Pairwise (Nat.Coprime on Nat.coprimes a)
<VAR>l : List ℕ<VAR>i : Fin l.length<GOAL>(Nat.unbeta l).beta ↑i = l.get i
<VAR>α : Type u_1<GOAL>RegularExpression.zero = 0
<VAR>α : Type u_1<GOAL>RegularExpression.epsilon = 1
<VAR>α : Type u_1<VAR>P Q : RegularExpression α<GOAL>P.plus Q = P + Q
<VAR>α : Type u_1<VAR>P Q : RegularExpression α<GOAL>P.comp Q = P * Q
<VAR>α : Type u_1<GOAL>RegularExpression.matches' 0 = 0
<VAR>α : Type u_1<GOAL>RegularExpression.matches' 1 = 1
<VAR>α : Type u_1<VAR>a : α<GOAL>(RegularExpression.char a).matches' = {[a]}
<VAR>α : Type u_1<VAR>P Q : RegularExpression α<GOAL>(P + Q).matches' = P.matches' + Q.matches'
<VAR>α : Type u_1<VAR>P Q : RegularExpression α<GOAL>(P * Q).matches' = P.matches' * Q.matches'
<VAR>α : Type u_1<VAR>P : RegularExpression α<VAR>n : ℕ<GOAL>(P ^ n).matches' = P.matches' ^ n
<VAR>α : Type u_1<VAR>P : RegularExpression α<GOAL>P.star.matches' = P.matches'∗
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>a : α<GOAL>RegularExpression.deriv 0 a = 0
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>a : α<GOAL>RegularExpression.deriv 1 a = 0
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>a : α<GOAL>(RegularExpression.char a).deriv a = 1
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>a b : α<VAR>h : a ≠ b<GOAL>(RegularExpression.char a).deriv b = 0
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>P Q : RegularExpression α<VAR>a : α<GOAL>(P + Q).deriv a = P.deriv a + Q.deriv a
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>P : RegularExpression α<VAR>a : α<GOAL>P.star.deriv a = P.deriv a * P.star
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>x : List α<GOAL>RegularExpression.rmatch 0 x = false
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>x : List α<GOAL>RegularExpression.rmatch 1 x = true ↔ x = []
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>a : α<VAR>x : List α<GOAL>(RegularExpression.char a).rmatch x = true ↔ x = [a]
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>P Q : RegularExpression α<VAR>x : List α<GOAL>(P + Q).rmatch x = true ↔ P.rmatch x = true ∨ Q.rmatch x = true
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>P Q : RegularExpression α<VAR>x : List α<GOAL>(P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>P : RegularExpression α<VAR>x : List α<GOAL>P.star.rmatch x = true ↔ ∃ S, x = S.join ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
<VAR>α : Type u_1<VAR>dec : DecidableEq α<VAR>P : RegularExpression α<VAR>x : List α<GOAL>P.rmatch x = true ↔ x ∈ P.matches'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>P : RegularExpression α<VAR>n : ℕ<GOAL>RegularExpression.map f (P ^ n) = RegularExpression.map f P ^ n
<VAR>α : Type u_1<VAR>P : RegularExpression α<GOAL>RegularExpression.map id P = P
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>P : RegularExpression α<GOAL>RegularExpression.map g (RegularExpression.map f P) = RegularExpression.map (g ∘ f) P
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>P : RegularExpression α<GOAL>(RegularExpression.map f P).matches' = (Language.map f) P.matches'
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableEq α<VAR>IsIrrefl α r<GOAL>Relation.CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) ⇑Multiset.toFinsupp
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Multiset α<VAR>x : α<VAR>h : ∀ x' ∈ s, r x' x<GOAL>Relation.CutExpand r s {x}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x' x : α<VAR>h : r x' x<GOAL>Relation.CutExpand r {x'} {x}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>t u : Multiset α<VAR>s : Multiset α<GOAL>Relation.CutExpand r (s + t) (s + u) ↔ Relation.CutExpand r t u
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s' s : Multiset α<VAR>t : Multiset α<GOAL>Relation.CutExpand r (s' + t) (s + t) ↔ Relation.CutExpand r s' s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableEq α<VAR>IsIrrefl α r<VAR>s' s : Multiset α<GOAL>Relation.CutExpand r s' s ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>s : Multiset α<GOAL>¬Relation.CutExpand r s 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : α<GOAL>Relation.CutExpand r 0 {x}
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Relation.Fibration (Prod.GameAdd (Relation.CutExpand r) (Relation.CutExpand r)) (Relation.CutExpand r) fun s => s.1 + s.2
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>p : α → Prop<VAR>h : ∀ {a' a : α}, r a' a → p a → p a'<VAR>s' s : Multiset α<GOAL>Relation.CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a a₁ a₂ : α<VAR>h₁ : r a₁ a<VAR>h₂ : r a₂ a<GOAL>Relation.CutExpand r {a₁, a₂} {a}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a' a b : α<VAR>hr : r a' a<GOAL>Relation.CutExpand r {a', b} {a, b}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b' b : α<VAR>hr : r b' b<GOAL>Relation.CutExpand r {a, b'} {a, b}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a a₁ a₂ b : α<VAR>h₁ : r a₁ a<VAR>h₂ : r a₂ a<GOAL>Relation.CutExpand r {a₁, a₂, b} {a, b}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>s : Multiset α<VAR>hs : ∀ a ∈ s, Acc (Relation.CutExpand r) {a}<GOAL>Acc (Relation.CutExpand r) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsIrrefl α r<VAR>a : α<VAR>hacc : Acc r a<GOAL>Acc (Relation.CutExpand r) {a}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hr : WellFounded r<GOAL>WellFounded (Relation.CutExpand r)
<VAR>α : Sort u_4<VAR>self : IsEmpty α<GOAL>α → False
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>IsEmpty β<VAR>f : α → β<GOAL>IsEmpty α
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>IsEmpty α<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>IsEmpty β
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>hp : ∀ (a : α), ¬p a<GOAL>IsEmpty (Subtype p)
<VAR>α : Sort u_1<GOAL>IsEmpty α ↔ α → False
<VAR>p : Prop<GOAL>IsEmpty p ↔ ¬p
<VAR>α : Sort u_1<VAR>IsEmpty α<VAR>p : α → Prop<GOAL>(∀ (a : α), p a) ↔ True
<VAR>α : Sort u_1<VAR>IsEmpty α<VAR>p : α → Prop<GOAL>(∃ a, p a) ↔ False
<VAR>α : Sort u_1<GOAL>¬Nonempty α ↔ IsEmpty α
<VAR>α : Sort u_1<GOAL>¬IsEmpty α ↔ Nonempty α
<VAR>α : Sort u_1<VAR>π : α → Sort u_4<GOAL>IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β
<VAR>α : Type u_5<VAR>E : α → Type u_4<GOAL>IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)
<VAR>α : Sort u_5<VAR>E : α → Sort u_4<GOAL>IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)
<VAR>α : Sort u_1<VAR>p : α → Prop<GOAL>IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x
<VAR>α : Type u_4<VAR>β : Type u_5<GOAL>IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>IsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β
<VAR>α : Type u_4<VAR>β : Type u_5<GOAL>IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
<VAR>α : Sort u_4<VAR>β : Sort u_5<GOAL>IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β
<VAR>α : Type u_4<GOAL>IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α
<VAR>α : Sort u_4<GOAL>IsEmpty (PLift α) ↔ IsEmpty α
<VAR>α : Sort u_4<VAR>IsEmpty α<VAR>r : α → α → Prop<GOAL>WellFounded r
<VAR>α : Sort u_1<GOAL>IsEmpty α ∨ Nonempty α
<VAR>α : Sort u_1<VAR>h : Nonempty α<GOAL>¬IsEmpty α
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>IsEmpty α<VAR>f : α → β<VAR>g : α → γ<VAR>h : β → γ<GOAL>Function.extend f g h = h
<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>x : P × P × P<VAR>hx12 : x.1 ≠ x.2.1<VAR>hx32 : x.2.2 ≠ x.2.1<GOAL>ContinuousAt (fun y => ∡ y.1 y.2.1 y.2.2) x
<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<GOAL>∡ p₁ p₁ p₂ = 0
<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<GOAL>∡ p₁ p₂ p₂ = 0
<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<GOAL>∡ p₁ p₂ p₁ = 0
<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₃ ≠ 0<GOAL>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₃ ≠ 0<GOAL>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₃ ≠ 0<GOAL>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₃ = ↑π<GOAL>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₃ = ↑π<GOAL>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₃ = ↑π<GOAL>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₂
<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₂
<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₃
<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₂
<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₂
<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₃
<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₃).sign ≠ 0<GOAL>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₃).sign ≠ 0<GOAL>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₃).sign ≠ 0<GOAL>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₃).sign = 1<GOAL>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₃).sign = 1<GOAL>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₃).sign = 1<GOAL>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₃).sign = -1<GOAL>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₃).sign = -1<GOAL>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₃).sign = -1<GOAL>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<GOAL>∡ p₃ p₂ p₁ = -∡ p₁ 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<GOAL>∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₁ = 0
<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<GOAL>∡ p₁ p₂ p₃ = 0 ↔ ∡ p₃ p₂ p₁ = 0
<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<GOAL>∡ p₁ p₂ p₃ = ↑π ↔ ∡ p₃ 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<GOAL>∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ ↑π ↔ AffineIndependent ℝ ![p₁, 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<GOAL>∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = ↑π ↔ Collinear ℝ {p₁, 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<GOAL>(∡ p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ {p₁, 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₄ p₅ p₆ : P<VAR>h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆<GOAL>AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, 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₄ p₅ p₆ : P<VAR>h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆<GOAL>Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₄, 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₄ p₅ p₆ : P<VAR>h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}<VAR>h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ 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₄ p₅ p₆ : P<VAR>h₁₂₄₅ : affineSpan ℝ {p₁, p₂} ∥ affineSpan ℝ {p₄, p₅}<VAR>h₃₂₆₅ : affineSpan ℝ {p₃, p₂} ∥ affineSpan ℝ {p₆, p₅}<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ 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₃ : P<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<VAR>hp₃ : p₃ ≠ p<GOAL>∡ p₁ p p₂ + ∡ p₂ p p₃ = ∡ p₁ 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₃ : P<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<VAR>hp₃ : p₃ ≠ p<GOAL>∡ p₂ p p₃ + ∡ p₁ p p₂ = ∡ p₁ 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₃ : P<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<VAR>hp₃ : p₃ ≠ p<GOAL>∡ p₁ p p₃ - ∡ p₁ p p₂ = ∡ p₂ 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₃ : P<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<VAR>hp₃ : p₃ ≠ p<GOAL>∡ p₁ p p₃ - ∡ p₂ p p₃ = ∡ p₁ 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₃ : P<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<VAR>hp₃ : p₃ ≠ p<GOAL>∡ p₁ p p₂ + ∡ p₂ p p₃ + ∡ p₃ p p₁ = 0
<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 : dist p₁ p₂ = dist p₁ p₃<GOAL>∡ p₁ p₂ p₃ = ∡ p₂ 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>hn : p₂ ≠ p₃<VAR>h : dist p₁ p₂ = dist p₁ p₃<GOAL>∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ 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 : dist p₁ p₂ = dist p₁ p₃<GOAL>|(∡ p₁ p₂ p₃).toReal| < π / 2