ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>S : Submonoid R<GOAL>Subsingleton (LocalizedModule S M) ↔ LinearMap.ker (mkLinearMap S M) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>S : Submonoid R<GOAL>Subsingleton (LocalizedModule S M) ↔ ⊤ ≤ LinearMap.ker (mkLinearMap S M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>S : Submonoid R<VAR>H : ⊤ ≤ LinearMap.ker (mkLinearMap S M)<VAR>x : LocalizedModule S M<GOAL>x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>S : Submonoid R<VAR>H : ⊤ ≤ LinearMap.ker (mkLinearMap S M)<VAR>x : M<VAR>s : ↥S<GOAL>Function.uncurry (IsLocalizedModule.mk' (mkLinearMap S M)) (x, s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hf : AEStronglyMeasurable f ρ<GOAL>AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)<GOAL>AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>s✝ : WSeq α<VAR>s1 s2 : Computation (List α)<VAR>l' : List α<VAR>s : WSeq α<VAR>h : s1 = Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l' ++ l, s) ∧ s2 = Computation.map (fun x => l.reverse ++ x) (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l', s))<GOAL>Computation.BisimO (fun c1 c2 => ∃ l' s, c1 = Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l' ++ l, s) ∧ c2 = Computation.map (fun x => l.reverse ++ x) (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l', s))) s1.destruct s2.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>s✝ : WSeq α<VAR>s1 s2 : Computation (List α)<VAR>l' : List α<VAR>s : WSeq α<VAR>h : s1 = Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l' ++ l, s) ∧ s2 = Computation.map (fun x => l.reverse ++ x) (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l', s))<GOAL>Computation.BisimO (fun c1 c2 => ∃ l' s, c1 = Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l' ++ l, s) ∧ c2 = Computation.map (fun x => l.reverse ++ x) (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l', s))) (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l' ++ l, s)).destruct (Computation.map (fun x => l.reverse ++ x) (Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l', s))).destruct
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.92908, u_1} J<VAR>inst✝ : Category.{?u.93383, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>s : ↑(F ⋙ coyoneda.obj (op X)).sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>𝟙 X ≫ ↑s j' = ↑s j ≫ F.map f
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.92908, u_1} J<VAR>inst✝ : Category.{?u.93383, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>s : ↑(F ⋙ coyoneda.obj (op X)).sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>↑s j' = ↑s j ≫ F.map f
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.92908, u_1} J<VAR>inst✝ : Category.{?u.93383, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>τ : (const J).obj X ⟶ F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>(F ⋙ coyoneda.obj (op X)).map f (τ.app j) = τ.app j'
<VAR>L : Language<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : L.Structure M<VAR>inst✝⁶ : L.Structure N✝<VAR>inst✝⁵ : L.Structure P<VAR>inst✝⁴ : L.Structure Q<VAR>N : Type u_5<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L[[M]].Structure N<VAR>inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N<VAR>inst✝ : N ⊨ L.elementaryDiagram M<VAR>n : ℕ<VAR>φ : L.Formula (Fin n)<VAR>x : Fin n → M<GOAL>φ.Realize ((constantMap ∘ Sum.inr) ∘ x) ↔ φ.Realize x
<VAR>L : Language<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : L.Structure M<VAR>inst✝⁶ : L.Structure N✝<VAR>inst✝⁵ : L.Structure P<VAR>inst✝⁴ : L.Structure Q<VAR>N : Type u_5<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L[[M]].Structure N<VAR>inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N<VAR>inst✝ : N ⊨ L.elementaryDiagram M<VAR>n : ℕ<VAR>φ : L.Formula (Fin n)<VAR>x : Fin n → M<GOAL>φ.Realize ((constantMap ∘ Sum.inr) ∘ x) ↔ N ⊨ (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls
<VAR>L : Language<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : L.Structure M<VAR>inst✝⁶ : L.Structure N✝<VAR>inst✝⁵ : L.Structure P<VAR>inst✝⁴ : L.Structure Q<VAR>N : Type u_5<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L[[M]].Structure N<VAR>inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N<VAR>inst✝ : N ⊨ L.elementaryDiagram M<VAR>n : ℕ<VAR>φ : L.Formula (Fin n)<VAR>x : Fin n → M<GOAL>M ⊨ (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls ↔ φ.Realize x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s✝ s₁ s₂ : Finset ι<VAR>t✝ t₁ t₂ : (i : ι) → Finset (α i)<VAR>f✝ : (i : ι) × α i → β<VAR>inst✝ : CompleteLattice β<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (α i)<VAR>f : Sigma α → β<GOAL>⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : SeminormedAddCommGroup α<VAR>v : n → α<GOAL>‖row ι v‖₊ = ∑ i : n, ‖v i‖₊
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Inducing f<VAR>h : StableUnderSpecialization (Set.range f)<VAR>x y : X<VAR>e : flip (fun x x_1 => x ⤳ x_1) (f y) (f x)<GOAL>∃ a', flip (fun x x_1 => x ⤳ x_1) a' x ∧ f a' = f y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>s t : Set α<VAR>a✝ b✝ x y : α<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>h : g.IsCycleOn s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>(g.extendDomain f).SameCycle ((Subtype.val ∘ ⇑f) a) ((Subtype.val ∘ ⇑f) b)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : Nontrivial R<VAR>X Y : R<VAR>h : W'.toAffine.Nonsingular X Y<VAR>h0 : fromAffine (Affine.Point.some h) = 0<GOAL>False
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : Nontrivial R<VAR>X Y : R<VAR>h : W'.toAffine.Nonsingular X Y<VAR>h0 : fromAffine (Affine.Point.some h) = 0<VAR>u : Rˣ<VAR>eq : (fun m => m • ![1, 1, 0]) u = ![X, Y, 1]<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : CoheytingAlgebra α<VAR>a : α<GOAL>a ∆ (￢a) = ⊤
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>u : F α → α<VAR>x y : (P F).W<VAR>h : Wequiv x y<GOAL>recF u x = recF u y
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>K✝ : Type u_3<VAR>inst✝⁹ : CommSemiring E✝<VAR>inst✝⁸ : Semiring K✝<VAR>inst✝⁷ : SMul F✝ E✝<VAR>inst✝⁶ : Algebra E✝ K✝<VAR>inst✝⁵ : CommSemiring F✝<VAR>inst✝⁴ : Algebra F✝ K✝<VAR>inst✝³ : IsScalarTower F✝ E✝ K✝<VAR>L : Subalgebra F✝ K✝<VAR>F : Type u_4<VAR>inst✝² : CommSemiring F<VAR>E : Type u_5<VAR>inst✝¹ : CommSemiring E<VAR>inst✝ : Algebra F E<VAR>K : Subalgebra F E<VAR>S : Set E<GOAL>Subalgebra.restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>-(J l R * Aᵀ * J l R * A) = -J l R * (Aᵀ * J l R * A)
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>-J l R * (Aᵀ * J l R * A) = -J l R * J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : Aᵀ * J l R * A = J l R<GOAL>-J l R * (Aᵀ * J l R * A) = -J l R * J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>-J l R * J l R = -1 • (J l R * J l R)
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>-1 • (J l R * J l R) = -1 • -1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>-1 • -1 = 1
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>a.im ^ 2 = -↑(normSq a.im)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a x : G<GOAL>x ∈ ⋃ k, op (a * ↑k) • ↑H ↔ x ∈ doset a ↑H ↑K
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a x : G<GOAL>(∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>G.IsNClique 1 s ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>(∃ a, s = {a}) → G.IsClique ↑s
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>hs : autoParam s.Finite _auto✝<GOAL>s.ncard = (Finite.toFinset hs).card
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Semifield R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : HasContinuousInv₀ R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ : R → R<VAR>a✝ : A<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<VAR>a : Aˣ<VAR>hf : autoParam (ContinuousOn f ((fun x => x⁻¹) '' spectrum R ↑a)) _auto✝<VAR>ha : autoParam (p ↑a) _auto✝<GOAL>cfc (fun x => f x⁻¹) ↑a = cfc f ↑a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] ∅<GOAL>s ∪ t =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] ∅<GOAL>s = s ∪ ∅
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{v}<GOAL>lift.{u, v} a < lift.{u, v} b ↔ a < b
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.203239}<VAR>ι α : Type u<VAR>A : ι → Set α<VAR>s : Set ι<GOAL>#↑(⋃ x ∈ s, A x) ≤ #↑s * ⨆ x, #↑(A ↑x)
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.203239}<VAR>ι α : Type u<VAR>A : ι → Set α<VAR>s : Set ι<GOAL>#↑(⋃ x, A ↑x) ≤ #↑s * ⨆ x, #↑(A ↑x)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(X ^ n).trailingDegree = ↑n
<VAR>q₁ q₂ : ℚ<GOAL>(q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
<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 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : MapsTo h s s'<GOAL>HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s 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 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : MapsTo h s s'<GOAL>HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>y : Set β<GOAL>minimals r (⇑f ⁻¹' y) = ⇑f ⁻¹' minimals s (y ∩ range ⇑f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>y : Set β<GOAL>⇑f ⁻¹' minimals s (y ∩ range ⇑f) = univ ∩ ⇑f ⁻¹' minimals s (⇑f '' univ ∩ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<VAR>f : α → β<VAR>h : ker f ≤ r<VAR>hf : Surjective f<GOAL>r.map f = r.mapOfSurjective f h hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<VAR>f : α → β<VAR>h : ker f ≤ r<VAR>hf : Surjective f<GOAL>r.map f = EqvGen.Setoid Setoid.r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c x : α<GOAL>x ∈ Iic a \ {a} ↔ x ∈ Iio a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>k : Fin n → ℕ<VAR>x : Fin n → R<VAR>hk : Function.Injective k<VAR>hx : ∀ (i : Fin n), x i ≠ 0<GOAL>(∑ i : Fin n, C (x i) * X ^ k i).support.card = n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>k : Fin n → ℕ<VAR>x : Fin n → R<VAR>hk : Function.Injective k<VAR>hx : ∀ (i : Fin n), x i ≠ 0<GOAL>(∑ i : Fin n, C (x i) * X ^ k i).support = image k univ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>n : ℕ<VAR>k : Fin n → ℕ<VAR>x : Fin n → R<VAR>hk : Function.Injective k<VAR>hx : ∀ (i : Fin n), x i ≠ 0<GOAL>∀ (a : ℕ), (∑ x_1 : Fin n, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ ∃ a_1, k a_1 = a
<VAR>M✝ : Type u_1<VAR>inst✝² : Monoid M✝<VAR>s✝ : Set M✝<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>s : Set M<VAR>hs : IsSubmonoid s<VAR>m : Multiset M<GOAL>(∀ a ∈ m, a ∈ s) → m.prod ∈ s
<VAR>M✝ : Type u_1<VAR>inst✝² : Monoid M✝<VAR>s✝ : Set M✝<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>s : Set M<VAR>hs : IsSubmonoid s<VAR>m : Multiset M<VAR>l : List M<VAR>hl : ∀ a ∈ ⟦l⟧, a ∈ s<GOAL>Multiset.prod ⟦l⟧ ∈ s
<VAR>M✝ : Type u_1<VAR>inst✝² : Monoid M✝<VAR>s✝ : Set M✝<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>s : Set M<VAR>hs : IsSubmonoid s<VAR>m : Multiset M<VAR>l : List M<VAR>hl : ∀ a ∈ ⟦l⟧, a ∈ s<GOAL>l.prod ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<GOAL>∫⁻ (a : α), ↑‖(-f) a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<GOAL>A.adjugateᵀ.map star = (Aᵀ.map star).adjugate
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<VAR>this : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate<GOAL>A.adjugateᵀ.map star = (Aᵀ.map star).adjugate
<VAR>n : ℕ+<VAR>a : ℕ<VAR>h : a ∣ ↑n<GOAL>0 < a
<VAR>n : ℕ+<VAR>a : ℕ<VAR>h : a ∣ ↑n<GOAL>a ≠ 0
<VAR>n : ℕ+<VAR>a : ℕ<VAR>h : 0 ∣ ↑n<VAR>hzero : a = 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>s : (x : B) → E x<VAR>x₀ : B<GOAL>ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (s x)) x₀ ↔ ContMDiffAt IB 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>s : (x : B) → E x<VAR>x₀ : B<GOAL>ContMDiffAt IB 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) x₀ → ContMDiffAt IB IB n (fun x => x) x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>s : (x : B) → E x<VAR>x₀ : B<VAR>a✝ : ContMDiffAt IB 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) x₀<GOAL>ContMDiffAt IB IB n (fun x => x) x₀
<VAR>x y : ℝ<VAR>h : 0 < x<VAR>h₁ : 0 < y<GOAL>log x ≤ log y ↔ x ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : a ∉ s → f a = 1<GOAL>∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : a ∉ s → f a = 1<VAR>x : α<VAR>hx : x ∈ mulSupport f<GOAL>x ∈ insert a s → x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>b : α<VAR>s t : Set α<VAR>x : α<VAR>hx : x ∈ mulSupport f<VAR>h : x ∉ s → f x = 1<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : a ∉ s → f a = 1<VAR>x : α<VAR>hx : x ∈ mulSupport f<VAR>hxs : x ∈ s<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>(insert a s \ {b}).ncard = s.ncard