ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<VAR>x✝¹ x✝ : E →ₗ.[R] F<VAR>hy₁ : f.graph.topologicalClosure = x✝¹.graph<VAR>hy₂ : f.graph.topologicalClosure = x✝.graph<GOAL>x✝¹.graph = x✝.graph
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>h : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this : IsAffine ↑U<GOAL>((↑U).isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom ⋯).op)).val.base ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(Spec Γ(X, U)).toPresheafedSpace
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>h : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this : IsAffine ↑U<VAR>e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↑↑(Spec (X.presheaf.obj (op U))).toPresheafedSpace<GOAL>⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(↑U).toPresheafedSpace
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>h : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this : IsAffine ↑U<VAR>e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↑↑(Spec (X.presheaf.obj (op U))).toPresheafedSpace<GOAL>↑⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = ↑(genericPoint ↑↑(↑U).toPresheafedSpace)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f : E → F<VAR>R : ℝ<VAR>s : Set E<VAR>hR : 0 < R<GOAL>∫ (x : E) in s, f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ (x : E) in R • s, f x ∂μ
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<GOAL>∃ n < p, x - ↑n ∈ maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<GOAL>∃ n < p, ‖x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<GOAL>∃ n < p, ‖x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<GOAL>∃ n < p, ‖x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℤ<VAR>hzn : 0 ≤ n<VAR>hnp : n < ↑p<VAR>hn : ‖⟨↑r, H⟩ - ↑n‖ < 1<GOAL>∃ n < p, ‖x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℕ<VAR>hnp : ↑n < ↑p<VAR>hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1<GOAL>∃ n < p, ‖x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℕ<VAR>hnp : ↑n < ↑p<VAR>hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1<GOAL>n < p ∧ ‖x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℕ<VAR>hnp : ↑n < ↑p<VAR>hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1<GOAL>‖x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℕ<VAR>hnp : ↑n < ↑p<VAR>hn : ‖↑r - ↑↑↑n‖ < 1<GOAL>‖↑x - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℕ<VAR>hnp : ↑n < ↑p<VAR>hn : ‖↑r - ↑↑↑n‖ < 1<GOAL>‖↑x - ↑r + (↑r - ↑n)‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℕ<VAR>hnp : ↑n < ↑p<VAR>hn : ‖↑r - ↑↑↑n‖ < 1<GOAL>max ‖↑x - ↑r‖ ‖↑r - ↑n‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ : ℚ<VAR>x : ℤ_[p]<VAR>r : ℚ<VAR>hr : ‖↑x - ↑r‖ < 1<VAR>H : ‖↑r‖ ≤ 1<VAR>n : ℕ<VAR>hnp : ↑n < ↑p<VAR>hn : ‖↑r - ↑↑↑n‖ < 1<GOAL>‖↑r - ↑n‖ < 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>L : IntermediateField F E<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>x : E<VAR>h : x ∈ L<GOAL>IsSeparable F x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : SurjOn f₁ s t<VAR>H : EqOn f₁ f₂ s<GOAL>SurjOn f₂ s t
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Embedding ⇑f<VAR>hg : Embedding ⇑g<GOAL>Function.Injective ⇑(prod.map f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Embedding ⇑f<VAR>hg : Embedding ⇑g<VAR>this : Mono f<GOAL>Function.Injective ⇑(prod.map f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>W X Y Z : TopCat<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>hf : Embedding ⇑f<VAR>hg : Embedding ⇑g<VAR>this✝ : Mono f<VAR>this : Mono g<GOAL>Function.Injective ⇑(prod.map f g)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>χ : MulChar F R<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ ζ ∈ rootsOfUnity ⟨orderOf χ, ⋯⟩ R, ↑ζ = χ a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>χ : MulChar F R<VAR>a : F<VAR>ha : a ≠ 0<VAR>hu : IsUnit (χ a)<GOAL>∃ ζ ∈ rootsOfUnity ⟨orderOf χ, ⋯⟩ R, ↑ζ = χ a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>χ : MulChar F R<VAR>a : F<VAR>ha : a ≠ 0<VAR>hu : IsUnit (χ a)<GOAL>hu.unit ∈ rootsOfUnity ⟨orderOf χ, ⋯⟩ R
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>S : Set F<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : F →+* K<VAR>s : Set K<VAR>hs : IsSubfield s<VAR>a : F<VAR>ha : f a ∈ s<GOAL>f a⁻¹ ∈ s
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>S : Set F<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : F →+* K<VAR>s : Set K<VAR>hs : IsSubfield s<VAR>a : F<VAR>ha : f a ∈ s<GOAL>(f a)⁻¹ ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>f g : ι → α<VAR>B : BddAbove (range g)<VAR>H : ∀ (x : ι), f x ≤ g x<GOAL>iSup f ≤ iSup g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>f g : ι → α<VAR>B : BddAbove (range g)<VAR>H : ∀ (x : ι), f x ≤ g x<VAR>h✝ : IsEmpty ι<GOAL>iSup f ≤ iSup g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>f g : ι → α<VAR>B : BddAbove (range g)<VAR>H : ∀ (x : ι), f x ≤ g x<VAR>h✝ : Nonempty ι<GOAL>iSup f ≤ iSup g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>c : α<GOAL>c ∈ Ici (⨆ i, f i) ↔ c ∈ ⨆ i, Ici (f i)
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>f u v : R⟦X⟧<VAR>hu : u * v = 1<VAR>hv : v * u = 1<VAR>hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f<GOAL>f.order = 0
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>f u v : R⟦X⟧<VAR>hu : u * v = 1<VAR>hv : v * u = 1<VAR>hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f<GOAL>f.order = 0 ∧ ?intro.mk.b
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>f u v : R⟦X⟧<VAR>hu : u * v = 1<VAR>hv : v * u = 1<VAR>hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f<GOAL>Prop
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>f u v : R⟦X⟧<VAR>hu : u * v = 1<VAR>hv : v * u = 1<VAR>hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f<GOAL>(↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.101103 ≤ (u * v).order
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>f u v : R⟦X⟧<VAR>hu : u * v = 1<VAR>hv : v * u = 1<VAR>hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f<GOAL>PartENat
<VAR>α : Type u_1<VAR>l l₁ l₂✝ : List α<VAR>p : α → Prop<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₂ : List α<GOAL>a ∈ [].bagInter l₂ ↔ a ∈ [] ∧ a ∈ l₂
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ prod.fst = prod.fst ≫ prod.fst
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<VAR>f : P ≃ᵃ[R] P'<GOAL>Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>n : ℕ<VAR>c d : List Γ'<GOAL>Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trList [n]) [] c d } { l := some q, var := none, stk := elim (trList [n.succ]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>n : ℕ<VAR>c d : List Γ'<GOAL>Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trNum ↑n ++ [Γ'.cons]) [] c d } { l := some q, var := none, stk := elim (trNum (↑n).succ ++ [Γ'.cons]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>n : ℕ<VAR>c d : List Γ'<VAR>a : PosNum<GOAL>Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) [] c d } { l := some q, var := none, stk := elim (trPosNum a.succ ++ [Γ'.cons]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>n : ℕ<VAR>c d : List Γ'<VAR>a : PosNum<GOAL>∀ (l₁ : List Γ'), ∃ l₁' l₂' s', l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧ Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum a ++ [Γ'.cons]) l₁ c d } { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
<VAR>m c : ℤ<GOAL>1 + (2 * c + 1) / 2 * 2 = 2 * c + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s : Finset γ<VAR>f : γ → α<VAR>g : γ → β<VAR>this : DecidableEq γ<GOAL>∀ ⦃a : γ⦄ {s : Finset γ}, a ∉ s → (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x) → (∏ x ∈ insert a s, f x, ∏ x ∈ insert a s, g x) = ∏ x ∈ insert a s, (f x, g x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>g : N →ₙ* P<VAR>f₁ f₂ : M →ₙ* N<VAR>hg : Function.Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>x : M<GOAL>g (f₁ x) = g (f₂ x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h0 : p ≠ 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>h0 : p ≠ 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm' f p.toReal μ = 0 ↔ f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>p : α → Prop<VAR>u : List β<GOAL>Forall₂ (fun a b => p a ∧ R a b) [] u ↔ (∀ (a : α), a ∈ [] → p a) ∧ Forall₂ R [] u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<VAR>u : List β<GOAL>Forall₂ (fun a b => p a ∧ R a b) (a :: l) u ↔ (∀ (a_1 : α), a_1 ∈ a :: l → p a_1) ∧ Forall₂ R (a :: l) u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<VAR>u : List β<GOAL>(p a ∧ ∃ x, R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ x_1, Forall₂ R l x_1 ∧ u = x :: x_1) ↔ p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ b, R a b ∧ ∃ x, Forall₂ R l x ∧ u = b :: x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<GOAL>cthickening δ ∅ = ∅
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<GOAL>𝒜.shatterer = 𝒜 ↔ IsLowerSet ↑𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : 𝒜.shatterer = 𝒜<GOAL>IsLowerSet ↑𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : IsLowerSet ↑𝒜<VAR>s : Finset α<VAR>hs : s ∈ 𝒜.shatterer<GOAL>s ∈ 𝒜
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>hf' : UniformCauchySeqOnFilter f' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : Cauchy (map (fun n => f n x) l)<GOAL>UniformCauchySeqOnFilter f l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>hf' : UniformCauchySeqOnFilter f' l (𝓝 x)<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2<GOAL>UniformCauchySeqOnFilter f l (𝓝 x)
<VAR>J : Type v'<VAR>inst✝⁸ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>D : Type u''<VAR>inst✝⁶ : Category.{v'', u''} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : Adhesive D<VAR>inst✝⁴ : HasPullbacks C<VAR>inst✝³ : HasPushouts C<VAR>inst✝² : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape WalkingSpan F<VAR>inst✝ : F.ReflectsIsomorphisms<VAR>this✝ : ReflectsLimitsOfShape WalkingCospan F<VAR>this : ReflectsColimitsOfShape WalkingSpan F<GOAL>Adhesive C
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>0⁻¹ = (starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<VAR>h₀ : z ≠ 0<GOAL>z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h_meas_s : MeasurableSet s<GOAL>(μ - ν).restrict s = μ.restrict s - ν.restrict s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h_meas_s : MeasurableSet s<GOAL>(sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h_meas_s : MeasurableSet s<VAR>h_nonempty : {d | μ ≤ d + ν}.Nonempty<GOAL>(sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h_meas_s : MeasurableSet s<VAR>h_nonempty : {d | μ ≤ d + ν}.Nonempty<GOAL>sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν}) = sInf {d | μ.restrict s ≤ d + ν.restrict s}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h_meas_s : MeasurableSet s<VAR>h_nonempty : {d | μ ≤ d + ν}.Nonempty<GOAL>sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν}) ≤ sInf {d | μ.restrict s ≤ d + ν.restrict s}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h_meas_s : MeasurableSet s<VAR>h_nonempty : {d | μ ≤ d + ν}.Nonempty<GOAL>sInf {d | μ.restrict s ≤ d + ν.restrict s} ≤ sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν})
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>x ≤ y ^ z ↔ log x ≤ z * log y
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>y z a b : α<VAR>ha : a ∣ y<VAR>hb : b ∣ z<VAR>H1 : IsRelPrime (a * b) z<VAR>H2 : a * b ∣ y * z<VAR>h : IsPrimal (a * b)<GOAL>a * b ∣ y
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M : Sublattice α<VAR>f✝ : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>f : ι → Sublattice α<GOAL>a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M : Sublattice α<VAR>f✝ : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>f : ι → Sublattice α<GOAL>a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Semiring α<VAR>inst✝ : DecidableEq n<VAR>M : Matrix l m α<VAR>f : m ≃. n<VAR>i : l<VAR>j : n<GOAL>(M * f.toMatrix) i j = Option.casesOn (f.symm j) 0 fun fj => M i fj
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Semiring α<VAR>inst✝ : DecidableEq n<VAR>M : Matrix l m α<VAR>f : m ≃. n<VAR>i : l<VAR>j : n<GOAL>(∑ j_1 : m, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) (f.symm j)
<VAR>n : ℕ+<VAR>m : ℕ<VAR>u : PrimeMultiset := n.factorMultiset<GOAL>(n ^ m).factorMultiset = m • n.factorMultiset
<VAR>n : ℕ+<VAR>m : ℕ<VAR>u : PrimeMultiset := n.factorMultiset<VAR>this : n = u.prod<GOAL>(n ^ m).factorMultiset = m • n.factorMultiset
<VAR>n : ℕ+<VAR>m : ℕ<VAR>u : PrimeMultiset := n.factorMultiset<VAR>this : n = u.prod<GOAL>(m • u).prod.factorMultiset = m • u.prod.factorMultiset
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>padicValNat p (p * n)! = padicValNat p n ! + n
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>↑(padicValNat p (p * n)!) = ↑(padicValNat p n ! + n)
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>multiplicity p (p * n)! = multiplicity p n ! + ↑n
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹³ : Field A<VAR>inst✝¹² : Ring B<VAR>inst✝¹¹ : Algebra A B<VAR>x : B<VAR>R : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>L : Type u_6<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : CommRing L<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsScalarTower R S L<VAR>s : S<GOAL>minpoly K ((algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹³ : Field A<VAR>inst✝¹² : Ring B<VAR>inst✝¹¹ : Algebra A B<VAR>x : B<VAR>R : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>L : Type u_6<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : CommRing L<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsScalarTower R S L<VAR>s : S<GOAL>(Polynomial.aeval ((algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹³ : Field A<VAR>inst✝¹² : Ring B<VAR>inst✝¹¹ : Algebra A B<VAR>x : B<VAR>R : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>L : Type u_6<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : CommRing L<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsScalarTower R S L<VAR>s : S<GOAL>(algebraMap K L).comp (algebraMap R K) = (algebraMap S L).comp (algebraMap R S)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<GOAL>ζ ^ ↑k = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<GOAL>ζ ^ k = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>val✝ : Encodable β<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : IsEmpty β<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : Nonempty β<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : Nonempty β<VAR>inhabited_h : Inhabited β<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<VAR>val✝ : Encodable β<VAR>h✝ : Nonempty β<VAR>inhabited_h : Inhabited β<VAR>this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1) (hμs : μ s_1 < ⊤), (fun f => ∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c)