ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_smul : DominatedFinMeasAdditive (c • μ) T C'<VAR>f : α → E<VAR>hc0 : ¬c = 0<GOAL>setToFun μ T hT f = setToFun (c • μ) T hT_smul f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_smul : DominatedFinMeasAdditive (c • μ) T C'<VAR>f : α → E<VAR>hc0 : ¬c = 0<GOAL>c⁻¹ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_smul : DominatedFinMeasAdditive (c • μ) T C'<VAR>f : α → E<VAR>hc0 : ¬c = 0<GOAL>μ = c⁻¹ • c • μ
<VAR>α✝ β α : Type u<VAR>h : #α = ℵ₀<GOAL>Nonempty (Denumerable α)
<VAR>α✝ β α : Type u<VAR>h : #α = ℵ₀<VAR>f : α ≃ ULift.{u, 0} ℕ<GOAL>Nonempty (Denumerable α)
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<GOAL>(↑t).Pairwise (IsCoprime on s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
<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>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>g : β → γ<VAR>f : α → β<VAR>hg : QuasiMeasurePreserving g μb μc<VAR>hf : QuasiMeasurePreserving f μa μb<GOAL>map (g ∘ f) μa ≪ μc
<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>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>g : β → γ<VAR>f : α → β<VAR>hg : QuasiMeasurePreserving g μb μc<VAR>hf : QuasiMeasurePreserving f μa μb<GOAL>map g (map f μa) ≪ μc
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>(bind₁ verschiebungPoly) (wittPolynomial p ℤ n) = if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>∀ (x : ℕ → ℤ), (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) = (MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B✝ : Matrix n n α<VAR>B : Matrix m n α<VAR>h : IsUnit A.det<GOAL>B * A⁻¹ * A = B
<VAR>a : EReal<VAR>h₁ : a ≠ ⊥<VAR>h₂ : a ≠ ⊤<VAR>h₃ : a ≠ 0<GOAL>a / a = 1
<VAR>a : EReal<VAR>h₁ : a ≠ ⊥<VAR>h₂ : a ≠ ⊤<VAR>h₃ : ↑a.toReal ≠ 0<GOAL>↑a.toReal / ↑a.toReal = 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝³ : (i : ι) → Sub (α i)<VAR>inst✝² : ∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a b : α i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)<GOAL>f.support \ g.support ⊆ (f - g).support
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>B A₁ A₂ A₃ : C<VAR>f : A₁ ⟶ B<VAR>inst✝² : Mono f<VAR>g : A₂ ⟶ B<VAR>inst✝¹ : Mono g<VAR>h : A₃ ⟶ B<VAR>inst✝ : Mono h<VAR>h₁ : mk f ≤ mk g<VAR>h₂ : mk g ≤ mk h<GOAL>ofMkLEMk f g h₁ ≫ ofMkLEMk g h h₂ = ofMkLEMk f h ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>B A₁ A₂ A₃ : C<VAR>f : A₁ ⟶ B<VAR>inst✝² : Mono f<VAR>g : A₂ ⟶ B<VAR>inst✝¹ : Mono g<VAR>h : A₃ ⟶ B<VAR>inst✝ : Mono h<VAR>h₁ : mk f ≤ mk g<VAR>h₂ : mk g ≤ mk h<GOAL>(underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso h).hom = (underlyingIso f).inv ≫ underlying.map ⋯.hom ≫ (underlyingIso h).hom
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>f₁ f₂ : M →ₛₗ[τ₁₂] M₂<GOAL>comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>f₁ f₂ : M →ₛₗ[τ₁₂] M₂<GOAL>∀ ⦃x : M⦄, x ∈ comap f₁ q ⊓ comap f₂ q → x ∈ comap (f₁ + f₂) q
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>f₁ f₂ : M →ₛₗ[τ₁₂] M₂<VAR>m : M<VAR>h : f₁ m ∈ q ∧ f₂ m ∈ q<GOAL>f₁ m + f₂ m ∈ q
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>n : ℕ<VAR>hn : 1 ≤ n<GOAL>f (1 * c ^ n) / f c ^ n = 1
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<VAR>A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<VAR>A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})<VAR>B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>t_ne_zero' : t ≠ 0<VAR>t_ne_zero : ↑t ≠ 0<VAR>ν : Measure α := μ.withDensity (v.limRatioMeas hρ)<VAR>f : α → ℝ≥0∞ := v.limRatioMeas hρ<VAR>f_meas : Measurable f<VAR>A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})<VAR>B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})<VAR>C : ∀ (n : ℤ), ρ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (t • ν) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))<GOAL>ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<GOAL>Pairwise (Disjoint on disjointed f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>h : m < n<GOAL>Disjoint (disjointed f m) (disjointed f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>m n✝ : ℕ<VAR>h : m < n✝ + 1<GOAL>Disjoint (disjointed f m) (disjointed f (n✝ + 1))
<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>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p b : P<GOAL>(s.weightedVSubOfPoint (fun x => p) b) w = (∑ i ∈ s, w i) • (p -ᵥ b)
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : Nat.Prime (orderOf σ)<VAR>h2 : Fintype.card α < 2 * orderOf σ<GOAL>σ.IsCycle
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ha : a ≠ 0<GOAL>((monomial n) a).trailingDegree = ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ha : a ≠ 0<GOAL>↑n = ↑n
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>hn : Odd n<GOAL>commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>hn : Odd n<GOAL>↑((n + 3) / 2) / ↑(2 * n) = (↑n + 3) / (4 * ↑n)
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>hn : Odd n<GOAL>(↑n + 3) / 2 / (2 * ↑n) = (↑n + 3) / (4 * ↑n)
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>hn : Odd n<GOAL>(↑n + 3) / (2 * 2 * ↑n) = (↑n + 3) / (4 * ↑n)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>hgf : ⇑g ∘ e = ⇑f<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>hgf : ⇑g ∘ e = ⇑f<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<VAR>dg : Y →ᵇ ℝ<VAR>dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)<VAR>dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})<VAR>dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<VAR>dg : Y →ᵇ ℝ<VAR>dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)<VAR>dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})<VAR>dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)<VAR>hgf : ∀ (x : X), (g - dg) (e x) = f x<GOAL>∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<VAR>dg : Y →ᵇ ℝ<VAR>dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)<VAR>dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})<VAR>dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)<VAR>hgf : ∀ (x : X), (g - dg) (e x) = f x<VAR>y : Y<GOAL>∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<VAR>dg : Y →ᵇ ℝ<VAR>dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)<VAR>dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})<VAR>dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)<VAR>hgf : ∀ (x : X), (g - dg) (e x) = f x<VAR>y : Y<VAR>hyb : (g - dg) y < b<GOAL>∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<VAR>dg : Y →ᵇ ℝ<VAR>dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)<VAR>dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})<VAR>dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)<VAR>hgf : ∀ (x : X), (g - dg) (e x) = f x<VAR>y : Y<VAR>hyb : (g - dg) y < b<VAR>xu : X<VAR>hyxu : (g - dg) y < f xu<VAR>right✝ : f xu ≤ b<GOAL>∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<VAR>dg : Y →ᵇ ℝ<VAR>dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)<VAR>dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})<VAR>dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)<VAR>hgf : ∀ (x : X), (g - dg) (e x) = f x<VAR>y : Y<VAR>hyb : (g - dg) y < b<VAR>xu : X<VAR>hyxu : (g - dg) y < f xu<VAR>right✝ : f xu ≤ b<VAR>hc : c < g y<GOAL>∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)