ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝¹ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.degree ≤ 1<VAR>n✝ n : ℕ<GOAL>p.coeff Nat.zero.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff Nat.zero.succ
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝¹ m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.degree ≤ 1<VAR>n✝ n m : ℕ<GOAL>p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝¹ m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.degree ≤ 1<VAR>n✝ n m : ℕ<VAR>this : p.degree < ↑m.succ.succ<GOAL>p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : 0 ≤ R<VAR>θ : ℝ<GOAL>circleMap c R θ ∈ sphere c R
<VAR>x✝ y x : ℝ<GOAL>rexp (arsinh x) = x + √(1 + x ^ 2)
<VAR>x✝ y x : ℝ<GOAL>0 < x + √(1 + x ^ 2)
<VAR>x✝ y x : ℝ<GOAL>-x < √(1 + x ^ 2)
<VAR>x✝ y x : ℝ<GOAL>(-x) ^ 2 < 1 + x ^ 2
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>ha : 0 ^ n ≠ 0<GOAL>False
<VAR>s : ℂ<VAR>X : ℝ<VAR>hs : 0 < s.re<VAR>hX : 0 ≤ X<GOAL>IntervalIntegrable (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) volume 0 X
<VAR>s : ℂ<VAR>X : ℝ<VAR>hs : 0 < s.re<VAR>hX : 0 ≤ X<GOAL>IntegrableOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioc 0 X) volume
<VAR>x y : ℂ<GOAL>cosh (-x) = cosh x
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : NonUnitalRing A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : IsScalarTower ℂ A A<VAR>inst✝ : SMulCommClass ℂ A A<VAR>a : A<GOAL>QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ σₙ ℂ a, x = ↑x.re
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>z : N<GOAL>f.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 * z
<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>hf : HasFPowerSeriesOnBall f p x r<GOAL>TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (EMetric.ball x r)
<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>hf : HasFPowerSeriesOnBall f p x r<VAR>A : ContinuousOn (fun y => y - x) (EMetric.ball x r)<GOAL>TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (EMetric.ball x r)
<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>hf : HasFPowerSeriesOnBall f p x r<VAR>A : ContinuousOn (fun y => y - x) (EMetric.ball x r)<GOAL>f = (fun y => f (x + y)) ∘ fun y => y - x
<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>hf : HasFPowerSeriesOnBall f p x r<VAR>A : ContinuousOn (fun y => y - x) (EMetric.ball x r)<GOAL>MapsTo (fun y => y - x) (EMetric.ball x r) (EMetric.ball 0 r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<VAR>h : ω ≤ o<GOAL>(aleph' (succ o)).IsRegular
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<VAR>h : ω ≤ o<GOAL>(succ (aleph' o)).IsRegular
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : NormedField 𝕜₂<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>s : Finset ι<VAR>f : E →ₛₗ[σ₁₂] F<VAR>x : E<GOAL>((s.sup q).comp f) x = (s.sup (q.comp f)) x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : NormedField 𝕜₂<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>q : SeminormFamily 𝕜₂ F ι<VAR>s : Finset ι<VAR>f : E →ₛₗ[σ₁₂] F<VAR>x : E<GOAL>↑(s.sup fun i => ⟨(q i) (f x), ⋯⟩) = ↑(s.sup fun i => ⟨(q.comp f i) x, ⋯⟩)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : SeminormedAddCommGroup α<VAR>v : m → α<GOAL>‖col ι v‖₊ = ‖v‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : SeminormedAddCommGroup α<VAR>v : m → α<GOAL>(Finset.univ.sup fun i => ∑ j : ι, ‖col ι v i j‖₊) = Finset.univ.sup fun b => ‖v b‖₊
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>↑(upperClosure s) * t = ↑(upperClosure (s * t))
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>t * ↑(upperClosure s) = ↑(upperClosure (t * s))
<VAR>c d a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<GOAL>(↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ z
<VAR>c d a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<GOAL>(↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ (↑c / ↑d).sqrtTwoAddSeries n
<VAR>c d a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<GOAL>(√(2 + ↑a / ↑b)).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries n
<VAR>c d a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<GOAL>√(2 + ↑a / ↑b) ≤ ↑c / ↑d
<VAR>c d a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<VAR>hb' : 0 < ↑b<GOAL>√(2 + ↑a / ↑b) ≤ ↑c / ↑d
<VAR>c d a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<VAR>hb' : 0 < ↑b<VAR>hd' : 0 < ↑d<GOAL>√(2 + ↑a / ↑b) ≤ ↑c / ↑d
<VAR>c d a b n : ℕ<VAR>z : ℝ<VAR>hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b<VAR>hb' : 0 < ↑b<VAR>hd' : 0 < ↑d<GOAL>(2 * ↑b + ↑a) * ↑d ^ 2 ≤ ↑c ^ 2 * ↑b
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x y : E<GOAL>(p.changeOrigin x).sum y = p.sum (x + y)
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x y : E<VAR>f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y<GOAL>(p.changeOrigin x).sum y = p.sum (x + y)
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x y : E<VAR>f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y<VAR>finsupp : (Function.support f).Finite<VAR>hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)<VAR>hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)<GOAL>(p.changeOrigin x).sum y = p.sum (x + y)
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x y : E<VAR>f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y<VAR>finsupp : (Function.support f).Finite<VAR>hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)<VAR>hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)<VAR>hf : HasSum f ((p.changeOrigin x).sum y)<GOAL>(p.changeOrigin x).sum y = p.sum (x + y)
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>x y : E<VAR>f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y<VAR>finsupp : (Function.support f).Finite<VAR>hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)<VAR>hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)<VAR>hf : HasSum f ((p.changeOrigin x).sum y)<GOAL>HasSum (f ∘ ⇑changeOriginIndexEquiv.symm) (p.sum (x + y))
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n✝ : ℕ<VAR>hn : ∀ (m : ℕ), n✝ ≤ m → p m = 0<VAR>x y : E<VAR>f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y<VAR>finsupp : (Function.support f).Finite<VAR>hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)<VAR>hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)<VAR>hf : HasSum f ((p.changeOrigin x).sum y)<VAR>n : ℕ<GOAL>HasSum (fun c => (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) ((p n) fun x_1 => x + y)
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n✝ : ℕ<VAR>hn : ∀ (m : ℕ), n✝ ≤ m → p m = 0<VAR>x y : E<VAR>f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y<VAR>finsupp : (Function.support f).Finite<VAR>hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)<VAR>hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)<VAR>hf : HasSum f ((p.changeOrigin x).sum y)<VAR>n : ℕ<GOAL>HasSum (fun c => (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) (∑ s : Finset (Fin n), (p n) (s.piecewise (fun x_1 => x) fun x => y))
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n✝ : ℕ<VAR>hn : ∀ (m : ℕ), n✝ ≤ m → p m = 0<VAR>x y : E<VAR>f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y<VAR>finsupp : (Function.support f).Finite<VAR>hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)<VAR>hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)<VAR>hf : HasSum f ((p.changeOrigin x).sum y)<VAR>n : ℕ<GOAL>HasSum (fun c => (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) (∑ x_1 : Finset (Fin n), ((p.changeOriginSeriesTerm (changeOriginIndexEquiv.symm ⟨n, x_1⟩).fst (changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.fst ↑(changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.snd ⋯) fun x_2 => x) fun x => y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<GOAL>f.IsCycleOn {a} ↔ f a = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>IsOpen (f.extend I).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>IsOpen f.source
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f = (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫ (J.isoRightDerivedObj F n).inv
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁹ : DecidableEq ι<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Algebra A B<VAR>inst✝¹⁵ : CommRing C<VAR>inst✝¹⁴ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : Module.Finite K L<VAR>inst✝⁴ : IsAlgClosed E<VAR>b✝ : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝³ : CommRing R<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>b : ι → L<VAR>h : ∀ (i : ι), IsIntegral R (b i)<GOAL>IsIntegral R (discr K b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : Option β → α<VAR>c : α<GOAL>⨆ o, f o ≤ c ↔ f none ⊔ ⨆ b, f (some b) ≤ c
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>inst✝² : CommSemiring S₂<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : Algebra R S₂<VAR>f : S₁ →ₐ[R] S₂<VAR>r : R<VAR>h₁ : (algebraMap R (MvPolynomial σ S₁)) r = C ((algebraMap R S₁) r)<VAR>h₂ : (algebraMap R (MvPolynomial σ S₂)) r = C ((algebraMap R S₂) r)<GOAL>(↑↑__src✝).toFun ((algebraMap R (MvPolynomial σ S₁)) r) = (algebraMap R (MvPolynomial σ S₂)) r
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>inst✝² : CommSemiring S₂<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : Algebra R S₂<VAR>f : S₁ →ₐ[R] S₂<VAR>r : R<VAR>h₁ : (algebraMap R (MvPolynomial σ S₁)) r = C ((algebraMap R S₁) r)<VAR>h₂ : (algebraMap R (MvPolynomial σ S₂)) r = C ((algebraMap R S₂) r)<GOAL>↑↑(map ↑f) ((algebraMap R (MvPolynomial σ S₁)) r) = (algebraMap R (MvPolynomial σ S₂)) r
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>inst✝² : CommSemiring S₂<VAR>inst✝¹ : Algebra R S₁<VAR>inst✝ : Algebra R S₂<VAR>f : S₁ →ₐ[R] S₂<VAR>r : R<VAR>h₁ : (algebraMap R (MvPolynomial σ S₁)) r = C ((algebraMap R S₁) r)<VAR>h₂ : (algebraMap R (MvPolynomial σ S₂)) r = C ((algebraMap R S₂) r)<GOAL>(map ↑f) ((algebraMap R (MvPolynomial σ S₁)) r) = (algebraMap R (MvPolynomial σ S₂)) r
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a✝ b✝ c d : α<VAR>h : IsUnit c<VAR>a b : α<GOAL>c * a / (c * b) = a / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>c : α<GOAL>c ∈ Iic (⨅ i, f i) ↔ c ∈ ⨅ i, Iic (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝¹ : Matroid α<VAR>N : Matroid β<VAR>E X✝ I : Set α<VAR>M✝ M : Matroid α<VAR>X : Set α<GOAL>(M.restrictSubtype X).map Subtype.val ⋯ = M ↾ X
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : x ≤ 1<VAR>hz : 0 ≤ z<GOAL>x ^ z ≤ 1
<VAR>z : ℝ<VAR>hz : 0 ≤ z<VAR>x : ℝ≥0<VAR>hx : ↑x ≤ 1<GOAL>↑x ^ z ≤ 1
<VAR>z : ℝ<VAR>hz : 0 ≤ z<VAR>x : ℝ≥0<VAR>hx : x ≤ 1<GOAL>↑x ^ z ≤ 1
<VAR>x y : PGame<VAR>k : (x * y).LeftMoves<VAR>P : (x * y).LeftMoves → Prop<VAR>hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))<VAR>hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))<GOAL>P k
<VAR>x y : PGame<VAR>k : (x * y).LeftMoves<VAR>P : (x * y).LeftMoves → Prop<VAR>hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))<VAR>hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))<GOAL>P (toLeftMovesMul (toLeftMovesMul.symm k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>x ∈ box n d ↔ ∀ (i : Fin n), x i < d
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Ioc a b = ∅ ↔ ¬a < b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid A<VAR>inst✝¹⁰ : Module R A<VAR>inst✝⁹ : AddCommMonoid B<VAR>inst✝⁸ : Module R B<VAR>inst✝⁷ : AddCommMonoid C<VAR>inst✝⁶ : Module R C<VAR>inst✝⁵ : AddCommMonoid D<VAR>inst✝⁴ : Module R D<VAR>inst✝³ : CoalgebraStruct R A<VAR>inst✝² : CoalgebraStruct R B<VAR>inst✝¹ : CoalgebraStruct R C<VAR>inst✝ : CoalgebraStruct R D<GOAL>map __src✝ __src✝ ∘ₗ comul = comul ∘ₗ __src✝
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝ : MeasurableSpace ι<VAR>h : ProgMeasurable f u<VAR>i : ι<GOAL>StronglyMeasurable (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝ : MeasurableSpace ι<VAR>h : ProgMeasurable f u<VAR>i : ι<VAR>this : u i = (fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x)<GOAL>StronglyMeasurable (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝ : MeasurableSpace ι<VAR>h : ProgMeasurable f u<VAR>i : ι<VAR>this : u i = (fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x)<GOAL>StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun x => (⟨i, ⋯⟩, x))
<VAR>X Y : Type u<VAR>inst✝¹ : Mul X<VAR>inst✝ : Mul Y<VAR>e : X ≃* Y<VAR>x✝ : (forget MagmaCat).obj (MagmaCat.of X)<GOAL>(e.toMulHom ≫ e.symm.toMulHom) x✝ = (𝟙 (MagmaCat.of X)) x✝
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<GOAL>∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<GOAL>∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<VAR>l : List α<VAR>e : ⟦l⟧ = univ.val<GOAL>∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<VAR>l : List α<VAR>e : ⟦l⟧ = univ.val<VAR>this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val<GOAL>∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l