ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<VAR>this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c<VAR>bdd : BddAbove (range fun x => f x * c)<VAR>hs : ℵ₀ ≤ ⨆ i, f i<GOAL>⨆ i, f i ≤ ⨆ i, f i * c ∧ c ≤ ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<VAR>this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c<VAR>bdd : BddAbove (range fun x => f x * c)<VAR>hs : ℵ₀ ≤ ⨆ i, f i<VAR>i : ι<VAR>hi : 1 < f i<GOAL>⨆ i, f i ≤ ⨆ i, f i * c ∧ c ≤ ⨆ i, f i * c
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>𝟙_ C ◁ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>𝟙_ C ◁ f = (𝟙_ C ◁ f ≫ (λ_ Y).hom) ≫ (λ_ Y).inv
<VAR>α : Type u_1<VAR>f✝ : Filter α<VAR>β : Type u_2<VAR>inst✝¹ : Countable β<VAR>f : Filter α<VAR>inst✝ : CountableInterFilter f<VAR>g : Filter β<VAR>u : α → β → ℝ≥0∞<GOAL>∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun a' => u a' b) f
<VAR>α : Type u_1<VAR>f✝ : Filter α<VAR>β : Type u_2<VAR>inst✝¹ : Countable β<VAR>f : Filter α<VAR>inst✝ : CountableInterFilter f<VAR>g : Filter β<VAR>u : α → β → ℝ≥0∞<GOAL>∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun a' => u a' i) f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s✝ : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>s : Set M<VAR>p : (x : M) → x ∈ closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>one : p 1 ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ closure s<GOAL>p x hx
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s✝ : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>s : Set M<VAR>p : (x : M) → x ∈ closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>one : p 1 ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ closure s<GOAL>∃ (x_1 : x ∈ closure s), p x x_1
<VAR>m n : ℕ<VAR>h : m.Coprime n<VAR>hmn0 : m * n = 0<GOAL>φ (m * n) = φ m * φ n
<VAR>m n : ℕ<VAR>h : m.Coprime n<VAR>hmn0 : ¬m * n = 0<VAR>this : NeZero (m * n)<GOAL>φ (m * n) = φ m * φ n
<VAR>m n : ℕ<VAR>h : m.Coprime n<VAR>hmn0 : ¬m * n = 0<VAR>this✝ : NeZero (m * n)<VAR>this : NeZero m<GOAL>φ (m * n) = φ m * φ n
<VAR>m n : ℕ<VAR>h : m.Coprime n<VAR>hmn0 : ¬m * n = 0<VAR>this✝¹ : NeZero (m * n)<VAR>this✝ : NeZero m<VAR>this : NeZero n<GOAL>φ (m * n) = φ m * φ n
<VAR>m n : ℕ<VAR>h : m.Coprime n<VAR>hmn0 : ¬m * n = 0<VAR>this✝¹ : NeZero (m * n)<VAR>this✝ : NeZero m<VAR>this : NeZero n<GOAL>Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ (v + 1 - 1)) - v * (↑x ^ (u + 1 - 1) * (1 - ↑x) ^ (v - 1))) volume 0 1<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1<VAR>int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1<VAR>int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0<VAR>hF0 : F 0 = 0<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1<VAR>int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0<VAR>hF0 : F 0 = 0<VAR>hF1 : F 1 = 0<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1<VAR>int_ev : (u * ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0 ..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0<VAR>hF0 : F 0 = 0<VAR>hF1 : F 1 = 0<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1<VAR>int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0<VAR>hF0 : F 0 = 0<VAR>hF1 : F 1 = 0<GOAL>IntervalIntegrable (fun y => u * (↑y ^ (u - 1) * (1 - ↑y) ^ v)) volume 0 1
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<VAR>F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v<VAR>hu' : 0 < (u + 1).re<VAR>hv' : 0 < (v + 1).re<VAR>hc : ContinuousOn F (Icc 0 1)<VAR>hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x<VAR>h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1<VAR>int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0<VAR>hF0 : F 0 = 0<VAR>hF1 : F 1 = 0<GOAL>IntervalIntegrable (fun y => v * (↑y ^ u * (1 - ↑y) ^ (v - 1))) volume 0 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Inter α<VAR>a b : Part α<VAR>hab : (a ∩ b).Dom<GOAL>(a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Inter α<VAR>a b : Part α<VAR>hab : (a ∩ b).Dom<GOAL>(a.bind fun y => map (fun x => y ∩ x) b).get ⋯ = a.get ⋯ ∩ b.get ⋯
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Multiset α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>a : α<VAR>s : Multiset α<VAR>h : p a<VAR>_l : List α<GOAL>count a (filter p (Quot.mk Setoid.r _l)) = count a (Quot.mk Setoid.r _l)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Multiset α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>a : α<VAR>s : Multiset α<VAR>h : p a<VAR>_l : List α<GOAL>List.count a (List.filter (fun b => decide (p b)) _l) = List.count a _l
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Multiset α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>a : α<VAR>s : Multiset α<VAR>h : p a<VAR>_l : List α<GOAL>decide (p a) = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>x₀ : E'<VAR>m : ℕ<VAR>h : 1 < m<GOAL>(fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => x - x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<GOAL>(f + g).lintegral μ = ∑ x ∈ (f.pair g).range, (x.1 * μ (↑(f.pair g) ⁻¹' {x}) + x.2 * μ (↑(f.pair g) ⁻¹' {x}))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<GOAL>∑ x ∈ (f.pair g).range, (x.1 + x.2) * μ (↑(f.pair g) ⁻¹' {x}) = ∑ x ∈ (f.pair g).range, (x.1 * μ (↑(f.pair g) ⁻¹' {x}) + x.2 * μ (↑(f.pair g) ⁻¹' {x}))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<GOAL>∑ x ∈ (f.pair g).range, (x.1 * μ (↑(f.pair g) ⁻¹' {x}) + x.2 * μ (↑(f.pair g) ⁻¹' {x})) = ∑ x ∈ (f.pair g).range, x.1 * μ (↑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (↑(f.pair g) ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<GOAL>∑ x ∈ (f.pair g).range, x.1 * μ (↑(f.pair g) ⁻¹' {x}) + ∑ x ∈ (f.pair g).range, x.2 * μ (↑(f.pair g) ⁻¹' {x}) = (map Prod.fst (f.pair g)).lintegral μ + (map Prod.snd (f.pair g)).lintegral μ
<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>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet E)
<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>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<VAR>i : ι<GOAL>f i ≤ ⨆ i, adjoin F ((minpoly F i.snd).rootSet E)
<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>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<VAR>i : ι<VAR>x1 : E<VAR>hx1 : x1 ∈ f i<GOAL>x1 ∈ ⨆ i, adjoin F ((minpoly F i.snd).rootSet E)
<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>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<VAR>i : ι<VAR>x1 : E<VAR>hx1 : x1 ∈ f i<GOAL>adjoin F ((minpoly F x1).rootSet E) ≤ adjoin F ((minpoly F ⟨i, ⟨x1, hx1⟩⟩.snd).rootSet E)
<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>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<VAR>i : ι<VAR>x1 : E<VAR>hx1 : x1 ∈ f i<GOAL>x1 ∈ (minpoly F x1).rootSet E
<VAR>α : Sort u_1<VAR>inst✝ : IsEmpty α<VAR>f : α → ℝ<GOAL>⨅ i, f i = 0
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>not_field : ¬IsField R<VAR>h : M = ⊥<VAR>_h1 : ⊥ ≠ ⊤<VAR>h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>M : Ideal R<VAR>not_field : ¬IsField R<VAR>h : M = ⊥<VAR>_h1 : ⊥ ≠ ⊤<VAR>h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤<VAR>I : Ideal R<VAR>hIbot : ⊥ < I<VAR>hItop : I < ⊤<GOAL>False
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>∅ ∉ hC.diffFinset hs ht
<VAR>w x y✝ z y : ℝ<VAR>hy : 0 < y<GOAL>(orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯
<VAR>w x y✝ z y : ℝ<VAR>hy : 0 < y<GOAL>(StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯).symm = StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) ⋯ (fun x => x ^ y) ⋯
<VAR>n : ℤ<GOAL>cos (↑n * (2 * π) + π) = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>ha : a ∉ s<VAR>hf : 0 ≤ f<VAR>hts : t = insert a s<VAR>ht : t ∈ 𝒜<GOAL>f t ≤ collapse 𝒜 a f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>ha : a ∉ s<VAR>hf : 0 ≤ f<VAR>hts : t = insert a s<VAR>ht : t ∈ 𝒜<GOAL>f t ≤ (if s ∈ 𝒜 then f s else 0) + f t
<VAR>n : ℕ<VAR>α : Type u_1<VAR>f : Fin 0 → α<GOAL>(ofFn f).toList = List.ofFn f
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<GOAL>(ofFn f).toList = List.ofFn f
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>hx : x ≠ 0<VAR>this : ‖x‖ ≠ 0<GOAL>‖(↑‖x‖)⁻¹ • x‖ = 1
<VAR>n : ℕ<GOAL>↑(Nat.fib (n + 1)) - φ * ↑(Nat.fib n) = ψ ^ n
<VAR>n : ℕ<GOAL>(φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
<VAR>n : ℕ<GOAL>(φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n
<VAR>n : ℕ<VAR>nz : √5 ≠ 0<GOAL>√5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<GOAL>#{ s // #↑s < (#α).ord.cof } = #α
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>ha : #α = 0<GOAL>#{ s // #↑s < (#α).ord.cof } = #α
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>ha : #α ≠ 0<GOAL>#{ s // #↑s < (#α).ord.cof } = #α
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>ha : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<GOAL>#{ s // #↑s < (#α).ord.cof } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>ha : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>hr : (#α).ord = type r<GOAL>#{ s // #↑s < (#α).ord.cof } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>ha : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>this : IsWellOrder α r<GOAL>#{ s // #↑s < (#α).ord.cof } = #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>ha : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>this : IsWellOrder α r<GOAL>#{ s // #↑s < (#α).ord.cof } ≤ #α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>h : ∀ x < #α, 2 ^ x < #α<VAR>ha : #α ≠ 0<VAR>h' : (#α).IsStrongLimit<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>hr : (#α).ord = type r<VAR>this : IsWellOrder α r<GOAL>#α ≤ #{ s // #↑s < (#α).ord.cof }
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>h : angle x y = 0<GOAL>‖x + y‖ = ‖x‖ + ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>h : angle x y = 0<GOAL>‖x‖ ^ 2 + 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x} / ball 1 δ = ball x δ
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>Q : Type w₃<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : LieRingModule L N<VAR>inst✝⁸ : LieModule R L N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L P<VAR>inst✝⁴ : LieModule R L P<VAR>inst✝³ : AddCommGroup Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : LieRingModule L Q<VAR>inst✝ : LieModule R L Q<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((liftLie R L M N P) f) (m ⊗ₜ[R] n) = (f m) n
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x y : R✝<VAR>r : ℝ<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>f : MulRingNorm R<GOAL>f ↑n ≤ ↑n
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x : E<GOAL>φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x : E<GOAL>x = φ.symm (φ x)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x : E<GOAL>o = (map (Fin 2) φ.toLinearEquiv) o
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>s ⊆ ⇑e.symm '' t ↔ ⇑e.symm.symm '' s ⊆ t
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>⇑e.symm.symm '' s ⊆ t ↔ ⇑e '' s ⊆ t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>inst✝¹ : HasColimits C<VAR>inst✝ : PreservesColimits S<VAR>A : CostructuredArrow S T<VAR>P : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>hf : Mono f<GOAL>S.map (Subobject.mk f.unop.left.op).arrow.unop ≫ S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ (unop P).hom = A.hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>inst✝¹ : HasColimits C<VAR>inst✝ : PreservesColimits S<VAR>A : CostructuredArrow S T<VAR>P : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>hf : Mono f<GOAL>S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ (Subobject.mk f.unop.left.op).arrow).unop ≫ (unop P).hom = A.hom
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<GOAL>(p.toSubring T hp).Monic ↔ p.Monic
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<GOAL>(p.toSubring T hp).coeff p.natDegree = 1 ↔ ↑((p.toSubring T hp).coeff p.natDegree) = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf : AEStronglyMeasurable f ρ<GOAL>(∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧ Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ Integrable f ρ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)<GOAL>(∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧ Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ Integrable f ρ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)<GOAL>(∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧ Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
<VAR>x✝ y x : ℝ<VAR>hx : x ∈ Icc (-1) 1<GOAL>sin (arcsin x) = x
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S✝<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module S✝ M<VAR>inst✝⁴ : SMul S✝ R<VAR>inst✝³ : IsScalarTower S✝ R M<VAR>p q : Submodule R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝² : Ring R'<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R' M'<VAR>S T : Submodule R' M'<VAR>s t : M'<VAR>hs : s ∈ S<VAR>ht : t ∈ T<GOAL>s - t ∈ S ⊔ T
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S✝<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module S✝ M<VAR>inst✝⁴ : SMul S✝ R<VAR>inst✝³ : IsScalarTower S✝ R M<VAR>p q : Submodule R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝² : Ring R'<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R' M'<VAR>S T : Submodule R' M'<VAR>s t : M'<VAR>hs : s ∈ S<VAR>ht : t ∈ T<GOAL>s + -t ∈ S ⊔ T