ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : T1Space α<VAR>inst✝ : Countable α<VAR>s : Set α<VAR>x✝ : MeasurableSet s<GOAL>MeasurableSet (⋃ x ∈ s, {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : T1Space α<VAR>inst✝ : Countable α<VAR>s : Set α<VAR>x✝ : MeasurableSet s<GOAL>∀ b ∈ s, MeasurableSet {b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : T1Space α<VAR>inst✝ : Countable α<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>x : α<VAR>a✝ : x ∈ s<GOAL>MeasurableSet {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : T1Space α<VAR>inst✝ : Countable α<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>x : α<VAR>a✝ : x ∈ s<GOAL>MeasurableSet {x}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : T1Space α<VAR>inst✝ : Countable α<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>x : α<VAR>a✝ : x ∈ s<GOAL>{x}ᶜ ∈ {s | IsOpen s}
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>Ico a a = 0
<VAR>x y : ℝ<GOAL>AntitoneOn (fun x => log x / √x) {x | rexp 2 ≤ x}
<VAR>x y : ℝ<GOAL>AntitoneOn (fun x => log x / x ^ (1 / 2)) {x | rexp 2 ≤ x}
<VAR>x y x✝ : ℝ<GOAL>2 = 1 / (1 / 2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>x y : α<GOAL>IsLUB (f '' {x, y}) (f x ⊔ f y)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>p : α → Prop<VAR>step : ∀ (a : α), p a → a ≤ lfp f → p (f a)<VAR>hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)<VAR>s : Set α := {a | a ≤ lfp f ∧ p a}<GOAL>p (lfp f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>p : α → Prop<VAR>step : ∀ (a : α), p a → a ≤ lfp f → p (f a)<VAR>s : Set α := {a | a ≤ lfp f ∧ p a}<VAR>hSup : p (sSup s)<GOAL>p (lfp f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>p : α → Prop<VAR>step : ∀ (a : α), p a → a ≤ lfp f → p (f a)<VAR>s : Set α := {a | a ≤ lfp f ∧ p a}<VAR>hSup : p (sSup s)<GOAL>sSup s = lfp f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>p : α → Prop<VAR>step : ∀ (a : α), p a → a ≤ lfp f → p (f a)<VAR>s : Set α := {a | a ≤ lfp f ∧ p a}<VAR>hSup : p (sSup s)<VAR>h : sSup s ≤ lfp f<GOAL>sSup s = lfp f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>p : α → Prop<VAR>step : ∀ (a : α), p a → a ≤ lfp f → p (f a)<VAR>s : Set α := {a | a ≤ lfp f ∧ p a}<VAR>hSup : p (sSup s)<VAR>h : sSup s ≤ lfp f<VAR>hmem : f (sSup s) ∈ s<GOAL>sSup s = lfp f
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix p n R<GOAL>B * (Aᴴ * A) = 0 ↔ B * Aᴴ = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<GOAL>b ≤ ⌊a + ↑n⌋₊ ↔ b ≤ ⌊a⌋₊ + n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<GOAL>↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<VAR>hb : n ≤ b<GOAL>↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n✝ : ℕ<VAR>ha : 0 ≤ a<VAR>n b : ℕ<VAR>hb : b ≤ n<GOAL>↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>q : α → Prop<VAR>inst✝ : DecidablePred q<VAR>s : Multiset α<GOAL>countP p (filter q s) = countP (fun a => p a ∧ q a) s
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>𝕜₄ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>inst✝³¹ : AddCommGroup E<VAR>inst✝³⁰ : AddCommGroup F<VAR>inst✝²⁹ : AddCommGroup G<VAR>inst✝²⁸ : AddCommGroup H<VAR>inst✝²⁷ : NontriviallyNormedField 𝕜<VAR>inst✝²⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝²⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜₄<VAR>inst✝²³ : Module 𝕜 E<VAR>inst✝²² : Module 𝕜₂ F<VAR>inst✝²¹ : Module 𝕜₃ G<VAR>inst✝²⁰ : Module 𝕜₄ H<VAR>inst✝¹⁹ : TopologicalSpace E<VAR>inst✝¹⁸ : TopologicalSpace F<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>inst✝¹⁵ : TopologicalAddGroup G<VAR>inst✝¹⁴ : TopologicalAddGroup H<VAR>inst✝¹³ : ContinuousConstSMul 𝕜₃ G<VAR>inst✝¹² : ContinuousConstSMul 𝕜₄ H<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>σ₃₄ : 𝕜₃ →+* 𝕜₄<VAR>σ₄₃ : 𝕜₄ →+* 𝕜₃<VAR>σ₂₄ : 𝕜₂ →+* 𝕜₄<VAR>σ₁₄ : 𝕜 →+* 𝕜₄<VAR>inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝⁹ : RingHomInvPair σ₃₄ σ₄₃<VAR>inst✝⁸ : RingHomInvPair σ₄₃ σ₃₄<VAR>inst✝⁷ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>inst✝⁶ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>inst✝³ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₁<VAR>e₁₂ : E ≃SL[σ₁₂] F<VAR>e₄₃ : H ≃SL[σ₄₃] G<VAR>f g : E →SL[σ₁₄] H<GOAL>(fun L => (↑e₄₃).comp (L.comp ↑e₁₂.symm)) (f + g) = (fun L => (↑e₄₃).comp (L.comp ↑e₁₂.symm)) f + (fun L => (↑e₄₃).comp (L.comp ↑e₁₂.symm)) g
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>𝕜₄ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>inst✝³¹ : AddCommGroup E<VAR>inst✝³⁰ : AddCommGroup F<VAR>inst✝²⁹ : AddCommGroup G<VAR>inst✝²⁸ : AddCommGroup H<VAR>inst✝²⁷ : NontriviallyNormedField 𝕜<VAR>inst✝²⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝²⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜₄<VAR>inst✝²³ : Module 𝕜 E<VAR>inst✝²² : Module 𝕜₂ F<VAR>inst✝²¹ : Module 𝕜₃ G<VAR>inst✝²⁰ : Module 𝕜₄ H<VAR>inst✝¹⁹ : TopologicalSpace E<VAR>inst✝¹⁸ : TopologicalSpace F<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>inst✝¹⁵ : TopologicalAddGroup G<VAR>inst✝¹⁴ : TopologicalAddGroup H<VAR>inst✝¹³ : ContinuousConstSMul 𝕜₃ G<VAR>inst✝¹² : ContinuousConstSMul 𝕜₄ H<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>σ₃₄ : 𝕜₃ →+* 𝕜₄<VAR>σ₄₃ : 𝕜₄ →+* 𝕜₃<VAR>σ₂₄ : 𝕜₂ →+* 𝕜₄<VAR>σ₁₄ : 𝕜 →+* 𝕜₄<VAR>inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂<VAR>inst✝⁹ : RingHomInvPair σ₃₄ σ₄₃<VAR>inst✝⁸ : RingHomInvPair σ₄₃ σ₃₄<VAR>inst✝⁷ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>inst✝⁶ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>inst✝³ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₁<VAR>e₁₂ : E ≃SL[σ₁₂] F<VAR>e₄₃ : H ≃SL[σ₄₃] G<VAR>t : 𝕜₄<VAR>f : E →SL[σ₁₄] H<GOAL>{ toFun := fun L => (↑e₄₃).comp (L.comp ↑e₁₂.symm), map_add' := ⋯ }.toFun (t • f) = σ₄₃ t • { toFun := fun L => (↑e₄₃).comp (L.comp ↑e₁₂.symm), map_add' := ⋯ }.toFun f
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝² : DivInvMonoid M<VAR>inst✝¹ : PseudoMetricSpace M<VAR>inst✝ : IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>nndist (a / c) (b / c) = nndist a b
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<GOAL>0 < s.circumradius
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<GOAL>0 ≠ s.circumradius
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>h : 0 = s.circumradius<GOAL>False
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>h : 0 = s.circumradius<VAR>hr : ∀ (i : Fin (n + 1 + 1)), dist (s.points i) s.circumcenter = s.circumradius<GOAL>False
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>h : 0 = s.circumradius<VAR>hr : ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter<GOAL>False
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>h : 0 = s.circumradius<VAR>hr : ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter<VAR>h01 : s.points 0 ≠ s.points 1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<GOAL>p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ (a_1 : α), List.count a_1 p.support.tail = 1
<VAR>num : Int<VAR>den : Nat<VAR>nz : den ≠ 0<VAR>c : num.natAbs.Coprime den<GOAL>{ num := num, den := den, den_nz := nz, reduced := c } = num /. ↑den
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosDef<GOAL>M.PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosDef<GOAL>∀ (x : n → R), 0 ≤ star x ⬝ᵥ M *ᵥ x
<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 J' : Submodule B L<GOAL>I ≤ (J * J')ᵛ ↔ I * J ≤ J'ᵛ
<VAR>x : PartENat<VAR>n : ℕ<VAR>hx : x ≠ ⊤<GOAL>x < ↑n.succ ↔ x ≤ ↑n
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>h : ∀ (i : I), J i → K i<VAR>x : ↑C<VAR>i : I<GOAL>↑((ProjRestricts C h ∘ ProjRestrict C K) x) i = ↑(ProjRestrict C J x) i
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>h : ∀ (i : I), J i → K i<VAR>x : ↑C<VAR>i : I<GOAL>(if J i then if K i then ↑x i else false else false) = if J i then ↑x i else false
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>x : C<GOAL>adj1.unit.app x ≫ (adj1.rightAdjointUniq adj2).hom.app (F.obj x) = adj2.unit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>x : C<GOAL>adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>x : C<GOAL>adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x) ≫ adj1.counit.app (F.obj x)) = adj2.unit.app x
<VAR>x y : ℝ<GOAL>rexp (x + y) = rexp x * rexp y
<VAR>n : ℕ<VAR>i : Fin (n + 4)<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last (n + 3)<VAR>k : ℕ<VAR>h : k < n + 2<GOAL>Set.range ⇑(asOrderHom (standardSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯)) ∪ {i} ≠ Set.univ
<VAR>n : ℕ<VAR>i : Fin (n + 4)<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last (n + 3)<VAR>k : ℕ<VAR>h : k < n + 2<GOAL>∃ x, ¬i = x ∧ ∀ (x_1 : Fin (2 + 1)), ¬(Hom.toOrderHom ({ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm (Hom.mk { toFun := ![⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩], monotone' := ⋯ })).down) x_1 = x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q p : R[X]<VAR>hpl : 0 < p.degree<GOAL>¬IsUnit p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q p : R[X]<VAR>hpl : 0 < p.degree<VAR>h✝ : Subsingleton R<GOAL>¬IsUnit p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q p : R[X]<VAR>hpl : 0 < p.degree<VAR>h✝ : Nontrivial R<GOAL>¬IsUnit p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q p : R[X]<VAR>hpl : 0 < p.degree<VAR>h✝ : Nontrivial R<VAR>h : IsUnit p<GOAL>False
<VAR>f : Bool → Bool → Bool<GOAL>bitwise f 0 0 = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing 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>i j : ι<VAR>n : N<VAR>m : M<GOAL>((↑(P.reflection i).dualMap ∘ₗ P.toLin.flip) n) m = ((P.toLin.flip ∘ₗ ↑(P.coreflection i)) n) m
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<GOAL>finrank 𝕜 (X ⟶ X) = 1
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<GOAL>finrank 𝕜 (X ⟶ X) = 1
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<GOAL>∀ (w : X ⟶ X), ∃ c, c • 𝟙 X = w
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<VAR>f : X ⟶ X<GOAL>∃ c, c • 𝟙 X = f
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<VAR>f : X ⟶ X<VAR>this : Nontrivial (End X)<GOAL>∃ c, c • 𝟙 X = f
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<VAR>f : X ⟶ X<VAR>this✝ : Nontrivial (End X)<VAR>this : FiniteDimensional 𝕜 (End X)<GOAL>∃ c, c • 𝟙 X = f
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<VAR>f : X ⟶ X<VAR>this✝ : Nontrivial (End X)<VAR>this : FiniteDimensional 𝕜 (End X)<VAR>c : 𝕜<VAR>nu : c ∈ spectrum 𝕜 (End.of f)<GOAL>∃ c, c • 𝟙 X = f
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<VAR>f : X ⟶ X<VAR>this✝ : Nontrivial (End X)<VAR>this : FiniteDimensional 𝕜 (End X)<VAR>c : 𝕜<VAR>nu : c ∈ spectrum 𝕜 (End.of f)<GOAL>c • 𝟙 X = f
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : IsAlgClosed 𝕜<VAR>inst✝ : Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<VAR>id_nonzero : 𝟙 X ≠ 0<VAR>f : X ⟶ X<VAR>this✝ : Nontrivial (End X)<VAR>this : FiniteDimensional 𝕜 (End X)<VAR>c : 𝕜<VAR>nu : End.of f = c • 1<GOAL>c • 𝟙 X = f
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α✝ → β✝<VAR>s✝ t : Set α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>f : α → β<VAR>s : Set α<GOAL>f '' s = ∅ ↔ s = ∅
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α✝ → β✝<VAR>s✝ t : Set α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>f : α → β<VAR>s : Set α<GOAL>(∀ (x : β), x ∉ f '' s) ↔ ∀ (x : α), x ∉ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<GOAL>⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))<GOAL>⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>w : ℝ≥0∞<VAR>hw : w < ∫⁻ (x : α), f x ∂μ<GOAL>∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>w : ℝ≥0∞<VAR>hw : w < ∫⁻ (x : α), f x ∂μ<VAR>m : ℝ≥0∞<VAR>hm₁ : w < m<VAR>hm₂ : m < ∫⁻ (x : α), f x ∂μ<GOAL>∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))<VAR>w : ℝ≥0∞<VAR>hw : w < ∫⁻ (x : α), f x ∂μ<VAR>m : ℝ≥0∞<VAR>hm₁ : w < m<VAR>hm₂ : m < ∫⁻ (x : α), f x ∂μ<VAR>i : ι<VAR>hi : m ≤ ∫⁻ (x : α) in φ i, f x ∂μ<GOAL>∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<GOAL>⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>(∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>ρ : Measure (α × β)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>ρ.fst s = ρ (Prod.fst ⁻¹' s)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>M.Basis I (insert e I) ↔ e ∈ M.closure I
<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>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map₂ m (pure a) g = map (m a) g
<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>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map ((fun p => m p.1 p.2) ∘ Prod.mk a) g = map (m a) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>B : Set α<VAR>f : α → ℝ≥0∞<VAR>A : Set α<VAR>hB : MeasurableSet B<GOAL>∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ
<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>g : Vector ℕ (n + 1) →. ℕ<VAR>hf : Partrec' f<VAR>hg : Partrec' g<VAR>v : Vector ℕ n<GOAL>(mOfFn fun i => Fin.cases f (fun i v => ↑(some (v.get i))) i v) >>= g = (f v).bind fun a => g (a ::ᵥ v)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup V<VAR>inst✝ : SeminormedAddCommGroup W<VAR>f : V → W<VAR>M : ℝ<VAR>h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖<VAR>x : V<GOAL>M ≤ max M 1
<VAR>k : ℕ<GOAL>descFactorial 0 (k + 1) = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>h : IsClosed (range f)<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosed (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>h : IsClosed (range f)<VAR>t : Set Y<VAR>ht : IsClosed t<VAR>hs : IsClosed (f ⁻¹' t)<GOAL>IsClosed (f '' (f ⁻¹' t))