ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<VAR>hFf : 𝓕 f = fun x => 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)<VAR>h1 : 0 < (↑π * a).re<VAR>h2 : 0 < (↑π / a).re<VAR>f_bd : f =O[cocompact ℝ] fun x => |x| ^ (-2)<VAR>Ff_bd : 𝓕 f =O[cocompact ℝ] fun x => |x| ^ (-2)<GOAL>1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2) = ∑' (n : ℤ), 𝓕 f ↑n * (fourier n) ↑0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf✝ : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0✝ : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>hf : autoParam (ContinuousOn f (star '' σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ (fun x => f (star x)) a = cfcₙ f (star a)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Zero N<VAR>f g : α →₀ N<GOAL>f.neLocus g = g.neLocus f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>n : ℤ<GOAL>Tendsto ceil (𝓝[>] ↑n) (pure (n + 1))
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : z ∈ 𝒟ᵒ<GOAL>3 < 4 * z.im ^ 2
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : z ∈ 𝒟ᵒ<VAR>this : 1 < z.re * z.re + z.im * z.im<GOAL>3 < 4 * z.im ^ 2
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : z ∈ 𝒟ᵒ<VAR>this✝ : 1 < z.re * z.re + z.im * z.im<VAR>this : |z.re| < 1 / 2<GOAL>3 < 4 * z.im ^ 2
<VAR>θ : Angle<GOAL>(θ + ↑(π / 2)).cos = -θ.sin
<VAR>x✝ : ℝ<GOAL>(↑x✝ + ↑(π / 2)).cos = -(↑x✝).sin
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i : F →+* K<VAR>x : F<VAR>h : F[X]<VAR>h_sep : h.Separable<VAR>h_root : eval x h = 0<VAR>h_splits : Splits i h<VAR>h_roots : ∀ y ∈ (map i h).roots, y = i x<GOAL>h = C h.leadingCoeff * (X - C x)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i : F →+* K<VAR>x : F<VAR>h : F[X]<VAR>h_sep : h.Separable<VAR>h_root : eval x h = 0<VAR>h_splits : Splits i h<VAR>h_roots : ∀ y ∈ (map i h).roots, y = i x<VAR>h_ne_zero : h ≠ 0<GOAL>h = C h.leadingCoeff * (X - C x)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i : F →+* K<VAR>x : F<VAR>h : F[X]<VAR>h_sep : h.Separable<VAR>h_root : eval x h = 0<VAR>h_splits : Splits i h<VAR>h_roots : ∀ y ∈ (map i h).roots, y = i x<VAR>h_ne_zero : h ≠ 0<GOAL>(map i h).roots = {i x}
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>hY : QuasiSeparatedSpace ↑↑Y.toPresheafedSpace<VAR>inst✝ : QuasiSeparated f<GOAL>QuasiSeparatedSpace ↑↑X.toPresheafedSpace
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>hY : QuasiSeparated (terminal.from Y)<VAR>inst✝ : QuasiSeparated f<GOAL>QuasiSeparated (terminal.from X)
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>hY : QuasiSeparated (terminal.from Y)<VAR>inst✝ : QuasiSeparated f<GOAL>QuasiSeparated (f ≫ terminal.from Y)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hfB : IsInvariantBlock G B<VAR>g : G<GOAL>g • B = B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hfB : IsInvariantBlock G B<VAR>g : G<GOAL>B ≤ g • B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hfB : IsInvariantBlock G B<VAR>g : G<VAR>x : X<VAR>hx : x ∈ B<GOAL>x ∈ g • B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hfB : IsInvariantBlock G B<VAR>g : G<VAR>x : X<VAR>hx : x ∈ B<GOAL>g⁻¹ • x ∈ B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hfB : IsInvariantBlock G B<VAR>g : G<VAR>x : X<VAR>hx : x ∈ B<GOAL>g⁻¹ • x ∈ g⁻¹ • B
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>inst✝ : HasWidePullback B objs arrows<VAR>j : J<GOAL>π arrows j ≫ arrows j = base arrows
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.7851) (N : Type ?u.7850) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.7851) (N : Type ?u.7850) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : a ≤ y<VAR>hyb : y < b<VAR>z : α<VAR>hzc : c < z<VAR>hzd : z ≤ d<GOAL>(fun x x_1 => x * x_1) y z ∈ Ioo (a * c) (b * d)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : Group G<GOAL>∀ (L : List G), L.reverse.prod = (map (fun x => x⁻¹) L).prod⁻¹
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.IsPath ↔ p.IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w u v : V<VAR>p : G.Walk u v<VAR>h : p.reverse.IsPath<GOAL>p = p.reverse.reverse
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H K : Subgroup G<VAR>f : G →* N<VAR>hf : Injective ⇑f<GOAL>map f (H ⊓ K) = map f H ⊓ map f K
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H K : Subgroup G<VAR>f : G →* N<VAR>hf : Injective ⇑f<GOAL>↑(map f (H ⊓ K)) = ↑(map f H ⊓ map f K)
<VAR>r : ℝ<GOAL>r⁻¹.sign = r.sign
<VAR>r : ℝ<VAR>hn : r < 0<GOAL>r⁻¹.sign = r.sign
<VAR>r : ℝ<VAR>hp : 0 < r<GOAL>r⁻¹.sign = r.sign
<VAR>q r : ℚ<GOAL>q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
<VAR>q r : ℚ<VAR>hqd : ↑q.den ≠ 0<GOAL>q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
<VAR>q r : ℚ<VAR>hqd : ↑q.den ≠ 0<VAR>hrd : ↑r.den ≠ 0<GOAL>q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
<VAR>q r : ℚ<VAR>hqd : ↑q.den ≠ 0<VAR>hrd : ↑r.den ≠ 0<GOAL>(q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den) = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
<VAR>α : Type u_1<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder α<VAR>p : α<VAR>hp : Prime p<GOAL>Prime |p|
<VAR>α : Type u_1<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder α<VAR>p : α<VAR>hp : Prime p<VAR>h : |p| = p<GOAL>Prime p
<VAR>α : Type u_1<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder α<VAR>p : α<VAR>hp : Prime p<VAR>h : |p| = -p<GOAL>Prime (-p)
<VAR>Fq F : Type<VAR>inst✝² : Field Fq<VAR>inst✝¹ : Field F<VAR>inst✝ : DecidableEq (RatFunc Fq)<GOAL>inftyValuationDef Fq RatFunc.X = ↑(Multiplicative.ofAdd 1)
<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>hQz : Q z ≠ 0<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<GOAL>W'.dblY P = W'.dblU P ^ 3
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<GOAL>degree 0 = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>J : Type v<VAR>inst✝⁴ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i : ι<GOAL>{ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map (𝟙 i) = 𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.obj i)
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>J : Type v<VAR>inst✝⁴ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i : ι<GOAL>∀ (x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.obj i)), ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map (𝟙 i)) x = (𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.obj i)) x
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>J : Type v<VAR>inst✝⁴ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i : ι<VAR>x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.obj i)<GOAL>({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map (𝟙 i)) x = (𝟙 ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.obj i)) x
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>J : Type v<VAR>inst✝⁴ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>X✝ Y✝ Z✝ : ι<VAR>hij : X✝ ⟶ Y✝<VAR>hjk : Y✝ ⟶ Z✝<GOAL>{ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map (hij ≫ hjk) = { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map hij ≫ { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map hjk
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>J : Type v<VAR>inst✝⁴ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>X✝ Y✝ Z✝ : ι<VAR>hij : X✝ ⟶ Y✝<VAR>hjk : Y✝ ⟶ Z✝<GOAL>∀ (x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.obj X✝)), ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map (hij ≫ hjk)) x = ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map hij ≫ { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map hjk) x
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>J : Type v<VAR>inst✝⁴ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>X✝ Y✝ Z✝ : ι<VAR>hij : X✝ ⟶ Y✝<VAR>hjk : Y✝ ⟶ Z✝<VAR>x : ↑({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.obj X✝)<GOAL>({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map hij ≫ { obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map hjk) x = ({ obj := fun i => of R (G i), map := fun {X Y} hij => f X Y ⋯ }.map (hij ≫ hjk)) x
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd f g
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<GOAL>⊤ * a = if a = 0 then 0 else ⊤
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>x y : E<VAR>hy : y ∈ p.closedBall 0 r<VAR>hx : (fun x => a • x) y = x<GOAL>x ∈ p.closedBall 0 r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>x y : E<VAR>hy : y ∈ p.closedBall 0 r<VAR>hx : (fun x => a • x) y = x<GOAL>‖a‖ * p y ≤ r
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)<GOAL>M p
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)<VAR>a : R<GOAL>M (C a)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>M : R[T;T⁻¹] → Prop<VAR>p : R[T;T⁻¹]<VAR>h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)<VAR>h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)<VAR>a : R<GOAL>C a = C a * T 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : IsAtomic α<VAR>inst✝ : OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>a : α<GOAL>IsAtom (l a) ↔ IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : IsAtomic α<VAR>inst✝ : OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>a : α<VAR>hla : IsAtom (l a)<GOAL>IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : IsAtomic α<VAR>inst✝ : OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>a : α<VAR>hla : IsAtom (l a)<VAR>a' : α<VAR>ha' : IsAtom a'<VAR>hab' : a' ≤ u (l a)<GOAL>IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : IsAtomic α<VAR>inst✝ : OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>a : α<VAR>hla : IsAtom (l a)<VAR>a' : α<VAR>ha' : IsAtom a'<VAR>hab' : a' ≤ u (l a)<VAR>this : l a' = l a<GOAL>IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PartialOrder β<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : IsAtomic α<VAR>inst✝ : OrderBot β<VAR>l : α → β<VAR>u : β → α<VAR>gi : GaloisInsertion l u<VAR>hbot : u ⊥ = ⊥<VAR>h_atom : ∀ (a : α), IsAtom a → u (l a) = a<VAR>a : α<VAR>hla : IsAtom (l a)<VAR>a' : α<VAR>ha' : IsAtom a'<VAR>hab' : a' ≤ u (l a)<VAR>this : l a' = l a<VAR>haa' : a = a'<GOAL>IsAtom a
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<GOAL>card {a} = 1
<VAR>x✝ y x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<GOAL>|log x * x| < 1
<VAR>x✝ y x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>this : 0 < 1 / x<GOAL>|log x * x| < 1
<VAR>x✝ y x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>this : log (1 / x) ≤ 1 / x - 1<GOAL>|log x * x| < 1
<VAR>x✝ y x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>this : log (1 / x) < 1 / x<GOAL>|log x * x| < 1
<VAR>x✝ y x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>this : -log x * x < 1<GOAL>|log x * x| < 1
<VAR>x✝ y x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>this : -log x * x < 1<VAR>aux : 0 ≤ -log x * x<GOAL>|log x * x| < 1
<VAR>x✝ y x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x ≤ 1<VAR>this : |log x * x| < 1<VAR>aux : 0 ≤ -log x * x<GOAL>|log x * x| < 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>filter (fun x => x == a) l = replicate (count a l) a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>True ∧ ∀ (b : α), b ∈ l ∧ b = a → b = a
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>d * (n / d) < n ↔ ¬d ∣ n
<VAR>a b : ℕ+<GOAL>Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>hs : {i₂, i₃}ᶜ = {i₁}<VAR>he : univ.erase i₁ = {i₂, i₃}<GOAL>altitude t i₁ = mongePlane t i₂ i₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>hs : {i₂, i₃}ᶜ = {i₁}<VAR>he : univ.erase i₁ = {i₂, i₃}<GOAL>mk' (t.points i₁) (Submodule.span ℝ ((fun x => t.points i₂ -ᵥ x) '' (t.points '' ({i₂, i₃} \ {i₂}))))ᗮ ⊓ affineSpan ℝ (Set.range t.points) = mk' (t.points i₁) (Submodule.span ℝ {t.points i₂ -ᵥ t.points i₃})ᗮ ⊓ affineSpan ℝ (Set.range t.points)
<VAR>α : Type u_1<VAR>inst✝¹ : StrictOrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>x : ↑(Ioo 0 1)<GOAL>1 - ↑x < 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : PositiveCompacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>0 < sInf (Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V})
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : PositiveCompacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>¬∃ x ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : PositiveCompacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>∃ n, n ∈ Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<GOAL>Memℓp (f + g) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f 0<VAR>hg : Memℓp g 0<GOAL>Memℓp (f + g) 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f ⊤<VAR>hg : Memℓp g ⊤<GOAL>Memℓp (f + g) ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<VAR>hp : 0 < p.toReal<GOAL>Memℓp (f + g) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<VAR>hp : 0 < p.toReal<GOAL>Summable fun i => ‖(f + g) i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<VAR>hp : 0 < p.toReal<VAR>C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)<GOAL>Summable fun i => ‖(f + g) i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<VAR>hp : 0 < p.toReal<VAR>C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)<GOAL>∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<VAR>hp : 0 < p.toReal<VAR>C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)<VAR>i : α<GOAL>‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>g : β → γ<GOAL>mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>g : β → γ<GOAL>∀ (a : β), single (g a) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>g : β → γ<GOAL>∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = single (g a) b₁ + single (g a) b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>g : β → γ<GOAL>(v.sum fun a b => (single (f a) b).sum fun a => single (g a)) = mapDomain (g ∘ f) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>g : β → γ<VAR>x✝¹ : α<VAR>x✝ : x✝¹ ∈ v.support<GOAL>single (g (f x✝¹)) 0 = 0
<VAR>num : Int<VAR>den : Nat<VAR>den_nz : den ≠ 0<GOAL>normalize num den den_nz = { num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X✝ : Scheme<VAR>U✝ : X✝.Opens<VAR>s : Type u_1<VAR>X : Scheme<VAR>U : s → X.Opens<VAR>hU : ⨆ i, U i = ⊤<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ Set.range ⇑((fun i => (U i).ι) ((fun x => ⋯.choose) x)).val.base
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X✝ : Scheme<VAR>U✝ : X✝.Opens<VAR>s : Type u_1<VAR>X : Scheme<VAR>U : s → X.Opens<VAR>hU : ⨆ i, U i = ⊤<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ ↑(U ((fun x => ⋯.choose) x))
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X✝ : Scheme<VAR>U✝ : X✝.Opens<VAR>s : Type u_1<VAR>X : Scheme<VAR>U : s → X.Opens<VAR>hU : ⨆ i, U i = ⊤<VAR>x : ↑↑X.toPresheafedSpace<VAR>this : x ∈ ⨆ i, U i<GOAL>x ∈ ↑(U ((fun x => ⋯.choose) x))