ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>θ : Angle<VAR>x✝ : ℝ<GOAL>θ.cos = (↑x✝).cos ↔ θ = ↑x✝ ∨ θ = -↑x✝
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>e : Sym2 V<GOAL>e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ e ∈ {s(v, w)}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>e : Sym2 V<GOAL>∀ (x y : V), s(x, y) ∈ (G.subgraphOfAdj hvw).edgeSet ↔ s(x, y) ∈ {s(v, w)}
<VAR>a x z : ℂ<GOAL>arg 1 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>hsf : s.Finite<VAR>hs : s.Nontrivial<GOAL>s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q r : R[X]<GOAL>(X - C a).IsRoot b ↔ a = b
<VAR>N k n : ℕ<VAR>hn : n ∈ N.smoothNumbersUpTo k<GOAL>n ∈ Finset.image (fun x => match x with | (s, m) => m ^ 2 * s.prod id) (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)
<VAR>N k n : ℕ<VAR>hn : n ∈ N.smoothNumbersUpTo k<VAR>hn₁ : n ≤ N<VAR>hn₂ : n ∈ k.smoothNumbers<GOAL>n ∈ Finset.image (fun x => match x with | (s, m) => m ^ 2 * s.prod id) (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)
<VAR>N k n : ℕ<VAR>hn : n ∈ N.smoothNumbersUpTo k<VAR>hn₁ : n ≤ N<VAR>hn₂ : n ∈ k.smoothNumbers<VAR>s : Finset ℕ<VAR>hs : s ∈ k.primesBelow.powerset<VAR>m : ℕ<VAR>hm : n = m ^ 2 * s.prod id<GOAL>n ∈ Finset.image (fun x => match x with | (s, m) => m ^ 2 * s.prod id) (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0)
<VAR>N k n : ℕ<VAR>hn : n ∈ N.smoothNumbersUpTo k<VAR>hn₁ : n ≤ N<VAR>hn₂ : n ∈ k.smoothNumbers<VAR>s : Finset ℕ<VAR>hs : s ∈ k.primesBelow.powerset<VAR>m : ℕ<VAR>hm : n = m ^ 2 * s.prod id<GOAL>∃ a b, (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt.succ) ∧ b ^ 2 * ∏ x ∈ a, x = n
<VAR>N k n : ℕ<VAR>hn : n ∈ N.smoothNumbersUpTo k<VAR>hn₁ : n ≤ N<VAR>hn₂ : n ∈ k.smoothNumbers<VAR>s : Finset ℕ<VAR>hs : s ∈ k.primesBelow.powerset<VAR>m : ℕ<VAR>hm : n = m ^ 2 * s.prod id<GOAL>m ≠ 0
<VAR>N k n : ℕ<VAR>hn : n ∈ N.smoothNumbersUpTo k<VAR>hn₁ : n ≤ N<VAR>hn₂ : n ∈ k.smoothNumbers<VAR>s : Finset ℕ<VAR>hs : s ∈ k.primesBelow.powerset<VAR>m : ℕ<VAR>hm : n = m ^ 2 * s.prod id<GOAL>m < N.sqrt.succ
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝ : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝ : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this : Algebra.IsSeparable (↥L) K<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝ : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this : Algebra.IsSeparable (↥L) K<VAR>i : ↥S →+* ↥L := Subsemiring.inclusion ⋯<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝² : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this : Algebra.IsSeparable (↥L) K<VAR>i : ↥S →+* ↥L := Subsemiring.inclusion ⋯<VAR>x✝¹ : Algebra ↥S ↥L := i.toAlgebra<VAR>x✝ : SMul ↥S ↥L := Algebra.toSMul<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝² : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this✝ : Algebra.IsSeparable (↥L) K<VAR>i : ↥S →+* ↥L := Subsemiring.inclusion ⋯<VAR>x✝¹ : Algebra ↥S ↥L := i.toAlgebra<VAR>x✝ : SMul ↥S ↥L := Algebra.toSMul<VAR>this : IsScalarTower (↥S) (↥L) K<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝² : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this✝¹ : Algebra.IsSeparable (↥L) K<VAR>i : ↥S →+* ↥L := Subsemiring.inclusion ⋯<VAR>x✝¹ : Algebra ↥S ↥L := i.toAlgebra<VAR>x✝ : SMul ↥S ↥L := Algebra.toSMul<VAR>this✝ : IsScalarTower (↥S) (↥L) K<VAR>this : Algebra.IsAlgebraic F K<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝² : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this✝² : Algebra.IsSeparable (↥L) K<VAR>i : ↥S →+* ↥L := Subsemiring.inclusion ⋯<VAR>x✝¹ : Algebra ↥S ↥L := i.toAlgebra<VAR>x✝ : SMul ↥S ↥L := Algebra.toSMul<VAR>this✝¹ : IsScalarTower (↥S) (↥L) K<VAR>this✝ : Algebra.IsAlgebraic F K<VAR>this : IsPurelyInseparable (↥S) K<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>x : K<VAR>x✝² : x ∈ ⊤<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this✝³ : Algebra.IsSeparable (↥L) K<VAR>i : ↥S →+* ↥L := Subsemiring.inclusion ⋯<VAR>x✝¹ : Algebra ↥S ↥L := i.toAlgebra<VAR>x✝ : SMul ↥S ↥L := Algebra.toSMul<VAR>this✝² : IsScalarTower (↥S) (↥L) K<VAR>this✝¹ : Algebra.IsAlgebraic F K<VAR>this✝ : IsPurelyInseparable (↥S) K<VAR>this : IsPurelyInseparable (↥L) K<GOAL>x ∈ L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : Algebra.IsAlgebraic F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>S : IntermediateField F K := separableClosure F K<VAR>L : IntermediateField E K := adjoin E ↑S<VAR>this✝³ : Algebra.IsSeparable (↥L) K<VAR>i : ↥S →+* ↥L := Subsemiring.inclusion ⋯<VAR>x✝² : Algebra ↥S ↥L := i.toAlgebra<VAR>x✝¹ : SMul ↥S ↥L := Algebra.toSMul<VAR>this✝² : IsScalarTower (↥S) (↥L) K<VAR>this✝¹ : Algebra.IsAlgebraic F K<VAR>this✝ : IsPurelyInseparable (↥S) K<VAR>this : IsPurelyInseparable (↥L) K<VAR>y : ↥L<VAR>x✝ : (algebraMap (↥L) K) y ∈ ⊤<GOAL>(algebraMap (↥L) K) y ∈ L
<VAR>α : Type u_1<VAR>size✝ sz : ℕ<VAR>l' : Ordnode α<VAR>y : α<VAR>r' : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(node size✝ (node sz l' y r') x r).eraseMin.dual = (node size✝ (node sz l' y r') x r).dual.eraseMax
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>v : Set τ<VAR>hv : v ∈ f<GOAL>ω f ϕ s = ⋂ u, closure (image2 ϕ (↑u ∩ v) s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>v : Set τ<VAR>hv : v ∈ f<GOAL>⋂ u ∈ f, closure (image2 ϕ (u ∩ v) s) = ⋂ u, closure (image2 ϕ (↑u ∩ v) s)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>u : Set ι<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ ⋂ n ∈ u, s n<VAR>ht2 : t2 ∈ s'<VAR>n : ι<VAR>hn : n ∈ u<VAR>h : IndepSets (s n) s' κ μ<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Set X<GOAL>setOfIdeal (idealOfSet 𝕜 s) = interior s
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Set X<VAR>x : X<VAR>hx : x ∈ interior s<GOAL>x ∈ setOfIdeal (idealOfSet 𝕜 s)
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Set X<VAR>x : X<VAR>hx : x ∈ (closure sᶜ)ᶜ<GOAL>x ∈ setOfIdeal (idealOfSet 𝕜 s)
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Set X<VAR>x : X<VAR>hx : x ∈ (closure sᶜ)ᶜ<GOAL>∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>s : Set X<VAR>x : X<VAR>hx : x ∈ (closure sᶜ)ᶜ<VAR>g : C(X, ℝ)<VAR>hgs : Set.EqOn (⇑g) 0 (closure sᶜ)<VAR>hgx : Set.EqOn (⇑g) 1 {x}<GOAL>∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬r = 0<GOAL>(C r).support.gcd (C r).coeff = normalize r
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬r = 0<VAR>h : (C r).support = {0}<GOAL>(C r).support.gcd (C r).coeff = normalize r
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : α<VAR>hx : x ∉ s<VAR>this : ↑⟨x, ⋯⟩ ∈ sᶜ<GOAL>(Trans.trans (Trans.trans (Set.union ⋯).symm (Set.ofEq ⋯)) (Set.univ α)).symm x = Sum.inr ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>f✝ g : α → β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>a b : α<GOAL>AEStronglyMeasurable f (μ.restrict (Ι a b)) ↔ AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁹ : SeminormedAddCommGroup V<VAR>inst✝⁸ : PseudoMetricSpace P<VAR>inst✝⁷ : NormedAddTorsor V P<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : MetricSpace Q<VAR>inst✝⁴ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : Invertible 2<VAR>p₁ p₂ : P<GOAL>dist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ z₁ z₂ : ℝ≥0<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ z₁ z₂ : ℝ≥0<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h : (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤ ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p<GOAL>(w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ z₁ z₂ : ℝ≥0<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i = 1
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s s₁ s₂ : Set α<VAR>h₁ : m.IsCaratheodory s₁<VAR>h₂ : m.IsCaratheodory s₂<VAR>t : Set α<GOAL>m t = m (t ∩ (s₁ ∪ s₂)) + m (t \ (s₁ ∪ s₂))
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s s₁ s₂ : Set α<VAR>h₁ : m.IsCaratheodory s₁<VAR>h₂ : m.IsCaratheodory s₂<VAR>t : Set α<GOAL>m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) = m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + m (t ∩ (s₂ \ s₁)) + m (t \ (s₁ ∪ s₂))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp (m • p + a) b = m • p + toIocMod hp a b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q✝ : R[X]<VAR>x : A<VAR>p q : R[X]<VAR>hpq : p.comp q = X<VAR>hqp : q.comp p = X<GOAL>R[X] ≃ₐ[R] R[X]
<VAR>n : ℕ<VAR>a₁ b₁ : ℝ<VAR>m : ℕ<VAR>en : n + 1 = m<VAR>h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)<GOAL>|rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁
<VAR>n : ℕ<VAR>a₁ b₁ : ℝ<VAR>m : ℕ<VAR>en : n + 1 = m<VAR>h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)<GOAL>|1 + 1 / ↑m * ((a₁ - 1) * ↑m) - a₁| ≤ b₁ - |1| / ↑m * (b₁ * ↑m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>hxy : x ≠ y<GOAL>{x, y}.einfsep ≤ edist y x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>hxy : x ≠ y<GOAL>{y, x}.einfsep ≤ edist y x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq β<VAR>f g : α →. β<VAR>inst✝¹ : (x : α) → Decidable (f x).Dom<VAR>inst✝ : (x : α) → Decidable (g x).Dom<VAR>s t : Finset α<VAR>b x : β<GOAL>x ∈ pimage f s ↔ x ∈ image (fun x => (f ↑x).get ⋯) (filter (fun x => (f x).Dom) s).attach
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq β<VAR>f g : α →. β<VAR>inst✝¹ : (x : α) → Decidable (f x).Dom<VAR>inst✝ : (x : α) → Decidable (g x).Dom<VAR>s t : Finset α<VAR>b x : β<GOAL>(∃ a ∈ s, ∃ (h : (f a).Dom), (f a).get h = x) ↔ ∃ a, ∃ (hp : a ∈ s) (hq : (f a).Dom), (f a).get ⋯ = x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>q : ℕ<VAR>x y : R<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x - y) ^ q = x ^ q - y ^ q
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I J X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<GOAL>∃ I J, M.Basis I X ∧ M.Basis (I ∪ J) Y ∧ Disjoint X J
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>I I' : Set α<VAR>hI : M.Basis I X<VAR>hI' : M.Basis I' Y<VAR>hII' : I ⊆ I'<GOAL>∃ I J, M.Basis I X ∧ M.Basis (I ∪ J) Y ∧ Disjoint X J
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>I I' : Set α<VAR>hI : M.Basis I X<VAR>hI' : M.Basis I' Y<VAR>hII' : I ⊆ I'<GOAL>Disjoint X (I' \ I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>I I' : Set α<VAR>hI : M.Basis I X<VAR>hI' : M.Basis I' Y<VAR>hII' : I ⊆ I'<GOAL>∀ ⦃a : α⦄, a ∈ X → ∀ ⦃b : α⦄, b ∈ I' \ I → a ≠ b
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J X✝ Y✝ : Set α<VAR>e✝ : α<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>I I' : Set α<VAR>hI : M.Basis I X<VAR>hI' : M.Basis I' Y<VAR>hII' : I ⊆ I'<VAR>e : α<VAR>heX : e ∈ X<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝² : Fintype β<VAR>inst✝¹ : (b : β) → PseudoMetricSpace (π b)<VAR>inst✝ : Nonempty β<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>hr : r < 0<GOAL>closedBall x r = Set.univ.pi fun b => closedBall (x b) r
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>h : Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0<GOAL>setToSimpleFunc T (map Prod.fst (f.pair g)) = setToSimpleFunc T (map Prod.snd (f.pair g))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>h : Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0<VAR>h_pair : Integrable (↑(f.pair g)) μ<GOAL>setToSimpleFunc T (map Prod.fst (f.pair g)) = setToSimpleFunc T (map Prod.snd (f.pair g))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>h : Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0<VAR>h_pair : Integrable (↑(f.pair g)) μ<GOAL>∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) x.1 = setToSimpleFunc T (map Prod.snd (f.pair g))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>h : Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0<VAR>h_pair : Integrable (↑(f.pair g)) μ<GOAL>∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) x.1 = ∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) x.2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p✝ : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>h : Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0<VAR>h_pair : Integrable (↑(f.pair g)) μ<VAR>p : E × E<VAR>hp : p ∈ (f.pair g).range<GOAL>(T (↑(f.pair g) ⁻¹' {p})) p.1 = (T (↑(f.pair g) ⁻¹' {p})) p.2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>h : Pairwise fun x y => T (↑f ⁻¹' {x} ∩ ↑g ⁻¹' {y}) = 0<VAR>h_pair : Integrable (↑(f.pair g)) μ<VAR>a : α<VAR>hp : ↑(f.pair g) a ∈ (f.pair g).range<GOAL>(T (↑(f.pair g) ⁻¹' {↑(f.pair g) a})) (↑(f.pair g) a).1 = (T (↑(f.pair g) ⁻¹' {↑(f.pair g) a})) (↑(f.pair g) a).2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₂ : ι → P<VAR>p₁ : P<VAR>h : ∑ i ∈ s, w i = 1<GOAL>∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (affineCombination k s p₂) w
<VAR>m n a b c d : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>a * c ≡ b * c [ZMOD n * c]
<VAR>R✝ : Type u<VAR>M : Type v<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R✝ M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝⁷ : StrongRankCondition R✝<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : IsDomain S<VAR>inst✝² : Algebra R S<VAR>n : Type u_3<VAR>m : Type u_4<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype m<VAR>b : Basis n R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>c : Basis m R ↥I<GOAL>Fintype.card m = Fintype.card n
<VAR>R✝ : Type u<VAR>M : Type v<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R✝ M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝⁷ : StrongRankCondition R✝<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : IsDomain S<VAR>inst✝² : Algebra R S<VAR>n : Type u_3<VAR>m : Type u_4<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype m<VAR>b : Basis n R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>c : Basis m R ↥I<VAR>a : ↥I<VAR>ha : a ≠ 0<GOAL>Fintype.card m = Fintype.card n
<VAR>R✝ : Type u<VAR>M : Type v<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R✝ M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝⁷ : StrongRankCondition R✝<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : IsDomain S<VAR>inst✝² : Algebra R S<VAR>n : Type u_3<VAR>m : Type u_4<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype m<VAR>b : Basis n R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>c : Basis m R ↥I<VAR>a : ↥I<VAR>ha : a ≠ 0<VAR>this : LinearIndependent R fun i => b i • a<GOAL>Fintype.card m = Fintype.card n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s ∩ t = 0 ↔ s.Disjoint t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s ∩ t ⊆ 0 ↔ s.Disjoint t
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>inst✝ : S.HasHomology<GOAL>leftRightHomologyComparison' h₁ h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>inst✝ : S.HasHomology<GOAL>leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫ S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom