ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>zw : SqLe y d x c<VAR>h : SqLe (x + z) c (y + w) d<VAR>l : c * z * z > d * w * w<GOAL>d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>zw : SqLe y d x c<VAR>h : SqLe (x + z) c (y + w) d<VAR>l : c * z * z > d * w * w<VAR>hm : d * (y * w) ≤ c * (x * z)<GOAL>d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
<VAR>d✝ : ℤ<VAR>c d x y z w : ℕ<VAR>h : SqLe (x + z) c (y + w) d<VAR>hm : d * (y * w) ≤ c * (x * z)<VAR>l : d * (w * w) < c * (z * z)<VAR>zw : d * (y * y) ≤ c * (x * x)<GOAL>d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<VAR>x✝ : ℕ<GOAL>x✝ ∈ Nat.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉₊
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>B : C<VAR>ι : Type w<VAR>X : ι → C<VAR>f : (j : ι) → X j ⟶ B<VAR>inst✝¹ : HasWidePullback B X f<VAR>inst✝ : PreservesLimit (wideCospan B X f) (forget C)<VAR>x y : (forget C).obj (widePullback B X f)<VAR>h₀ : (base f) x = (base f) y<VAR>h : ∀ (j : ι), (π f j) x = (π f j) y<GOAL>x = y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>B : C<VAR>ι : Type w<VAR>X : ι → C<VAR>f : (j : ι) → X j ⟶ B<VAR>inst✝¹ : HasWidePullback B X f<VAR>inst✝ : PreservesLimit (wideCospan B X f) (forget C)<VAR>x y : (forget C).obj (widePullback B X f)<VAR>h₀ : (base f) x = (base f) y<VAR>h : ∀ (j : ι), (π f j) x = (π f j) y<GOAL>∀ (j : WidePullbackShape ι), (limit.π (wideCospan B X f) j) x = (limit.π (wideCospan B X f) j) y
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x y : (i : I) → f✝ i<VAR>i : I<VAR>inst✝ : One γ<VAR>f : α → β<VAR>x✝ : β<GOAL>extend f 1 1 x✝ = 1 x✝
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : Pseudofunctor B C<VAR>a✝ b✝ : B<VAR>f : a✝ ⟶ b✝<GOAL>F.map₂ (λ_ f).inv = (λ_ (F.map f)).inv ≫ (fun a => (F.mapId a).inv) a✝ ▷ F.map f ≫ (fun {a b c} f g => (F.mapComp f g).inv) (𝟙 a✝) f
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : Pseudofunctor B C<VAR>a✝ b✝ : B<VAR>f : a✝ ⟶ b✝<GOAL>(λ_ (F.map f)).hom = ((fun a => (F.mapId a).inv) a✝ ▷ F.map f ≫ (fun {a b c} f g => (F.mapComp f g).inv) (𝟙 a✝) f) ≫ (F.map₂Iso (λ_ f)).hom
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : Pseudofunctor B C<VAR>a✝ b✝ : B<VAR>f : a✝ ⟶ b✝<GOAL>F.map₂ (ρ_ f).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (fun a => (F.mapId a).inv) b✝ ≫ (fun {a b c} f g => (F.mapComp f g).inv) f (𝟙 b✝)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : Pseudofunctor B C<VAR>a✝ b✝ : B<VAR>f : a✝ ⟶ b✝<GOAL>(ρ_ (F.map f)).hom = (F.map f ◁ (fun a => (F.mapId a).inv) b✝ ≫ (fun {a b c} f g => (F.mapComp f g).inv) f (𝟙 b✝)) ≫ (F.map₂Iso (ρ_ f)).hom
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) = -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>{ a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂, c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄), d := -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ - (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } = { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)), c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂), d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x₀ : 𝕜<VAR>hf : HasDerivAt f f' x₀<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖f'‖ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>s t : Interval α<VAR>a b : α<GOAL>b ∈ pure a ↔ b = a
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>comm : (↑(insert a s)).Pairwise fun a b => Commute (f a) (f b)<VAR>ha : a ∉ s<GOAL>(insert a s).noncommProd f comm = f a * s.noncommProd f ⋯
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<GOAL>(μ.prod ν).map ⋯ = ν
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<GOAL>↑((μ.prod ν).map ⋯) = ↑ν
<VAR>a b : ℚ<GOAL>TotallyBounded (Icc a b)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>g h : M ⊗[R] N →ₗ[R] P<VAR>H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)<VAR>z : M ⊗[R] N<GOAL>g 0 = h 0
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>g h : M ⊗[R] N →ₗ[R] P<VAR>H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)<VAR>z x y : M ⊗[R] N<VAR>ihx : g x = h x<VAR>ihy : g y = h y<GOAL>g (x + y) = h (x + y)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>ψ : (p : ℤ) → F.X p ⟶ G.X p<VAR>p : ℤ<GOAL>(ofHoms ψ).v p p ⋯ = ψ p
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>han : (orderOf a).Coprime n<GOAL>a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>han : (orderOf a).Coprime n<GOAL>⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ ⊆ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>han : (orderOf a).Coprime n<VAR>b : A<VAR>hb : orderOf b = n<VAR>c : A<VAR>hc : c ∈ ball (a * b) δ<GOAL>c ∈ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>han : (orderOf a).Coprime n<VAR>b : A<VAR>hb : orderOf b = n<VAR>c : A<VAR>hc : c ∈ ball (a * b) δ<GOAL>∃ i, orderOf i = orderOf a * n ∧ c ∈ ball i δ
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>b : A<VAR>han : (orderOf a).Coprime (orderOf b)<VAR>hb : orderOf b = n<VAR>c : A<VAR>hc : c ∈ ball (a * b) δ<GOAL>orderOf (a * b) = orderOf a * orderOf b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<GOAL>↑(addNSMul h δ 0) = a
<VAR>a b m n✝ p✝ p k n : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<GOAL>p ^ k ∣ n ↔ k ≤ n.factorization p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a : α<VAR>b : β<VAR>fst✝¹ snd✝¹ fst✝ snd✝ : α<GOAL>GameAdd rα s(fst✝¹, snd✝¹) s(fst✝, snd✝) ↔ Prod.GameAdd rα rα (fst✝¹, snd✝¹) (fst✝, snd✝) ∨ Prod.GameAdd rα rα (fst✝¹, snd✝¹).swap (fst✝, snd✝)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < asympBound g a b (r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < asympBound g a b (r i x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<GOAL>HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • p.coeff n) (f z)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<GOAL>(∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))) ↔ ∀ᶠ (a : 𝕜) in 𝓝 0, HasSum (fun n => (z₀ + a - z₀) ^ n • p.coeff n) (f (z₀ + a))
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype m<VAR>A : Matrix m m R<GOAL>Function.Surjective A.mulVec ↔ IsUnit A
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.25254, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>c : KernelFork S.g<VAR>hc : IsLimit c<GOAL>((hc.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ 𝟙 c.pt) ≫ Fork.ι c = 0 ≫ Fork.ι c
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.25254, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>c : KernelFork S.g<VAR>hc : IsLimit c<GOAL>(hc.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ Fork.ι c = 0 ≫ Fork.ι c
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>j : ι<VAR>inst✝ : Decidable (i = j)<GOAL>(b.repr (b i)) j = if i = j then 1 else 0
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt f (f' y) y<VAR>hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y<VAR>hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[>] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[>] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[>] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[>] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[>] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[>] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : s ∈ 𝓝[>] a<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[>] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[>] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[>] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : ∃ u ∈ Ioi a, Ioo a u ⊆ s<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfa : Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ 𝓝[>] a<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ 𝓝[>] a<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ 𝓝[>] a<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>u : ℝ<VAR>hau : u ∈ Ioi a<VAR>hu : Ioo a u ⊆ s<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.19515, u_1} D<VAR>P : MorphismProperty C<VAR>hP : P.RespectsIso<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>hf' : P f'<VAR>e : Arrow.mk f' ≅ Arrow.mk f<GOAL>P f
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<GOAL>A i₁ = A i₀
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hbj : ¬b.degree ≤ ↑j<GOAL>(A i₁).coeff j = (A i₀).coeff j
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hbj : ↑j < b.degree<GOAL>(A i₁).coeff j = (A i₀).coeff j
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff ↑j<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hbj : ↑j < b.degree<GOAL>j < d
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_∅, f ∂μ) x = f x
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<GOAL>(∫⁻ (y : (i : { x // x ∈ ∅ }) → π ↑i), f (updateFinset x ∅ y) ∂Measure.dirac fun a => isEmptyElim a) = f x
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<GOAL>Measurable fun a => f (updateFinset x ∅ a)
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<VAR>α' : Type u_3<VAR>inst✝¹ : MeasurableSpace α'<VAR>β' : Type u_4<VAR>inst✝ : MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>(μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<VAR>α' : Type u_3<VAR>inst✝¹ : MeasurableSpace α'<VAR>β' : Type u_4<VAR>inst✝ : MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>↑((μ.map ⋯).prod (ν.map ⋯)) = ↑((μ.prod ν).map ⋯)
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<VAR>α' : Type u_3<VAR>inst✝¹ : MeasurableSpace α'<VAR>β' : Type u_4<VAR>inst✝ : MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>(Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.28154, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X✝ Y✝ : HomologicalComplex Vᵒᵖ c.symm<VAR>f : X✝ ⟶ Y✝<VAR>i j : ι<VAR>x✝ : c.Rel i j<GOAL>(fun i => (f.f i).unop) i ≫ X✝.unopSymm.d i j = Y✝.unopSymm.d i j ≫ (fun i => (f.f i).unop) j
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>ha : fract a ≠ 0<GOAL>↑⌈a⌉ = a + 1 - fract a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>ha : fract a ≠ 0<GOAL>↑⌈a⌉ = a + 1 - (a + 1 - ↑⌈a⌉)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>α : Type u_6<VAR>inst✝¹ : Subsingleton α<VAR>inst✝ : Preorder α<GOAL>atTop = ⊤
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>α : Type u_6<VAR>inst✝¹ : Subsingleton α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s ∈ atTop<VAR>x : α<GOAL>x ∈ s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>α : Type u_6<VAR>inst✝¹ : Subsingleton α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>x : α<VAR>hs : Ici x ⊆ s<GOAL>x ∈ s
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>L : List α<VAR>h' : ∀ (a : α), a ∈ L → p a<GOAL>pmap f L h' = List.pmapImpl f L h'
<VAR>a b : ℤ<VAR>h : a ≤ b + 1<GOAL>↑(Fintype.card ↑(Set.Icc a b)) = b + 1 - a
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Type u_2<VAR>inst✝² : Ring S<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>hf : Surjective ⇑f<VAR>H : IsArtinianRing R<GOAL>IsArtinianRing S
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Type u_2<VAR>inst✝² : Ring S<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>hf : Surjective ⇑f<VAR>H : WellFounded fun x x_1 => x < x_1<GOAL>WellFounded fun x x_1 => x < x_1