ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>m n : ℕ<VAR>_i : Fact (finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<VAR>A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1<GOAL>o.volumeForm.measure = volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>m n : ℕ<VAR>_i : Fact (finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<VAR>A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1<GOAL>addHaarMeasure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f<VAR>hfi : IntervalIntegrable f μ a b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hfi : IntervalIntegrable f μ a b<VAR>hab : a ≤ b<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hfi : IntervalIntegrable f μ a b<VAR>hab : b ≤ a<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>eval (v i) (Lagrange.basis s v i) = 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j)) = 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j✝ : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>H : j ∈ s.erase i<GOAL>eval (v i) (basisDivisor (v i) (v j)) = 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j✝ : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>H : j ∈ s.erase i<GOAL>v i ≠ v j
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j✝ : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>H : j ∈ s.erase i<VAR>hij : j ≠ i<VAR>hj : j ∈ s<GOAL>v i ≠ v j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>hr : 0 < r<VAR>p : (b : β) → π b<GOAL>p ∈ ball x r ↔ p ∈ Set.univ.pi fun b => ball (x b) r
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>hr : 0 ≤ r<GOAL>dist z w = r ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>hr : 0 ≤ r<GOAL>dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (z.im * w.im)) = sinh (r / 2) ^ 2
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>hr : 0 ≤ r<GOAL>0 ≤ z.im * w.im
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>hr : 0 ≤ r<GOAL>0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>hr : 0 ≤ r<GOAL>0 ≤ sinh (r / 2)
<VAR>v : Multiset ℕ+<VAR>h : ∀ p ∈ v, p.Prime<GOAL>Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨↑p, hp⟩) v h) = v
<VAR>v : Multiset ℕ+<VAR>h : ∀ p ∈ v, p.Prime<VAR>this : (fun p h => Coe.coe ⟨↑p, h⟩) = fun p x => id p<GOAL>Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨↑p, hp⟩) v h) = v
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>dite P (fun x => a) B ≠ a ↔ ∃ h, a ≠ B h
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>(∃ x, ¬B x = a) ↔ ∃ h, a ≠ B h
<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>inst✝ : PartialOrder 𝕜<GOAL>HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : ↑n ≠ 0<GOAL>↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : ↑n ≠ 0<VAR>hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0<GOAL>↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : ↑n ≠ 0<VAR>hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0<GOAL>∏ i ∈ n.primeFactors, ↑(i - 1) = ∏ x ∈ n.primeFactors, (1 - (↑x)⁻¹) * ↑x
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : ↑n ≠ 0<VAR>hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0<VAR>p : ℕ<VAR>hp : p ∈ n.primeFactors<GOAL>↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : ↑n ≠ 0<VAR>hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0<VAR>p : ℕ<VAR>hp✝ : p ∈ n.primeFactors<VAR>hp : 0 < p<GOAL>↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>hn' : ↑n ≠ 0<VAR>hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0<VAR>p : ℕ<VAR>hp✝ : p ∈ n.primeFactors<VAR>hp : 0 < p<VAR>hp' : ↑p ≠ 0<GOAL>↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 ≤ z i<GOAL>(∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ ≤ (∑ i ∈ s, w i * z i) / ∑ i ∈ s, w i
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 ≤ z i<GOAL>(∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 ≤ z i<GOAL>(∑ i ∈ s, w i * z i) / ∑ i ∈ s, w i = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 ≤ z i<GOAL>∀ i ∈ s, 0 ≤ (fun i => w i / ∑ i ∈ s, w i) i
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 ≤ z i<GOAL>∑ i ∈ s, (fun i => w i / ∑ i ∈ s, w i) i = 1
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : AList β<VAR>h : s₁.Disjoint s₂<VAR>x✝ : α<VAR>y✝ : β x✝<GOAL>y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : AList β<VAR>h : s₁.Disjoint s₂<VAR>x✝ : α<VAR>y✝ : β x✝<GOAL>dlookup x✝ s₁.entries = some y✝ ∨ x✝ ∉ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝ ↔ dlookup x✝ s₂.entries = some y✝ ∨ x✝ ∉ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>hab : b ≤ a<GOAL>f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>hab : a < b<GOAL>f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)}
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 ≤ a_1} ∩ {a_1 | a_1 < g a.1}})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedCommRing 𝕜<VAR>inst✝² : NoZeroDivisors 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>hs : s ≠ t<VAR>c : E<GOAL>[c + x-[𝕜]c + t • y] ∩ [c + x-[𝕜]c + s • y] = {c + x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedCommRing 𝕜<VAR>inst✝² : NoZeroDivisors 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>hs : s ≠ t<VAR>c : E<GOAL>LinearIndependent 𝕜 ![c + t • y - (c + x), c + s • y - (c + x)]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedCommRing 𝕜<VAR>inst✝² : NoZeroDivisors 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>hs : s ≠ t<VAR>c : E<GOAL>LinearIndependent 𝕜 ![t • y - x, s • y - x]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedCommRing 𝕜<VAR>inst✝² : NoZeroDivisors 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>hs : s ≠ t<VAR>c : E<GOAL>LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedCommRing 𝕜<VAR>inst✝² : NoZeroDivisors 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>hs : s ≠ t<VAR>c : E<GOAL>-1 * s - t * -1 ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedCommRing 𝕜<VAR>inst✝² : NoZeroDivisors 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>c : E<VAR>hs : -1 * s - t * -1 = 0<GOAL>s = t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedCommRing 𝕜<VAR>inst✝² : NoZeroDivisors 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y : E<VAR>h : LinearIndependent 𝕜 ![x, y]<VAR>s t : 𝕜<VAR>c : E<VAR>hs : -1 * s - t * -1 = 0<GOAL>t = s
<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✝ : CompleteLattice α<VAR>s : Finset α<GOAL>s.sup id = sSup ↑s
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>h : s ≠ t<GOAL>(edge s t).edgeSet = {s(s, t)}
<VAR>a : ℤ<GOAL>↑a.natAbs ≤ a ^ 2
<VAR>a : ℤ<GOAL>↑a.natAbs ≤ ↑a.natAbs * ↑a.natAbs
<VAR>a : ℤ<GOAL>a.natAbs ≤ a.natAbs * a.natAbs
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I J : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>mk I = mk J ↔ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I J : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>(∃ i, (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I * (toPrincipalIdeal R (FractionRing R)) i = (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) J) ↔ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>s : CompleteSublattice (Submodule R M) := (AEval.comapSubmodule R M f).range<GOAL>f.IsSemisimple ↔ ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>s : CompleteSublattice (Submodule R M) := (AEval.comapSubmodule R M f).range<VAR>h : ↑s = {p | p ≤ Submodule.comap f p}<GOAL>f.IsSemisimple ↔ ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>s : CompleteSublattice (Submodule R M) := (AEval.comapSubmodule R M f).range<VAR>h : ↑s = {p | p ≤ Submodule.comap f p}<VAR>e : Submodule R[X] (AEval R M f) ≃o ↥(AEval.comapSubmodule R M f).range := (AEval.comapSubmodule R M f).toOrderIsoRangeOfInjective ⋯<GOAL>f.IsSemisimple ↔ ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>i : ι<VAR>a : G i<VAR>f : ↥(lp G 2)<GOAL>⟪f, lp.single 2 i a⟫_𝕜 = ⟪↑f i, a⟫_𝕜
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring R<VAR>a b : R<VAR>n : ℕ<GOAL>a * (-1) ^ n = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>(((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) 1 0) 0 = (f 0) 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>⇑h '' EMetric.ball x r = EMetric.ball (h x) r
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>g : Y ⟶ X<VAR>hom_inv_id : f ≫ g = 𝟙 X<GOAL>inv f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>g : Y ⟶ X<VAR>hom_inv_id : f ≫ g = 𝟙 X<GOAL>f ≫ inv f = f ≫ g
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ X✝ Y✝ : C<VAR>f✝ : A✝ ⟶ X✝<VAR>i✝ : A✝ ⟶ B✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>g✝ : B✝ ⟶ Y✝<VAR>sq✝ : CommSq f✝ i✝ p✝ g✝<VAR>A B X Y : Cᵒᵖ<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<GOAL>sq.HasLift ↔ ⋯.HasLift
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ X✝ Y✝ : C<VAR>f✝ : A✝ ⟶ X✝<VAR>i✝ : A✝ ⟶ B✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>g✝ : B✝ ⟶ Y✝<VAR>sq✝ : CommSq f✝ i✝ p✝ g✝<VAR>A B X Y : Cᵒᵖ<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<GOAL>Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>e : A ≅ B<GOAL>e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>adj3 : F'' ⊣ G<VAR>x : C<GOAL>(adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>adj3 : F'' ⊣ G<VAR>x : C<GOAL>(adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = ((adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom).app x
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist 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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))
<VAR>x✝ x y : ℝ<VAR>h : x ≤ y<VAR>n : ℕ<GOAL>√(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : Finite ι<GOAL>MeasurableSet (fundamentalDomain b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>MeasurableSet (fundamentalDomain b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>this : FiniteDimensional ℝ E<GOAL>MeasurableSet (fundamentalDomain b)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>Γ' : Type u_3<VAR>inst✝ : PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x✝ : Γ'<GOAL>(embDomain f 0).coeff x✝ = coeff 0 x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a * b * a⁻¹ = 1 ↔ b = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : ι → E<VAR>inst✝ : DecidableEq E<VAR>v' : ι' → E<VAR>h : Orthonormal 𝕜 v'<VAR>s : Finset ι'<VAR>i : { x // x ∈ s }<GOAL>↑((OrthonormalBasis.span h s) i) = v' ↑i
<VAR>x✝ y : ℝ<VAR>f : CauSeq ℚ abs<VAR>x : ℝ<VAR>i : ℕ<VAR>H : ∀ j ≥ i, ↑(↑f j) ≤ x<GOAL>mk f ≤ x
<VAR>x✝ y : ℝ<VAR>f : CauSeq ℚ abs<VAR>x : ℝ<VAR>i : ℕ<VAR>H : ∀ j ≥ i, ↑(↑f j) ≤ x<GOAL>-x ≤ mk (-f)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>h : a * b ≠ ⊤<VAR>ha : a ≠ 0<GOAL>b * a ≠ ⊤
<VAR>z : ℝ<VAR>h : 0 ≤ z<VAR>h0 : 0 = z<GOAL>Monotone fun x => x ^ 0
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∃ n, p n<GOAL>Nat.find h = 0 ↔ p 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<VAR>h : s ⊆ t<GOAL>s.ndunion t = t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a✝ b✝ : List α<VAR>h : Quot.mk Setoid.r a✝ ⊆ Quot.mk Setoid.r b✝<GOAL>ndunion (Quot.mk Setoid.r a✝) (Quot.mk Setoid.r b✝) = Quot.mk Setoid.r b✝
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>xᶜ \ yᶜ = y \ x
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : CharZero A<VAR>inst✝ : IsAlgClosed A<GOAL>Fintype.card (K →+* A) = finrank ℚ K
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))<VAR>s_eq : s = ⋃ n, s ∩ t n<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hμf : μ {x | x ∈ s ∧ f x = ⊤} ≠ 0<GOAL>μ {x | x ∈ s ∧ f x = ⊤} ≤ (μ.restrict s) {x | f x = ⊤}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hμf : μ {x | x ∈ s ∧ f x = ⊤} ≠ 0<GOAL>μ ({a | f a = ⊤} ∩ s) ≤ (μ.restrict s) {x | f x = ⊤}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs_zero : μ s = 0<GOAL>(fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>γ : Type u_5<VAR>f g : α → γ<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs_zero : μ s = 0<VAR>h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}<GOAL>(fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] g