ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(∃ a_1 ∈ P.parts.attach, b ∈ (Q ↑a_1 ⋯).parts) ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<GOAL>finrank (↥(subfield G F)) F ≤ Fintype.card G
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<GOAL>Module.rank (↥(subfield G F)) F ≤ ↑(Fintype.card G)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Ici a = Iic (a / c)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>b : Con (M × ↥S)<VAR>H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}<VAR>x✝² x✝¹ : M × ↥S<VAR>p : M<VAR>q : ↥S<VAR>x : M<VAR>y : ↥S<VAR>x✝ : (r' S) (p, q) (x, y)<VAR>t : ↥S<VAR>ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)<GOAL>b (p, q) (x, y)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>b : Con (M × ↥S)<VAR>H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}<VAR>x✝² x✝¹ : M × ↥S<VAR>p : M<VAR>q : ↥S<VAR>x : M<VAR>y : ↥S<VAR>x✝ : (r' S) (p, q) (x, y)<VAR>t : ↥S<VAR>ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)<GOAL>b (1 * (p, q)) (1 * (x, y))
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>b : Con (M × ↥S)<VAR>H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}<VAR>x✝² x✝¹ : M × ↥S<VAR>p : M<VAR>q : ↥S<VAR>x : M<VAR>y : ↥S<VAR>x✝ : (r' S) (p, q) (x, y)<VAR>t : ↥S<VAR>ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)<GOAL>b ((↑(t * y), t * y) * (p, q)) (1 * (x, y))
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>b : Con (M × ↥S)<VAR>H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}<VAR>x✝² x✝¹ : M × ↥S<VAR>p : M<VAR>q : ↥S<VAR>x : M<VAR>y : ↥S<VAR>x✝ : (r' S) (p, q) (x, y)<VAR>t : ↥S<VAR>ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)<GOAL>(↑(t * y), t * y) * (p, q) = (↑(t * q), t * q) * (x, y)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>b : Con (M × ↥S)<VAR>H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}<VAR>x✝² x✝¹ : M × ↥S<VAR>p : M<VAR>q : ↥S<VAR>x : M<VAR>y : ↥S<VAR>x✝ : (r' S) (p, q) (x, y)<VAR>t : ↥S<VAR>ht : ↑t * (↑y * p) = ↑t * (↑q * x)<GOAL>(↑t * ↑y * p, t * y * q) = (↑t * ↑q * x, t * q * y)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : (Matrix m m R)ˣ<VAR>N : Matrix m m R<GOAL>(↑M * N * ↑M⁻¹).det = N.det
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : LinearOrder α<VAR>a b c d : α<GOAL>a < b ⊔ c ↔ a < b ∨ a < c
<VAR>b : ℝ<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2
<VAR>b : ℝ<VAR>hb : b ≤ 0<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Ioi 0, ↑(rexp (-b * x ^ 2)) = ↑(√(π / b) / 2)
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>x✝ : ℝ<GOAL>↑(rexp (-b * x✝ ^ 2)) = cexp (-↑b * ↑x✝ ^ 2)
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>↑(√(π / b) / 2) = (↑π / ↑b) ^ (1 / 2) / 2
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>hs : s.Finite<VAR>g : G<VAR>this✝ : Fintype ↑s<VAR>this : Fintype ↑(g • s)<GOAL>g ∈ stabilizer G s ↔ g • s ⊆ s
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>s : Set α<VAR>hs : s.Finite<VAR>g : G<VAR>this✝ : Fintype ↑s<VAR>this : Fintype ↑(g • s)<GOAL>g • s = s ↔ g • s ⊆ s
<VAR>n m l : ℕ<VAR>hlm : l ≤ m<GOAL>filter (fun x => decide (x < l)) (Ico n m) = Ico n l
<VAR>n m l : ℕ<VAR>hlm : l ≤ m<VAR>hnl : n ≤ l<GOAL>filter (fun x => decide (x < l)) (Ico n m) = Ico n l
<VAR>n m l : ℕ<VAR>hlm : l ≤ m<VAR>hln : l ≤ n<GOAL>filter (fun x => decide (x < l)) (Ico n m) = Ico n l
<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 N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<VAR>ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂<VAR>l : ℕ<GOAL>lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
<VAR>n✝ n k : ℕ<VAR>hk : k ≠ 0<GOAL>(n ^ k).minFac = n.minFac
<VAR>n k : ℕ<VAR>hk : k ≠ 0<GOAL>(1 ^ k).minFac = minFac 1
<VAR>n✝ n k : ℕ<VAR>hk : k ≠ 0<VAR>hn : n ≠ 1<GOAL>(n ^ k).minFac = n.minFac
<VAR>n✝ n k : ℕ<VAR>hk : k ≠ 0<VAR>hn : n ≠ 1<VAR>hnk : n ^ k ≠ 1<GOAL>(n ^ k).minFac = n.minFac
<VAR>n✝ n k : ℕ<VAR>hk : k ≠ 0<VAR>hn : n ≠ 1<VAR>hnk : n ^ k ≠ 1<GOAL>n.minFac ≤ (n ^ k).minFac
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>s ∈ coclosedCompact X ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ sᶜ ⊆ t
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsUpperModularLattice α<VAR>a b : α<GOAL>a ⊓ b ⋖ b → a ⋖ a ⊔ b
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsUpperModularLattice α<VAR>a b : α<GOAL>b ⊓ a ⋖ b → a ⋖ b ⊔ a
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))<VAR>loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))<GOAL>toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))<VAR>loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))<GOAL>toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f = (IsLocalization.Away.lift r ⋯).comp (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))) ↔ f = X.toΓSpecCApp r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<GOAL>inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g = (range (rTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<GOAL>∀ (x : N ⊗[R] Q), (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) x = (range (rTensor Q f)).mkQ x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : N ⊗[R] Q<GOAL>(inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) y = (range (rTensor Q f)).mkQ y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>e : Perm α<GOAL>Perm.sign (optionCongr e) = Perm.sign e
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>e : Perm α<GOAL>Perm.sign (optionCongr 1) = Perm.sign 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>e : Perm α<GOAL>∀ (f : Perm α) (x y : α), x ≠ y → Perm.sign (optionCongr f) = Perm.sign f → Perm.sign (optionCongr (swap x y * f)) = Perm.sign (swap x y * f)
<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 : Memℒp f p μ<GOAL>‖Memℒp.toLp f hf‖ = (eLpNorm f p μ).toReal
<VAR>α✝ : Sort u_1<VAR>x₁ x₂ : α✝<GOAL>x₁ = x₂ ↔ x₁ = x₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Ring S<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : FiniteDimensional K L<VAR>x : L<VAR>hx : IsIntegral R x<GOAL>IsIntegral R ((norm K) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Ring S<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : FiniteDimensional K L<VAR>x : L<VAR>hx : IsIntegral R x<VAR>hx' : IsIntegral K x<GOAL>IsIntegral R ((norm K) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Ring S<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : FiniteDimensional K L<VAR>x : L<VAR>hx : IsIntegral R x<VAR>hx' : IsIntegral K x<GOAL>IsIntegral R (((minpoly K x).aroots (AlgebraicClosure L)).prod ^ finrank (↥K⟮x⟯) L)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Ring S<VAR>inst✝¹² : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra K E<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : FiniteDimensional K L<VAR>x : L<VAR>hx : IsIntegral R x<VAR>hx' : IsIntegral K x<GOAL>Splits (algebraMap K (AlgebraicClosure L)) (minpoly K x)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<GOAL>univ.Finite
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L<GOAL>f x ∈ f.idealRange
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L<GOAL>f x ∈ LieIdeal.map f ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ X.δ i.succ = 𝟙 (X _[n])
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>r : R<VAR>M : Matrix n n R<GOAL>(1 + r • M).det = 1 + M.trace * r + eval r (1 + X • M.map ⇑C).det.divX.divX * r ^ 2
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hroots : card p.roots = p.natDegree<VAR>k : ℕ<VAR>h : k ≤ p.natDegree<GOAL>p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hroots : card p.roots = p.natDegree<VAR>k : ℕ<VAR>h : k ≤ p.natDegree<GOAL>(C p.leadingCoeff * (map (fun a => X - C a) p.roots).prod).coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hroots : card p.roots = p.natDegree<VAR>k : ℕ<VAR>h : k ≤ p.natDegree<GOAL>p.leadingCoeff * (map (fun a => X - C a) p.roots).prod.coeff k = p.leadingCoeff * ((-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k))
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hroots : card p.roots = p.natDegree<VAR>k : ℕ<VAR>h : k ≤ p.natDegree<VAR>this : k ≤ card p.roots<GOAL>(map (fun a => X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.30699<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq (Finset α)<VAR>s : Finset α<GOAL>s.powerset = (range (s.card + 1)).biUnion fun i => powersetCard i s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>f : α → Option β<VAR>s : l₁ <+ l₂<GOAL>filterMap f l₁ <+ filterMap f l₂
<VAR>M : Type u_1<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : Pow M ℕ<VAR>inst✝ : NatPowAssoc M<VAR>x : M<VAR>m n : ℕ<GOAL>x ^ (m * n) = (x ^ m) ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Div α<VAR>a b : Part α<VAR>hab : (a / b).Dom<GOAL>(a / b).get hab = a.get ⋯ / b.get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Div α<VAR>a b : Part α<VAR>hab : (a / b).Dom<GOAL>(a.bind fun y => map (fun x => y / x) b).get ⋯ = a.get ⋯ / b.get ⋯
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<GOAL>IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f f' g : ↥(Lp E 2 μ)<GOAL>⟪f + f', g⟫_𝕜 = ⟪f, g⟫_𝕜 + ⟪f', g⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f f' g : ↥(Lp E 2 μ)<GOAL>∫ (a : α), ⟪↑↑(f + f') a, ↑↑g a⟫_𝕜 ∂μ = ∫ (a : α), ⟪↑↑f a + ↑↑f' a, ↑↑g a⟫_𝕜 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f f' g : ↥(Lp E 2 μ)<VAR>x : α<VAR>hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x<GOAL>(fun a => ⟪↑↑(f + f') a, ↑↑g a⟫_𝕜) x = (fun a => ⟪↑↑f a + ↑↑f' a, ↑↑g a⟫_𝕜) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f f' g : ↥(Lp E 2 μ)<VAR>x : α<VAR>hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x<GOAL>⟪↑↑(f + f') x, ↑↑g x⟫_𝕜 = ⟪↑↑f x + ↑↑f' x, ↑↑g x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>c : F<GOAL>HasStrictFDerivAt (fun x => f x - c) f' x
<VAR>M : Type u_1<VAR>M₂ : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>F : Type u_3<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : DivisionRing R<VAR>inst✝² : DivisionRing S<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module S M₂<VAR>c : ℚ<VAR>x : M<GOAL>f (↑c • x) = ↑c • f x
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f✝ : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>N : Type ?u.1048911<VAR>N' : Type ?u.1048914<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S g<VAR>f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M<GOAL>iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f✝ : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>N : Type ?u.1048911<VAR>N' : Type ?u.1048914<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S g<VAR>f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M<VAR>e : LocalizedModule S M →ₗ[R] LocalizedModule S M<VAR>left✝ : e ∘ₗ f = f<VAR>univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l => l ∘ₗ f = f) y → y = e<GOAL>iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'<VAR>f✝ : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>N : Type ?u.1048911<VAR>N' : Type ?u.1048914<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S g<VAR>f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M<VAR>e : LocalizedModule S M →ₗ[R] LocalizedModule S M<VAR>left✝ : e ∘ₗ f = f<VAR>univ : ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M), (fun l => l ∘ₗ f = f) y → y = e<GOAL>e = ↑(LinearEquiv.refl R (LocalizedModule S M))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>xs✝ ys : List α<VAR>ls : List (List α)<VAR>f : List α → List α<VAR>x : α<VAR>xs : List α<GOAL>(if p x = true then [].reverse :: splitOnP.go p xs [] else splitOnP.go p xs [x]) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>c : ℝ≥0∞<VAR>h : levyProkhorovEDist μ ν < c<VAR>B : Set Ω<VAR>B_mble : MeasurableSet B<GOAL>ν B ≤ μ (thickening c.toReal B) + c
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>c : ℝ≥0∞<VAR>h : levyProkhorovEDist μ ν < c<VAR>B : Set Ω<VAR>B_mble : MeasurableSet B<VAR>c' : ℝ≥0∞<VAR>hc' : c' ∈ {ε | ∀ (B : Set Ω), MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε}<VAR>lt_c : c' < c<GOAL>ν B ≤ μ (thickening c.toReal B) + 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>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>(p.append p').support.tail = p.support.tail ++ p'.support.tail
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d : α<GOAL>TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d : α<VAR>h : TransGen r a c<GOAL>∃ b, ReflTransGen r a b ∧ r b c
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>x : R⟦X⟧<VAR>n : ℕ<GOAL>(coeff R n) ((rescale 0) x) = (coeff R n) (((C R).comp (constantCoeff R)) x)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>x : R⟦X⟧<VAR>n : ℕ<GOAL>(coeff R n) ({ toFun := fun f => mk fun n => 0 ^ n * (coeff R n) f, map_one' := ⋯, map_mul' := ⋯ } x) = if n = 0 then (constantCoeff R) x else 0
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝¹³ : Semiring R<VAR>φ : ι → Type u_1<VAR>ψ : ι → Type u_2<VAR>χ : ι → Type u_3<VAR>inst✝¹² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹¹ : (i : ι) → Module R (φ i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (ψ i)<VAR>inst✝⁹ : (i : ι) → Module R (ψ i)<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (χ i)<VAR>inst✝⁷ : (i : ι) → Module R (χ i)<VAR>S : Type u_4<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>f : ι → M<VAR>g : ι → R<GOAL>((piRing R M ι S).symm f) g = ∑ i : ι, g i • f i
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>ι' : Sort u_2<VAR>inst✝ : UniformSpace β<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>ha : (𝓤 α).HasBasis p s<VAR>q : ι' → Prop<VAR>t : ι' → Set (β × β)<VAR>hb : (𝓤 β).HasBasis q t<VAR>f : α → β<GOAL>(∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ x ∈ s ia, (f x.1, f x.2) ∈ t ib) ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i