ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : M →ₗ[R] N<VAR>this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)<VAR>this✝¹ : IsCentralScalar R M<VAR>this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)<VAR>this : IsCentralScalar R N<GOAL>(f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ toTrivSqZeroExt.toLinearMap = f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ toTrivSqZeroExt.toLinearMap
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : Generators R S<VAR>x : P.Ring<VAR>i : P.vars<GOAL>(P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.Ring] (D R P.Ring) x)) i = (aeval P.val) ((pderiv i) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ : ℝ<GOAL>∑ k ∈ Finset.range (n + 1 + 1), (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)) ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) = ∑ k ∈ Finset.range (n + 1), (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)) ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) + (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)) ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>∃ n, upperCrossingTime a b f N n ω = N
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>h : ¬∃ n, upperCrossingTime a b f N n ω = N<GOAL>False
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N<GOAL>False
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N<VAR>this : StrictMono fun n => upperCrossingTime a b f N n ω<GOAL>False
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N<VAR>this : StrictMono fun n => upperCrossingTime a b f N n ω<VAR>k : ℕ<VAR>hk : N < (fun n => upperCrossingTime a b f N n ω) k<GOAL>False
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>inst✝¹ : Fintype V<VAR>inst✝ : Fintype W<GOAL>Fintype.card V = Fintype.card W
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : G ≃g G'<VAR>inst✝¹ : Fintype V<VAR>inst✝ : Fintype W<GOAL>Fintype.card W = Fintype.card W
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q : ℕ<VAR>h✝ : ExpChar F q<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Finset β<GOAL>(SimpleGraph.map f G).IsClique ↑t ↔ t.card ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Finset β<VAR>ht : t.card ≤ 1<GOAL>(SimpleGraph.map f G).IsClique ↑t ↔ t.card ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Finset β<VAR>ht : 1 < t.card<GOAL>(SimpleGraph.map f G).IsClique ↑t ↔ t.card ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Finset β<VAR>ht : 1 < t.card<GOAL>(∃ s, G.IsClique ↑s ∧ map f s = t) ↔ ¬1 < t.card ∨ ∃ s, G.IsClique ↑s ∧ map f s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Finset β<VAR>ht : 1 < t.card<GOAL>t.Nontrivial
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ i, 0 < (f i) x
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>x : X<VAR>hx : x ∈ s<VAR>H : ∑ᶠ (i : ι), (f i) x = 1<GOAL>∃ i, 0 < (f i) x
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>x : X<VAR>hx : x ∈ s<VAR>H : ∀ (i : ι), (f i) x ≤ 0<GOAL>∑ᶠ (i : ι), (f i) x ≠ 1
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>a b : ℤ<GOAL>↑(a /. b) = ↑a / ↑b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)<GOAL>IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)<VAR>x : FractionalIdeal A⁰ (FractionRing A)<GOAL>x ≠ ⊥ → x * x⁻¹ = 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)<VAR>x : FractionalIdeal A⁰ (FractionRing A)<GOAL>x ≠ ⊥ → h.toEquiv (x * x⁻¹) = h.toEquiv 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>i : σ<VAR>j : σ →₀ ℕ<VAR>r : R<GOAL>X i ∣ (monomial j) r ↔ r = 0 ∨ j i ≠ 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>i : σ<VAR>j : σ →₀ ℕ<VAR>r : R<GOAL>(r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ j i ≠ 0
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>C : G.ConnectedComponent<VAR>φ : G →g G'<VAR>ψ : G' →g G''<GOAL>map ψ (map φ C) = map (ψ.comp φ) C
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>C : G.ConnectedComponent<VAR>φ : G →g G'<VAR>ψ : G' →g G''<GOAL>∀ (v : V), map ψ (map φ (G.connectedComponentMk v)) = map (ψ.comp φ) (G.connectedComponentMk v)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>p : HolorIndex (d :: ds) → Prop<VAR>t : HolorIndex (d :: ds)<VAR>i : ℕ<VAR>is : List ℕ<VAR>h : ↑t = i :: is<GOAL>Forall₂ (fun x x_1 => x < x_1) (↑t) (d :: ds)
<VAR>α : Type u_1<VAR>l₁ l₂ : List (List α)<VAR>h : l₁ ~ l₂<GOAL>l₁.join ~ l₂.join
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CoheytingAlgebra α<VAR>inst✝¹ : CoheytingAlgebra β<VAR>inst✝ : CoheytingHomClass F α β<VAR>f : F<VAR>a : α<GOAL>f (￢a) = ￢f a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α✝<VAR>inst✝⁶ : MeasurableSpace α✝<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>π : δ' → Type u_6<VAR>π' : δ' → Type u_7<VAR>inst✝² : (x : δ') → MeasurableSpace (π x)<VAR>inst✝¹ : (x : δ') → MeasurableSpace (π' x)<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_8<VAR>inst✝ : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>i : Fin (n + 1)<GOAL>Measurable fun x => (Equiv.piFinSuccAbove α i).symm x i
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α✝<VAR>inst✝⁶ : MeasurableSpace α✝<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>π : δ' → Type u_6<VAR>π' : δ' → Type u_7<VAR>inst✝² : (x : δ') → MeasurableSpace (π x)<VAR>inst✝¹ : (x : δ') → MeasurableSpace (π' x)<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_8<VAR>inst✝ : (i : Fin (n + 1)) → MeasurableSpace (α i)<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>Measurable fun x => (Equiv.piFinSuccAbove α i).symm x (i.succAbove j)
<VAR>X : Sort ?u.71899<VAR>inst✝ : DecidableEq X<VAR>x : X<VAR>Y : Sort ?u.71935<VAR>f : { x' // x' ≠ x } → Y<VAR>y : Y<GOAL>(fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y) ∘ Subtype.val = f
<VAR>X : Sort ?u.71899<VAR>inst✝ : DecidableEq X<VAR>x : X<VAR>Y : Sort ?u.71935<VAR>f : { x' // x' ≠ x } → Y<VAR>y : Y<VAR>x' : { x' // x' ≠ x }<GOAL>((fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y) ∘ Subtype.val) x' = f x'
<VAR>X : Sort ?u.71899<VAR>inst✝ : DecidableEq X<VAR>x : X<VAR>Y : Sort ?u.71935<VAR>f : { x' // x' ≠ x } → Y<VAR>y : Y<VAR>x' : { x' // x' ≠ x }<GOAL>↑x' = x → y = f x'
<VAR>X : Sort ?u.71899<VAR>inst✝ : DecidableEq X<VAR>x : X<VAR>Y : Sort ?u.71935<VAR>f : { x' // x' ≠ x } → Y<VAR>y : Y<VAR>x' : { x' // x' ≠ x }<VAR>w : ↑x' = x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>u : Finset α<GOAL>u ∈ Ico s t ↔ u ∈ image (fun x => s ∪ x) (t \ s).ssubsets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>u : Finset α<GOAL>s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x✝² x✝¹ : Scheme<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>Surjective x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) x✝
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<GOAL>(mkMetric m) s ≤ liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<GOAL>⨆ r, ⨆ (_ : 0 < r), ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<GOAL>⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>c : ℝ≥0∞<VAR>hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c<GOAL>⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ c
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>c : ℝ≥0∞<VAR>hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c<VAR>n : β<VAR>hn : ∑' (i : ι n), m (diam (t n i)) < c<VAR>hrn : r n < ε<VAR>htn : ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hstn : s ⊆ ⋃ i, t n i<GOAL>⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ c
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>c : ℝ≥0∞<VAR>hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c<VAR>n : β<VAR>hn : ∑' (i : ι n), m (diam (t n i)) < c<VAR>hrn : r n < ε<VAR>htn : ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hstn : s ⊆ ⋃ i, t n i<VAR>u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b<GOAL>⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n)) ≤ c
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>c : ℝ≥0∞<VAR>hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c<VAR>n : β<VAR>hn : ∑' (i : ι n), m (diam (t n i)) < c<VAR>hrn : r n < ε<VAR>htn : ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hstn : s ⊆ ⋃ i, t n i<VAR>u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b<GOAL>⨅ (_ : ∀ (n : ℕ), diam (u n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (diam (u n)) ≤ c
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>c : ℝ≥0∞<VAR>hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c<VAR>n : β<VAR>hn : ∑' (i : ι n), m (diam (t n i)) < c<VAR>hrn : r n < ε<VAR>htn : ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hstn : s ⊆ ⋃ i, t n i<VAR>u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b<VAR>j : ℕ<GOAL>diam (u j) ≤ ε
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁴ : EMetricSpace X<VAR>inst✝³ : EMetricSpace Y<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : BorelSpace X<VAR>β : Type u_4<VAR>ι : β → Type u_5<VAR>inst✝ : ∀ (n : β), Countable (ι n)<VAR>s : Set X<VAR>l : Filter β<VAR>r : β → ℝ≥0∞<VAR>hr : Tendsto r l (𝓝 0)<VAR>t : (n : β) → ι n → Set X<VAR>ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>this : (n : β) → Encodable (ι n)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>c : ℝ≥0∞<VAR>hc : liminf (fun n => ∑' (i : ι n), m (diam (t n i))) l < c<VAR>n : β<VAR>hn : ∑' (i : ι n), m (diam (t n i)) < c<VAR>hrn : r n < ε<VAR>htn : ∀ (i : ι n), diam (t n i) ≤ r n<VAR>hstn : s ⊆ ⋃ i, t n i<VAR>u : ℕ → Set X := fun j => ⋃ b ∈ decode₂ (ι n) j, t n b<GOAL>∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (diam (u n)) ≤ c
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>a : α<GOAL>Measurable ((fun p => κ.rnDerivAux η p.1 p.2) ∘ fun x => (a, x))
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : IsCompact s<GOAL>IsCompact (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : IsCompact s<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : μ.everywherePosSubset s = s \ u<GOAL>IsCompact (μ.everywherePosSubset s)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : IsCompact s<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : μ.everywherePosSubset s = s \ u<GOAL>IsCompact (s \ u)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>↑(round x) ≤ x + 1 / 2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimit (constPUnitFunctor C)<VAR>x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})<VAR>h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}<GOAL>IsConnected C
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimit (constPUnitFunctor C)<VAR>x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})<VAR>h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}<VAR>this : Nonempty C<GOAL>IsConnected C
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimit (constPUnitFunctor C)<VAR>x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})<VAR>h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}<VAR>this : Nonempty C<VAR>c d : C<GOAL>Zigzag c d
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimit (constPUnitFunctor C)<VAR>x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})<VAR>h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}<VAR>this : Nonempty C<VAR>c d : C<GOAL>EqvGen (Quot.Rel (constPUnitFunctor C)) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>toMonoidHom✝¹ : R →* R'<VAR>map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0<VAR>toMonoidHom✝ : R →* R'<VAR>map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0<VAR>h : ∀ (a : R), { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } a = { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a<GOAL>toMonoidHom✝¹ = toMonoidHom✝
<VAR>m n✝¹ n✝ a✝ n : ℕ<VAR>hpos : NeZero n<VAR>a : ZMod n<GOAL>a.valMinAbs.natAbs = min a.val (n - a.val)
<VAR>m n✝¹ n✝ a✝ n : ℕ<VAR>hpos : NeZero n<VAR>a : ZMod n<GOAL>(if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = min a.val (n - a.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ⩿ b<GOAL>a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ⩿ b<GOAL>c = a ∨ c = b → a ≤ c ∧ c ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>b c : α<VAR>h : c ⩿ b<GOAL>c ≤ c ∧ c ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a c : α<VAR>h : a ⩿ c<GOAL>a ≤ c ∧ c ≤ c
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>ι α : Type u<VAR>t : ι → Set α<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>#↑(⋃ i, t i) < c ↔ ∀ (i : ι), #↑(t i) < c
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>ι α : Type u<VAR>t : ι → Set α<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>h : ∀ (i : ι), #↑(t i) < c<GOAL>#↑(⋃ i, t i) < c
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>ι α : Type u<VAR>t : ι → Set α<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>h : ∀ (i : ι), #↑(t i) < c<GOAL>#↑(range fun i => t i) * ⨆ s, #↑↑s < c
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>ι α : Type u<VAR>t : ι → Set α<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>h : ∀ (i : ι), #↑(t i) < c<GOAL>⨆ s, #↑↑s < c
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>ι α : Type u<VAR>t : ι → Set α<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<VAR>h : ∀ (i : ι), #↑(t i) < c<GOAL>∀ (i : ↑(range fun i => t i)), #↑↑i < c
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffAt 𝕜 n f x<GOAL>ContinuousAt f 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>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<GOAL>smulRight 1 (deriv f x) = fderiv 𝕜 f x
<VAR>R : Type u_1<VAR>l : ℕ<VAR>hl : Squarefree l<GOAL>μ l ^ 2 = 1
<VAR>f : ℍ → ℂ<GOAL>IsBoundedAtImInfty f ↔ ∃ M A, ∀ (z : ℍ), A ≤ z.im → Complex.abs (f z) ≤ M
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : SimplicialCategory C<VAR>K L L' L'' : C<VAR>g : L ⟶ L'<VAR>g' : L' ⟶ L''<GOAL>(ρ_ (sHom K L)).inv ≫ sHom K L ◁ (homEquiv L L'') (g ≫ g') ≫ sHomComp K L L'' = ((ρ_ (sHom K L)).inv ≫ sHom K L ◁ (homEquiv L L') g ≫ sHomComp K L L') ≫ (ρ_ (sHom K L')).inv ≫ sHom K L' ◁ (homEquiv L' L'') g' ≫ sHomComp K L' L''