ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>h : (a :: b :: l).split = (l₁, l₂)<VAR>l₁' l₂' : List α<VAR>e : l.split = (l₁', l₂')<VAR>fst_eq✝ : a :: l₁' = l₁<VAR>snd_eq✝ : b :: l₂' = l₂<GOAL>l₁.length < (a :: b :: l).length ∧ l₂.length < (a :: b :: l).length
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁' l₂' : List α<VAR>e : l.split = (l₁', l₂')<VAR>h : (a :: b :: l).split = (a :: l₁', b :: l₂')<GOAL>(a :: l₁').length < (a :: b :: l).length ∧ (b :: l₂').length < (a :: b :: l).length
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁' l₂' : List α<VAR>e : l.split = (l₁', l₂')<VAR>h : (a :: b :: l).split = (a :: l₁', b :: l₂')<VAR>h₁ : l₁'.length ≤ l.length<VAR>h₂ : l₂'.length ≤ l.length<GOAL>(a :: l₁').length < (a :: b :: l).length ∧ (b :: l₂').length < (a :: b :: l).length
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>1 ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>1 * a ≤ a⁻¹ * a ↔ a ≤ 1
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>x : M₁<VAR>i : m<GOAL>((toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x)) i = (v₂.repr (f x)) i
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>x : M₁<VAR>i : m<GOAL>(v₂.repr (f (v₁.equivFun.symm ⇑(v₁.repr x)))) i = (v₂.repr (f x)) i
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>x : M₁<VAR>i : m<GOAL>v₁.equivFun.symm ⇑(v₁.repr x) = x
<VAR>z : ℂ<GOAL>(↑π * z).cot = (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))
<VAR>z : ℂ<GOAL>(cexp (2 * I * (↑π * z)) + 1) / (I * (1 - cexp (2 * I * (↑π * z)))) = (cexp (2 * ↑π * I * z) + 1) / (I * (1 - cexp (2 * ↑π * I * z)))
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : Submartingale f ℱ μ<GOAL>Submartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : Submartingale f ℱ μ<GOAL>Submartingale (-(c • -f)) ℱ μ
<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hμs_ne_zero : μ s ≠ 0<GOAL>‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖
<VAR>f✝ g : CircleDeg1Lift<VAR>f : CircleDeg1Liftˣ<GOAL>τ ↑f⁻¹ + τ ↑f = 0
<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 : Matroid α<VAR>hM : M.E = E<GOAL>(M.restrictSubtype E)✶ = M✶.restrictSubtype E
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H✝ K : Subgroup G<VAR>S T : Set G<VAR>H' H : Subgroup G<VAR>h : H' ≤ H<VAR>H'' : Subgroup ↥H := comap H.subtype H'<VAR>this : H' = map H.subtype H''<GOAL>∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H✝ K : Subgroup G<VAR>S✝ T : Set G<VAR>H' H : Subgroup G<VAR>h : H' ≤ H<VAR>H'' : Subgroup ↥H := comap H.subtype H'<VAR>this : H' = map H.subtype H''<VAR>S : Set ↥H<VAR>cmem : S ∈ leftTransversals ↑H''<GOAL>∃ S, S * ↑(map H.subtype H'') = ↑H ∧ Nat.card ↑S * Nat.card ↥(map H.subtype H'') = Nat.card ↥H
<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✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : G.Dart<VAR>hx : x ∈ (p.dropUntil u h).darts<GOAL>x ∈ p.darts
<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✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : G.Dart<VAR>hx : x ∈ (p.dropUntil u h).darts<GOAL>x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
<VAR>α : Sort u<VAR>β : Sort v<GOAL>Uncountable α ↔ IsEmpty (α ↪ ℕ)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4360, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<GOAL>S.Exact ↔ IsZero h.right.H
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4360, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<VAR>this : S.HasHomology<GOAL>S.Exact ↔ IsZero h.right.H
<VAR>a b : ℕ+<GOAL>a.gcdD b = a.gcd b
<VAR>a b : ℕ+<VAR>left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat<VAR>h₁ : a = a.gcdA' b * a.gcdD b<VAR>h₂ : b = a.gcdB' b * a.gcdD b<VAR>left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat<VAR>left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat<VAR>h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)<VAR>right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)<GOAL>a.gcdD b = a.gcd b
<VAR>a b : ℕ+<VAR>left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat<VAR>h₁ : a = a.gcdA' b * a.gcdD b<VAR>h₂ : b = a.gcdB' b * a.gcdD b<VAR>left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat<VAR>left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat<VAR>h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)<VAR>right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)<GOAL>a.gcdD b ∣ a.gcd b
<VAR>a b : ℕ+<VAR>left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat<VAR>h₁ : a = a.gcdA' b * a.gcdD b<VAR>h₂ : b = a.gcdB' b * a.gcdD b<VAR>left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat<VAR>left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat<VAR>h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)<VAR>right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)<GOAL>a.gcd b ∣ a.gcdD b
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ.addHaarScalarFactor volume • volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>Tendsto (fun w => μ.addHaarScalarFactor volume • ∫ (v : V), 𝐞 (-w v) • f v ∂volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>Tendsto (fun w => μ.addHaarScalarFactor volume • ∫ (v : V), 𝐞 (-w v) • f v ∂volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 (μ.addHaarScalarFactor volume • 0))
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>Tendsto (fun x => ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm<GOAL>Tendsto (fun x => ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm<VAR>this : (fun w => ∫ (v : V), 𝐞 (-w v) • f v) = (fun w => ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) ∘ ⇑A<GOAL>Tendsto (fun x => ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : NormedSpace.Dual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm<VAR>this : (fun w => ∫ (v : V), 𝐞 (-w v) • f v) = (fun w => ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) ∘ ⇑A<GOAL>Tendsto ((fun w => ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) ∘ ⇑A) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>inst✝ : LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊔ b = b * (a / b)⁺ᵐ
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : IsAntisymm α r₂<VAR>h : ∀ (a b : α), r₁ a b → r₂ a b<VAR>a : α<VAR>ha : a ∈ minimals r₂ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : r₁ b a<GOAL>r₁ a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : IsAntisymm α r₂<VAR>h : ∀ (a b : α), r₁ a b → r₂ a b<VAR>a : α<VAR>ha : a ∈ minimals r₂ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : r₁ b a<VAR>this : a = b<GOAL>r₁ a b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>init n (x * y) = init n (init n x * init n y)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₁<VAR>l : List Γ<GOAL>Part.map (fun c => c.Tape.right₀) (trCfg M <$> eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) = TM1.eval M l
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₁<VAR>l : List Γ<GOAL>Part.map ((fun c => c.Tape.right₀) ∘ trCfg M) (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) = Part.map (fun c => c.Tape.right₀) (eval (TM1.step M) (TM1.init l))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : 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>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>Inducing f ↔ (∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : 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>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f : Sigma σ → X<VAR>h : Inducing f<VAR>i : ι<GOAL>∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : 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>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>((∀ (i : ι), Inducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i) → Inducing f
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.degree ≤ 0<VAR>n : ℕ<GOAL>p.coeff (n + 1) = (C (p.coeff 0)).coeff (n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.degree ≤ 0<VAR>n : ℕ<GOAL>p.degree < ↑(n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<GOAL>t ∈ ⨅ i ∈ dom, l i ↔ ∃ i, (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<GOAL>(∃ i ∈ dom, t ∈ l i) ↔ ∃ a b, ((a, b).1 ∈ dom ∧ p (a, b).1 (a, b).2) ∧ s (a, b).1 (a, b).2 ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i✝ : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<VAR>i : ι<GOAL>i ∈ dom ∧ t ∈ l i → ∃ b, ((i, b).1 ∈ dom ∧ p (i, b).1 (i, b).2) ∧ s (i, b).1 (i, b).2 ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i✝ : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>dom : Set ι<VAR>hdom : dom.Nonempty<VAR>l : ι → Filter α<VAR>s : ι → ι' → Set α<VAR>p : ι → ι' → Prop<VAR>hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)<VAR>h : DirectedOn (l ⁻¹'o GE.ge) dom<VAR>t : Set α<VAR>i : ι<GOAL>(∃ b, ((i, b).1 ∈ dom ∧ p (i, b).1 (i, b).2) ∧ s (i, b).1 (i, b).2 ⊆ t) → i ∈ dom ∧ t ∈ l i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<VAR>h : p.coeff i = 0<GOAL>coeffIntegerNormalization M p i = 0
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<VAR>h : a * ↑u = 1<GOAL>↑u⁻¹ = 1 * ↑u⁻¹
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<VAR>h : a * ↑u = 1<GOAL>1 * ↑u⁻¹ = a
<VAR>Ω : Type u_1<VAR>inst✝⁴ : TopologicalSpace Ω<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ℕ → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c<VAR>fs_lim : Tendsto (fun n ω => (fs n) ω) atTop (𝓝 (E.indicator fun x => 1))<GOAL>Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) atTop (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>inst✝⁴ : TopologicalSpace Ω<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : ℝ≥0<VAR>E : Set Ω<VAR>E_mble : MeasurableSet E<VAR>fs : ℕ → Ω →ᵇ ℝ≥0<VAR>fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c<VAR>fs_lim : Tendsto (fun n ω => (fs n) ω) atTop (𝓝 (E.indicator fun x => 1))<VAR>fs_lim' : ∀ (ω : Ω), Tendsto (fun n => (fs n) ω) atTop (𝓝 (E.indicator (fun x => 1) ω))<GOAL>Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) atTop (𝓝 (μ E))
<VAR>a : ℝ<VAR>hane : a ≠ 0<VAR>ha : Tendsto stirlingSeq atTop (𝓝 a)<GOAL>Tendsto Wallis.W atTop (𝓝 (a ^ 2 / 2))
<VAR>a : ℝ<VAR>hane : a ≠ 0<VAR>ha : Tendsto stirlingSeq atTop (𝓝 a)<GOAL>Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))
<VAR>a : ℝ<VAR>hane : a ≠ 0<VAR>ha : Tendsto stirlingSeq atTop (𝓝 a)<VAR>h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)<GOAL>Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))
<VAR>a : ℝ<VAR>hane : a ≠ 0<VAR>ha : Tendsto stirlingSeq atTop (𝓝 a)<VAR>h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)<GOAL>Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 4 / a ^ 2 * (1 / 2)))
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : DecidableEq α<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>inst✝ : LocallyFiniteOrderTop α<VAR>a b : α<GOAL>↑(Ioi a * Ici b) ⊆ ↑(Ioi (a * b))
<VAR>n : ℤ<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : p ∣ n.natAbs ^ k<GOAL>p ∣ n.natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : BorelSpace γ<VAR>inst✝ : MeasurableSpace δ<GOAL>Prod.instMeasurableSpace ≤ borel (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : BorelSpace γ<VAR>inst✝ : MeasurableSpace δ<GOAL>MeasurableSpace.comap Prod.fst (borel α) ≤ borel (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : BorelSpace γ<VAR>inst✝ : MeasurableSpace δ<GOAL>MeasurableSpace.comap Prod.snd (borel β) ≤ borel (α × β)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<GOAL>IsNormalClosure F K ↥(normalClosure F K L)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<GOAL>(∀ (x : K), Splits (algebraMap F ↥(normalClosure F K L)) (minpoly F x)) ∧ normalClosure F K ↥(normalClosure F K L) = ⊤
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<GOAL>normalClosure F K ↥(normalClosure F K L) = ⊤
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<GOAL>⊤ ≤ ⨆ f, f.fieldRange
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>x : ↥(⨆ f, f.fieldRange)<VAR>x✝ : x ∈ ⊤<GOAL>(⨆ f, f.fieldRange).val.toRingHom x ∈ ⇑(⨆ f, f.fieldRange).val.toRingHom '' ↑(⨆ f, f.fieldRange)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>x : ↥(⨆ f, f.fieldRange)<VAR>x✝ : x ∈ ⊤<GOAL>↑x ∈ IntermediateField.map (⨆ f, f.fieldRange).val (⨆ f, f.fieldRange)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>x : ↥(⨆ f, f.fieldRange)<VAR>x✝ : x ∈ ⊤<GOAL>↑x ∈ ⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange