ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.366230<VAR>S'' : Type ?u.366233<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>x✝ : P.vars<VAR>m✝ : P'.vars →₀ ℕ<GOAL>coeff m✝ (((Hom.id P').comp f).val x✝) = coeff m✝ (f.val x✝)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>image2 f (↑s ∪ ↑s') (↑t ∩ ↑t') ⊆ image2 f ↑s ↑t ∪ image2 f ↑s' ↑t'
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : AddGroup A<VAR>s : Set G<VAR>inst✝¹ : Group α<VAR>inst✝ : MulDistribMulAction α G<VAR>H : Subgroup G<VAR>h : G<VAR>hh : h ∈ H<VAR>this : {x | x ∈ H} = ↑H<GOAL>{h} * ↑H = ↑H
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>w : Set M<VAR>x : ↥(span R w)<GOAL>(Finsupp.total (↑w) M R Subtype.val) (repr R w x) = ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>w : Set M<VAR>x : ↥(span R w)<GOAL>(Finsupp.total (↑w) M R Subtype.val) ⋯.choose = ↑x
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>P y ≠ W'.negY P
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0<GOAL>P y ≠ W'.negY P
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0<VAR>hy : P y = W'.negY P<GOAL>P y * Q z ^ 3 = Q y * P z ^ 3
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : U ≤ V<VAR>u : ↑↑X.toPresheafedSpace<VAR>hu : u ∈ ↑U<GOAL>f.val.base u ∈ ↑(f ''ᵁ V)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A B : Matrix n n α<VAR>k : α<VAR>inst✝ : Invertible k<VAR>h : IsUnit A.det<GOAL>⅟k • A⁻¹ * k • A = 1
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>hs : s₁ ⊆ s₂<GOAL>extend m s₁ ≤ extend m s₂
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>hs : s₁ ⊆ s₂<GOAL>∀ (i : MeasurableSet s₂), extend m s₁ ≤ m s₂ i
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>hs : s₁ ⊆ s₂<VAR>h₂ : MeasurableSet s₂<GOAL>extend m s₁ ≤ m s₂ h₂
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>hs : s₁ ⊆ s₂<VAR>h₂ : MeasurableSet s₂<VAR>this : extend m (s₁ ∪ s₂ \ s₁) = extend m s₁ + extend m (s₂ \ s₁)<GOAL>extend m s₁ ≤ m s₂ h₂
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>hs : s₁ ⊆ s₂<VAR>h₂ : MeasurableSet s₂<VAR>this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)<GOAL>extend m s₁ ≤ m s₂ h₂
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>s₁ s₂ : Set α<VAR>h₁ : MeasurableSet s₁<VAR>hs : s₁ ⊆ s₂<VAR>h₂ : MeasurableSet s₂<VAR>this : extend m s₂ = extend m s₁ + extend m (s₂ \ s₁)<GOAL>extend m s₁ ≤ extend m s₂
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>Ioc a a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : ι → Set α<GOAL>⋂ i, f i = ∅ ↔ ∀ (x : α), ∃ i, x ∉ f i
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n : ℕ<GOAL>0 < 1 / (↑n + 1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n : ℕ<GOAL>0 < (↑n + 1)⁻¹
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>P : RatFunc K → Prop<VAR>x : FractionRing K[X]<VAR>f : ∀ (p q : K[X]), q ≠ 0 → P (RatFunc.mk p q)<VAR>x✝ : K[X] × ↥K[X]⁰<VAR>p : K[X]<VAR>q : ↥K[X]⁰<GOAL>P { toFractionRing := Localization.mk (p, q).1 (p, q).2 }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hab : b₁ ≤ b₂<VAR>hcd : a ≤ d<GOAL>b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulMono α β<VAR>b₁ : α<VAR>a d : β<VAR>hcd : a ≤ d<VAR>b₂ : α<VAR>hab : b₁ ≤ b₁ + b₂<GOAL>b₁ • d + (b₁ + b₂) • a ≤ b₁ • a + (b₁ + b₂) • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulMono α β<VAR>b₁ : α<VAR>a : β<VAR>b₂ : α<VAR>hab : b₁ ≤ b₁ + b₂<VAR>d : β<VAR>hcd : a ≤ a + d<GOAL>b₁ • (a + d) + (b₁ + b₂) • a ≤ b₁ • a + (b₁ + b₂) • (a + d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulMono α β<VAR>b₁ : α<VAR>a : β<VAR>b₂ : α<VAR>hab : b₁ ≤ b₁ + b₂<VAR>d : β<VAR>hcd : a ≤ a + d<GOAL>b₁ • a + (b₁ + b₂) • a + b₁ • d ≤ b₁ • a + (b₁ + b₂) • a + (b₁ • d + b₂ • d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulMono α β<VAR>b₁ : α<VAR>a : β<VAR>b₂ : α<VAR>hab : 0 ≤ b₂<VAR>d : β<VAR>hcd : 0 ≤ d<GOAL>b₁ • a + (b₁ + b₂) • a + b₁ • d ≤ b₁ • a + (b₁ + b₂) • a + (b₁ • d + b₂ • d)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m✝ : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>N : ℕ<VAR>hN : N ∉ Finset.range m<GOAL>((p N) fun x => y) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m✝ : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f p x n r<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>N : ℕ<VAR>hN : m ≤ N<GOAL>((p N) fun x => y) = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>u : V →L[R] R<VAR>ux : u x = 1<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>u : V →L[R] R<VAR>ux : u x = 1<VAR>uy : u y ≠ 0<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>u : V →L[R] R<VAR>ux : u x = 1<VAR>uy : u y = 0<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>u : V →L[R] R<VAR>ux : u x = 1<VAR>uy : u y = 0<VAR>v : V →L[R] R<VAR>vy : v y = 1<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>u : V →L[R] R<VAR>ux : u x = 1<VAR>uy : u y = 0<VAR>v : V →L[R] R<VAR>vy : v y = 1<VAR>vx : v x ≠ 0<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>u : V →L[R] R<VAR>ux : u x = 1<VAR>uy : u y = 0<VAR>v : V →L[R] R<VAR>vy : v y = 1<VAR>vx : v x = 0<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>a b m n p : ℕ<GOAL>((a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1).Coprime ((a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n)
<VAR>a b m n p✝ p : ℕ<VAR>hp : p ∈ (a.lcm b).factorization.support<VAR>q : ℕ<VAR>hq : q ∈ (a.lcm b).factorization.support<GOAL>((fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1) p ((a.lcm b).factorization p)).Coprime ((fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n) q ((a.lcm b).factorization q))
<VAR>a b m n p✝ p : ℕ<VAR>hp : p ∈ (a.lcm b).factorization.support<VAR>q : ℕ<VAR>hq : q ∈ (a.lcm b).factorization.support<VAR>h : b.factorization p ≤ a.factorization p<VAR>h' : b.factorization q ≤ a.factorization q<GOAL>(p ^ (a.lcm b).factorization p).Coprime 1
<VAR>a b m n p✝ p : ℕ<VAR>hp : p ∈ (a.lcm b).factorization.support<VAR>q : ℕ<VAR>hq : q ∈ (a.lcm b).factorization.support<VAR>h : b.factorization p ≤ a.factorization p<VAR>h' : ¬b.factorization q ≤ a.factorization q<GOAL>(p ^ (a.lcm b).factorization p).Coprime (q ^ (a.lcm b).factorization q)
<VAR>a b m n p✝ p : ℕ<VAR>hp : p ∈ (a.lcm b).factorization.support<VAR>q : ℕ<VAR>hq : q ∈ (a.lcm b).factorization.support<VAR>h : ¬b.factorization p ≤ a.factorization p<VAR>h✝ : b.factorization q ≤ a.factorization q<GOAL>Coprime 1 1
<VAR>a b m n p✝ p : ℕ<VAR>hp : p ∈ (a.lcm b).factorization.support<VAR>q : ℕ<VAR>hq : q ∈ (a.lcm b).factorization.support<VAR>h : ¬b.factorization p ≤ a.factorization p<VAR>h✝ : ¬b.factorization q ≤ a.factorization q<GOAL>Coprime 1 (q ^ (a.lcm b).factorization q)
<VAR>a b m n p✝ p : ℕ<VAR>hp : p ∈ (a.lcm b).factorization.support<VAR>q : ℕ<VAR>hq : q ∈ (a.lcm b).factorization.support<VAR>h : b.factorization p ≤ a.factorization p<VAR>h' : ¬b.factorization q ≤ a.factorization q<GOAL>p ≠ q
<VAR>a b m n p✝ p : ℕ<VAR>hp : p ∈ (a.lcm b).factorization.support<VAR>q : ℕ<VAR>hq : q ∈ (a.lcm b).factorization.support<VAR>h : b.factorization p ≤ a.factorization p<VAR>h' : p = q<GOAL>b.factorization q ≤ a.factorization q
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<VAR>hE : CompleteSpace E<GOAL>HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<VAR>hE : CompleteSpace E<GOAL>HasSum (fun x => ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<VAR>hE : CompleteSpace E<GOAL>∑' (i : ι), ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<VAR>hE : CompleteSpace E<VAR>this : ∀ (i : ι), ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊<GOAL>∑' (i : ι), ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<VAR>hE : CompleteSpace E<VAR>this : ∀ (i : ι), ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊<GOAL>↑(∑' (x : ι), ‖∫ (a : α), ‖F x a‖ ∂μ‖₊) ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>F : ι → α → E<VAR>hF_int : ∀ (i : ι), Integrable (F i) μ<VAR>hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ<VAR>hE : CompleteSpace E<VAR>this : ∀ (i : ι), ∫⁻ (a : α), ↑‖F i a‖₊ ∂μ = ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊<GOAL>Summable fun x => ‖∫ (a : α), ‖F x a‖ ∂μ‖₊
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>‖f.normComp‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>h : f ≤ᶠ[ae μ] g<VAR>A : CompleteSpace ℝ<GOAL>(if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0 else 0) ≤ if h : True then if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0 else 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>inst✝ : MeasurableSpace α<VAR>f : α → F<VAR>h0 : p ≠ 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm f p 0 = 0
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : Field L<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : FiniteDimensional K L<VAR>F : Type u_3<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Algebra K F<VAR>inst✝⁶ : Algebra.IsSeparable K F<VAR>inst✝⁵ : FiniteDimensional K F<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : Algebra F L<VAR>inst✝² : Algebra.IsSeparable F L<VAR>inst✝¹ : FiniteDimensional F L<VAR>inst✝ : IsScalarTower K F L<VAR>x : 𝓞 L<GOAL>(norm K) ((norm F) x) = (norm K) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<GOAL>U R 2 = 4 * X ^ 2 - 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>this : U R (0 + 2) = 2 * X * U R (0 + 1) - U R 0<GOAL>U R 2 = 4 * X ^ 2 - 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>this : U R 2 = 2 * X * (2 * X) - 1<GOAL>U R 2 = 4 * X ^ 2 - 1
<VAR>R : Type u_1<VAR>inst✝¹ : MulZeroClass R<VAR>b : R<VAR>inst✝ : Nontrivial R<VAR>la : IsLeftRegular 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : MulZeroClass R<VAR>b : R<VAR>inst✝ : Nontrivial R<VAR>la : IsLeftRegular 0<VAR>x y : R<VAR>xy : x ≠ y<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : MulZeroClass R<VAR>b : R<VAR>inst✝ : Nontrivial R<VAR>la : IsLeftRegular 0<VAR>x y : R<VAR>xy : x ≠ y<GOAL>0 * x = 0 * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫⁻ (x : α) in s, f x ∂μ
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (expSeries 𝕜 R n) fun x_1 => x.fst) e<GOAL>HasSum (fun n => (expSeries 𝕜 (tsze R M) n) fun x_1 => x) (inl e + inr (e • x.snd))
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>e : R<VAR>h : HasSum (fun n => (expSeries 𝕜 R n) fun x_1 => x.fst) e<VAR>this : HasSum (fun n => ((expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst) e<GOAL>HasSum (fun n => (expSeries 𝕜 (tsze R M) n) fun x_1 => x) (inl e + inr (e • x.snd))
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>K : Compacts G<GOAL>(fun s => ↑(μ.toFun s)) K ≤ μ.outerMeasure ↑K
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>K : Compacts G<GOAL>(fun s => ↑(μ.toFun s)) K ≤ ⨅ t, ⨅ (ht : IsOpen t), ⨅ (_ : ↑K ⊆ t), μ.innerContent { carrier := t, is_open' := ht }
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>K : Compacts G<GOAL>∀ ⦃f : ℕ → Set G⦄, (∀ (i : ℕ), IsOpen (f i)) → IsOpen (⋃ i, f i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>K : Compacts G<GOAL>∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)), μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>K : Compacts G<GOAL>∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂), s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }
<VAR>s : Set ℕ<VAR>h : s.Nonempty<GOAL>sInf s ∈ s
<VAR>s : Set ℕ<VAR>h : s.Nonempty<GOAL>Nat.find h ∈ s
<VAR>a b : ℝ≥0<VAR>ha : 0 < a<VAR>hb : b < 1<GOAL>∃ n, b ^ n < a