ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<GOAL>p %ₘ q = p - q * (p /ₘ q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree<GOAL>p %ₘ q = p - q * (p /ₘ q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree<VAR>ih : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q = p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) - q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)<GOAL>(if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).2 else p) = p - q * if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).1 else 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree<VAR>ih : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q = p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) - q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)<GOAL>(C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2).2 = p - q * if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).1 else 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree<VAR>ih : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 = p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) - q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)<GOAL>(C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2).2 = p - q * if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).1 else 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree<VAR>ih : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 = p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) - q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)<GOAL>p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) - q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q) = p - q * if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).1 else 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree<VAR>ih : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 = p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) - q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)<GOAL>(p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) - q * if hq : q.Monic then ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).1 else 0) = p - q * if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).1 else 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)<GOAL>(if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).2 else p) = p - q * if h : q.Monic then (if q.degree ≤ p.degree ∧ ¬p = 0 then (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) + ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1, ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2) else (0, p)).1 else 0
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (z * y + x) y<GOAL>IsCoprime x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s : Sym α n<VAR>a b : α<GOAL>s = replicate n a ↔ ∀ b ∈ s, b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s : Sym α n<VAR>a b : α<GOAL>(Multiset.card ↑s = n ∧ ∀ b ∈ ↑s, b = a) ↔ ∀ b ∈ s, b = a
<VAR>α✝ : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<GOAL>Small.{v, u} α ↔ lift.{v + 1, u} #α < univ.{v, max u (v + 1)}
<VAR>α✝ : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<GOAL>Small.{v, u} α ↔ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>g : σ → τ<VAR>p : MvPolynomial σ R<GOAL>(map f) ((rename g) p) = (rename g) ((map f) p)
<VAR>x y : ℝ<GOAL>sinh (x + y) = sinh x * cosh y + cosh x * sinh y
<VAR>x y : ℝ<GOAL>↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<GOAL>a < b - c ↔ a + c < b
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<VAR>h' : a < b - c<GOAL>a + c ≠ b
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ a + c<VAR>h' : a < a + c - c<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C✝ C : ℝ<VAR>hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C<GOAL>∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : Nonempty α<VAR>r : α → β → Prop<GOAL>(∃ b, ∀ᶠ (a : α) in atBot, r a b) ↔ ∀ᶠ (a₀ : α) in atBot, ∃ b, ∀ a ≤ a₀, r a b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : Nonempty α<VAR>r : α → β → Prop<GOAL>(∃ x y, ∀ b ≤ x, r b y) ↔ ∃ a, ∀ b ≤ a, ∃ b_1, ∀ a ≤ b, r a b_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioc b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioc b₁ b₂))
<VAR>p : ℝ<VAR>hp : 0 < p<VAR>x : ℝ<GOAL>‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
<VAR>p : ℝ<VAR>hp : 0 < p<VAR>x : ℝ<GOAL>‖↑x‖ = |p| * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>this : LocallyCompactSpace H<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<VAR>hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι✝ I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<VAR>hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f<VAR>ι : Type uM<VAR>c : ι → M<VAR>f : (a : ι) → SmoothBumpFunction I (c a)<VAR>hf : ∀ (a : ι), c a ∈ s ∧ tsupport ↑(f a) ⊆ U (c a)<VAR>hsub' : s ⊆ ⋃ a, support ↑(f a)<VAR>hfin : LocallyFinite fun a => support ↑(f a)<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι✝ I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<VAR>hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f<VAR>ι : Type uM<VAR>c : ι → M<VAR>f : (a : ι) → SmoothBumpFunction I (c a)<VAR>hsub' : s ⊆ ⋃ a, support ↑(f a)<VAR>hfin : LocallyFinite fun a => support ↑(f a)<VAR>hcs : ∀ (a : ι), c a ∈ s<VAR>hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι✝ I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<VAR>hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f<VAR>ι : Type uM<VAR>c : ι → M<VAR>f : (a : ι) → SmoothBumpFunction I (c a)<VAR>hsub' : s ⊆ ⋃ a, support ↑(f a)<VAR>hfin : LocallyFinite fun a => support ↑(f a)<VAR>hcs : ∀ (a : ι), c a ∈ s<VAR>hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)<VAR>V : ι → Set M<VAR>hsV : s ⊆ iUnion V<VAR>hVc : ∀ (i : ι), IsClosed (V i)<VAR>hVf : ∀ (i : ι), V i ⊆ support ↑(f i)<GOAL>∃ ι f, f.IsSubordinate U
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι✝ I M s<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>hs : IsClosed s<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<VAR>hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f<VAR>ι : Type uM<VAR>c : ι → M<VAR>f : (a : ι) → SmoothBumpFunction I (c a)<VAR>hsub' : s ⊆ ⋃ a, support ↑(f a)<VAR>hfin : LocallyFinite fun a => support ↑(f a)<VAR>hcs : ∀ (a : ι), c a ∈ s<VAR>hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)<VAR>V : ι → Set M<VAR>hsV : s ⊆ iUnion V<VAR>hVc : ∀ (i : ι), IsClosed (V i)<VAR>hVf : ∀ (i : ι), V i ⊆ support ↑(f i)<VAR>r : ι → ℝ<VAR>hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut<VAR>hr : ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)<GOAL>∃ ι f, f.IsSubordinate U
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f : α → ℝ<VAR>t : Set α<VAR>hf : IntegrableOn f t μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ<GOAL>0 ≤ᶠ[ae (μ.restrict t)] f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f : α → ℝ<VAR>t : Set α<VAR>hf : IntegrableOn f t μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h's : (μ.restrict t) s < ⊤<GOAL>0 ≤ ∫ (x : α) in s, f x ∂μ.restrict t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f : α → ℝ<VAR>t : Set α<VAR>hf : IntegrableOn f t μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h's : (μ.restrict t) s < ⊤<GOAL>0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f : α → ℝ<VAR>t : Set α<VAR>hf : IntegrableOn f t μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h's : (μ.restrict t) s < ⊤<GOAL>μ (s ∩ t) < ⊤
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t u : Multiset α<GOAL>s.Disjoint (t + u) ↔ s.Disjoint t ∧ s.Disjoint u
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t u : Multiset α<GOAL>t.Disjoint s ∧ u.Disjoint s ↔ s.Disjoint t ∧ s.Disjoint u
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : 0 < ad<VAR>hbd : 0 < bd<VAR>hgcd : 0 < gcd<GOAL>(a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<GOAL>{p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<VAR>h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)<GOAL>{p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<VAR>h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)<GOAL>(∀ s ∈ (fun φ => {p | φ ∈ p}) '' S, s = Set.univ) ↔ ∀ φ ∈ S, {p | φ ∈ p} = Set.univ
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : UniformContinuousOn f s<GOAL>ContinuousOn f s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : UniformContinuous (s.restrict f)<GOAL>ContinuousOn f s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : UniformContinuous (s.restrict f)<GOAL>Continuous (s.restrict f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>h0 : 0 < k<GOAL>ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>h0 : 0 < k<GOAL>IsPrimitiveRoot ζ k → ζ ^ k = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A✝ A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>-J l R * Aᵀ * J l R * A = 1
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>PG₁ PG₂ : Pregroupoid H<VAR>h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s<GOAL>PG₁.groupoid ≤ PG₂.groupoid
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>PG₁ PG₂ : Pregroupoid H<VAR>h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ PG₁.groupoid<GOAL>e ∈ PG₂.groupoid
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>PG₁ PG₂ : Pregroupoid H<VAR>h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s<VAR>e : PartialHomeomorph H H<VAR>he : PG₁.property (↑e) e.source ∧ PG₁.property (↑e.symm) e.target<GOAL>PG₂.property (↑e) e.source ∧ PG₂.property (↑e.symm) e.target
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ∨ o.oangle x y = ↑π ↔ x = 0 ∨ ∃ r, y = r • x
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ x = 0 ∨ ∃ r, y = r • x
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>0 ^ ↑n = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>n ≠ 0