ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0<VAR>g : α → ℝ≥0<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>lim : Tendsto f u (𝓝 g)<VAR>hf : ∀ (i : ι), Measurable fun x => ↑(f i x)<GOAL>Measurable fun x => ↑(g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0<VAR>g : α → ℝ≥0<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>lim : Tendsto f u (𝓝 g)<VAR>hf : ∀ (i : ι), Measurable fun x => ↑(f i x)<GOAL>Tendsto (fun i x => ↑(f i x)) u (𝓝 fun x => ↑(g x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0<VAR>g : α → ℝ≥0<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))<VAR>hf : ∀ (i : ι), Measurable fun x => ↑(f i x)<GOAL>∀ (x : α), Tendsto (fun i => ↑(f i x)) u (𝓝 ↑(g x))
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ≥0<VAR>hr : 0 < r<GOAL>∃ d, f ↑d < r
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>g : Γ₀ˣ<VAR>hg1 : g ≠ 1<GOAL>∃ d, f ↑d < r
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>g : Γ₀ˣ<VAR>hg1 : g ≠ 1<VAR>u : Γ₀ˣ := if g < 1 then g else g⁻¹<VAR>hu : u = if g < 1 then g else g⁻¹<VAR>hfu : f ↑u < 1<GOAL>∃ d, f ↑d < r
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>g : Γ₀ˣ<VAR>hg1 : g ≠ 1<VAR>u : Γ₀ˣ := if g < 1 then g else g⁻¹<VAR>hu : u = if g < 1 then g else g⁻¹<VAR>hfu : f ↑u < 1<VAR>n : ℕ<VAR>hn : f ↑u ^ n < r<GOAL>∃ d, f ↑d < r
<VAR>Γ₀ : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>h : Nontrivial Γ₀ˣ<VAR>f : Γ₀ →*₀ ℝ≥0<VAR>hf : StrictMono ⇑f<VAR>r : ℝ≥0<VAR>hr : 0 < r<VAR>g : Γ₀ˣ<VAR>hg1 : g ≠ 1<VAR>u : Γ₀ˣ := if g < 1 then g else g⁻¹<VAR>hu : u = if g < 1 then g else g⁻¹<VAR>hfu : f ↑u < 1<VAR>n : ℕ<VAR>hn : f ↑u ^ n < r<GOAL>f ↑(u ^ n) < r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : NormedLinearOrderedField K<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝² : FloorRing K<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : HasSolidNorm K<VAR>m : E<GOAL>‖fract b m‖ ≤ ∑ i : ι, ‖b i‖
<GOAL>Gamma (1 / 2) = ↑π ^ (1 / 2)
<GOAL>Gamma (1 / 2) = ↑(Real.Gamma (1 / 2))
<GOAL>↑π ^ (1 / 2) = ↑√π
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<VAR>cs : α<VAR>hcs : cs ∈ s<VAR>ct : α<VAR>hct : ct ∈ t<GOAL>hausdorffEdist s t ≠ ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<VAR>cs : α<VAR>hcs : cs ∈ s<VAR>ct : α<VAR>hct : ct ∈ t<VAR>rs : ℝ<VAR>hrs : s ⊆ closedBall ct rs<GOAL>hausdorffEdist s t ≠ ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<VAR>cs : α<VAR>hcs : cs ∈ s<VAR>ct : α<VAR>hct : ct ∈ t<VAR>rs : ℝ<VAR>hrs : s ⊆ closedBall ct rs<VAR>rt : ℝ<VAR>hrt : t ⊆ closedBall cs rt<GOAL>hausdorffEdist s t ≠ ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<VAR>cs : α<VAR>hcs : cs ∈ s<VAR>ct : α<VAR>hct : ct ∈ t<VAR>rs : ℝ<VAR>hrs : s ⊆ closedBall ct rs<VAR>rt : ℝ<VAR>hrt : t ⊆ closedBall cs rt<VAR>this : hausdorffEdist s t ≤ ENNReal.ofReal (max rs rt)<GOAL>hausdorffEdist s t ≠ ⊤
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V : Set (β × β)<VAR>hV : Prod.swap ⁻¹' V = V<VAR>x y : β<GOAL>(x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<GOAL>sSup S = conGen fun x y => ∃ c ∈ S, c x y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<GOAL>sSup S = sInf {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<VAR>x✝ : Con M<GOAL>x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ w x y : K<VAR>hxy : x ≤ y<VAR>z : K<GOAL>z + x ≤ z + y
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ w x y : K<VAR>hxy : re x ≤ re y ∧ im x = im y<VAR>z : K<GOAL>re (z + x) ≤ re (z + y) ∧ im (z + x) = im (z + y)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w x : K<GOAL>0 ≤ x ↔ ∃ s, x = star s * s
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w x : K<GOAL>0 ≤ re x ∧ im x = 0 ↔ ∃ s, x = star s * s
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w x : K<GOAL>(∃ s, x = star s * s) → 0 ≤ re x ∧ im x = 0
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w s : K<GOAL>0 ≤ re (star s * s) ∧ im (star s * s) = 0
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasFiniteBiproducts C<VAR>inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<GOAL>∃ e, ∀ (a : α), g (e a) = f a
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasFiniteBiproducts C<VAR>inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<GOAL>(c : ι) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasFiniteBiproducts C<VAR>inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<VAR>c : ι<GOAL>Nonempty (↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasFiniteBiproducts C<VAR>inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<VAR>c : ι<GOAL>Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasFiniteBiproducts C<VAR>inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<VAR>c : ι<VAR>val✝ : Fintype α<GOAL>Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasFiniteBiproducts C<VAR>inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<VAR>c : ι<VAR>val✝¹ : Fintype α<VAR>val✝ : Fintype β<GOAL>Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasFiniteBiproducts C<VAR>inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)<VAR>c : ι<VAR>val✝¹ : Fintype α<VAR>val✝ : Fintype β<GOAL>Fintype.card ↑(f ⁻¹' {c}) = Fintype.card ↑(g ⁻¹' {c})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>limsup u f \ a = limsup (fun b => u b \ a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>(⨅ s ∈ f, ⨆ a ∈ s, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
<VAR>b c n : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<GOAL>log b n ≤ log c n
<VAR>b c : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<GOAL>log b 0 ≤ log c 0
<VAR>b c n : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<VAR>hn : n ≠ 0<GOAL>log b n ≤ log c n
<VAR>b c n : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<VAR>hn : n ≠ 0<GOAL>c ^ log b n ≤ n
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>β : Type u_5<VAR>hα : IsEmpty α<VAR>f : α →ₛ β<GOAL>f.range = ∅
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>β : Type u_5<VAR>hα : IsEmpty α<VAR>f : α →ₛ β<GOAL>¬f.range.Nonempty
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>β : Type u_5<VAR>hα : IsEmpty α<VAR>f : α →ₛ β<VAR>y : β<VAR>hy_mem : y ∈ f.range<GOAL>False
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>β : Type u_5<VAR>hα : IsEmpty α<VAR>f : α →ₛ β<VAR>y : β<VAR>hy_mem : ∃ y_1, ↑f y_1 = y<GOAL>False
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>β : Type u_5<VAR>hα : IsEmpty α<VAR>f : α →ₛ β<VAR>y : β<VAR>x : α<VAR>hxy : ↑f x = y<GOAL>False
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>β : Type u_5<VAR>hα : α → False<VAR>f : α →ₛ β<VAR>y : β<VAR>x : α<VAR>hxy : ↑f x = y<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s s₁ s₂ : Set α<VAR>t : Finset α<VAR>a b : α<VAR>m n : ℕ<GOAL>G.CliqueFreeOn {a} n ↔ 1 < n
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>Splits (RingHom.id (ZMod p)) (X ^ p - X)
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hp : 1 < p<GOAL>Splits (RingHom.id (ZMod p)) (X ^ p - X)
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hp : 1 < p<VAR>h1 : (X ^ p - X).roots = univ.val<GOAL>Splits (RingHom.id (ZMod p)) (X ^ p - X)
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hp : 1 < p<VAR>h1 : (X ^ p - X).roots = univ.val<VAR>h2 : (X ^ p - X).natDegree = p<GOAL>Splits (RingHom.id (ZMod p)) (X ^ p - X)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝¹ n n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>hp : 1 < n✝ + 1<VAR>h1 : (X ^ (n✝ + 1) - X).roots = univ.val<VAR>h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1<GOAL>Splits (RingHom.id (ZMod (n✝ + 1))) (X ^ (n✝ + 1) - X)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>ppredB predB : K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>nth_den_eq : g.dens n = ppredB<VAR>succ_nth_den_eq : g.dens (n + 1) = predB<GOAL>g.dens (n + 2) = gp.b * predB + gp.a * ppredB
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>predB : K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>succ_nth_den_eq : g.dens (n + 1) = predB<VAR>ppredConts : Pair K<VAR>nth_conts_eq : g.conts n = ppredConts<VAR>nth_den_eq : g.dens n = ppredConts.b<GOAL>g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>ppredConts : Pair K<VAR>nth_conts_eq : g.conts n = ppredConts<VAR>nth_den_eq : g.dens n = ppredConts.b<VAR>predConts : Pair K<VAR>succ_nth_conts_eq : g.conts (n + 1) = predConts<VAR>succ_nth_den_eq : g.dens (n + 1) = predConts.b<GOAL>g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s U : Set X<GOAL>ContinuousOn U.boolIndicator s ↔ IsClopen (Subtype.val ⁻¹' U)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s U : Set X<GOAL>Continuous (s.restrict U.boolIndicator) ↔ Continuous (Subtype.val ⁻¹' U).boolIndicator
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, 1 = b - a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>l : Y ⟶ X<VAR>hl : l ≫ f = g<GOAL>l = lift f g H'
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n✝ : ℕ<VAR>a : M<VAR>n : ℕ<GOAL>a ^ (n + 1 + 1) = a * a ^ (n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy this : span B ↑y = ⊤<GOAL>∃ B₀, B₀.FG ∧ ⊤.FG
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy : span B ↑y = ⊤<VAR>this : ∀ (x : C), ∃ f, ∑ i ∈ y, f i • i = x<GOAL>∃ B₀, B₀.FG ∧ ⊤.FG
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy : span B ↑y = ⊤<VAR>f : C → C → B<VAR>hf : ∀ (x : C), ∑ i ∈ y, f x i • i = x<VAR>s : Finset B := image₂ f (x ∪ y * y) y<GOAL>∃ B₀, B₀.FG ∧ ⊤.FG
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy : span B ↑y = ⊤<VAR>f : C → C → B<VAR>hf : ∀ (x : C), ∑ i ∈ y, f x i • i = x<VAR>s : Finset B := image₂ f (x ∪ y * y) y<VAR>hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<GOAL>∃ B₀, B₀.FG ∧ ⊤.FG
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy : span B ↑y = ⊤<VAR>f : C → C → B<VAR>hf : ∀ (x : C), ∑ i ∈ y, f x i • i = x<VAR>s : Finset B := image₂ f (x ∪ y * y) y<VAR>hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<VAR>hyy : span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<GOAL>∃ B₀, B₀.FG ∧ ⊤.FG
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy : span B ↑y = ⊤<VAR>f : C → C → B<VAR>hf : ∀ (x : C), ∑ i ∈ y, f x i • i = x<VAR>s : Finset B := image₂ f (x ∪ y * y) y<VAR>hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<VAR>hyy : span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<GOAL>span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy : span B ↑y = ⊤<VAR>f : C → C → B<VAR>hf : ∀ (x : C), ∑ i ∈ y, f x i • i = x<VAR>s : Finset B := image₂ f (x ∪ y * y) y<VAR>hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<VAR>hyy : span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<GOAL>restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)) = restrictScalars A ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>inst✝⁶ : CommSemiring A<VAR>inst✝⁵ : CommSemiring B<VAR>inst✝⁴ : Semiring C<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra B C<VAR>inst✝¹ : Algebra A C<VAR>inst✝ : IsScalarTower A B C<VAR>x : Finset C<VAR>hx : Algebra.adjoin A ↑x = ⊤<VAR>y : Finset C<VAR>hy : span B ↑y = ⊤<VAR>f : C → C → B<VAR>hf : ∀ (x : C), ∑ i ∈ y, f x i • i = x<VAR>s : Finset B := image₂ f (x ∪ y * y) y<VAR>hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<VAR>hyy : span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)<GOAL>↑(Submonoid.closure ↑x) ⊆ ↑(restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(IsBigOWith c l f'' fun _x => 0) ↔ f'' =ᶠ[l] 0
<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>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<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>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>this : Tendsto (fun ε => ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑0 * μ s))<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<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>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>this : Tendsto (fun ε => ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<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>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>this : Tendsto (fun ε => ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))<GOAL>∀ᶠ (c : ℝ≥0) in 𝓝[>] 0, μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑c * μ 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>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>this : Tendsto (fun ε => ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))<GOAL>∀ a ∈ Ioi 0, μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑a * μ 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>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>this : Tendsto (fun ε => ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))<VAR>ε : ℝ≥0<VAR>εpos : ε ∈ Ioi 0<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s