ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : LieRingModule L M<VAR>inst✝⁶ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : LieRingModule L M₂<VAR>inst✝² : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>N₁ N₂ : LieSubmodule R L M<VAR>h : Codisjoint N₁ N₂<VAR>l : ℕ<VAR>hl : ∀ b ≥ l, ⨅ k, lowerCentralSeries R L (↥↑N₁) k = lowerCentralSeries R L (↥↑N₁) b ∧ ⨅ k, lowerCentralSeries R L (↥↑N₂) k = lowerCentralSeries R L (↥↑N₂) b ∧ ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M b<GOAL>LieSubmodule.map N₁.incl (posFittingComp R L ↥↑N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥↑N₂) = posFittingComp R L M
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>inst✝¹⁰ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : LieRingModule L M<VAR>inst✝⁶ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : LieRingModule L M₂<VAR>inst✝² : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>N₁ N₂ : LieSubmodule R L M<VAR>h : Codisjoint N₁ N₂<VAR>l : ℕ<VAR>hl : ∀ b ≥ l, ⨅ k, lowerCentralSeries R L (↥↑N₁) k = lowerCentralSeries R L (↥↑N₁) b ∧ ⨅ k, lowerCentralSeries R L (↥↑N₂) k = lowerCentralSeries R L (↥↑N₂) b ∧ ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M b<VAR>hl₁ : ⨅ k, lowerCentralSeries R L (↥↑N₁) k = lowerCentralSeries R L (↥↑N₁) l<VAR>hl₂ : ⨅ k, lowerCentralSeries R L (↥↑N₂) k = lowerCentralSeries R L (↥↑N₂) l<VAR>hl₃ : ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l<GOAL>LieSubmodule.map N₁.incl (posFittingComp R L ↥↑N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥↑N₂) = posFittingComp R L M
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.3910, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : Karoubi (HomologicalComplex C c)<VAR>n : ι<GOAL>P.p.f n ≫ P.p.f n = P.p.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.3910, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : Karoubi (HomologicalComplex C c)<VAR>i j : ι<VAR>hij : ¬c.Rel i j<GOAL>(fun i j => { f := P.p.f i ≫ P.X.d i j, comm := ⋯ }) i j = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.3910, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : Karoubi (HomologicalComplex C c)<VAR>i j : ι<VAR>hij : ¬c.Rel i j<GOAL>P.p.f i ≫ P.X.d i j = 0
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderTop α<VAR>a b c : α<VAR>h : b ⊓ a ≤ c<VAR>hd : Codisjoint b c<GOAL>a ⊓ 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>v : V<VAR>e : Sym2 V<VAR>p : G.Path v v<GOAL>e ∉ (↑p).edges
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<GOAL>e.restr (e.source ∩ s) = e.restr s
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<GOAL>(e.restr (e.source ∩ s)).source = (e.restr s).source
<VAR>x y z : ℝ<GOAL>∀ (x : ℝ), 0 < deriv sinh x
<VAR>x y z : ℝ<GOAL>∀ (x : ℝ), 0 < cosh x
<VAR>m : ℕ+<VAR>p : Nat.Primes<VAR>k : ℕ<GOAL>↑p ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset
<VAR>m : ℕ+<VAR>p : Nat.Primes<VAR>k : ℕ<GOAL>k • PrimeMultiset.ofPrime p ≤ m.factorMultiset ↔ Multiset.replicate k p ≤ m.factorMultiset
<VAR>m : ℕ+<VAR>p : Nat.Primes<VAR>k : ℕ<VAR>e_1✝ : PrimeMultiset = Multiset Nat.Primes<GOAL>k • PrimeMultiset.ofPrime p = Multiset.replicate k p
<VAR>m : ℕ+<VAR>p : Nat.Primes<VAR>k : ℕ<VAR>e_1✝ : PrimeMultiset = Multiset Nat.Primes<GOAL>Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ b ∈ k • PrimeMultiset.ofPrime p, b = p
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (β i)<VAR>M : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubmonoidClass S M<VAR>A : ι → S<VAR>i j : ι<VAR>x : ↥(A i)<GOAL>↑(((of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (β i)<VAR>M : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubmonoidClass S M<VAR>A : ι → S<VAR>i : ι<VAR>x : ↥(A i)<GOAL>↑(((of (fun i => ↥(A i)) i) x) i) = ↑(if i = i then x else 0)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (β i)<VAR>M : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubmonoidClass S M<VAR>A : ι → S<VAR>i j : ι<VAR>x : ↥(A i)<VAR>h : i ≠ j<GOAL>↑(((of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<GOAL>∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<GOAL>∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<GOAL>∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α), (μ.rnDeriv ν * f) a ∂ν
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y✝ : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hg : DifferentiableOn 𝕜 g s<VAR>hs' : UniqueDiffOn 𝕜 s<VAR>hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x<VAR>hx : x ∈ s<VAR>hfgx : f x = g x<VAR>y : E<VAR>hy : y ∈ s<GOAL>f y = g y
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y✝ : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hg : DifferentiableOn 𝕜 g s<VAR>hs' : UniqueDiffOn 𝕜 s<VAR>hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x<VAR>hx : x ∈ s<VAR>hfgx : f x = g x<VAR>y : E<VAR>hy : y ∈ s<GOAL>f x - g x = f y - g y
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y✝ : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hg : DifferentiableOn 𝕜 g s<VAR>hs' : UniqueDiffOn 𝕜 s<VAR>hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x<VAR>hx : x ∈ s<VAR>hfgx : f x = g x<VAR>y : E<VAR>hy : y ∈ s<VAR>z : E<VAR>hz : z ∈ s<GOAL>fderivWithin 𝕜 (fun y => f y - g y) s z = 0
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x
<VAR>α : Type u_1<VAR>t₁ t₂ : Ordnode α<VAR>h₁ : t₁.Sized<VAR>h₂ : t₂.Sized<VAR>h : t₁.toList = t₂.toList<GOAL>t₁.size = t₂.size
<VAR>α β γ : Type u<VAR>F : Type u → Type v<VAR>inst✝¹ : Applicative F<VAR>inst✝ : LawfulApplicative F<VAR>x : F (α → β)<VAR>f : γ → α<VAR>y : F γ<GOAL>(Seq.seq x fun x => f <$> y) = Seq.seq ((fun x => x ∘ f) <$> x) fun x => y
<VAR>α β γ : Type u<VAR>F : Type u → Type v<VAR>inst✝¹ : Applicative F<VAR>inst✝ : LawfulApplicative F<VAR>x : F (α → β)<VAR>f : γ → α<VAR>y : F γ<GOAL>(Seq.seq x fun x => Seq.seq (pure f) fun x => y) = Seq.seq (Seq.seq (pure fun x => x ∘ f) fun x_1 => x) fun x => y
<VAR>α β γ : Type u<VAR>F : Type u → Type v<VAR>inst✝¹ : Applicative F<VAR>inst✝ : LawfulApplicative F<VAR>x : F (α → β)<VAR>f : γ → α<VAR>y : F γ<GOAL>(Seq.seq ((fun x x_1 => x (f x_1)) <$> x) fun x => y) = Seq.seq (Seq.seq (pure fun x x_1 => x (f x_1)) fun x_1 => x) fun x => y
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd ω * (cs.rightInvSeq ω).getD j 1 = cs.wordProd (ω.eraseIdx j)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd ω * ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple (ω.get? j)).getD 1 * cs.wordProd (drop (j + 1) ω)) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd (take (j + 1) ω ++ drop (j + 1) ω) * ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple (ω.get? j)).getD 1 * cs.wordProd (drop (j + 1) ω)) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) * ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple (ω.get? j)).getD 1 * cs.wordProd (drop (j + 1) ω)) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<VAR>lt : j < ω.length<GOAL>cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) * ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple (ω.get? j)).getD 1 * cs.wordProd (drop (j + 1) ω)) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<VAR>le : ω.length ≤ j<GOAL>cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) * ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple (ω.get? j)).getD 1 * cs.wordProd (drop (j + 1) ω)) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : Fintype R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : card R = p ^ n<VAR>hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n<GOAL>CharP R (p ^ n)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : Fintype R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : card R = p ^ n<VAR>hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n<VAR>c : ℕ<VAR>hc : CharP R c<GOAL>CharP R (p ^ n)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : Fintype R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : card R = p ^ n<VAR>hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n<VAR>c : ℕ<VAR>hc : CharP R c<VAR>hcpn : c ∣ p ^ n<GOAL>CharP R (p ^ n)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : Fintype R<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : card R = p ^ n<VAR>hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n<VAR>i : ℕ<VAR>hi : i ≤ n<VAR>hc : CharP R (p ^ i)<VAR>hcpn : p ^ i ∣ p ^ n<GOAL>CharP R (p ^ n)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : Fintype R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>i : ℕ<VAR>hc : CharP R (p ^ i)<VAR>hn : card R = p ^ i<VAR>hR : ∀ i_1 ≤ i, ↑p ^ i_1 = 0 → i_1 = i<VAR>hi : i ≤ i<VAR>hcpn : p ^ i ∣ p ^ i<GOAL>CharP R (p ^ i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>IsLeast {t | s ⊆ ↑t} (toCone s hs)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x✝ : E<VAR>t : ConvexCone 𝕜 E<VAR>ht : t ∈ {t | s ⊆ ↑t}<VAR>x : E<VAR>hx : x ∈ toCone s hs<GOAL>x ∈ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<VAR>t : ConvexCone 𝕜 E<VAR>ht : t ∈ {t | s ⊆ ↑t}<VAR>c : 𝕜<VAR>hc : 0 < c<VAR>y : E<VAR>hy : y ∈ s<VAR>hx : c • y ∈ toCone s hs<GOAL>c • y ∈ t
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ last n<GOAL>(a.castPred ha).succ ≤ b ↔ a < b
<VAR>X Y : FintypeCat<VAR>f g : X ⟶ Y<VAR>h : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>X Y : FintypeCat<VAR>f g : X ⟶ Y<VAR>h : ∀ (x : ↑X), f x = g x<VAR>x✝ : ↑X<GOAL>f x✝ = g x✝
<VAR>q a b c : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>n₃ : ℤ<VAR>d₃ : ℕ<VAR>h₃ : d₃ ≠ 0<GOAL>(n₁ /. ↑d₁ + n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₃ /. ↑d₃) + n₂ /. ↑d₂ * (n₃ /. ↑d₃)
<VAR>q a b c : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>n₃ : ℤ<VAR>d₃ : ℕ<VAR>h₃ : d₃ ≠ 0<GOAL>(n₁ * ↑d₂ + n₂ * ↑d₁) * n₃ /. (↑d₁ * ↑d₂ * ↑d₃) = (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))
<VAR>q a b c : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>n₃ : ℤ<VAR>d₃ : ℕ<VAR>h₃ : d₃ ≠ 0<GOAL>(n₁ * ↑d₂ * n₃ * ↑d₃ + n₂ * ↑d₁ * n₃ * ↑d₃) /. (↑d₁ * ↑d₂ * ↑d₃ * ↑d₃) = (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))
<VAR>p : ℝ≥0∞<VAR>h : p ≤ 1<VAR>n : ℕ<GOAL>(binomial p h n) (Fin.last n) = p ^ n
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<GOAL>Unit_of_divided_by_X_pow_order 0 = 1
<VAR>z : ℂ<VAR>h₀ : z ≠ ↑π / 2<VAR>h₁ : -(π / 2) < z.re<VAR>h₂ : z.re ≤ π / 2<GOAL>cos z ≠ 0
<VAR>z : ℂ<VAR>h₀ : z ≠ ↑π / 2<VAR>h₁ : -(π / 2) < z.re<VAR>h₂ : z.re ≤ π / 2<VAR>k : ℤ<GOAL>z ≠ (2 * ↑k + 1) * ↑π / 2
<VAR>z : ℂ<VAR>h₀ : ¬z.re = (↑π / 2).re ∨ ¬z.im = (↑π / 2).im<VAR>h₁ : -(π / 2) < z.re<VAR>h₂ : z.re ≤ π / 2<VAR>k : ℤ<GOAL>¬z.re = ((2 * ↑k + 1) * ↑π / 2).re ∨ ¬z.im = ((2 * ↑k + 1) * ↑π / 2).im
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>r n : ℕ<GOAL>↑(n.choose r) ≤ ↑n ^ r / ↑r !
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>r n : ℕ<GOAL>↑r ! * ↑(n.choose r) ≤ ↑n ^ r
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>r n : ℕ<GOAL>0 < ↑r !
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.29<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>x : X<GOAL>Filter.comap (toPullbackDiag f) (𝓝 (toPullbackDiag f x)) = 𝓝 x
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.29<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>x : X<GOAL>Filter.comap (Prod.fst ∘ Subtype.val ∘ toPullbackDiag f) (𝓝 x) ⊓ Filter.comap (Prod.snd ∘ Subtype.val ∘ toPullbackDiag f) (𝓝 x) = 𝓝 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hsing : μ.singularPart ν ⟂ₘ ν<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)<VAR>heq' : ∀ (A : Set α), MeasurableSet A → (ν.withDensity f) A = ((ν.withDensity f).restrict (S ∩ T)) A<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)<VAR>heq' : ∀ (A : Set α), MeasurableSet A → (ν.withDensity f) A = ((ν.withDensity f).restrict (S ∩ T)) A<VAR>A : Set α<VAR>hA : MeasurableSet A<GOAL>(ν.withDensity f) A = (ν.withDensity (μ.rnDeriv ν)) A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)<VAR>heq' : ∀ (A : Set α), MeasurableSet A → (ν.withDensity f) A = ((ν.withDensity f).restrict (S ∩ T)) A<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>hνrn : (ν.withDensity (μ.rnDeriv ν)) (A ∩ (S ∩ T)ᶜ) = 0<GOAL>(ν.withDensity f) A = (ν.withDensity (μ.rnDeriv ν)) A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝¹ : Mul M<VAR>inst✝ : Mul N<VAR>f : M →ₙ* N<VAR>g : N → M<VAR>h₁ : LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<VAR>x y : N<GOAL>g (f (g x) * f (g y)) = g (f (g x * g y))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p p' : P<GOAL>Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p p' : P<GOAL>Collinear ℝ {s.secondInter p (p' -ᵥ p), p, p'}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>r : Set (α × α)<VAR>s : Set β<VAR>f g : β → α<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>hg : ∀ x ∈ s, ContinuousAt g x<VAR>hfg : EqOn f g s<VAR>hr : r ∈ 𝓤 α<GOAL>∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>r : Set (α × α)<VAR>s : Set β<VAR>f g : β → α<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>hg : ∀ x ∈ s, ContinuousAt g x<VAR>hfg : EqOn f g s<VAR>hr : r ∈ 𝓤 α<VAR>A : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r<GOAL>∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>r : Set (α × α)<VAR>s : Set β<VAR>f g : β → α<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>hg : ∀ x ∈ s, ContinuousAt g x<VAR>hfg : EqOn f g s<VAR>hr : r ∈ 𝓤 α<VAR>t : β → Set β<VAR>t_open : ∀ x ∈ s, IsOpen (t x)<VAR>xt : ∀ x ∈ s, x ∈ t x<VAR>ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r<GOAL>∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>r : Set (α × α)<VAR>s : Set β<VAR>f g : β → α<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>hg : ∀ x ∈ s, ContinuousAt g x<VAR>hfg : EqOn f g s<VAR>hr : r ∈ 𝓤 α<VAR>t : β → Set β<VAR>t_open : ∀ x ∈ s, IsOpen (t x)<VAR>xt : ∀ x ∈ s, x ∈ t x<VAR>ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r<GOAL>∀ x ∈ ⋃ x ∈ s, t x, (f x, g x) ∈ r