ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν] ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>this : SigmaFinite ((μ.singularPart ν).withDensity f)<GOAL>((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν] ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>this✝ : SigmaFinite ((μ.singularPart ν).withDensity f)<VAR>this : SigmaFinite ((ν.withDensity (μ.rnDeriv ν)).withDensity f)<GOAL>((ν.withDensity (μ.rnDeriv ν)).withDensity f).rnDeriv ν =ᶠ[ae ν] ((ν.withDensity (μ.rnDeriv ν)).withDensity f + (μ.singularPart ν).withDensity f).rnDeriv ν
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Semiring α<VAR>f : l ≃. m<VAR>M : Matrix m n α<VAR>i : l<VAR>j : n<GOAL>(f.toMatrix * M) i j = Option.casesOn (f i) 0 fun fi => M fi j
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Semiring α<VAR>f : l ≃. m<VAR>M : Matrix m n α<VAR>i : l<VAR>j : n<GOAL>∑ j_1 : m, (if j_1 ∈ f i then 1 else 0) * M j_1 j = Option.rec 0 (fun val => M val j) (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>a : α<GOAL>s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(∀ (b : α), ∀ x ∈ s.val, f x = b → b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<GOAL>(map f s).SSameSide (f x) (f y) ↔ s.SSameSide x y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>s : Set (GrothendieckTopology C)<GOAL>IsGLB s (sInf s)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>s : Set (GrothendieckTopology C)<GOAL>∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S R : Sieve X<VAR>J : GrothendieckTopology C<VAR>s : Set (GrothendieckTopology C)<GOAL>IsGLB (sieves '' s) (sInf s).sieves
<VAR>α✝ β α : Type u<VAR>n : ℕ<VAR>H : ∀ (s : Finset α), s.card ≤ n<GOAL>#α ≤ ↑n
<VAR>α✝ β α : Type u<VAR>n : ℕ<VAR>H : ↑n < #α<GOAL>∃ s, n < s.card
<VAR>α✝ β α : Type u<VAR>n : ℕ<VAR>H : ↑n < #α<GOAL>↑(n + 1) ≤ #α
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ a⁻¹ * b ∈ ker f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ f (a⁻¹ * b) = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>hs : NullMeasurableSet s μ<VAR>hp : p ≠ 0<VAR>hp_top : p ≠ ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>(fun x => ↑‖s.indicator (fun x => c) x‖₊ ^ p.toReal) = fun x => s.indicator (fun x => ↑‖c‖₊ ^ p.toReal) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>hs : NullMeasurableSet s μ<VAR>hp : p ≠ 0<VAR>hp_top : p ≠ ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>(fun x => ↑‖x‖₊ ^ p.toReal) 0 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>hs : NullMeasurableSet s μ<VAR>hp : p ≠ 0<VAR>hp_top : p ≠ ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>(∫⁻ (x : α), s.indicator (fun x => ↑‖c‖₊ ^ p.toReal) x ∂μ) ^ (1 / p.toReal) = ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s : Set α<VAR>c : G<VAR>hs : NullMeasurableSet s μ<VAR>hp : p ≠ 0<VAR>hp_top : p ≠ ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>0 ≤ 1 / p.toReal
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι✝ : Type u_4<VAR>inst✝⁶ : DecidableEq ι✝<VAR>inst✝⁵ : Fintype ι✝<VAR>e : Basis ι✝ R M<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Module A M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>ι : Type u_7<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → A) →ₗ[A] ι → A<GOAL>(toMatrix' f).det = LinearMap.det f
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<GOAL>⨆ i ∈ I, range (stdBasis R φ i) ≤ ⨅ i ∈ J, ker (proj i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<VAR>i : ι<VAR>hi : i ∈ I<GOAL>comap (stdBasis R φ i) (⨅ i ∈ J, ker (proj i)) = ⊤
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<VAR>i : ι<VAR>hi : i ∈ I<GOAL>∀ ⦃x : φ i⦄, x ∈ ⊤ → ∀ i_1 ∈ J, (proj i_1 ∘ₗ stdBasis R φ i) x = 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<VAR>i : ι<VAR>hi : i ∈ I<VAR>b : φ i<VAR>j : ι<VAR>hj : j ∈ J<GOAL>(proj j ∘ₗ stdBasis R φ i) b = 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<VAR>i : ι<VAR>hi : i ∈ I<VAR>b : φ i<VAR>j : ι<VAR>hj : j ∈ J<GOAL>j ≠ i
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I J : Set ι<VAR>h : Disjoint I J<VAR>j : ι<VAR>hj : j ∈ J<VAR>hi : j ∈ I<VAR>b : φ j<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p₂ : ι → P<VAR>p₁ : P<VAR>h : ∑ i ∈ s, w i = 0<GOAL>∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = -(s.weightedVSub p₂) w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>x' : β<VAR>hx : x' ∈ ↑t<VAR>y' : β<VAR>hy : y' ∈ ↑t<VAR>hne : x' ≠ y'<GOAL>(Disjoint on fun a => filter (fun x => f x = a) s) x' y'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>x' : β<VAR>hx : x' ∈ ↑t<VAR>y' : β<VAR>hy : y' ∈ ↑t<VAR>hne : x' ≠ y'<GOAL>∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
<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>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a✝ b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>a ⊔ ⨆ x, f x = ⨆ x, a ⊔ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>p : PMF α<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>hp : MeasurableSet p.support<GOAL>p.toMeasure (s ∩ p.support) = p.toMeasure s
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : Subfield E<VAR>HF : Set.range ⇑(algebraMap F E) ⊆ ↑K<VAR>HS : S ⊆ ↑K<GOAL>(adjoin F S).toSubfield ≤ K
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : Subfield E<VAR>HF : Set.range ⇑(algebraMap F E) ⊆ ↑K<VAR>HS : S ⊆ ↑K<GOAL>Set.range ⇑(algebraMap F E) ∪ S ⊆ ↑K
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>K : Subfield E<VAR>HF : Set.range ⇑(algebraMap F E) ⊆ ↑K<VAR>HS : S ⊆ ↑K<GOAL>Set.range ⇑(algebraMap F E) ⊆ ↑K ∧ S ⊆ ↑K
<VAR>m c : ℤ<GOAL>(2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
<VAR>m c : ℤ<GOAL>1 = (2 * c + 1) % 2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>↑(mrange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>ν : Measure β<VAR>e : α ≃ᵐ β<GOAL>Measure.map (⇑e.symm) (Measure.map (⇑e) μ) = μ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsAtomistic α<GOAL>sSup {a | IsAtom a} = ⊤
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsAtomistic α<VAR>x : α<GOAL>x ∈ {a | IsAtom a} ↔ x ∈ {a | IsAtom a ∧ a ≤ ⊤}
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x + y) y = ↑(Real.arcsin (‖x‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle y (x + y) = ↑(Real.arcsin (‖x‖ / ‖x + y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle y (y + x) = ↑(Real.arcsin (‖x‖ / ‖y + x‖))
<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>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' n'' : ℤ<VAR>hn' : n' + a = n<VAR>hn'' : n + a = n''<GOAL>(γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
<VAR>a b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>b : ℕ<VAR>hb2 : b + 2 > 1<GOAL>(0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<GOAL>(a + 1 + 1) / (b + 1) = (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<GOAL>(if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) = (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<GOAL>(if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) = (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : X<VAR>y z : Y<GOAL>(⨅ p, dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε + dist y z
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : X<VAR>y z : Y<GOAL>⨅ p, dist x (Φ p) + dist z (Ψ p) ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + dist y z
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : X<VAR>y z : Y<VAR>p : Z<GOAL>0 ∈ lowerBounds (range fun p => dist x (Φ p) + dist z (Ψ p))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>x : X<VAR>y z : Y<VAR>p : Z<GOAL>dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>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).degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>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).degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>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>this : (if hq : q.Monic then ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2 else p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < q.degree<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).degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>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>this : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2.degree < q.degree<GOAL>(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.degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>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>this : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2.degree < q.degree<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.degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)<GOAL>¬q.degree ≤ p.degree → (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).degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)<GOAL>¬q.degree ≤ p.degree → (0, p).2.degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)<VAR>hp : ¬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).degree < q.degree
<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✝ : R[X]<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)<VAR>hp : ¬p ≠ 0<GOAL>(0, 0).2.degree < q.degree
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>x : F α<VAR>p : α → Prop<GOAL>Liftp p x ↔ ∀ u ∈ supp x, p u
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>x : F α<VAR>p : α → Prop<GOAL>(∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp (abs (repr x)), p u
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>x : F α<VAR>p : α → Prop<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u<VAR>i : (P F).B a<GOAL>f i ∈ supp (abs ⟨a, f⟩)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>h : IsUniform<VAR>α : Type u<VAR>x : F α<VAR>p : α → Prop<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u<VAR>i : (P F).B a<GOAL>f i ∈ f '' univ
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiff I I' n f<VAR>hmn : m + 1 ≤ n<GOAL>ContMDiff I.tangent I'.tangent m (tangentMap I I' f)
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f univ<VAR>hmn : m + 1 ≤ n<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMap I I' f) univ