ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<VAR>fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0<VAR>fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹<VAR>hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x<VAR>hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x<VAR>this✝ : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l<VAR>this : Tendsto ((fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) ∘ fun r => r⁻¹) atTop l<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioi a, g' x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atTop l<VAR>a' : ℝ<VAR>haa' : a < a'<VAR>ha' : 0 < a'<VAR>fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0<VAR>fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹<VAR>hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x<VAR>hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x<VAR>this✝ : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l<VAR>this : Tendsto (fun x => (fun x => f x⁻¹ / g x⁻¹) ((fun r => r⁻¹) x)) atTop l<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (verticalIntegral b c) atTop (𝓝 0)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (fun x => ‖verticalIntegral b c x‖) atTop (𝓝 0)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (fun T => 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))) atTop (𝓝 0)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (fun T => 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))) atTop (𝓝 (2 * |c| * 0))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (fun T => b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2) atTop atTop
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (fun x => b.re * x ^ 2 - 2 * |b.im| * |c| * x) atTop atTop
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (fun x => (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (HMul.hMul b.re) atTop atTop
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>U : TopCat<VAR>X : PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>V : Opens ↑U<VAR>x : ↑U<VAR>hx : x ∈ V<GOAL>X.presheaf.germ ⟨f x, ⋯⟩ ≫ (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ ⟨x, hx⟩
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>a : α<VAR>inst✝ : Invertible a<GOAL>⅟a ≤ 0 ↔ a ≤ 0
<VAR>X : Type u_1<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ E<GOAL>Integrable (⇑f) μ
<VAR>X : Type u_1<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ E<GOAL>HasFiniteIntegral (⇑f) μ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(ᘁf ≫ g) = (ᘁg) ≫ ᘁf
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(ᘁf ≫ g) = (λ_ ᘁZ).inv ≫ η_ (ᘁY) Y ▷ ᘁZ ≫ ((ᘁf) ⊗ g) ▷ ᘁZ ≫ (α_ (ᘁX) Z ᘁZ).hom ≫ ᘁX ◁ ε_ (ᘁZ) Z ≫ (ρ_ ᘁX).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ ≫ (α_ (ᘁX) Z ᘁZ).hom ≫ ᘁX ◁ ε_ (ᘁZ) Z ≫ (ρ_ ᘁX).hom = (λ_ ᘁZ).inv ≫ η_ (ᘁY) Y ▷ ᘁZ ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ g) ▷ ᘁZ ≫ (α_ (ᘁX) Z ᘁZ).hom ≫ ᘁX ◁ ε_ (ᘁZ) Z ≫ (ρ_ ᘁX).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(((((λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ) ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ) ≫ (α_ (ᘁX) Z ᘁZ).hom) ≫ ᘁX ◁ ε_ (ᘁZ) Z) ≫ (ρ_ ᘁX).hom = (((((λ_ ᘁZ).inv ≫ η_ (ᘁY) Y ▷ ᘁZ) ≫ ((((((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY) ≫ (ᘁX ◁ f) ▷ ᘁY) ≫ (α_ (ᘁX) Y ᘁY).hom) ≫ ᘁX ◁ ε_ (ᘁY) Y) ≫ (ρ_ ᘁX).hom ⊗ g) ▷ ᘁZ) ≫ (α_ (ᘁX) Z ᘁZ).hom) ≫ ᘁX ◁ ε_ (ᘁZ) Z) ≫ (ρ_ ᘁX).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>((λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ) ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ = ((λ_ ᘁZ).inv ≫ η_ (ᘁY) Y ▷ ᘁZ) ≫ ((((((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY) ≫ (ᘁX ◁ f) ▷ ᘁY) ≫ (α_ (ᘁX) Y ᘁY).hom) ≫ ᘁX ◁ ε_ (ᘁY) Y) ≫ (ρ_ ᘁX).hom ⊗ g) ▷ ᘁZ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ = (λ_ ᘁZ).inv ≫ η_ (ᘁY) Y ▷ ᘁZ ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ g) ▷ ᘁZ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(λ_ ᘁZ).inv ≫ (η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ = (λ_ ᘁZ).inv ≫ (η_ (ᘁY) Y ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ g)) ▷ ᘁZ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝² : HasLeftDual X<VAR>inst✝¹ : HasLeftDual Y<VAR>inst✝ : HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>η_ (ᘁY) Y ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ g) = η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>ε_pos : 0 < ε<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>ε_pos : 0 < ε<VAR>D₀ D₁ : Set α<VAR>perf0 : Perfect D₀<VAR>non0 : D₀.Nonempty<VAR>sub0 : D₀ ⊆ C<VAR>hdisj : Disjoint D₀ D₁<VAR>perf1 : Perfect D₁<VAR>non1 : D₁.Nonempty<VAR>sub1 : D₁ ⊆ C<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>ε_pos : 0 < ε<VAR>D₀ D₁ : Set α<VAR>perf0 : Perfect D₀<VAR>sub0 : D₀ ⊆ C<VAR>hdisj : Disjoint D₀ D₁<VAR>perf1 : Perfect D₁<VAR>sub1 : D₁ ⊆ C<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ D₀<VAR>x₁ : α<VAR>hx₁ : x₁ ∈ D₁<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>ε_pos : 0 < ε<VAR>D₀ D₁ : Set α<VAR>perf0 : Perfect D₀<VAR>sub0 : D₀ ⊆ C<VAR>hdisj : Disjoint D₀ D₁<VAR>perf1 : Perfect D₁<VAR>sub1 : D₁ ⊆ C<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ D₀<VAR>x₁ : α<VAR>hx₁ : x₁ ∈ D₁<VAR>perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))<VAR>non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty<VAR>sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀<VAR>diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>ε_pos : 0 < ε<VAR>D₀ D₁ : Set α<VAR>perf0 : Perfect D₀<VAR>sub0 : D₀ ⊆ C<VAR>hdisj : Disjoint D₀ D₁<VAR>perf1 : Perfect D₁<VAR>sub1 : D₁ ⊆ C<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ D₀<VAR>x₁ : α<VAR>hx₁ : x₁ ∈ D₁<VAR>perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))<VAR>non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty<VAR>sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀<VAR>diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε<VAR>perf1' : Perfect (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))<VAR>non1' : (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)).Nonempty<VAR>sub1' : closure (EMetric.ball x₁ (ε / 2) ∩ D₁) ⊆ D₁<VAR>diam1 : EMetric.diam (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)) ≤ ε<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>ε_pos : 0 < ε<VAR>D₀ D₁ : Set α<VAR>perf0 : Perfect D₀<VAR>sub0 : D₀ ⊆ C<VAR>hdisj : Disjoint D₀ D₁<VAR>perf1 : Perfect D₁<VAR>sub1 : D₁ ⊆ C<VAR>x₀ : α<VAR>hx₀ : x₀ ∈ D₀<VAR>x₁ : α<VAR>hx₁ : x₁ ∈ D₁<VAR>perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))<VAR>non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty<VAR>sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀<VAR>diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε<VAR>perf1' : Perfect (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))<VAR>non1' : (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)).Nonempty<VAR>sub1' : closure (EMetric.ball x₁ (ε / 2) ∩ D₁) ⊆ D₁<VAR>diam1 : EMetric.diam (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)) ≤ ε<GOAL>Disjoint (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))
<VAR>α : Type u<VAR>c d : Cardinal.{u}<VAR>β : Type v<VAR>e : α ≃ β<GOAL>toNat #α = toNat #β
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hc : p.IsPath<VAR>h : u ∈ p.support<GOAL>(?m.20759.append (p.dropUntil u h)).IsPath
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>a b : Π₀ (i : ι), α i<VAR>h : a ≤ b<GOAL>toLex a ≤ toLex b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>a b : Π₀ (i : ι), α i<VAR>h : a ≤ b<VAR>hne : ¬toLex a = toLex b<GOAL>toLex a < toLex b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>x : α<GOAL>x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>x : α<VAR>hba : x < b<GOAL>x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>x : α<VAR>hba : b ≤ x<GOAL>x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (max b d)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q : ℕ<GOAL>(Q q).f 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>hf : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0 : autoParam (f✝ 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a✝)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>f : R → R<VAR>a : A<VAR>ha : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)<GOAL>cfcₙ f a = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.29373, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝ : K.HasHomology i<VAR>A : C<VAR>k : A ⟶ K.X i<VAR>j : ι<VAR>hj : c.next i = j<VAR>i' : ι<VAR>x : A ⟶ K.X i'<VAR>hx : k = x ≫ K.d i' i<GOAL>k ≫ K.d i j = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ (∀ (m : ℕ), ↑m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 (iteratedDeriv m f)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>↑(⨅ i, p i) = ⋂ i, ↑(p i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>⋂ s ∈ range fun i => p i, ↑s = ⋂ i, ↑(p i)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>I * dual A K I = dual A K 1
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionSemiring R<VAR>inst✝ : NeZero 2<VAR>a : R<GOAL>a / 2 + a / 2 = a
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<GOAL>ball x r = ball y r ∨ Disjoint (ball x r) (ball y r)
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<VAR>h : (ball x r ∩ ball y r).Nonempty<GOAL>ball x r = ball y r
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<VAR>h : (ball x r ∩ ball y r).Nonempty<VAR>h₁ : ball x r = ball h.some r<GOAL>ball x r = ball y r
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<VAR>h : (ball x r ∩ ball y r).Nonempty<VAR>h₁ : ball x r = ball h.some r<VAR>h₂ : ball y r = ball h.some r<GOAL>ball x r = ball y r
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedRing 𝔹<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>Summable (norm ∘ fun n => (↑n !)⁻¹ • x ^ n)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedRing 𝔹<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>Summable (norm ∘ fun n => (expSeries 𝕂 𝔸 n) fun x_1 => 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>μ : Measure ℝ<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[>] 0) (𝓝 (μ {b}))
<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>μ : Measure ℝ<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[>] 0) (𝓝 (μ (⋂ r, ⋂ (_ : r > 0), Icc (b - r) (b + r))))
<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>μ : Measure ℝ<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>∀ (i j : ℝ), 0 < i → i ≤ j → Icc (b - i) (b + i) ⊆ Icc (b - j) (b + j)
<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>μ : Measure ℝ<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>∃ r > 0, μ (Icc (b - r) (b + r)) ≠ ⊤
<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 : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>h : E → 𝕜<VAR>c' : 𝕜<VAR>z : E<VAR>S : Set E<VAR>hc : HasDerivAt c c' x<VAR>hx : c x ≠ 0<GOAL>HasDerivAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) x
<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 : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>h : E → 𝕜<VAR>c' : 𝕜<VAR>z : E<VAR>S : Set E<VAR>hc : HasDerivWithinAt c c' univ x<VAR>hx : c x ≠ 0<GOAL>HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) univ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>r : ι → ι → Prop<VAR>inst✝ : IsWellOrder ι r<VAR>f : ι → Ordinal.{max u v}<GOAL>(type r).bsup (bfamilyOfFamily' r f) = sup f
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<GOAL>∑ i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<VAR>cpos : 0 < c<GOAL>∑ i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
<VAR>N : ℕ<VAR>j : ℝ<VAR>hj : 0 < j<VAR>c : ℝ<VAR>hc : 1 < c<VAR>cpos : 0 < c<VAR>A : 0 < 1 - c⁻¹<GOAL>∑ i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.25858, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>addY (map W' f) (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A✝ B✝ A B C : Matrix n n α<VAR>inst✝ : Invertible A<VAR>h : B * A⁻¹ = C<GOAL>B = C * A
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A✝ B✝ A B C : Matrix n n α<VAR>inst✝ : Invertible A<VAR>h : B = C * A<GOAL>B * A⁻¹ = C
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<GOAL>(3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).coeff 4 = 3
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>x : α<VAR>h : f x = x<VAR>n✝ n : ℕ<VAR>ihn : f^[n] x = x<GOAL>f^[n.succ] x = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>e : α ≃ β<VAR>f₁ f₂ : α → α<GOAL>e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u v : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)
<VAR>a b c : ℤ<VAR>h : Minimal a b c<GOAL>IsCoprime a b
<VAR>a b c : ℤ<VAR>h : Minimal a b c<GOAL>a.gcd b = 1
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>hab : ¬a.gcd b = 1<GOAL>False
<VAR>a b c : ℤ<VAR>h : Minimal a b c<VAR>hab : ¬a.gcd b = 1<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpa : p ∣ a.natAbs<VAR>hpb : p ∣ b.natAbs<GOAL>False
<VAR>b c : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpb : p ∣ b.natAbs<VAR>a1 : ℤ<VAR>h : Minimal (↑p * a1) b c<VAR>hab : ¬(↑p * a1).gcd b = 1<VAR>hpa : p ∣ (↑p * a1).natAbs<GOAL>False
<VAR>c : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : ℤ<VAR>hpa : p ∣ (↑p * a1).natAbs<VAR>b1 : ℤ<VAR>hpb : p ∣ (↑p * b1).natAbs<VAR>h : Minimal (↑p * a1) (↑p * b1) c<VAR>hab : ¬(↑p * a1).gcd (↑p * b1) = 1<GOAL>False
<VAR>c : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : ℤ<VAR>hpa : p ∣ (↑p * a1).natAbs<VAR>b1 : ℤ<VAR>hpb : p ∣ (↑p * b1).natAbs<VAR>h : Minimal (↑p * a1) (↑p * b1) c<VAR>hab : ¬(↑p * a1).gcd (↑p * b1) = 1<VAR>hpc : ↑p ^ 2 ∣ c<GOAL>False
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : ℤ<VAR>hpa : p ∣ (↑p * a1).natAbs<VAR>b1 : ℤ<VAR>hpb : p ∣ (↑p * b1).natAbs<VAR>hab : ¬(↑p * a1).gcd (↑p * b1) = 1<VAR>c1 : ℤ<VAR>h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)<GOAL>False
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : ℤ<VAR>hpa : p ∣ (↑p * a1).natAbs<VAR>b1 : ℤ<VAR>hpb : p ∣ (↑p * b1).natAbs<VAR>hab : ¬(↑p * a1).gcd (↑p * b1) = 1<VAR>c1 : ℤ<VAR>h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)<VAR>hf : Fermat42 a1 b1 c1<GOAL>False
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : ℤ<VAR>hpa : p ∣ (↑p * a1).natAbs<VAR>b1 : ℤ<VAR>hpb : p ∣ (↑p * b1).natAbs<VAR>hab : ¬(↑p * a1).gcd (↑p * b1) = 1<VAR>c1 : ℤ<VAR>h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)<VAR>hf : Fermat42 a1 b1 c1<GOAL>c1.natAbs < (↑p ^ 2 * c1).natAbs
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : ℤ<VAR>hpa : p ∣ (↑p * a1).natAbs<VAR>b1 : ℤ<VAR>hpb : p ∣ (↑p * b1).natAbs<VAR>hab : ¬(↑p * a1).gcd (↑p * b1) = 1<VAR>c1 : ℤ<VAR>h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)<VAR>hf : Fermat42 a1 b1 c1<GOAL>1 < p ^ 2
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : ℤ<VAR>hpa : p ∣ (↑p * a1).natAbs<VAR>b1 : ℤ<VAR>hpb : p ∣ (↑p * b1).natAbs<VAR>hab : ¬(↑p * a1).gcd (↑p * b1) = 1<VAR>c1 : ℤ<VAR>h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)<VAR>hf : Fermat42 a1 b1 c1<GOAL>0 < c1.natAbs
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>(shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫ isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫ (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃)).hom.app X = (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)).hom.app X
<VAR>n : ℕ<GOAL>IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<GOAL>(M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<GOAL>BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E