ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>n : ℕ<GOAL>(int.divByNat n) ↑n = 0
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<GOAL>(int.divByNat 0) ↑0 = 0
<VAR>R : Type uR<VAR>inst✝³ : CommRing R<VAR>A : Type uA<VAR>inst✝² : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝¹ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝ : AddCommGroup B<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>(int.divByNat n) ↑n = 0
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<VAR>h₁ : a < c<VAR>h₂ : b < c<VAR>h : a ≤ b<GOAL>max a b < c
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<VAR>h₁ : a < c<VAR>h₂ : b < c<VAR>h : a > b<GOAL>max a b < c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Zero β<VAR>inst✝² : SMulZeroClass α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>inst✝¹ : Zero α<VAR>inst✝ : NoZeroSMulDivisors α β<VAR>ha : a ≠ 0<GOAL>0 ∈ a • t ↔ 0 ∈ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Zero β<VAR>inst✝² : SMulZeroClass α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>inst✝¹ : Zero α<VAR>inst✝ : NoZeroSMulDivisors α β<VAR>ha : a ≠ 0<GOAL>0 ∈ a • t → 0 ∈ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Zero β<VAR>inst✝² : SMulZeroClass α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>inst✝¹ : Zero α<VAR>inst✝ : NoZeroSMulDivisors α β<VAR>ha : a ≠ 0<VAR>b : β<VAR>hb : b ∈ t<VAR>h : (fun x => a • x) b = 0<GOAL>0 ∈ t
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<GOAL>IsClosed (range inr)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<GOAL>IsOpen (range inl)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : CommRing B<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra A K<VAR>inst✝¹² : Algebra B L<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : IsScalarTower A B L<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsFractionRing A K<VAR>inst✝⁴ : IsIntegralClosure B A L<VAR>inst✝³ : IsFractionRing B L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsDomain B<VAR>I J : Submodule B L<GOAL>I ≤ Jᵛ ↔ map (↑A (Algebra.trace K L)) (restrictScalars A (I * J)) ≤ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : CommRing B<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra A K<VAR>inst✝¹² : Algebra B L<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : IsScalarTower A B L<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsFractionRing A K<VAR>inst✝⁴ : IsIntegralClosure B A L<VAR>inst✝³ : IsFractionRing B L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsDomain B<VAR>I J : Submodule B L<GOAL>I ≤ Jᵛ ↔ ∀ m ∈ restrictScalars A I, ∀ n ∈ restrictScalars A J, m * n ∈ comap (↑A (Algebra.trace K L)) 1
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : StarMul A<VAR>a : A<VAR>u : ↥(unitary A)<GOAL>spectrum R (star ↑u * a * ↑u) = spectrum R a
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<GOAL>a - b ≤ a - c ↔ c ≤ b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<GOAL>a - b ≤ a - c → c ≤ b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<GOAL>a + c ≤ a + b → c ≤ b
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁶ : Semiring R✝<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R✝ M<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R✝ M'<VAR>b b₁ : Basis ι✝ R✝ M<VAR>i✝ : ι✝<VAR>c : R✝<VAR>x✝ : M<VAR>ι : Type u_10<VAR>R : Type u_11<VAR>inst✝¹ : Unique ι<VAR>inst✝ : Semiring R<VAR>x : R<VAR>i : ι<GOAL>((Basis.singleton ι R).repr x) i = x
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.39620, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.39627, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.39620, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.39627, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)<GOAL>∀ (j : J), IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.39620, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.39627, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)<VAR>j : J<GOAL>IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.39620, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.39627, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)<VAR>j : J<GOAL>IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.39620, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.39627, u_2} D<VAR>F G : J ⥤ C<VAR>α : F ⟶ G<VAR>inst✝ : IsIso α<VAR>c : Cocone G<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α' : F' ⟶ F<VAR>f : c'.pt ⟶ ((Cocones.precompose α).obj c).pt<VAR>e : α' ≫ ((Cocones.precompose α).obj c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α'<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocones.precompose α).obj c).ι.app j)<VAR>j : J<GOAL>IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) (f ≫ 𝟙 ((Cocones.precompose α).obj c).pt) (c.ι.app j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hst : ∀ (x : α), ∃ y ∈ s, x ≤ y<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>⨆ x ∈ s, μ (Iic x) = μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hst : ∀ (x : α), ∃ y ∈ s, x ≤ y<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>μ (⋃ i ∈ s, Iic i) = μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hst : ∀ (x : α), ∃ y ∈ s, x ≤ y<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>DirectedOn ((fun x x_1 => x ⊆ x_1) on Iic) s
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : KernelFork f<VAR>G : C ⥤ D<VAR>inst✝ : G.PreservesZeroMorphisms<GOAL>G.map (Fork.ι c) ≫ G.map f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddGroup α<VAR>h : Periodic f c<VAR>x : α<GOAL>f (x - c) = f x
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a : R<GOAL>a % 0 = a
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a / b = b⁻¹ * a
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>inst✝ : DecidableEq K<VAR>i : ℕ<GOAL>∑ x : Kˣ, ↑x ^ i = if q - 1 ∣ i then -1 else 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>inst✝ : DecidableEq K<VAR>i : ℕ<VAR>φ : Kˣ →* K := { toFun := fun x => ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }<GOAL>∑ x : Kˣ, ↑x ^ i = if q - 1 ∣ i then -1 else 0
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>c * b ≤ a * b⁻¹ * b ↔ c * b ≤ a
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>a : 𝕜'<VAR>ha : a ≠ 0<GOAL>logDeriv (fun z => f z * a) x = logDeriv f x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫_ℝ = 0<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hpt : p -ᵥ p₁ = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hpt : p -ᵥ p₁ = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>hop : t₁ = 0<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ p : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hpc₁ : dist p c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>hpc₂ : dist p c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hpt : p = t₂ • (p₂ -ᵥ p₁) +ᵥ p₁<VAR>hop : t₁ = 0<GOAL>p = p₁ ∨ p = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hop : t₁ = 0<VAR>hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s<VAR>hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁<VAR>hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂<GOAL>t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hop : t₁ = 0<VAR>hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s<VAR>hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁<VAR>hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂<VAR>hp' : p₂ -ᵥ p₁ ≠ 0<GOAL>t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hop : t₁ = 0<VAR>hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s<VAR>hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁<VAR>hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂<VAR>hp' : p₂ -ᵥ p₁ ≠ 0<VAR>hp₂ : dist (1 • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁<GOAL>t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hop : t₁ = 0<VAR>hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s<VAR>hpc₁ : t₂ = 0 ∨ t₂ = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫_ℝ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ<VAR>hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂<VAR>hp' : p₂ -ᵥ p₁ ≠ 0<VAR>hp₂ : 1 = 0 ∨ 1 = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫_ℝ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ<GOAL>t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hop : t₁ = 0<VAR>hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s<VAR>hpc₁ : t₂ = 0 ∨ t₂ = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫_ℝ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ<VAR>hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂<VAR>hp' : p₂ -ᵥ p₁ ≠ 0<VAR>hp₂ : 1 = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫_ℝ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ<GOAL>t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = 2<VAR>c₁ c₂ p₁ p₂ : P<VAR>hc₁s : c₁ ∈ s<VAR>hc₂s : c₂ ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>r₁ r₂ : ℝ<VAR>hc : c₁ ≠ c₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁c₁ : dist p₁ c₁ = r₁<VAR>hp₂c₁ : dist p₂ c₁ = r₁<VAR>hp₁c₂ : dist p₁ c₂ = r₂<VAR>hp₂c₂ : dist p₂ c₂ = r₂<VAR>ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫_ℝ = 0<VAR>b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]<VAR>hb : LinearIndependent ℝ b<VAR>hbs : Submodule.span ℝ (Set.range b) = s.direction<VAR>hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)<VAR>t₁ t₂ : ℝ<VAR>hop : t₁ = 0<VAR>hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s<VAR>hpc₁ : t₂ = 0 ∨ t₂ = 1<VAR>hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂<VAR>hp' : p₂ -ᵥ p₁ ≠ 0<VAR>hp₂ : 1 = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫_ℝ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ<GOAL>t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>hs : Balanced ℝ s<VAR>x : E<VAR>hx : x ∈ s<VAR>a : ℝ<VAR>ha₀ : 0 ≤ a<VAR>ha₁ : a ≤ 1<GOAL>‖a‖ ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Preorder α<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : Monotone g<GOAL>Monotone fun x => map f (g x)