ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A✝ A' B B' : C<VAR>inst✝⁶ : HasBinaryCoproduct A✝ B<VAR>inst✝⁵ : HasBinaryCoproduct A' B'<VAR>inst✝⁴ : HasBinaryCoproduct (F.obj A✝) (F.obj B)<VAR>inst✝³ : HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>inst✝² : HasBinaryCoproducts C<VAR>inst✝¹ : HasBinaryCoproducts D<VAR>A : C<VAR>inst✝ : ∀ (B : C), IsIso (coprodComparison F A B)<GOAL>IsIso { app := fun B => coprodComparison F A B, naturality := ⋯ }
<VAR>α : Type u<VAR>r : ℕ → ℕ → Prop<VAR>n a : ℕ<GOAL>Chain r a (range n.succ) ↔ r a 0 ∧ ∀ m < n, r m m.succ
<VAR>α : Type u<VAR>r : ℕ → ℕ → Prop<VAR>n a : ℕ<GOAL>r a 0 → (Chain r 0 (map succ (range n)) ↔ Chain' r (0 :: map succ (range n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>z : Sym2 α<GOAL>z ∈ s.sym2 ↔ z ∈ image Sym2.mk (s ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>z : Sym2 α<VAR>x y : α<GOAL>s(x, y) ∈ s.sym2 ↔ s(x, y) ∈ image Sym2.mk (s ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>z : Sym2 α<VAR>x y : α<GOAL>x ∈ s ∧ y ∈ s ↔ ∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>h : n ≠ 2<GOAL>(Algebra.norm K) (ζ - 1) = ↑(↑n).minFac
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>h : n ≠ 2<VAR>this : 2 < n<GOAL>(Algebra.norm K) (ζ - 1) = ↑(↑n).minFac
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>h : n ≠ 2<VAR>this : 2 < n<VAR>hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }<GOAL>(Algebra.norm K) (ζ - 1) = ↑(↑n).minFac
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>h : n ≠ 2<VAR>this : 2 < n<VAR>hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }<GOAL>↑(eval 1 (cyclotomic ↑n ℤ)) = ↑(↑n).minFac
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>h : n ≠ 2<VAR>this : 2 < n<VAR>hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }<GOAL>↑(eval 1 (cyclotomic ((↑n).minFac ^ (↑n).factorization (↑n).minFac) ℤ)) = ↑(↑n).minFac
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>hn : IsPrimePow ↑n<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>h : n ≠ 2<VAR>this : 2 < n<VAR>hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }<VAR>k : ℕ<VAR>hk : (↑n).factorization (↑n).minFac = k + 1<GOAL>↑(eval 1 (cyclotomic ((↑n).minFac ^ (↑n).factorization (↑n).minFac) ℤ)) = ↑(↑n).minFac
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>↑((toEven Q) ((ι Q) m)) = e0 Q * (v Q) 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>Q : QuadraticForm R M<VAR>m : M<GOAL>↑((LinearMap.codRestrict (evenOdd (Q' Q) 0) (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) ⋯) m) = e0 Q * (v Q) 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>Q : QuadraticForm R M<VAR>m : M<GOAL>(LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m = e0 Q * (v Q) m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>q : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<GOAL>eval (f q) (cyclotomic n S) = f (eval q (cyclotomic n R))
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).leadingCoeff = a
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α → Part β<VAR>g : α → β → Part γ<VAR>hf : Monotone f<VAR>hf' : Continuous { toFun := f, monotone' := hf }<VAR>hg : Monotone g<VAR>hg' : Continuous { toFun := g, monotone' := hg }<VAR>c : Chain α<GOAL>({ toFun := f, monotone' := hf }.partBind { toFun := g, monotone' := hg }) (ωSup c) = ωSup (c.map ({ toFun := f, monotone' := hf }.partBind { toFun := g, monotone' := hg }))
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : α → Part β<VAR>g : α → β → Part γ<VAR>hf : Monotone f<VAR>hf' : Continuous { toFun := f, monotone' := hf }<VAR>hg : Monotone g<VAR>hg' : Continuous { toFun := g, monotone' := hg }<VAR>c : Chain α<GOAL>({ toFun := f, monotone' := hf }.partBind { toFun := g, monotone' := hg }) (ωSup c) = { toFun := f, monotone' := hf } (ωSup c) >>= { toFun := g, monotone' := hg } (ωSup c)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>k : ℕ<VAR>s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}<GOAL>sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>k : ℕ<VAR>s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}<VAR>hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s<GOAL>sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Function.Injective ((fun f => F.map f a) ∘ fun f => f.hom)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Function.Injective fun f => F.map f a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Function.Injective fun f => f.hom
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>-x ‖ y ↔ x ‖ -y
<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✝ : MeasurableSingletonClass α<VAR>c : ℝ≥0∞<GOAL>∑' (x : α), c = c * count univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ b, s.max = ↑b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>a : α<VAR>h✝ : a ∈ s<VAR>b : α<VAR>h : s.sup WithBot.some = ↑b<VAR>right✝ : a ≤ b<GOAL>∃ b, s.max = ↑b
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>B : BilinForm R M<VAR>v : M<VAR>x : CliffordAlgebra Q<GOAL>((changeFormAux Q B) v) (((changeFormAux Q B) v) x) = (Q v - (B v) v) • x
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>B : BilinForm R M<VAR>v : M<VAR>x : CliffordAlgebra Q<GOAL>(ι Q) v * ((ι Q) v * x - (contractLeft (B v)) x) - (contractLeft (B v)) ((ι Q) v * x - (contractLeft (B v)) x) = (Q v - (B v) v) • x
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (Fin 0 → α) → Prop<GOAL>Forall P ↔ ∀ (x : Fin 0 → α), P x
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (Fin 0 → α) → Prop<GOAL>P ![] ↔ P finZeroElim
<VAR>m n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>P : (Fin n.succ → α) → Prop<GOAL>Forall P ↔ ∀ (x : Fin n.succ → α), P x
<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>HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<GOAL>MDifferentiableWithinAt I I'' (g ∘ f) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f'✝ f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<VAR>f' : E →L[𝕜] E'<VAR>hf' : HasFDerivWithinAt (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) f' (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x))<GOAL>MDifferentiableWithinAt I I'' (g ∘ f) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f'✝ f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<VAR>f' : E →L[𝕜] E'<VAR>hf' : HasFDerivWithinAt (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) f' (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x))<VAR>F : HasMFDerivWithinAt I I' f s x f'<GOAL>MDifferentiableWithinAt I I'' (g ∘ f) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f'✝ f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g'✝ : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<VAR>f' : E →L[𝕜] E'<VAR>hf' : HasFDerivWithinAt (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) f' (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x))<VAR>F : HasMFDerivWithinAt I I' f s x f'<VAR>g' : E' →L[𝕜] E''<VAR>hg' : HasFDerivWithinAt (↑I'' ∘ (↑(chartAt H'' (g (f x))) ∘ g ∘ ↑(chartAt H' (f x)).symm) ∘ ↑I'.symm) g' (↑I'.symm ⁻¹' (↑(chartAt H' (f x)).symm ⁻¹' u) ∩ range ↑I') (↑I' (↑(chartAt H' (f x)) (f x)))<GOAL>MDifferentiableWithinAt I I'' (g ∘ f) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f'✝ f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g'✝ : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<VAR>f' : E →L[𝕜] E'<VAR>hf' : HasFDerivWithinAt (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) f' (↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' s) ∩ range ↑I) (↑I (↑(chartAt H x) x))<VAR>F : HasMFDerivWithinAt I I' f s x f'<VAR>g' : E' →L[𝕜] E''<VAR>hg' : HasFDerivWithinAt (↑I'' ∘ (↑(chartAt H'' (g (f x))) ∘ g ∘ ↑(chartAt H' (f x)).symm) ∘ ↑I'.symm) g' (↑I'.symm ⁻¹' (↑(chartAt H' (f x)).symm ⁻¹' u) ∩ range ↑I') (↑I' (↑(chartAt H' (f x)) (f x)))<VAR>G : HasMFDerivWithinAt I' I'' g u (f x) g'<GOAL>MDifferentiableWithinAt I I'' (g ∘ f) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(κ.swapRight.fst a) s = (κ.snd a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(κ a) {p | p.swap ∈ {p | p.1 ∈ s}} = (κ a) {p | p.2 ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s}
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁸ : Ring R✝<VAR>inst✝¹⁷ : Ring R'✝<VAR>inst✝¹⁶ : AddCommGroup M<VAR>inst✝¹⁵ : AddCommGroup M'<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R✝ M<VAR>inst✝¹² : Module R✝ M'<VAR>inst✝¹¹ : Module R✝ M₁<VAR>inst✝¹⁰ : Module R'✝ M'<VAR>inst✝⁹ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>R' : Type w'<VAR>S'✝ : Type v'<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : Ring S'✝<VAR>inst✝³ : Algebra R' S'✝<VAR>S' : Type v<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R' →+* R<VAR>j : S →+* S'<VAR>hi : Injective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'<GOAL>Module.rank R S ≤ Module.rank R' S'
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>g : B →+* C<VAR>f : A →+* B<VAR>hg : g.Finite<VAR>hf : f.Finite<VAR>this✝⁴ : Algebra A B := f.toAlgebra<VAR>this✝³ : Algebra B C := g.toAlgebra<VAR>this✝² : Algebra A C := (g.comp f).toAlgebra<VAR>this✝¹ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C<VAR>this✝ : Module.Finite A B := hf<VAR>this : Module.Finite B C := hg<GOAL>(g.comp f).Finite
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<GOAL>a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<GOAL>lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0
<VAR>α : Sort ?u.31587<VAR>β : Sort ?u.31609<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x₀ : { a // p a } → β<VAR>x : { a // ¬p a } → β<VAR>x✝ : { a // ¬p a }<VAR>a : α<VAR>h : ¬p a<GOAL>(if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩) = x ⟨a, h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hs : MeasurableSet s<GOAL>Integrable (s.indicator f) μ ↔ IntegrableOn f s μ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x : B<VAR>h : IsIntegral R x<VAR>n : ℕ<GOAL>x ∈ Algebra.adjoin R {x}
<VAR>α : Type u<VAR>β : Type u_1<VAR>n✝ : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 ≤ 0<VAR>n : ℕ<GOAL>if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n✝ : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 ≤ 0<VAR>n : ℕ<VAR>hx0 : x ≤ 0<GOAL>if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n✝ : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 ≤ 0<VAR>hx0 : x ≤ 0<VAR>n : ℕ<VAR>ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i<GOAL>if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range (n + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n✝ : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 ≤ 0<VAR>hx0 : x ≤ 0<VAR>n : ℕ<VAR>ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i<GOAL>if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>S : Submonoid R<VAR>inst✝ : OreSet S<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<GOAL>r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>hus : s.card = (s.biUnion t).card<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑(↑s)ᶜ<VAR>this : DecidableEq ι<GOAL>s'.card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card