ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<VAR>this : ∀ (n : ℕ), HasSum (fun c => (4 ^ n)⁻¹) (2 ^ (n - 1) / 4 ^ n)<GOAL>Summable fun i => ∑' (y : Composition (i + 1)), (4 ^ ⟨i + 1, y⟩.fst)⁻¹
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<VAR>this : ∀ (n : ℕ), HasSum (fun c => (4 ^ n)⁻¹) (2 ^ (n - 1) / 4 ^ n)<GOAL>(fun i => ∑' (y : Composition (i + 1)), (4 ^ ⟨i + 1, y⟩.fst)⁻¹) = fun i => 1 / 4 * (1 / 2) ^ i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<VAR>this : ∀ (n : ℕ), HasSum (fun c => (4 ^ n)⁻¹) (2 ^ (n - 1) / 4 ^ n)<VAR>n : ℕ<GOAL>∑' (y : Composition (n + 1)), (4 ^ ⟨n + 1, y⟩.fst)⁻¹ = 1 / 4 * (1 / 2) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<VAR>this : ∀ (n : ℕ), HasSum (fun c => (4 ^ n)⁻¹) (2 ^ (n - 1) / 4 ^ n)<VAR>n : ℕ<GOAL>2 ^ n / 4 ^ (n + 1) = 1 / 4 * (1 / 2) ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>p : PMF α<VAR>s✝ t✝ s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : s ∩ p.support = t ∩ p.support<GOAL>p.toMeasure s = p.toMeasure t
<VAR>a✝ b✝ c✝ : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>a ♯ b ♯ c = a ♯ (b ♯ c)
<VAR>a✝ b✝ c✝ : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>max (a.blsub fun a' ha' => a' ♯ b ♯ c) (max (b.blsub fun b' hb' => a ♯ b' ♯ c) (c.blsub fun b' x => a ♯ b ♯ b')) = max (a.blsub fun a' x => a' ♯ (b ♯ c)) (max (b.blsub fun a' ha' => a ♯ (a' ♯ c)) (c.blsub fun b' hb' => a ♯ (b ♯ b')))
<VAR>a✝ b✝ c✝ : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>∀ {i j : Ordinal.{u_1}}, i < b ♯ c → j < b ♯ c → i ≤ j → a ♯ i ≤ a ♯ j
<VAR>a✝ b✝ c✝ : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>∀ {i j : Ordinal.{u_1}}, i < a ♯ b → j < a ♯ b → i ≤ j → i ♯ c ≤ j ♯ c
<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 : F<GOAL>deriv (fun y => f y - c) x = deriv f x
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>f g : M₁ →ₗ[R] M₁<GOAL>(toMatrix v₁ v₁) (f * g) = (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝² : LE α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x y : α<VAR>xy : ¬x ≤ y<VAR>yx : ¬y ≤ x<GOAL>False
<VAR>m n a b c d : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>c * a ≡ c * b [ZMOD c * n]
<VAR>m n a b c d : ℤ<VAR>h : a ≡ b [ZMOD n]<VAR>hc : c < 0<GOAL>c * a ≡ c * b [ZMOD c * n]
<VAR>m n a b d : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>0 * a ≡ 0 * b [ZMOD 0 * n]
<VAR>m n a b c d : ℤ<VAR>h : a ≡ b [ZMOD n]<VAR>hc : 0 < c<GOAL>c * a ≡ c * b [ZMOD c * n]
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite ν'<VAR>h1 : μ ≪ μ'<VAR>h2 : ν ≪ ν'<GOAL>μ.prod ν ≪ μ'.prod ν'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite ν'<VAR>h1 : μ ≪ μ'<VAR>h2 : ν ≪ ν'<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ'.prod ν') s = 0<GOAL>(μ.prod ν) s = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite ν'<VAR>h1 : μ ≪ μ'<VAR>h2 : ν ≪ ν'<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (fun x => ν' (Prod.mk x ⁻¹' s)) =ᶠ[ae μ'] 0<GOAL>(fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
<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>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝¹ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>inst✝ : J.Boundaryless<GOAL>(I.prod J).boundary (M × N) = (I.boundary M).prod 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>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝¹ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>inst✝ : J.Boundaryless<GOAL>univ.prod ∅ ∪ (I.boundary M).prod univ = (I.boundary M).prod 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>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁴ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝¹ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>inst✝ : J.Boundaryless<VAR>this : univ.prod ∅ = ∅<GOAL>univ.prod ∅ ∪ (I.boundary M).prod univ = (I.boundary M).prod univ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q : R[X]<VAR>x✝ : R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q : R[X]<VAR>x✝ : R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))) = eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>h : a ∉ s<GOAL>s ⊆ insert a t ↔ s ⊆ t
<VAR>f : CauSeq ℝ abs<VAR>S : Set ℝ := {x | const abs x < f}<GOAL>∃ x, f ≈ const abs x
<VAR>f : CauSeq ℝ abs<VAR>S : Set ℝ := {x | const abs x < f}<VAR>lb : ∃ x, x ∈ S<GOAL>∃ x, f ≈ const abs x
<VAR>f : CauSeq ℝ abs<VAR>S : Set ℝ := {x | const abs x < f}<VAR>lb : ∃ x, x ∈ S<VAR>ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ S, y ≤ x<GOAL>∃ x, f ≈ const abs x
<VAR>f : CauSeq ℝ abs<VAR>S : Set ℝ := {x | const abs x < f}<VAR>lb : ∃ x, x ∈ S<VAR>ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ S, y ≤ x<VAR>ub : ∃ x, ∀ y ∈ S, y ≤ x<GOAL>∃ x, f ≈ const abs x
<VAR>f : CauSeq ℝ abs<VAR>S : Set ℝ := {x | const abs x < f}<VAR>lb : ∃ x, x ∈ S<VAR>ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ S, y ≤ x<VAR>ub : ∃ x, ∀ y ∈ S, y ≤ x<VAR>h : f < const abs (sSup S)<GOAL>False
<VAR>f : CauSeq ℝ abs<VAR>S : Set ℝ := {x | const abs x < f}<VAR>lb : ∃ x, x ∈ S<VAR>ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ S, y ≤ x<VAR>ub : ∃ x, ∀ y ∈ S, y ≤ x<VAR>h : const abs (sSup S) < f<GOAL>False
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁ l₂ : List (Sigma β)<VAR>L : List (List (Sigma β))<GOAL>L.join.NodupKeys ↔ (∀ l ∈ L, l.NodupKeys) ∧ Pairwise Disjoint (map keys L)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁ l₂ : List (Sigma β)<VAR>L : List (List (Sigma β))<GOAL>(∀ l ∈ L, Pairwise (fun s s' => s.fst ≠ s'.fst) l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L ↔ (∀ l ∈ L, l.NodupKeys) ∧ Pairwise (fun a b => a.keys.Disjoint b.keys) L
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁ l₂ : List (Sigma β)<VAR>L : List (List (Sigma β))<GOAL>Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L ↔ Pairwise (fun a b => a.keys.Disjoint b.keys) L
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁ l₂ : List (Sigma β)<VAR>L : List (List (Sigma β))<GOAL>Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L = Pairwise (fun a b => a.keys.Disjoint b.keys) L
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>L : List (List (Sigma β))<VAR>l₁ l₂ : List (Sigma β)<GOAL>(∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) ↔ l₁.keys.Disjoint l₂.keys
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this : Module.Finite R ↥S<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this : Module.Finite R ↥S<VAR>p' : (↥S)[X] := p.toSubring S.toSubring ⋯<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this : Module.Finite R ↥S<VAR>p' : (↥S)[X] := p.toSubring S.toSubring ⋯<VAR>hSx : IsIntegral (↥S) x<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this : Module.Finite R ↥S<VAR>p' : (↥S)[X] := p.toSubring S.toSubring ⋯<VAR>hSx : IsIntegral (↥S) x<VAR>Sx : Submodule (↥S) B := Subalgebra.toSubmodule (adjoin ↥S {x})<VAR>MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this✝ : Module.Finite R ↥S<VAR>p' : (↥S)[X] := p.toSubring S.toSubring ⋯<VAR>hSx : IsIntegral (↥S) x<VAR>Sx : Submodule (↥S) B := Subalgebra.toSubmodule (adjoin ↥S {x})<VAR>MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx<VAR>this : Module.Finite ↥S ↥Sx<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this✝ : Module.Finite R ↥S<VAR>p' : (↥S)[X] := p.toSubring S.toSubring ⋯<VAR>hSx : IsIntegral (↥S) x<VAR>Sx : Submodule (↥S) B := Subalgebra.toSubmodule (adjoin ↥S {x})<VAR>MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx<VAR>this : Module.Finite ↥S ↥Sx<GOAL>(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (adjoin ↥S {x}))).FG
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this✝ : Module.Finite R ↥S<VAR>p' : (↥S)[X] := p.toSubring S.toSubring ⋯<VAR>hSx : IsIntegral (↥S) x<VAR>Sx : Submodule (↥S) B := Subalgebra.toSubmodule (adjoin ↥S {x})<VAR>MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx<VAR>this : Module.Finite ↥S ↥Sx<GOAL>Module.Finite R ↥(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (adjoin ↥S {x})))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Ring B<VAR>inst✝⁶ : CommRing S✝<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra R B<VAR>f : R →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : eval₂ (algebraMap A B) x p = 0<VAR>S : Subalgebra R A := adjoin R ↑p.coeffs<VAR>this✝² : Module.Finite R ↥S<VAR>p' : (↥S)[X] := p.toSubring S.toSubring ⋯<VAR>hSx : IsIntegral (↥S) x<VAR>Sx : Submodule (↥S) B := Subalgebra.toSubmodule (adjoin ↥S {x})<VAR>MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx<VAR>this✝¹ : Module.Finite ↥S ↥Sx<VAR>this✝ : SMul ↥S ↥Sx := { smul := SMul.smul }<VAR>this : IsScalarTower R ↥S ↥Sx<GOAL>Module.Finite R ↥(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (adjoin ↥S {x})))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>x✝ : α × List α<VAR>a : α<VAR>l : List α<GOAL>ContinuousAt (fun p => insertNth n p.1 p.2) (a, l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>x✝ : α × List α<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun p => insertNth n p.1 p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertNth n (a, l).1 (a, l).2))
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>choose (r + 1) (k + 1) = choose r k + choose r (k + 1)
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(fun x => (k + 1).factorial • x) (choose (r + 1) (k + 1)) = (fun x => (k + 1).factorial • x) (choose r k + choose r (k + 1))
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>k : ℕ<GOAL>(descPochhammer ℤ (k + 1)).smeval (r + 1) = (k + 1).factorial • choose r k + (descPochhammer ℤ (k + 1)).smeval r
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>(fun x y z => 𝒰.gluedCoverT' x y z) x y z ≫ pullback.snd ((fun x y => pullback.fst (𝒰.map x) (𝒰.map y)) y z) ((fun x y => pullback.fst (𝒰.map x) (𝒰.map y)) y x) = pullback.fst ((fun x y => pullback.fst (𝒰.map x) (𝒰.map y)) x y) ((fun x y => pullback.fst (𝒰.map x) (𝒰.map y)) x z) ≫ (fun x y => (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom) x y
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>r : R<GOAL>(monomial n) r * X = (monomial (n + 1)) r
<VAR>x y : ℝ<VAR>hx : 0 < x<VAR>h : x < y<GOAL>log x < log y
<VAR>k : ℕ<GOAL>(π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
<VAR>k : ℕ<GOAL>2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
<VAR>k : ℕ<GOAL>2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.restrictScalars S (ideal R S)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤ Submodule.restrictScalars S (ideal R S)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>Submodule.restrictScalars S (ideal R S) ≤ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
<VAR>n m l : ℕ<VAR>hml : m ≤ l<VAR>k : ℕ<VAR>hk : k ∈ Ico n m<GOAL>¬decide (l ≤ k) = true
<VAR>n m l : ℕ<VAR>hml : m ≤ l<VAR>k : ℕ<VAR>hk : k ∈ Ico n m<GOAL>¬l ≤ k
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (x / c + d) = c • ∫ (x : ℝ) in a / c + d..b / c + d, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SFinite ν<VAR>hμν : μ ≪ ν<GOAL>∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SFinite ν<VAR>hμν : μ ≪ ν<GOAL>{x | (fun x => 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SFinite ν<VAR>hμν : μ ≪ ν<VAR>x : α<VAR>hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x<VAR>hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x<GOAL>0 < ν.rnDeriv μ x