ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝ : SeminormedAddCommGroup β<VAR>v : n → α<GOAL>(∑ x : n, ‖col ι v x default‖ ^ 2) ^ (1 / 2) = (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖ ^ 2) ^ (1 / 2)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p q : R[X]<VAR>x : A<GOAL>(aeval x) p ∈ Algebra.adjoin R {x}
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(toLin' (lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<GOAL>f' ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<GOAL>∀ᶠ (c : ℝ) in 𝓝[>] x, slope f x c ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝 x, x_1 ∈ Ioi x → (f x_1 - f x) / (x_1 - x) ≤ (f y - f x) / (y - x)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<VAR>t : ℝ<VAR>ht : t < y<VAR>ht' : x < t<GOAL>(f t - f x) / (t - x) ≤ (f y - f x) / (y - x)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<VAR>t : ℝ<VAR>ht : t < y<VAR>ht' : x < t<GOAL>t ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>s t : Set β<VAR>κ : Kernel α β<VAR>hs : MeasurableSet s<VAR>a : α<VAR>ht : MeasurableSet t<GOAL>((κ.restrict hs) a) t = (κ a) (t ∩ s)
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>t : ℕ<VAR>ht : t ∈ Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1))<GOAL>t ∈ n.divisors
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>t : ℕ<VAR>ht : ∃ a < padicValNat p n + 1, p ^ a = t<GOAL>t ∈ n.divisors
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>k : ℕ<VAR>hk : k < padicValNat p n + 1<GOAL>p ^ k ∈ n.divisors
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>k : ℕ<VAR>hk : k < padicValNat p n + 1<GOAL>p ^ k ∣ n ∧ n ≠ 0
<VAR>α : Type u_1<VAR>M : Type u<VAR>N : Type v<VAR>P : Type w<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>f : M →* N<VAR>g : M → Nˣ<VAR>h : ∀ (x : M), ↑(g x) = f x<VAR>x : M<GOAL>↑((liftRight f g h) x)⁻¹ * f x = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>g : N →* P<VAR>f : M →* N<GOAL>map g (mrange f) = mrange (g.comp f)
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>ω ^ 2 ^ (p' + 1) = -1
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<VAR>k : ℤ<VAR>w : ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1<GOAL>ω ^ 2 ^ (p' + 1) = -1
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<VAR>k : ℤ<VAR>w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1<GOAL>ω ^ 2 ^ (p' + 1) = -1
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝¹ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b c a : α<GOAL>(mabs a)⁻¹ ≤ a⁻¹
<VAR>m n : ℕ<VAR>a : ℤ<VAR>b : ℕ<GOAL>↑(a % ↑b) = ↑a
<VAR>m n : ℕ<VAR>a : ℤ<VAR>b : ℕ<GOAL>a % ↑b ≡ a [ZMOD ↑b]
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Group α<VAR>a b : α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(Equiv.mulRight a ^ n) x✝ = (Equiv.mulRight (a ^ n)) x✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Star A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Star B<VAR>inst✝² : Semiring C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Star C<VAR>f : A →⋆ₐ[R] B<VAR>g : A →⋆ₐ[R] C<VAR>x : A<GOAL>(↑↑__src✝.toRingHom).toFun (star x) = star ((↑↑__src✝.toRingHom).toFun x)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y Z : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C<VAR>inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C<VAR>hφ : φ ≫ πY = πX<VAR>i : I<VAR>t : A i ⟶ X<VAR>b : B i ⟶ S<VAR>w : t ≫ πX = f i ≫ b<VAR>t' : A i ⟶ Y<VAR>fac : t ≫ φ = t'<GOAL>t' ≫ πY = f i ≫ b
<VAR>α : Type u_1<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<VAR>b : ℝ≥0<VAR>h : a ≤ ↑b<GOAL>a.toReal ≤ ↑b
<VAR>α : Type u_1<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q b a : ℝ≥0<VAR>h : ↑a ≤ ↑b<GOAL>(↑a).toReal ≤ ↑b
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<GOAL>finrank ℚ K ≤ rankOfDiscrBdd N
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>h_nz : N ≠ 0<GOAL>finrank ℚ K ≤ rankOfDiscrBdd N
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>h_nz : N ≠ 0<VAR>h₂ : 1 < 3 * π / 4<GOAL>finrank ℚ K ≤ rankOfDiscrBdd N
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>h_nz : N ≠ 0<VAR>h₂ : 1 < 3 * π / 4<VAR>h : 1 < finrank ℚ K<GOAL>finrank ℚ K ≤ rankOfDiscrBdd N
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>h_nz : N ≠ 0<VAR>h₂ : 1 < 3 * π / 4<VAR>h : finrank ℚ K ≤ 1<GOAL>finrank ℚ K ≤ rankOfDiscrBdd N
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>x y : α<VAR>hx : Irreducible x<GOAL>gcd x y = 1 ↔ ¬x ∣ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>h : succ (sup (typein fun x x_1 => x < x_1)) = lsub (typein fun x x_1 => x < x_1)<GOAL>sup (typein fun x x_1 => x < x_1) = o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>h : succ (sup (typein fun x x_1 => x < x_1)) = lsub (typein fun x x_1 => x < x_1)<GOAL>lsub (typein fun x x_1 => x < x_1) = succ o
<VAR>Ω✝ : Type u_1<VAR>inst✝⁸ : PseudoEMetricSpace Ω✝<VAR>inst✝⁷ : MeasurableSpace Ω✝<VAR>inst✝⁶ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁵ : L.NeBot<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure Ω<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>G : Set Ω<VAR>G_open : IsOpen G<GOAL>μ G ≤ liminf (fun i => (μs i) G) L
<VAR>Ω✝ : Type u_1<VAR>inst✝⁸ : PseudoEMetricSpace Ω✝<VAR>inst✝⁷ : MeasurableSpace Ω✝<VAR>inst✝⁶ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁵ : L.NeBot<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure Ω<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>G : Set Ω<VAR>G_open : IsOpen G<GOAL>limsup (fun i => (μs i) Gᶜ) L ≤ μ Gᶜ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp (a - m • p) b = toIocDiv hp a b + m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t<GOAL>s ∈ minimals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t<GOAL>P s → ((∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y) ↔ ∀ x ∈ s, ¬P (s \ {x}))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x✝¹ : α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t<VAR>x✝ : P s<VAR>h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y<VAR>x : α<VAR>hx : x ∈ s<VAR>hxs : P (s \ {x})<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t✝ : Set α<VAR>a b x✝¹ : α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t<VAR>x✝ : P s<VAR>h : ∀ x ∈ s, ¬P (s \ {x})<VAR>t : Set α<VAR>ht : P t<VAR>hst : t ⊆ s<VAR>x : α<VAR>hxs : x ∈ s<GOAL>x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NegZeroClass β<VAR>h : Antiperiodic f c<VAR>hi : f 0 = 0<GOAL>f (↑0 * c) = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e✝ : α<VAR>M : Matroid α<VAR>e : α<VAR>X : Set α<GOAL>M.closure (insert e (M.closure X)) = M.closure (insert e X)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>u v : n → R<GOAL>(M.updateColumn j (u + v)).det = (M.updateColumn j u).det + (M.updateColumn j v).det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>u v : n → R<GOAL>(Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateColumn j u).det + (M.updateColumn j v).det
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : CliffordAlgebra Q →ₐ[R] A<VAR>h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : CliffordAlgebra Q →ₐ[R] A<VAR>h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q<GOAL>(lift Q).symm f = (lift Q).symm g
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : CliffordAlgebra Q →ₐ[R] A<VAR>h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q<GOAL>⟨f.toLinearMap ∘ₗ ι Q, ⋯⟩ = ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T✝ : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : CommSemiring A'<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Algebra R A'<VAR>inst✝⁵ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>S : Type u_3<VAR>T : Type u_4<VAR>U : Type u_5<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : CommSemiring T<VAR>inst✝² : Semiring U<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra T U<VAR>φ : R →+* T<VAR>ψ : S →+* U<VAR>h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)<VAR>p : R[X]<VAR>a : S<GOAL>ψ ((aeval a) p) = (aeval (ψ a)) (map φ p)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T✝ : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : CommSemiring A'<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Algebra R A'<VAR>inst✝⁵ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>S : Type u_3<VAR>T : Type u_4<VAR>U : Type u_5<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : CommSemiring T<VAR>inst✝² : Semiring U<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra T U<VAR>φ : R →+* T<VAR>ψ : S →+* U<VAR>h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)<VAR>p : R[X]<VAR>a : S<GOAL>ψ ((aeval a) p) = eval (ψ a) (map (algebraMap T U) (map φ p))
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>a✝ : MeasurableSet s<GOAL>(Measure.toFiniteAux 0) s = 0 s
<VAR>z✝ : ℂ<VAR>n✝ : ℕ<VAR>z : ℂ<VAR>n : ℕ<GOAL>Complex.sin (↑π * z) = ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
<VAR>z : ℂ<VAR>n✝ n : ℕ<GOAL>Complex.sin (↑π * 0) = ((↑π * 0 * ∏ j ∈ Finset.range n, (1 - 0 ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * 0 * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
<VAR>z✝ : ℂ<VAR>n✝ : ℕ<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<GOAL>Complex.sin (↑π * z) = ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ s<VAR>y : F<VAR>hy : y ∈ B.polar s<GOAL>‖(B.flip y) x‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ s<VAR>y : F<VAR>hy : y ∈ B.polar s<GOAL>‖(B x) y‖ ≤ 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>I : Set ι<VAR>hI : I.Finite<VAR>h : ∀ i ∈ I, s i ∈ f i<GOAL>I.pi s ∈ pi f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>I : Set ι<VAR>hI : I.Finite<VAR>h : ∀ i ∈ I, s i ∈ f i<GOAL>⋂ x, eval ↑x ⁻¹' s ↑x ∈ pi f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>I : Set ι<VAR>hI : I.Finite<VAR>h : ∀ i ∈ I, s i ∈ f i<VAR>i : ↑I<GOAL>eval ↑i ⁻¹' s ↑i ∈ comap (eval ↑i) (f ↑i)
<GOAL>Tendsto (fun x => x ^ (1 / x)) atTop (𝓝 1)
<VAR>x✝ : ℝ<GOAL>x✝ = 1 * x✝ + 0
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>h.π ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).inv = h.cyclesIso.inv ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom
<VAR>n m : ℕ<GOAL>(nim ↑n + nim ↑m).grundyValue = ↑(n ^^^ m)
<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ (m_1 : ℕ), (nim ↑m + nim ↑m_1).grundyValue = ↑(m ^^^ m_1)<VAR>m : ℕ<GOAL>(nim ↑n + nim ↑m).grundyValue = ↑(n ^^^ m)
<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ (m_1 : ℕ), (nim ↑m + nim ↑m_1).grundyValue = ↑(m ^^^ m_1)<VAR>m : ℕ<VAR>hm : ∀ m_1 < m, (nim ↑n + nim ↑m_1).grundyValue = ↑(n ^^^ m_1)<GOAL>(nim ↑n + nim ↑m).grundyValue = ↑(n ^^^ m)
<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ (m_1 : ℕ), (nim ↑m + nim ↑m_1).grundyValue = ↑(m ^^^ m_1)<VAR>m : ℕ<VAR>hm : ∀ m_1 < m, (nim ↑n + nim ↑m_1).grundyValue = ↑(n ^^^ m_1)<GOAL>(mex fun i => ((nim ↑n + nim ↑m).moveLeft i).grundyValue) = ↑(n ^^^ m)
<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ (m_1 : ℕ), (nim ↑m + nim ↑m_1).grundyValue = ↑(m ^^^ m_1)<VAR>m : ℕ<VAR>hm : ∀ m_1 < m, (nim ↑n + nim ↑m_1).grundyValue = ↑(n ^^^ m_1)<VAR>i : (nim ↑n + nim ↑m).LeftMoves<GOAL>((nim ↑n + nim ↑m).moveLeft i).grundyValue ≠ ↑(n ^^^ m)
<VAR>n : ℕ<VAR>hn : ∀ m < n, ∀ (m_1 : ℕ), (nim ↑m + nim ↑m_1).grundyValue = ↑(m ^^^ m_1)<VAR>m : ℕ<VAR>hm : ∀ m_1 < m, (nim ↑n + nim ↑m_1).grundyValue = ↑(n ^^^ m_1)<VAR>ou : Ordinal.{u}<VAR>hu : ou < ↑(n ^^^ m)<GOAL>∃ i, ((nim ↑n + nim ↑m).moveLeft i).grundyValue = ou
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 1<GOAL>AffineIndependent k p ↔ finrank k ↥(vectorSpan k (Set.range p)) = n
<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>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<VAR>h : ∃ i, p i<VAR>this : Nonempty { i // p i }<GOAL>(⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a
<VAR>C : Type u_5<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_5} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_3<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<GOAL>(add F s i a b).hom.app (F.obj X) = (i (a + b)).hom.app X ≫ F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)
<VAR>C : Type u_5<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_5} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_3<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<VAR>h : whiskerLeft F (add F s i a b).hom = (i (a + b) ≪≫ isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫ (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫ isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫ ((shiftFunctor C a).associator F (s b)).symm ≪≫ isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom<GOAL>(add F s i a b).hom.app (F.obj X) = (i (a + b)).hom.app X ≫ F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.Φ n).natDegree ≤ n.natAbs ^ 2
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>a b : α<VAR>s : Set α<VAR>f : ι → α<GOAL>(sSup s)ᶜ = ⨅ i ∈ s, iᶜ
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>n : ℕ<VAR>h : I ⊔ J = ⊤<GOAL>I ⊔ J ^ n = ⊤
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>n : ℕ<VAR>h : I ⊔ J = ⊤<GOAL>I ⊔ ∏ _x ∈ Finset.range n, J = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι✝ : Type u_4<VAR>s✝ : Finset ι✝<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → V<VAR>hw : s.sum w = 0<GOAL>(s.weightedVSub p) w = ∑ i ∈ s, w i • p i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s₂ : Seq α<VAR>a : α<VAR>ss : Seq α<VAR>h : a ∈ ss<GOAL>∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = ss → a ∈ s₁ ∨ a ∈ s₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s₂ : Seq α<VAR>a : α<VAR>ss : Seq α<VAR>h : a ∈ ss<GOAL>∀ (b : α) (s' : Seq α), (a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) → ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>b✝ : α<VAR>l : List α<VAR>a : α<VAR>al✝ : a ∈ b✝ :: l<VAR>pa : p a = true<VAR>b : α<VAR>al : Mem a l<VAR>pb : ¬p b = true<VAR>c : α<VAR>l₁ l₂ : List α<VAR>h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true<VAR>h₂ : p c = true<VAR>h₃ : l = l₁ ++ c :: l₂<VAR>h₄ : eraseP p l = l₁ ++ l₂<GOAL>b :: l = b :: l₁ ++ c :: l₂
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : AddCommMonoid N<VAR>inst✝²¹ : CommSemiring R<VAR>inst✝²⁰ : CommSemiring S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : Module R M<VAR>inst✝¹⁷ : Module R N<VAR>inst✝¹⁶ : Module S N<VAR>inst✝¹⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝¹⁴ : AddCommMonoid P<VAR>inst✝¹³ : Module R P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁰ : CommSemiring T<VAR>inst✝⁹ : Algebra R T<VAR>inst✝⁸ : Algebra S T<VAR>inst✝⁷ : IsScalarTower R S T<VAR>inst✝⁶ : AddCommMonoid O<VAR>inst✝⁵ : Module R O<VAR>inst✝⁴ : Module S O<VAR>inst✝³ : Module T O<VAR>inst✝² : IsScalarTower S T O<VAR>inst✝¹ : IsScalarTower R S O<VAR>inst✝ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<GOAL>IsBaseChange T (↑R g ∘ₗ f)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : AddCommMonoid N<VAR>inst✝²¹ : CommSemiring R<VAR>inst✝²⁰ : CommSemiring S<VAR>inst✝¹⁹ : Algebra R S<VAR>inst✝¹⁸ : Module R M<VAR>inst✝¹⁷ : Module R N<VAR>inst✝¹⁶ : Module S N<VAR>inst✝¹⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝¹⁴ : AddCommMonoid P<VAR>inst✝¹³ : Module R P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁰ : CommSemiring T<VAR>inst✝⁹ : Algebra R T<VAR>inst✝⁸ : Algebra S T<VAR>inst✝⁷ : IsScalarTower R S T<VAR>inst✝⁶ : AddCommMonoid O<VAR>inst✝⁵ : Module R O<VAR>inst✝⁴ : Module S O<VAR>inst✝³ : Module T O<VAR>inst✝² : IsScalarTower S T O<VAR>inst✝¹ : IsScalarTower R S O<VAR>inst✝ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<GOAL>∀ (Q : Type (max v₁ u_5 u_4)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module T Q] [inst_3 : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = g_1
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : AddCommMonoid N<VAR>inst✝²⁵ : CommSemiring R<VAR>inst✝²⁴ : CommSemiring S<VAR>inst✝²³ : Algebra R S<VAR>inst✝²² : Module R M<VAR>inst✝²¹ : Module R N<VAR>inst✝²⁰ : Module S N<VAR>inst✝¹⁹ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q✝ : Type u_3<VAR>inst✝¹⁸ : AddCommMonoid P<VAR>inst✝¹⁷ : Module R P<VAR>inst✝¹⁶ : AddCommMonoid Q✝<VAR>inst✝¹⁵ : Module S Q✝<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝¹⁴ : CommSemiring T<VAR>inst✝¹³ : Algebra R T<VAR>inst✝¹² : Algebra S T<VAR>inst✝¹¹ : IsScalarTower R S T<VAR>inst✝¹⁰ : AddCommMonoid O<VAR>inst✝⁹ : Module R O<VAR>inst✝⁸ : Module S O<VAR>inst✝⁷ : Module T O<VAR>inst✝⁶ : IsScalarTower S T O<VAR>inst✝⁵ : IsScalarTower R S O<VAR>inst✝⁴ : IsScalarTower R T O<VAR>f : M →ₗ[R] N<VAR>hf : IsBaseChange S f<VAR>g : N →ₗ[S] O<VAR>hg : IsBaseChange T g<VAR>Q : Type (max v₁ u_5 u_4)<VAR>inst✝³ : AddCommMonoid Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : Module T Q<VAR>inst✝ : IsScalarTower R T Q<VAR>i : M →ₗ[R] Q<VAR>this : Module S Q := Module.compHom Q (algebraMap S T)<GOAL>∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = i