ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F G H : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>φ' : G ⟶ H<VAR>P : Karoubi C<VAR>h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f<VAR>h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f<GOAL>(F.map P.p).f ≫ (φ.app P.X).f ≫ (φ'.app P.X).f = ((F.map P.p).f ≫ (φ.app P.X).f) ≫ (φ'.app P.X).f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>K : ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>K ≤ ↑K.toNNReal
<VAR>s : ℝ<VAR>hs : s ∈ Ioi 0<GOAL>(log ∘ doublingGamma) s = (fun s => log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
<VAR>s : ℝ<VAR>hs : s ∈ Ioi 0<VAR>h1 : √π ≠ 0<GOAL>(log ∘ doublingGamma) s = (fun s => log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
<VAR>s : ℝ<VAR>hs : s ∈ Ioi 0<VAR>h1 : √π ≠ 0<VAR>h2 : Gamma (s / 2) ≠ 0<GOAL>(log ∘ doublingGamma) s = (fun s => log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
<VAR>s : ℝ<VAR>hs : s ∈ Ioi 0<VAR>h1 : √π ≠ 0<VAR>h2 : Gamma (s / 2) ≠ 0<VAR>h3 : Gamma (s / 2 + 1 / 2) ≠ 0<GOAL>(log ∘ doublingGamma) s = (fun s => log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
<VAR>s : ℝ<VAR>hs : s ∈ Ioi 0<VAR>h1 : √π ≠ 0<VAR>h2 : Gamma (s / 2) ≠ 0<VAR>h3 : Gamma (s / 2 + 1 / 2) ≠ 0<VAR>h4 : 2 ^ (s - 1) ≠ 0<GOAL>(log ∘ doublingGamma) s = (fun s => log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
<VAR>s : ℝ<VAR>hs : s ∈ Ioi 0<VAR>h1 : √π ≠ 0<VAR>h2 : Gamma (s / 2) ≠ 0<VAR>h3 : Gamma (s / 2 + 1 / 2) ≠ 0<VAR>h4 : 2 ^ (s - 1) ≠ 0<GOAL>log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + (s - 1) * log 2 - log √π = (fun s => log (Gamma (s / 2)) + log (Gamma (s / 2 + 1 / 2)) + s * log 2 - (log 2 + log √π)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : 1 < s.ncard<VAR>a : α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : 1 < s.ncard<VAR>a : α<VAR>hsf : s.Finite<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>a : α<VAR>hsf : s.Finite<VAR>hs : 1 < hsf.toFinset.card<GOAL>∃ b ∈ s, b ≠ a
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<GOAL>D f K ⊆ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<GOAL>D f K ⊆ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>this : ∀ (e : ℕ), ∃ n, ∀ (p q : ℕ), n ≤ p → n ≤ q → ∃ L ∈ K, x ∈ A f L ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f L ((1 / 2) ^ q) ((1 / 2) ^ e)<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e<VAR>L0 : ℕ → F := fun e => L e (n e) (n e)<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e<VAR>L0 : ℕ → F := fun e => L e (n e) (n e)<VAR>this : CauchySeq L0<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e<VAR>L0 : ℕ → F := fun e => L e (n e) (n e)<VAR>this : CauchySeq L0<VAR>f' : F<VAR>f'K : f' ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e<VAR>L0 : ℕ → F := fun e => L e (n e) (n e)<VAR>this : CauchySeq L0<VAR>f' : F<VAR>f'K : f' ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<VAR>Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e<VAR>L0 : ℕ → F := fun e => L e (n e) (n e)<VAR>this✝ : CauchySeq L0<VAR>f' : F<VAR>f'K : f' ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<VAR>Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e<VAR>this : HasDerivWithinAt f f' (Ici x) x<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>x : ℝ<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e<VAR>L0 : ℕ → F := fun e => L e (n e) (n e)<VAR>this✝ : CauchySeq L0<VAR>f' : F<VAR>f'K : derivWithin f (Ici x) x ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<VAR>Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e<VAR>this : HasDerivWithinAt f f' (Ici x) x<GOAL>x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>x ⧏ 0 ↔ ∃ j, x.moveRight j ≤ 0
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>((∃ i, x ≤ moveLeft 0 i) ∨ ∃ j, x.moveRight j ≤ 0) ↔ ∃ j, x.moveRight j ≤ 0
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : Ring S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module.Free R M<VAR>inst✝⁷ : Module.Finite R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : SMulCommClass R S N<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : StrongRankCondition S<VAR>inst✝ : Module.Free S N<GOAL>finrank S (M →ₗ[R] N) = finrank R M * finrank S N
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q p₁ p₂ q₁ q₂ : R[X]<VAR>hp₁ : p₁ ≠ 0<VAR>hq₁ : q₁ ≠ 0<VAR>hp₂ : p₂ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h_eq : p₁ * q₂ = p₂ * q₁<GOAL>↑p₁.natDegree - ↑q₁.natDegree = ↑p₂.natDegree - ↑q₂.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q p₁ p₂ q₁ q₂ : R[X]<VAR>hp₁ : p₁ ≠ 0<VAR>hq₁ : q₁ ≠ 0<VAR>hp₂ : p₂ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h_eq : p₁ * q₂ = p₂ * q₁<GOAL>↑p₁.natDegree + ↑q₂.natDegree = ↑p₂.natDegree + ↑q₁.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q p₁ p₂ q₁ q₂ : R[X]<VAR>hp₁ : p₁ ≠ 0<VAR>hq₁ : q₁ ≠ 0<VAR>hp₂ : p₂ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h_eq : p₁ * q₂ = p₂ * q₁<GOAL>p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>ha : a ≠ 0<GOAL>a * b ≤ a * c ↔ b ≤ c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>ha : a ≠ 0<GOAL>b * a ≤ c * a ↔ b ≤ c
<VAR>a b m n✝ p✝ n p : ℕ<GOAL>count p n.primeFactorsList = n.factorization p
<VAR>a b m n p✝ p : ℕ<GOAL>count p (primeFactorsList 0) = (factorization 0) p
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn0 : n > 0<GOAL>count p n.primeFactorsList = n.factorization p
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn0 : n > 0<VAR>pp : Prime p<GOAL>count p n.primeFactorsList = n.factorization p
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn0 : n > 0<VAR>pp : Prime p<GOAL>count p n.primeFactorsList = padicValNat p n
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn0 : n > 0<VAR>pp : Prime p<GOAL>count p n.primeFactorsList ≤ padicValNat p n
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn0 : n > 0<VAR>pp : Prime p<GOAL>padicValNat p n ≤ count p n.primeFactorsList
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>bc : b ≤ c<GOAL>(variationOnFromTo f s a - f) b ≤ (variationOnFromTo f s a - f) c
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → ℝ<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>bc : b ≤ c<GOAL>f c - f b ≤ variationOnFromTo f s a c - variationOnFromTo f s a b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>a : Multiset α<VAR>i : Multiset (Multiset α)<GOAL>a.Disjoint i.sum ↔ ∀ b ∈ i, a.Disjoint b
<VAR>x y : ZFSet<VAR>x✝¹ x✝ : PSet<VAR>α : Type u<VAR>A : α → PSet<VAR>β : Type u<VAR>B : β → PSet<GOAL>PSet.mk β B ∈ (PSet.mk α A).powerset ↔ ⟦PSet.mk β B⟧ ⊆ ⟦PSet.mk α A⟧
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>b - toIocMod hp a b = toIocDiv hp a b • p
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i✝ j✝ : n<GOAL>toMatrix' id i✝ j✝ = 1 i✝ j✝
<VAR>X✝ : Type u_1<VAR>inst✝⁴ : PseudoMetricSpace X✝<VAR>m✝ : MeasurableSpace X✝<VAR>μ✝ : Measure X✝<VAR>inst✝³ : μ✝.IsOpenPosMeasure<VAR>X : Type u_2<VAR>inst✝² : MetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : NoAtoms μ<VAR>x : X<VAR>r : ℝ<GOAL>0 < μ (closedBall x r) ↔ 0 < r
<VAR>X✝ : Type u_1<VAR>inst✝⁴ : PseudoMetricSpace X✝<VAR>m✝ : MeasurableSpace X✝<VAR>μ✝ : Measure X✝<VAR>inst✝³ : μ✝.IsOpenPosMeasure<VAR>X : Type u_2<VAR>inst✝² : MetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : NoAtoms μ<VAR>x : X<VAR>r : ℝ<VAR>h : 0 < μ (closedBall x r)<GOAL>0 < r
<VAR>X✝ : Type u_1<VAR>inst✝⁴ : PseudoMetricSpace X✝<VAR>m✝ : MeasurableSpace X✝<VAR>μ✝ : Measure X✝<VAR>inst✝³ : μ✝.IsOpenPosMeasure<VAR>X : Type u_2<VAR>inst✝² : MetricSpace X<VAR>m : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : NoAtoms μ<VAR>x : X<VAR>r : ℝ<VAR>h : r ≤ 0<GOAL>μ (closedBall x r) ≤ 0
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>x : A<VAR>r : R<VAR>y : A<GOAL>x * (algebraMap R A) r * y = x * y * (algebraMap R A) r
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>(cyclotomic n R).degree = ↑n.totient
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>(map (Int.castRingHom R) (cyclotomic n ℤ)).degree = ↑n.totient
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>(cyclotomic n ℤ).degree = ↑n.totient
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>(Int.castRingHom R) (cyclotomic n ℤ).leadingCoeff ≠ 0
<GOAL>LinearEquiv.det conjAe.toLinearEquiv = -1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>y : R<VAR>m : ↥M<GOAL>↑(M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y)) = ↑(y • m)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>y : R<VAR>m : ↥M<GOAL>(M.mulMap 1) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • ↑m
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>y : R<VAR>m : ↥M<GOAL>(M.mulMap 1) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = ↑m * (algebraMap R S) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>h : ¬SameRay ℝ x y<GOAL>|‖x‖ - ‖y‖| < ‖x - y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>h : ¬SameRay ℝ x y<GOAL>‖y‖ - ‖x‖ < ‖x - y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>h : ¬SameRay ℝ x y<GOAL>‖y‖ - ‖x‖ < ‖y - x‖
<VAR>T : ℝ<VAR>inst✝ : Fact (0 < T)<VAR>n : ℤ<GOAL>‖fourier n‖ = 1
<VAR>T : ℝ<VAR>inst✝ : Fact (0 < T)<VAR>n : ℤ<GOAL>⨆ x, ‖(fourier n) x‖ = 1
<VAR>T : ℝ<VAR>inst✝ : Fact (0 < T)<VAR>n : ℤ<VAR>this : ∀ (x : AddCircle T), ‖(fourier n) x‖ = 1<GOAL>⨆ x, ‖(fourier n) x‖ = 1
<VAR>T : ℝ<VAR>inst✝ : Fact (0 < T)<VAR>n : ℤ<VAR>this : ∀ (x : AddCircle T), ‖(fourier n) x‖ = 1<GOAL>⨆ x, 1 = 1
<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>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>x : ι → R<GOAL>b.equivFun.symm x = ∑ i : ι, x i • b i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LE α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : IsSimpleOrder α<GOAL>⊥ ≠ ⊤
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LE α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : IsSimpleOrder α<VAR>a b : α<VAR>h : a ≠ b<GOAL>⊥ ≠ ⊤
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : 𝓢(ℝ, F)<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M<GOAL>(SchwartzMap.seminorm 𝕜 k n) f ≤ M
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : 𝓢(ℝ, F)<VAR>M : ℝ<VAR>hMp : 0 ≤ M<VAR>hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M<GOAL>∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>hf : InjOn f (f ⁻¹' ↑t)<GOAL>(∀ x ∈ s, f x ∈ t) ↔ s ⊆ t.preimage f hf
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hr : r.Sized<GOAL>(l.rotateR x r).dual.Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<VAR>hr : r.Sized<GOAL>(r.dual.rotateL x l.dual).Sized
<VAR>p : ℕ<VAR>z : ℤ<VAR>h : ¬↑p ∣ z<GOAL>(if h : p ≠ 1 ∧ 0 < z.natAbs then (multiplicity p z.natAbs).get ⋯ else 0) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.23384, u_1} C<VAR>inst✝ : Preadditive C<VAR>P Q : Karoubi C<GOAL>0 = P.p ≫ 0 ≫ Q.p
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>α' : Type u_1<VAR>σ' : Type u_2<VAR>f : α' → α<VAR>s : σ<VAR>x : List α'<GOAL>(comap f M).evalFrom s x = M.evalFrom s (List.map f x)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>m : ι → MeasurableSpace Ω<VAR>hm : ∀ (i : ι), m i ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>iCondIndep m' hm' m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>m : ι → MeasurableSpace Ω<VAR>hm : ∀ (i : ι), m i ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>(∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) → μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']) ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>m : ι → MeasurableSpace Ω<VAR>hm : ∀ (i : ι), m i ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>∀ (i : ι), ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>x✝ : p ∣ a<VAR>b : α<VAR>hb : a = p * b<VAR>hb0 : b ≠ 0<GOAL>p * b ~ᵤ (p ::ₘ normalizedFactors b).prod
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>x✝ : p ∣ a<VAR>b : α<VAR>hb : a = p * b<VAR>hb0 : b ≠ 0<GOAL>p * b ~ᵤ p * (normalizedFactors b).prod
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf : BddBelow (f '' Ioi x)<VAR>hf_mono : Monotone f<GOAL>⨅ r, f ↑r = ⨅ q, f ↑↑q
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf : BddBelow (f '' Ioi x)<VAR>hf_mono : Monotone f<GOAL>⨅ r, f ↑r ≤ ⨅ q, f ↑↑q
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hf : BddBelow (f '' Ioi x)<VAR>hf_mono : Monotone f<GOAL>⨅ q, f ↑↑q ≤ ⨅ r, f ↑r
<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 (c * x + d) = c⁻¹ • ∫ (x : ℝ) in c * a + d..c * b + d, f x
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ r, 0 < r ∧ Pairwise fun x x_1 => r ≤ dist x x_1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>x : F<VAR>m : MeasurableSpace α<GOAL>setToSimpleFunc T (const α x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>x : F<VAR>m : MeasurableSpace α<VAR>h✝ : IsEmpty α<GOAL>setToSimpleFunc T (const α x) = (T Set.univ) x