ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>i j : σ<GOAL>Finsupp.single i 1 ≤ Finsupp.single j 1 ↔ i = j
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Continuous fun p => ∑ i : α, a i * b i ^ p
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>x✝ : i ∈ univ<GOAL>Continuous (HPow.hPow (b i))
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x : α<VAR>n : ℕ<GOAL>(∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x : α<VAR>n : ℕ<VAR>this : (∑ i ∈ range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n<GOAL>(∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x : α<VAR>n : ℕ<VAR>this : (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n<GOAL>(∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Group G<VAR>𝔖✝ : Set (Set α)<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>𝔖 : Set (Set α)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 1).HasBasis p b<GOAL>(𝓝 1).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, (toFun 𝔖) f x ∈ b Si.2}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Group G<VAR>𝔖✝ : Set (Set α)<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>𝔖 : Set (Set α)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 1).HasBasis p b<VAR>this : (𝓤 G).HasBasis p fun i => {x | x.1 / x.2 ∈ b i}<GOAL>(𝓝 1).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, (toFun 𝔖) f x ∈ b Si.2}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Group G<VAR>𝔖✝ : Set (Set α)<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>𝔖 : Set (Set α)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 1).HasBasis p b<VAR>this : (𝓤 G).HasBasis p fun i => {x | x.1 / x.2 ∈ b i}<VAR>x✝¹ : Set α × ι<VAR>x✝ : α →ᵤ[𝔖] G<GOAL>(∀ x ∈ x✝¹.1, (toFun 𝔖) x✝ x ∈ b x✝¹.2) ↔ (x✝, 1) ∈ UniformOnFun.gen 𝔖 x✝¹.1 {x | x.1 / x.2 ∈ b x✝¹.2}
<VAR>S : Type u_1<VAR>inst✝³ : AddCommGroupWithOne S<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasShift C S<VAR>n : S<VAR>X : DifferentialObject S C<GOAL>((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) = 0
<VAR>S : Type u_1<VAR>inst✝³ : AddCommGroupWithOne S<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasShift C S<VAR>n : S<VAR>X✝ Y✝ : DifferentialObject S C<VAR>f : X✝ ⟶ Y✝<GOAL>((CategoryTheory.shiftFunctor C n).map X✝.d ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj) ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.f) = (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj
<VAR>S : Type u_1<VAR>inst✝³ : AddCommGroupWithOne S<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasShift C S<VAR>n : S<VAR>X✝ Y✝ : DifferentialObject S C<VAR>f : X✝ ⟶ Y✝<GOAL>(CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftComm Y✝.obj 1 n).hom = (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj
<VAR>S : Type u_1<VAR>inst✝³ : AddCommGroupWithOne S<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasShift C S<VAR>n : S<VAR>X : DifferentialObject S C<GOAL>autoParam ((CategoryTheory.shiftFunctor C n).map (𝟙 X.obj) = 𝟙 ((CategoryTheory.shiftFunctor C n).obj X.obj)) _auto✝
<VAR>S : Type u_1<VAR>inst✝³ : AddCommGroupWithOne S<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasShift C S<VAR>n : S<VAR>X✝ Y✝ Z✝ : DifferentialObject S C<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>autoParam ((CategoryTheory.shiftFunctor C n).map (f.f ≫ g.f) = (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map g.f) _auto✝
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<GOAL>IsOpen (A f L r ε)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<GOAL>∀ x ∈ A f L r ε, ∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<VAR>x : E<VAR>r' : ℝ<VAR>r'_mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<GOAL>∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<VAR>x : E<VAR>r' : ℝ<VAR>r'_mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<GOAL>∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<VAR>x : E<VAR>r' : ℝ<VAR>r'_mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<VAR>this : s ∈ Ioc (r / 2) r<GOAL>∃ ε_1 > 0, ball x ε_1 ⊆ A f L r ε
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<VAR>x : E<VAR>r' : ℝ<VAR>r'_mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<VAR>this : s ∈ Ioc (r / 2) r<VAR>x' : E<VAR>hx' : x' ∈ ball x (r' - s)<GOAL>∀ y ∈ ball x' s, ∀ z ∈ ball x' s, ‖f z - f y - L (z - y)‖ < ε * r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>r ε : ℝ<VAR>x : E<VAR>r' : ℝ<VAR>r'_mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<VAR>this : s ∈ Ioc (r / 2) r<VAR>x' : E<VAR>hx' : x' ∈ ball x (r' - s)<VAR>B : ball x' s ⊆ ball x r'<GOAL>∀ y ∈ ball x' s, ∀ z ∈ ball x' s, ‖f z - f y - L (z - y)‖ < ε * r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p : α → Prop<VAR>f : β → α<VAR>hs : NullMeasurableSet s μ<GOAL>μ sᶜ = 1 ↔ μ s = 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(normalizedFactors a).prod ~ᵤ a
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(Multiset.map (⇑normalize) (Classical.choose ⋯)).prod ~ᵤ a
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(Multiset.map (⇑normalize) (Classical.choose ⋯)).prod ~ᵤ (Classical.choose ⋯).prod
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(Multiset.map (Associates.mk ∘ ⇑normalize) (Classical.choose ⋯)).prod = (Multiset.map Associates.mk (Classical.choose ⋯)).prod
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<VAR>x✝ : α<GOAL>(Associates.mk ∘ ⇑normalize) x✝ = Associates.mk x✝
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<GOAL>clog b 1 = 0
<VAR>n✝ n : ℕ<VAR>this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)<GOAL>Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))
<VAR>d : ℕ<VAR>a b : ℤ√↑d<GOAL>0 ≤ a → 0 ≤ b → 0 ≤ a * b
<VAR>d : ℕ<VAR>a b : ℤ√↑d<GOAL>a.Nonneg → b.Nonneg → (a * b).Nonneg
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Submonoid.closure s)<GOAL>0 * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Submonoid.closure s)<GOAL>0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Submonoid.closure s)<VAR>p₁ p₂ : R<VAR>ihp₁ : p₁ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>ihp₂ : p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)<GOAL>p₁ * q + p₂ * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝¹ : R<VAR>h : x✝¹ ∈ closure s<VAR>x✝ y : R<VAR>hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>q : R<VAR>hq : q ∈ ↑(Submonoid.closure s)<VAR>x : R<VAR>hx : x * q ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>f : -x * q = -(x * q)<GOAL>-(x * q) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<GOAL>x * 0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<GOAL>0 ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>q₁ q₂ : R<VAR>ihq₁ : x * q₁ ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>ihq₂ : x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)<GOAL>x * q₁ + x * q₂ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>x✝ : R<VAR>h : x✝ ∈ closure s<VAR>x y : R<VAR>hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>hy : y ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>z : R<VAR>hz : x * z ∈ AddSubgroup.closure ↑(Submonoid.closure s)<VAR>f : x * -z = -(x * z)<GOAL>-(x * z) ∈ AddSubgroup.closure ↑(Submonoid.closure s)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hbc : AddLECancellable (b - c)<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ b<GOAL>a = a - b + c + (b - c)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>ENNReal.ofReal T * (addHaarMeasure ⊤) univ = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>ENNReal.ofReal T * (addHaarMeasure ⊤) ↑⊤ = ENNReal.ofReal T
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>aA : a0 ∈ A<VAR>bB : b0 ∈ B<VAR>h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0<VAR>x1 x2 : G<VAR>a✝ : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0<VAR>J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)<VAR>x y : G<VAR>hx : x ∈ A<VAR>hy : y ∈ B<VAR>l : x * y = a0 * b0<GOAL>x = a0 ∧ y = b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>aA : a0 ∈ A<VAR>bB : b0 ∈ B<VAR>h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0<VAR>x y : G<VAR>hx : x ∈ A<VAR>hy : y ∈ B<VAR>l : x * y = a0 * b0<VAR>a✝ : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0<VAR>J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)<GOAL>x = a0 ∧ y = b0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>f : α → β<GOAL>ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>x : ↑X<VAR>V : Opens ↑X<VAR>hV : x ∈ V<GOAL>((pullback C f).obj F).germ ⟨x, hV⟩ ≫ stalkPullbackInv C f F x = germToPullbackStalk C f F V ⟨x, hV⟩
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v w : E<GOAL>‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<GOAL>⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>a₁ : α<VAR>b₁ : β<VAR>a₂ : α<VAR>b₂ : β<VAR>h : (a₁, b₁) < (a₂, b₂)<GOAL>toLex (a₁, b₁) < toLex (a₂, b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>a₁ : α<VAR>b₁ b₂ : β<VAR>h : (a₁, b₁) < (a₁, b₂)<GOAL>toLex (a₁, b₁) < toLex (a₁, b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>a₁ : α<VAR>b₁ : β<VAR>a₂ : α<VAR>b₂ : β<VAR>h : (a₁, b₁) < (a₂, b₂)<VAR>ha : (a₁, b₁).1 < (a₂, b₂).1<GOAL>toLex (a₁, b₁) < toLex (a₂, b₂)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>b⁻¹ * a ≤ c ↔ a ≤ b * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfm : Monotone f<VAR>k : ℕ<GOAL>∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i ≤ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfm : Monotone f<VAR>k : ℕ<VAR>hm : Monotone fun n => ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i<GOAL>∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i ≤ l
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>v : Fin (n + 1) → α<VAR>i : Fin (n + 1)<GOAL>vecAlt1 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 => n_1 + n_1 + 1) i
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>v : Fin (n + 1) → α<VAR>i : Fin (n + 1)<GOAL>(if h : ↑i + ↑i + 1 < n + 1 then v ⟨↑i + ↑i + 1, ⋯⟩ else v ⟨↑i + ↑i + 1 - (n + 1), ⋯⟩) = v (i + i + 1)
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>Reaches₁ (TM2.step tr) { l := some (head main q), var := s, stk := elim (trList L) [] c d } { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = []) (fun a => natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr ((fun x => Λ'.read fun s => (if s = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev q)) o)) o (update (update (update (elim (trList L) [] c d) main (trList L.tail)) rev ((trNat L.headI).reverseAux (elim (trList L) [] c d rev))) rev ((fun s => ((fun x => some Γ'.cons) s).iget) o :: update (update (elim (trList L) [] c d) main (trList L.tail)) rev ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev))) { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>TransGen (fun a b => (match a with | { l := none, var := var, stk := stk } => none | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) = some b) { l := some ((if o = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev q)), var := o, stk := elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d } { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>TransGen (fun a b => (match a with | { l := none, var := var, stk := stk } => none | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) = some b) { l := some (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main (unrev q)), var := o, stk := elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d } { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>∀ x ∈ elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d main, decide (x = Γ'.consₗ) = false
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>TransGen (fun a b => b ∈ TM2.step tr a) { l := some (unrev q), var := none, stk := update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] } { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }
<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L : List ℕ<VAR>c d : List Γ'<VAR>o : Option Γ' := List.casesOn L none fun x x => some Γ'.cons<GOAL>elim (trNat L.headI ++ [Γ'.cons]) [] c d = update (update (update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main []) rev []) main ((update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] rev).reverseAux (update (elim (trList L.tail) ((some Γ'.cons).iget :: (trNat L.headI).reverseAux []) c d) main [] main))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>n : ℤ<GOAL>‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Matrix V V α<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i : V<GOAL>¬A i i = 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝¹ : UniformSpace ι<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>UniformInducing (⇑UniformFun.ofFun ∘ F) ↔ UniformInducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝¹ : UniformSpace ι<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>UniformSpace.comap (⇑UniformFun.ofFun ∘ F) (UniformFun.uniformSpace X α) = inst✝¹ ↔ UniformSpace.comap F (UniformFun.uniformSpace X α) = inst✝¹
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : IsNat b nb<VAR>pe' : IsNat (a ^ nb) ne<GOAL>IsNat (a ^ b) ne
<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>v w : V<GOAL>G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
<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>v w : V<GOAL>¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>n : ℕ<GOAL>(s.drop (n + 1)).destruct = s.destruct >>= drop.aux (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>n : ℕ<GOAL>(s.destruct >>= fun x => tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>p.comp (C a) = C (eval a p)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hyz : s.WSameSide y z<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>s.WSameSide x z