ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a✝ n a : ℕ<VAR>L₀ : List ℕ<VAR>hL₀ : Sorted (fun x x_1 => x < x_1) L₀<VAR>hL✝ : Sorted (fun x x_1 => x < x_1) (a :: map (fun x => x + a + 1) L₀)<VAR>hL : Sorted (fun x x_1 => x < x_1) (map (fun x => x + a + 1) L₀)<VAR>haL : ∀ b ∈ map (fun x => x + a + 1) L₀, a + 1 ≤ b<VAR>x✝ : L₀.length < (a :: map (fun x => x + a + 1) L₀).length<VAR>hrw : ((fun x => 2 ^ x) ∘ fun x => x + a + 1) = fun i => 2 ^ a * (2 * 2 ^ i)<GOAL>(2 ^ a * 1 + 2 ^ a * (2 * (map (HPow.hPow 2) L₀).sum)).bitIndices = a :: map (fun x => x + a + 1) L₀
<VAR>a✝ n a : ℕ<VAR>L₀ : List ℕ<VAR>hL₀ : Sorted (fun x x_1 => x < x_1) L₀<VAR>hL✝ : Sorted (fun x x_1 => x < x_1) (a :: map (fun x => x + a + 1) L₀)<VAR>hL : Sorted (fun x x_1 => x < x_1) (map (fun x => x + a + 1) L₀)<VAR>haL : ∀ b ∈ map (fun x => x + a + 1) L₀, a + 1 ≤ b<VAR>x✝ : L₀.length < (a :: map (fun x => x + a + 1) L₀).length<VAR>hrw : ((fun x => 2 ^ x) ∘ fun x => x + a + 1) = fun i => 2 ^ a * (2 * 2 ^ i)<GOAL>map (fun x => x + a) (0 :: map (fun x => x + 1) L₀) = a :: map (fun x => x + a + 1) L₀
<VAR>α : Type u_1<VAR>inst✝² : CompleteLattice α<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : IsCoatomic α<VAR>a : α<VAR>h : a ⊔ radical α = ⊤<GOAL>a = ⊤
<VAR>α : Type u_1<VAR>inst✝² : CompleteLattice α<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : IsCoatomic α<VAR>h : ⊤ ⊔ radical α = ⊤<GOAL>⊤ = ⊤
<VAR>α : Type u_1<VAR>inst✝² : CompleteLattice α<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : IsCoatomic α<VAR>a : α<VAR>h : a ⊔ radical α = ⊤<VAR>w : ∃ a_1, IsCoatom a_1 ∧ a ≤ a_1<GOAL>a = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : Nonempty ι<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set γ<VAR>f : γ → α<VAR>hf : BddAbove (f '' s)<VAR>hne : s.Nonempty<GOAL>l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : Nonempty ι<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set γ<VAR>f : γ → α<VAR>hf : BddAbove (f '' s)<VAR>hne : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : Nonempty ι<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>s : Set γ<VAR>f : γ → α<VAR>hf : BddAbove (range fun x => f ↑x)<VAR>hne : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>h₁ : LiftRel r s x y<VAR>h₂ : x.isRight = true<GOAL>∃ b d, s b d ∧ x = inr b ∧ y = inr d
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>w✝ : β<VAR>h₁ : LiftRel r s (inr w✝) y<VAR>h₂ : (inr w✝).isRight = true<GOAL>∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>w✝ : β<VAR>h₂ : (inr w✝).isRight = true<VAR>h₁ : ∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d<GOAL>∃ b d, s b d ∧ inr w✝ = inr b ∧ y = inr d
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>s : Heap α<GOAL>((tail? le s).getD nil).realSize = s.realSize - 1
<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>inst✝ : CompleteLattice β<VAR>f : α ≃o β<VAR>x✝ : ι → α<VAR>x : α<GOAL>f (⨆ i, x✝ i) ≤ f x ↔ ⨆ i, f (x✝ i) ≤ f x
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>hp : Nat.Prime p<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>hp : p = 0<GOAL>Nonempty (K ≃+* L)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>p₁ p₂ p₃ : ι<VAR>h₂₁ : p₂ = p₁<VAR>h₃₂ : p₃ = p₂<GOAL>eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>c : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → β<GOAL>map f (c • μ) = c • map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>μ : Measure α<VAR>f : α → β<GOAL>map f (0 • μ) = 0 • map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>c : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → β<VAR>hc : c ≠ 0<GOAL>map f (c • μ) = c • map f μ
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f : V →ₗ[K] V₂<GOAL>finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f : V →ₗ[K] V₂<GOAL>finrank K (V ⧸ ker f) + finrank K ↥(ker f) = finrank K V
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m p q : ℤ<VAR>hpq : p + 2 = q<GOAL>(δ 1 2 (Cochain.diff K)).v p q hpq = Cochain.v 0 p q hpq
<VAR>x : ℝ<GOAL>sin (π / 3) = √3 / 2
<VAR>x : ℝ<GOAL>cos (π / 2 - π / 3) = cos (π / 6)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<GOAL>IsTorsionBySet R M s ↔ IsTorsionBySet R M ↑(Ideal.span s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<GOAL>NullMeasurableSet {a | f a ≤ g a} μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<GOAL>{a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a | f a ≤ g a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g✝ : α → β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>x : α<VAR>hfx : f x = AEStronglyMeasurable.mk f hf x<VAR>hgx : g x = AEStronglyMeasurable.mk g hg x<GOAL>{a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a | f a ≤ g a} x
<VAR>b : Bool<VAR>n : ℕ<GOAL>(bit b ↑n).testBit 0 = b
<VAR>b : Bool<VAR>n : ℕ<GOAL>(↑(Nat.bit b n)).testBit 0 = b
<VAR>b : Bool<VAR>n : ℕ<GOAL>(bit b -[n+1]).testBit 0 = b
<VAR>b : Bool<VAR>n : ℕ<GOAL>-[Nat.bit (!b) n+1].testBit 0 = b
<VAR>b : Bool<VAR>n : ℕ<GOAL>(!(Nat.bit (!b) n).testBit 0) = b
<VAR>b : Bool<VAR>n : ℕ<GOAL>(!!b) = b
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<GOAL>∀ᶠ (z : 𝕜) in cobounded 𝕜, IsUnit (resolvent a z)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<GOAL>∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Set.Ioi i → IsUnit (resolvent a x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<VAR>A : Set β<VAR>hA : MeasurableSet A<GOAL>∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a = ((κ a) (A ×ˢ Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<VAR>A : Set β<VAR>hA : MeasurableSet A<GOAL>∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a ≤ ((κ a) (A ×ˢ Iic ↑q)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>q : ℚ<VAR>A : Set β<VAR>hA : MeasurableSet A<GOAL>((κ a) (A ×ˢ Iic ↑q)).toReal ≤ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a
<VAR>R : Type u1<VAR>inst✝¹² : CommRing R<VAR>M : Type u2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>A : Type u_1<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R N'<VAR>inst✝³ : Module Rᵐᵒᵖ M<VAR>inst✝² : IsCentralScalar R M<VAR>inst✝¹ : Module Rᵐᵒᵖ N<VAR>inst✝ : IsCentralScalar R N<VAR>f : M →ₗ[R] N<GOAL>toTrivSqZeroExt.comp (map f) = (TrivSqZeroExt.map f).comp toTrivSqZeroExt
<VAR>R : Type u1<VAR>inst✝¹² : CommRing R<VAR>M : Type u2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>A : Type u_1<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R N'<VAR>inst✝³ : Module Rᵐᵒᵖ M<VAR>inst✝² : IsCentralScalar R M<VAR>inst✝¹ : Module Rᵐᵒᵖ N<VAR>inst✝ : IsCentralScalar R N<VAR>f : M →ₗ[R] N<GOAL>(toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R = ((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R
<VAR>R : Type u1<VAR>inst✝¹² : CommRing R<VAR>M : Type u2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>A : Type u_1<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R N'<VAR>inst✝³ : Module Rᵐᵒᵖ M<VAR>inst✝² : IsCentralScalar R M<VAR>inst✝¹ : Module Rᵐᵒᵖ N<VAR>inst✝ : IsCentralScalar R N<VAR>f : M →ₗ[R] N<GOAL>∀ (x : M), ((toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R) x = (((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R) x
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<VAR>x : ↑(X ⨯ Y)<GOAL>(X.prodIsoProd Y).hom x = (prod.fst x, prod.snd x)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<VAR>x : ↑(X ⨯ Y)<GOAL>((X.prodIsoProd Y).hom x).1 = (prod.fst x, prod.snd x).1
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<VAR>x : ↑(X ⨯ Y)<GOAL>((X.prodIsoProd Y).hom x).2 = (prod.fst x, prod.snd x).2
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : ContinuousConstSMul 𝕜₃ G<VAR>inst✝ : ContinuousConstSMul 𝕜₂ F<VAR>L : F →SL[τ] G<VAR>this : UniformSpace G := TopologicalAddGroup.toUniformSpace G<GOAL>Continuous { toFun := fun f => L.comp f, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : ContinuousConstSMul 𝕜₃ G<VAR>inst✝ : ContinuousConstSMul 𝕜₂ F<VAR>L : F →SL[τ] G<VAR>this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G<VAR>this : UniformAddGroup G<GOAL>Continuous { toFun := fun f => L.comp f, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : ContinuousConstSMul 𝕜₃ G<VAR>inst✝ : ContinuousConstSMul 𝕜₂ F<VAR>L : F →SL[τ] G<VAR>this✝¹ : UniformSpace G := TopologicalAddGroup.toUniformSpace G<VAR>this✝ : UniformAddGroup G<VAR>this : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>Continuous { toFun := fun f => L.comp f, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : ContinuousConstSMul 𝕜₃ G<VAR>inst✝ : ContinuousConstSMul 𝕜₂ F<VAR>L : F →SL[τ] G<VAR>this✝² : UniformSpace G := TopologicalAddGroup.toUniformSpace G<VAR>this✝¹ : UniformAddGroup G<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>Continuous { toFun := fun f => L.comp f, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : ContinuousConstSMul 𝕜₃ G<VAR>inst✝ : ContinuousConstSMul 𝕜₂ F<VAR>L : F →SL[τ] G<VAR>this✝² : UniformSpace G := TopologicalAddGroup.toUniformSpace G<VAR>this✝¹ : UniformAddGroup G<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>Continuous ((⇑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) ∘ DFunLike.coe) ∘ { toFun := fun f => L.comp f, map_add' := ⋯, map_smul' := ⋯ }.toFun)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s✝ t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>s : Set α<VAR>f g : α → M<GOAL>(s.mulIndicator fun a => f a * g a) = fun a => s.mulIndicator f a * s.mulIndicator g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s✝ t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>s : Set α<VAR>f g : α → M<VAR>x✝ : α<GOAL>s.mulIndicator (fun a => f a * g a) x✝ = s.mulIndicator f x✝ * s.mulIndicator g x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s✝ t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>s : Set α<VAR>f g : α → M<VAR>x✝ : α<VAR>h✝ : x✝ ∉ s<GOAL>1 = 1 * 1
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set ℝ<VAR>f f' : ℝ → ℝ<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : ℝ → F<GOAL>IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x => |f' x| • g (f x)) s volume
<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>α : Type u_9<VAR>β : Type u_10<VAR>s : Set (α → β → Prop)<VAR>a : α<VAR>b : β<GOAL>sSup s a b ↔ ∃ r ∈ s, r a 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>α : Type u_9<VAR>β : Type u_10<VAR>s : Set (α → β → Prop)<VAR>a : α<VAR>b : β<GOAL>(⨆ f, ↑f a) b ↔ ∃ r ∈ s, r a b
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>p : Fin (n + 1)<VAR>x : α p<VAR>f : (j : Fin (n + 1)) → α j<GOAL>p.insertNth x (p.removeNth f) = update f p x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup EM<VAR>inst✝¹⁷ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹³ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝⁹ : TopologicalSpace N<VAR>inst✝⁸ : ChartedSpace H N<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : ChartedSpace H A<VAR>inst✝³ : TopologicalSpace A'<VAR>inst✝² : ChartedSpace H' A'<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : ChartedSpace H R<VAR>x : M<GOAL>Function.Surjective (eval IM I N x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup EM<VAR>inst✝¹⁷ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹³ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝⁹ : TopologicalSpace N<VAR>inst✝⁸ : ChartedSpace H N<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : ChartedSpace H A<VAR>inst✝³ : TopologicalSpace A'<VAR>inst✝² : ChartedSpace H' A'<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : ChartedSpace H R<VAR>x : M<GOAL>∀ (t : N), ∃ U f, ∃ (_ : (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred f), f ⟨x, ⋯⟩ = t
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup EM<VAR>inst✝¹⁷ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹³ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝⁹ : TopologicalSpace N<VAR>inst✝⁸ : ChartedSpace H N<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : ChartedSpace H A<VAR>inst✝³ : TopologicalSpace A'<VAR>inst✝² : ChartedSpace H' A'<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : ChartedSpace H R<VAR>x : M<VAR>n : N<GOAL>∃ U f, ∃ (_ : (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred f), f ⟨x, ⋯⟩ = n
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>f : Γ → Stmt Bool Λ' σ<VAR>v : σ<VAR>L R : ListBlank Γ<GOAL>stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>f : Γ → Stmt Bool Λ' σ<VAR>v : σ<VAR>L R : ListBlank Γ<GOAL>∀ (f : Vector Bool n → Stmt Bool Λ' σ), stepAux (readAux n f) v (trTape' enc0 L R) = stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>f : Γ → Stmt Bool Λ' σ<VAR>v : σ<VAR>L : ListBlank Γ<VAR>a : Γ<VAR>R : ListBlank Γ<GOAL>∀ (f : Vector Bool n → Stmt Bool Λ' σ), stepAux (readAux n f) v (trTape' enc0 L (ListBlank.cons a R)) = stepAux (f (enc (ListBlank.cons a R).head)) v (trTape' enc0 (ListBlank.cons (ListBlank.cons a R).head L) (ListBlank.cons a R).tail)