ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ✝ ν : Measure α<VAR>s t : Set α<VAR>f g : α → E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : NeZero μ<VAR>c : E<GOAL>⨍ (_x : α), c ∂μ = c
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d✝ : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>d : 𝕜'<GOAL>HasDerivWithinAt (fun x => c x / d) (c' / d) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>h : ¬∃ t, IsChain r s ∧ SuperChain r s t<GOAL>s ⊆ SuccChain r s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)<GOAL>s ⊆ SuccChain r s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(univ.pi fun i => Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(univ.pi fun i => Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E<GOAL>T x₀ = ↑(T.rayleighQuotient x₀) • x₀
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E<VAR>hSA : ↑⋯.toSelfAdjoint ∈ selfAdjoint (E →L[ℝ] E) := Subtype.prop (LinearMap.IsSymmetric.restrictScalars (isSymmetric hT)).toSelfAdjoint<GOAL>T x₀ = ↑(T.rayleighQuotient x₀) • x₀
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>X₁ : C₁<VAR>a : X₂ ⟶ T.obj X₁<VAR>b : L.obj X₁ ⟶ X₃<VAR>comm : R.map a ≫ w.app X₁ ≫ B.map b = g<VAR>f : w.StructuredArrowRightwards g<GOAL>∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g✝ : R.obj X₂ ⟶ B.obj X₃<VAR>X₁ : C₁<VAR>a : X₂ ⟶ T.obj X₁<VAR>b : L.obj X₁ ⟶ X₃<VAR>comm : R.map a ≫ w.app X₁ ≫ B.map b = g✝<VAR>g : CostructuredArrow L X₃<VAR>φ : CostructuredArrow.mk g✝ ⟶ (w.costructuredArrowRightwards X₃).obj g<GOAL>∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g✝), StructuredArrow.mk φ = mk w g✝ X₁ a b comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>X₁✝ : C₁<VAR>a : X₂ ⟶ T.obj X₁✝<VAR>b✝ : L.obj X₁✝ ⟶ X₃<VAR>comm : R.map a ≫ w.app X₁✝ ≫ B.map b✝ = g<VAR>X₁ : C₁<VAR>b : L.obj X₁ ⟶ X₃<VAR>φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)<GOAL>∃ X₁_1 a b_1, ∃ (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g), StructuredArrow.mk φ = mk w g X₁_1 a b_1 comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>X₁✝ : C₁<VAR>a✝ : X₂ ⟶ T.obj X₁✝<VAR>b✝ : L.obj X₁✝ ⟶ X₃<VAR>comm : R.map a✝ ≫ w.app X₁✝ ≫ B.map b✝ = g<VAR>X₁ : C₁<VAR>b : L.obj X₁ ⟶ X₃<VAR>a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left<VAR>ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom<GOAL>∃ X₁_1 a_1 b_1, ∃ (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g), StructuredArrow.mk (CostructuredArrow.homMk a ha) = mk w g X₁_1 a_1 b_1 comm
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a✝ b c : α<VAR>m n : ℕ<VAR>a : α<VAR>h : m ≤ n<GOAL>a ^ n = a ^ m * a ^ (n - m)
<VAR>α : Type u_1<VAR>inst✝¹ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝ : UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>f✝ f : α → β<VAR>g : pkg.space → pkg'.space<VAR>hg : UniformContinuous g<VAR>h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)<VAR>a : α<GOAL>pkg.extend (fun x => (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 y t<GOAL>StarConvex 𝕜 (x + y) (s + t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>ht : StarConvex 𝕜 y t<GOAL>StarConvex 𝕜 (x + y) ((fun x => x.1 + x.2) '' s ×ˢ t)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>inst✝⁸ : MeasurableSpace ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : OrderTopology ι<VAR>inst✝⁵ : SecondCountableTopology ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝² : MetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>hf_prog : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<GOAL>Measurable (stoppedValue u τ)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>inst✝⁸ : MeasurableSpace ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : OrderTopology ι<VAR>inst✝⁵ : SecondCountableTopology ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝² : MetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>hf_prog : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => min (τ ω) i)<GOAL>Measurable (stoppedValue u τ)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>inst✝⁸ : MeasurableSpace ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : OrderTopology ι<VAR>inst✝⁵ : SecondCountableTopology ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝² : MetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>hf_prog : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => min (τ ω) i)<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>i : ι<GOAL>MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>inst✝⁸ : MeasurableSpace ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : OrderTopology ι<VAR>inst✝⁵ : SecondCountableTopology ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝² : MetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>hf_prog : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => min (τ ω) i)<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>i : ι<GOAL>stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} = (stoppedValue u fun ω => min (τ ω) i) ⁻¹' t ∩ {ω | τ ω ≤ i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>inst✝⁸ : MeasurableSpace ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : OrderTopology ι<VAR>inst✝⁵ : SecondCountableTopology ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝² : MetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>hf_prog : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => min (τ ω) i)<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>i : ι<VAR>ω : Ω<GOAL>ω ∈ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ i} ↔ ω ∈ (stoppedValue u fun ω => min (τ ω) i) ⁻¹' t ∩ {ω | τ ω ≤ i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>inst✝⁸ : MeasurableSpace ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : OrderTopology ι<VAR>inst✝⁵ : SecondCountableTopology ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝² : MetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>hf_prog : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => min (τ ω) i)<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>i : ι<VAR>ω : Ω<GOAL>τ ω ≤ i → (u (τ ω) ω ∈ t ↔ u (min (τ ω) i) ω ∈ t)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>inst✝⁸ : MeasurableSpace ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : OrderTopology ι<VAR>inst✝⁵ : SecondCountableTopology ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝² : MetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>hf_prog : ProgMeasurable f u<VAR>hτ : IsStoppingTime f τ<VAR>h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω => min (τ ω) i)<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>i : ι<VAR>ω : Ω<VAR>h : τ ω ≤ i<GOAL>u (τ ω) ω ∈ t ↔ u (min (τ ω) i) ω ∈ t
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>Z : Set (PrimeSpectrum R)<GOAL>IsClosed Z ↔ ∃ s, Z = zeroLocus s
<VAR>x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>rexp (log (x / y)) = rexp (log x - log y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : AddZeroClass N<VAR>f : M → N<VAR>hf : f 0 = 0<VAR>hf' : ∀ (x y : M), f (x + y) = f x + f y<VAR>v₁ v₂ : α →₀ M<VAR>x✝ : α<GOAL>(mapRange f hf (v₁ + v₂)) x✝ = (mapRange f hf v₁ + mapRange f hf v₂) x✝
<VAR>x✝ y x : ℝ<VAR>hx : cos x ≠ 0<VAR>this : Complex.cos ↑x ≠ 0<GOAL>↑(1 + tan x ^ 2)⁻¹ = ↑(cos x ^ 2)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>S₁.homologyπ ≫ homologyMap φ ≫ S₂.homologyι = S₁.iCycles ≫ φ.τ₂ ≫ S₂.pOpcycles
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : AddCommGroup V₂<VAR>inst✝³ : Module k V₁<VAR>inst✝² : Module k V₂<VAR>inst✝¹ : AddTorsor V₁ P₁<VAR>inst✝ : AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>hEF : AffineSubspace.map φ E ≤ F<GOAL>E.direction ≤ Submodule.comap φ.linear F.direction
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : AddCommGroup V₂<VAR>inst✝³ : Module k V₁<VAR>inst✝² : Module k V₂<VAR>inst✝¹ : AddTorsor V₁ P₁<VAR>inst✝ : AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>hEF : AffineSubspace.map φ E ≤ F<GOAL>(AffineSubspace.map φ E).direction ≤ F.direction
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<VAR>x : L<VAR>y : ↥N<VAR>n : ℕ<GOAL>↑(((toEnd R L ↥↑N) x ^ n) y) = ((toEnd R L M) x ^ n) ↑y
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<VAR>R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t<GOAL>IsPreconnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<VAR>R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t<VAR>P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)<GOAL>IsPreconnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<VAR>R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t<VAR>P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)<GOAL>∀ x ∈ ⋃ n ∈ t, s n, ∀ y ∈ ⋃ n ∈ t, s n, ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<VAR>R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t<VAR>P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)<VAR>x : α<VAR>hx : x ∈ ⋃ n ∈ t, s n<VAR>y : α<VAR>hy : y ∈ ⋃ n ∈ t, s n<GOAL>∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<VAR>R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t<VAR>P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)<VAR>x : α<VAR>hx : x ∈ ⋃ n ∈ t, s n<VAR>y : α<VAR>hy : y ∈ ⋃ n ∈ t, s n<VAR>i : ι<VAR>hi : i ∈ t<VAR>hxi : x ∈ s i<GOAL>∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<VAR>R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t<VAR>P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)<VAR>x : α<VAR>hx : x ∈ ⋃ n ∈ t, s n<VAR>y : α<VAR>hy : y ∈ ⋃ n ∈ t, s n<VAR>i : ι<VAR>hi : i ∈ t<VAR>hxi : x ∈ s i<VAR>j : ι<VAR>hj : j ∈ t<VAR>hyj : y ∈ s j<GOAL>∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v : Set α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<VAR>R : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t<VAR>P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)<VAR>x : α<VAR>hx : x ∈ ⋃ n ∈ t, s n<VAR>y : α<VAR>hy : y ∈ ⋃ n ∈ t, s n<VAR>i : ι<VAR>hi : i ∈ t<VAR>hxi : x ∈ s i<VAR>j : ι<VAR>hj : j ∈ t<VAR>hyj : y ∈ s j<VAR>p : Set ι<VAR>hpt : p ⊆ t<VAR>hip : i ∈ p<VAR>hjp : j ∈ p<VAR>hp : IsPreconnected (⋃ j ∈ p, s j)<GOAL>∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l : Subspace η α ι<VAR>x : η → α<VAR>i : ι<VAR>a : α<VAR>e : η<VAR>h : l.idxFun i = Sum.inl a<GOAL>↑l x i = a
<VAR>α✝ : Type u_1<VAR>l : RBNode α✝<VAR>v : α✝<VAR>r : RBNode α✝<VAR>cl : RBColor<VAR>n : Nat<VAR>hl : l.Balanced cl (n + 1)<VAR>hr : RedRed True r n<GOAL>RedRed (cl = red) (l.balRight v r) (n + 1)
<VAR>α✝ : Type u_1<VAR>l : RBNode α✝<VAR>v : α✝<VAR>r : RBNode α✝<VAR>cl : RBColor<VAR>n : Nat<VAR>hl : l.Balanced cl (n + 1)<VAR>hr : RedRed True r n<GOAL>RedRed (cl = red) (r.reverse.balLeft v l.reverse).reverse (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : (sort (fun x x_1 => x ≤ x_1) s).length - 1 < (sort (fun x x_1 => x ≤ x_1) s).length<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : s.card - 1 < s.card<GOAL>s.Nonempty
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>P.pairing i j = 0 ∨ P.pairing j i = 0 ↔ P.IsOrthogonal i j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<VAR>h : P.pairing i j = 0 ∨ P.pairing j i = 0<GOAL>P.IsOrthogonal i j
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b c : α<GOAL>lcm (b * a) (c * a) = lcm b c * normalize a
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<GOAL>s = univ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<VAR>p : P<VAR>hp : p ∈ s<GOAL>s = univ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h₁ : s.Subsingleton<VAR>h₂ : affineSpan k s = ⊤<VAR>p : P<VAR>hp : p ∈ s<VAR>this : s = {p}<GOAL>s = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>¬μ univ = 0
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>HasSum (fun n => z ^ n / ↑n) (-log (1 - z))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>HasSum (fun n => - -(z ^ n / ↑n)) (-log (1 - z))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>HasSum (fun n => -(z ^ n / ↑n)) (log (1 - z))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>n : ℕ<GOAL>-(z ^ n / ↑n) = (-1) ^ (n + 1) * (-z) ^ n / ↑n
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>-(z ^ 0 / ↑0) = (-1) ^ (0 + 1) * (-z) ^ 0 / ↑0
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>n : ℕ<VAR>hn : n > 0<GOAL>-(z ^ n / ↑n) = (-1) ^ (n + 1) * (-z) ^ n / ↑n
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>n : ℕ<VAR>hn : n > 0<GOAL>-z ^ n / ↑n = (-1) ^ (n + 1) * (-z) ^ n / ↑n
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>n : ℕ<VAR>hn : n > 0<GOAL>↑n ≠ 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : eval (W.addX x₁ x₂ L) (derivative (W.addPolynomial x₁ y₁ L)) ≠ 0<GOAL>W.Nonsingular (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : eval (W.addX x₁ x₂ L) (derivative (W.addPolynomial x₁ y₁ L)) ≠ 0<GOAL>evalEval (W.addX x₁ x₂ L) (L * (W.addX x₁ x₂ L - x₁) + y₁) (C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄)) ≠ 0 ∨ evalEval (W.addX x₁ x₂ L) (L * (W.addX x₁ x₂ L - x₁) + y₁) (C (C 2) * Y + C (C W.a₁ * X + C W.a₃)) ≠ 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : eval (W.addX x₁ x₂ L) (derivative (W.addPolynomial x₁ y₁ L)) ≠ 0<GOAL>W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) - (3 * W.addX x₁ x₂ L ^ 2 + 2 * W.a₂ * W.addX x₁ x₂ L + W.a₄) ≠ 0 ∨ 2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) ≠ 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) - (3 * W.addX x₁ x₂ L ^ 2 + 2 * W.a₂ * W.addX x₁ x₂ L + W.a₄) = 0 ∧ 2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) = 0<GOAL>eval (W.addX x₁ x₂ L) (derivative (W.addPolynomial x₁ y₁ L)) = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : W.a₁ * (L * (W.addX x₁ x₂ L - x₁) + y₁) - (3 * W.addX x₁ x₂ L ^ 2 + 2 * W.a₂ * W.addX x₁ x₂ L + W.a₄) = 0 ∧ 2 * (L * (W.addX x₁ x₂ L - x₁) + y₁) + (W.a₁ * W.addX x₁ x₂ L + W.a₃) = 0<GOAL>eval (W.addX x₁ x₂ L) (derivative (eval (C L * (X - C x₁) + C y₁) (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)))) = 0