ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i1 i2 j : ℕ<VAR>hi : i1 ≤ i2<VAR>cell : (i2, j) ∈ μ<GOAL>T i1 j ≤ T i2 j
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i1 i2 j : ℕ<VAR>hi : i1 ≤ i2<VAR>cell : (i2, j) ∈ μ<VAR>h : i1 = i2<GOAL>T i1 j ≤ T i2 j
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i1 i2 j : ℕ<VAR>hi : i1 ≤ i2<VAR>cell : (i2, j) ∈ μ<VAR>h : i1 < i2<GOAL>T i1 j ≤ T i2 j
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>X : Type u_3<VAR>inst✝ : TopologicalSpace X<VAR>hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U<VAR>S : Set X<VAR>hS : IsPreconnected S<GOAL>∀ ⦃x : X⦄, x ∈ S → ∀ ⦃y : X⦄, y ∈ S → x = 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>X : Type u_3<VAR>inst✝ : TopologicalSpace X<VAR>hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U<VAR>S : Set X<VAR>hS : IsPreconnected S<VAR>h_contra : ∃ x ∈ S, ∃ y ∈ S, x ≠ y<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>X : Type u_3<VAR>inst✝ : TopologicalSpace X<VAR>hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U<VAR>S : Set X<VAR>hS : IsPreconnected S<VAR>x : X<VAR>hx : x ∈ S<VAR>y : X<VAR>hy : y ∈ S<VAR>hxy : x ≠ y<VAR>U : Set X<VAR>hU : IsClopen U<VAR>hxU : x ∈ U<VAR>hyU : y ∉ U<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>X : Type u_3<VAR>inst✝ : TopologicalSpace X<VAR>hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U<VAR>S : Set X<VAR>x : X<VAR>hx : x ∈ S<VAR>y : X<VAR>hy : y ∈ S<VAR>hxy : x ≠ y<VAR>U : Set X<VAR>hU : IsClopen U<VAR>hxU : x ∈ U<VAR>hyU : y ∉ U<VAR>hS : (S ∩ (U ∩ Uᶜ)).Nonempty<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>X : Type u_3<VAR>inst✝ : TopologicalSpace X<VAR>hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U<VAR>S : Set X<VAR>x : X<VAR>hx : x ∈ S<VAR>y : X<VAR>hy : y ∈ S<VAR>hxy : x ≠ y<VAR>U : Set X<VAR>hU : IsClopen U<VAR>hxU : x ∈ U<VAR>hyU : y ∉ U<VAR>hS : ∅.Nonempty<GOAL>False
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>n : ℕ<GOAL>∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i)
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>n : ℕ<GOAL>∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i)
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>n j : ℕ<VAR>j_in : j ∈ range n<GOAL>op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>n j : ℕ<VAR>j_in : j + 1 ≤ n<GOAL>op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>n j : ℕ<VAR>j_in : j + 1 ≤ n<GOAL>n - 1 - (n - 1 - j) = j
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>n j : ℕ<VAR>j_in : j + 1 ≤ n<GOAL>j ≤ n - 1
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>h : π.IsPartition<VAR>hJ : J ≤ I<GOAL>(π.restrict J).iUnion = ↑J
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DivisionMonoid α<VAR>s t : Finset α<VAR>inst✝ : Fintype α<GOAL>univ / univ = univ
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>(lambda c t ≫ T.ε.app c.pt) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<GOAL>lambda c t ≫ T.δ.app c.pt = lambda c t ≫ T.map (lambda c t)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>(lambda c t ≫ T.δ.app c.pt) ≫ (T.mapCone (T.mapCone c)).π.app j = (lambda c t ≫ T.map (lambda c t)) ≫ (T.mapCone (T.mapCone c)).π.app j
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>(c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>j : J<GOAL>c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>n : N<GOAL>∃ m, f m = n ∧ ‖m‖ < ‖n‖ + ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>m : M<GOAL>∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>m : M<VAR>nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty<GOAL>∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>m : M<VAR>nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty<VAR>x : M<VAR>hx : x ∈ ↑f.ker<VAR>H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑f.ker) + ε<GOAL>∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε
<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>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<GOAL>c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ : X.Opens<VAR>U V : X.Opensᵒᵖ<VAR>i : U ⟶ V<GOAL>(X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map i ≫ ((fun U => Functor.mapIso X.presheaf (eqToIso ⋯).symm.op) V).hom = ((fun U => Functor.mapIso X.presheaf (eqToIso ⋯).symm.op) U).hom ≫ X.presheaf.map i
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ : X.Opens<VAR>U V : X.Opensᵒᵖ<VAR>i : U ⟶ V<GOAL>Hom.app (X.restrictFunctor.map i.unop).left ⊤ ≫ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map i
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ : X.Opens<VAR>U V : X.Opensᵒᵖ<VAR>i : U ⟶ V<GOAL>X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map ((eqToHom ⋯).op ≫ i)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity fun x => c) s = (c • μ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<GOAL>infEdist x (closure s) = infEdist x s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<GOAL>infEdist x s ≤ infEdist x (closure s)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x (closure s) < ⊤<GOAL>infEdist x s ≤ infEdist x (closure s) + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x (closure s) < ⊤<VAR>ε0 : 0 < ↑ε / 2<GOAL>infEdist x s ≤ infEdist x (closure s) + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x (closure s) < ⊤<VAR>ε0 : 0 < ↑ε / 2<VAR>this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2<GOAL>infEdist x s ≤ infEdist x (closure s) + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y✝ : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x (closure s) < ⊤<VAR>ε0 : 0 < ↑ε / 2<VAR>this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2<VAR>y : α<VAR>ycs : y ∈ closure s<VAR>hy : edist x y < infEdist x (closure s) + ↑ε / 2<GOAL>infEdist x s ≤ infEdist x (closure s) + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y✝ : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x (closure s) < ⊤<VAR>ε0 : 0 < ↑ε / 2<VAR>this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2<VAR>y : α<VAR>ycs : y ∈ closure s<VAR>hy : edist x y < infEdist x (closure s) + ↑ε / 2<VAR>z : α<VAR>zs : z ∈ s<VAR>dyz : edist y z < ↑ε / 2<GOAL>infEdist x s ≤ infEdist x (closure s) + ↑ε
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>n : ℕ<GOAL>Splits (RingHom.id K) (cyclotomic' n K)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>n : ℕ<GOAL>∀ j ∈ primitiveRoots n K, Splits (RingHom.id K) (X - C j)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>z : K<VAR>a✝ : z ∈ primitiveRoots n K<GOAL>Splits (RingHom.id K) (X - C z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : OrderBot α<VAR>n : α<VAR>φ : α → α<GOAL>StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : OrderBot α<VAR>n : α<VAR>φ : α → α<GOAL>∀ (a : α), (fun n => StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m) a → (fun n => StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m) (succ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : OrderBot α<VAR>n : α<VAR>φ : α → α<VAR>k : α<VAR>ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m<VAR>hφ : StrictMonoOn φ (Iic (succ k))<VAR>m : α<VAR>hm : m ≤ succ k<VAR>hk : ¬IsMax k<GOAL>m ≤ φ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : OrderBot α<VAR>n : α<VAR>φ : α → α<VAR>k : α<VAR>ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m<VAR>hφ : StrictMonoOn φ (Iic (succ k))<VAR>hk : ¬IsMax k<VAR>hm : succ k ≤ succ k<GOAL>succ k ≤ φ (succ k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : OrderBot α<VAR>n : α<VAR>φ : α → α<VAR>k : α<VAR>ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m<VAR>hφ : StrictMonoOn φ (Iic (succ k))<VAR>m : α<VAR>hm : m ≤ succ k<VAR>hk : ¬IsMax k<VAR>h : m ≤ k<GOAL>m ≤ φ m
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>hA : 0 ∈ A<GOAL>schnirelmannDensity A = 1 ↔ A = Set.univ
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>hA : 0 ∈ A<GOAL>{0}ᶜ ⊆ A ↔ A = Set.univ
<GOAL>{x | Liouville x} = {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
<GOAL>{x | Liouville x} ⊆ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
<GOAL>{x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ {x | Liouville x}
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom = X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>((β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom) ≫ (α_ Z Y X).inv = (X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv = X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContMDiffWithinAt I' I n f s x₀<VAR>hg : ContMDiffWithinAt I' I n g s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => f x / g x) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁸ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>F : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>J : ModelWithCorners 𝕜 F F<VAR>G : Type u_5<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : ChartedSpace H G<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : LieGroup I G<VAR>E' : Type u_6<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H' M<VAR>E'' : Type u_9<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_10<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M' : Type u_11<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H'' M'<VAR>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContMDiffWithinAt I' I n f s x₀<VAR>hg : ContMDiffWithinAt I' I n g s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => f x * (g x)⁻¹) s x₀
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : MeasurableSpace α<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>hre : AEMeasurable (fun x => RCLike.re (f x)) μ<VAR>him : AEMeasurable (fun x => RCLike.im (f x)) μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : MeasurableSpace α<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>hre : AEMeasurable (fun x => RCLike.re (f x)) μ<VAR>him : AEMeasurable (fun x => RCLike.im (f x)) μ<VAR>x✝ : α<GOAL>f x✝ = (RCLike.ofReal ∘ fun x => RCLike.re (f x)) x✝ + (RCLike.ofReal ∘ fun x => RCLike.im (f x)) x✝ * RCLike.I
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>u : Rˣ<VAR>v : Module.Ray R M<GOAL>u • v = v ↔ 0 < ↑u
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>u : Rˣ<VAR>v : M<VAR>hv : v ≠ 0<GOAL>u • rayOfNeZero R v hv = rayOfNeZero R v hv ↔ 0 < ↑u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ ν : Measure α<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(ν.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ ν : Measure α<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(ν.withDensity (s.indicator 1)).rnDeriv ν =ᶠ[ae ν] s.indicator 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : IsKilling K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α : Weight K (↥H) L<VAR>h : α.IsNonZero<VAR>e : (-α).IsZero<GOAL>α.IsZero
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<GOAL>(∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<GOAL>(∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = ∏ _x ∈ finPairsLT n, 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r : ℝ≥0∞<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>H : μ.InnerRegularWRT IsClosed IsOpen<GOAL>μ.WeaklyRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r : ℝ≥0∞<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>H : μ.InnerRegularWRT IsClosed IsOpen<VAR>hfin : ∀ {s : Set α}, μ s ≠ ⊤<GOAL>μ.WeaklyRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r : ℝ≥0∞<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>H : μ.InnerRegularWRT IsClosed IsOpen<VAR>hfin : ∀ {s : Set α}, μ s ≠ ⊤<GOAL>∀ (s : Set α), MeasurableSet s → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r : ℝ≥0∞<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>H : μ.InnerRegularWRT IsClosed IsOpen<VAR>hfin : ∀ {s : Set α}, μ s ≠ ⊤<GOAL>∀ (U : Set α), IsOpen U → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed F ∧ IsOpen U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r : ℝ≥0∞<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>H : μ.InnerRegularWRT IsClosed IsOpen<VAR>hfin : ∀ {s : Set α}, μ s ≠ ⊤<GOAL>∀ (t : Set α), MeasurableSet t → (∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ t, ∃ U ⊇ t, IsClosed F ∧ IsOpen U ∧ μ t ≤ μ F + ε ∧ μ U ≤ μ t + ε) → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ tᶜ, ∃ U ⊇ tᶜ, IsClosed F ∧ IsOpen U ∧ μ tᶜ ≤ μ F + ε ∧ μ U ≤ μ tᶜ + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r : ℝ≥0∞<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>H : μ.InnerRegularWRT IsClosed IsOpen<VAR>hfin : ∀ {s : Set α}, μ s ≠ ⊤<GOAL>∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ) (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ f i, ∃ U ⊇ f i, IsClosed F ∧ IsOpen U ∧ μ (f i) ≤ μ F + ε ∧ μ U ≤ μ (f i) + ε) → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ ⋃ i, f i, ∃ U ⊇ ⋃ i, f i, IsClosed F ∧ IsOpen U ∧ μ (⋃ i, f i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, f i) + ε
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<GOAL>X ∣ p - C (p.coeff 0)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<GOAL>v.valuation ((algebraMap R K) r) ≤ 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<GOAL>v.intValuation r ≤ 1
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<GOAL>Irreducible (X ^ n - X - 1)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<GOAL>Irreducible (X ^ n - X - 1)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<GOAL>Irreducible (X ^ n - X - 1)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<GOAL>Irreducible (trinomial 0 1 n (-1) (-1) 1)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<GOAL>∀ (z : ℂ), ¬((aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0 ∧ (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0<VAR>h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0<GOAL>False
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hn : 1 < n<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>z : ℂ<VAR>h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0<VAR>h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0<GOAL>z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0