ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<GOAL>IsOpen (Iio ⊤)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<VAR>x : L<VAR>h : optParam (∀ (m : M) (hm : m ∈ ↑N), ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N) ⋯<VAR>x✝ : ↥↑N<GOAL>↑((LinearMap.restrict ((toEnd R L M) x) h) x✝) = ↑(((toEnd R L ↥↑N) x) x✝)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<GOAL>∃ n, Nat.Prime p ∧ q = p ^ ↑n
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<GOAL>∃ n, Nat.Prime p ∧ q = p ^ ↑n
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<GOAL>∃ n, Nat.Prime p ∧ q = p ^ ↑n
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<VAR>n : ℕ<VAR>h : q = Fintype.card (ZMod p) ^ n<GOAL>∃ n, Nat.Prime p ∧ q = p ^ ↑n
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<VAR>n : ℕ<VAR>h : q = p ^ n<GOAL>∃ n, Nat.Prime p ∧ q = p ^ ↑n
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<VAR>n : ℕ<VAR>h : q = p ^ n<GOAL>0 < n
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<VAR>n : ℕ<VAR>h : q = p ^ n<GOAL>¬n = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<VAR>h : q = p ^ 0<GOAL>False
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<VAR>h : q = 1<GOAL>False
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>hp : Fact (Nat.Prime p)<VAR>this✝ : Module (ZMod p) K := let __src := (ZMod.castHom ⋯ K).toModule; Module.mk ⋯ ⋯<VAR>h : q = 1<VAR>this : 0 = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>hp : IsPrimitive 0<GOAL>False
<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>f : ↥(Lp E p μ)<VAR>hp : 0 < p<VAR>hf : ‖f‖₊ = 0<GOAL>f = 0
<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>f : ↥(Lp E p μ)<VAR>hp : 0 < p<VAR>hf : eLpNorm (↑↑f) p μ = 0 ∨ eLpNorm (↑↑f) p μ = ⊤<GOAL>f = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ≤ b ⇨ c ↔ b ≤ a ⇨ c
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFiltered D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<GOAL>Nonempty C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFiltered D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>this : Nonempty D<GOAL>Nonempty C
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x y : ℝ<GOAL>↑x < ↑y ↔ x < y
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x y : ℝ<GOAL>re ↑x < re ↑y ∧ im ↑x = im ↑y ↔ x < y
<VAR>m n k : ℕ<GOAL>(fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)
<VAR>K : Type u<VAR>inst✝³ : CommRing K<VAR>inst✝² : IsDomain K<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Algebra R K[X]<VAR>x : R<GOAL>(algebraMap R (RatFunc K)) x = (algebraMap K[X] (RatFunc K)) ((algebraMap R K[X]) x) / (algebraMap K[X] (RatFunc K)) 1
<VAR>K : Type u<VAR>inst✝³ : CommRing K<VAR>inst✝² : IsDomain K<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Algebra R K[X]<VAR>x : R<GOAL>(algebraMap R (RatFunc K)) x = RatFunc.mk ((algebraMap R K[X]) x) 1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t✝ : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s t : Set X<GOAL>frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t✝ : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s t : Set X<GOAL>closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆ closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t✝ : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s t : Set X<GOAL>closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) = closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>s t : Set Ω<VAR>h : (condCount s) t ≠ 0<GOAL>s.Finite
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>s t : Set Ω<VAR>h : (condCount s) t ≠ 0<VAR>hs' : ¬s.Finite<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<VAR>n : ℕ<VAR>H : ∀ (l : List α), l ∈ L → l.length = n<GOAL>(foldr (fun y r => (permutationsAux2 t ts r y id).2) r L).length = n * L.length + r.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<VAR>n : ℕ<VAR>H : ∀ (l : List α), l ∈ L → l.length = n<GOAL>Nat.sum (map length L) = n * L.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List (List α)<VAR>n : ℕ<VAR>l : List α<VAR>L : List (List α)<VAR>ih : (∀ (l : List α), l ∈ L → l.length = n) → Nat.sum (map length L) = n * L.length<VAR>H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n<GOAL>Nat.sum (map length (l :: L)) = n * (l :: L).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List (List α)<VAR>n : ℕ<VAR>l : List α<VAR>L : List (List α)<VAR>ih : (∀ (l : List α), l ∈ L → l.length = n) → Nat.sum (map length L) = n * L.length<VAR>H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n<VAR>sum_map : Nat.sum (map length L) = n * L.length<GOAL>Nat.sum (map length (l :: L)) = n * (l :: L).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List (List α)<VAR>n : ℕ<VAR>l : List α<VAR>L : List (List α)<VAR>ih : (∀ (l : List α), l ∈ L → l.length = n) → Nat.sum (map length L) = n * L.length<VAR>H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n<VAR>sum_map : Nat.sum (map length L) = n * L.length<VAR>length_l : l.length = n<GOAL>Nat.sum (map length (l :: L)) = n * (l :: L).length
<VAR>a b✝ c n : ℕ<VAR>hn : n ≠ 0<VAR>b : ℕ<GOAL>b ∈ range n ↔ b ∈ Icc 0 (n - 1)
<VAR>a b✝ c n : ℕ<VAR>hn : n ≠ 0<VAR>b : ℕ<GOAL>b < n ↔ b ≤ n - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝¹ : s.HaveLebesgueDecomposition μ<VAR>inst✝ : t.HaveLebesgueDecomposition μ<VAR>hst : (s - t).HaveLebesgueDecomposition μ<GOAL>(s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝¹ : s.HaveLebesgueDecomposition μ<VAR>inst✝ : t.HaveLebesgueDecomposition μ<VAR>hst : (s + -t).HaveLebesgueDecomposition μ<GOAL>(s - t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ - t.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝¹ : s.HaveLebesgueDecomposition μ<VAR>inst✝ : t.HaveLebesgueDecomposition μ<VAR>hst : (s + -t).HaveLebesgueDecomposition μ<GOAL>(s + -t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + -t.rnDeriv μ
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>x : ι → ℝ<GOAL>(filter (fun J => x ∈ Box.Icc J) π.boxes).card ≤ 2 ^ Fintype.card ι
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>x : ι → ℝ<GOAL>(filter (fun J => x ∈ Box.Icc J) π.boxes).card ≤ Fintype.card (Set ι)
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>x : ι → ℝ<GOAL>InjOn (fun J => {i | J.lower i = x i}) ↑(filter (fun J => x ∈ Box.Icc J) π.boxes)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a : α<GOAL>{a}.OrdConnected
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>a : α<GOAL>(Icc a a).OrdConnected
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.268852, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.268859, u_2} D<VAR>X✝ Y✝ X Y : C<VAR>c : BinaryCofan X Y<VAR>cofans : (X Y : C) → BinaryCofan X Y<VAR>colimits : (X Y : C) → IsColimit (cofans X Y)<VAR>cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g<VAR>limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)<VAR>h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt), αX ≫ c.inl = (cofans X' Y').inl ≫ f → αY ≫ c.inr = (cofans X' Y').inr ≫ f → IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr<VAR>h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.268852, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.268859, u_2} D<VAR>X✝ Y✝ X Y : C<VAR>c : BinaryCofan X Y<VAR>cofans : (X Y : C) → BinaryCofan X Y<VAR>colimits : (X Y : C) → IsColimit (cofans X Y)<VAR>cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g<VAR>limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)<VAR>h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt), αX ≫ c.inl = (cofans X' Y').inl ≫ f → αY ≫ c.inr = (cofans X' Y').inr ≫ f → IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr<VAR>h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)<GOAL>∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt), αX ≫ c.inl = c'.inl ≫ f → αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>hs : MeasurableSet s<VAR>t : Set G<VAR>ht : MeasurableSet t<GOAL>μ' s * ν' t = ν' s * μ' t
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>hs : MeasurableSet s<VAR>t : Set G<VAR>ht : MeasurableSet t<VAR>h1 : ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (x : G), t.indicator (fun x => 1) x ∂ν'<GOAL>μ' s * ν' t = ν' s * μ' t
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>hs : MeasurableSet s<VAR>t : Set G<VAR>ht : MeasurableSet t<VAR>h1 : ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (x : G), t.indicator (fun x => 1) x ∂ν'<VAR>h2 : μ' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (x : G), t.indicator (fun x => 1) x ∂μ'<GOAL>μ' s * ν' t = ν' s * μ' t
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>hs : MeasurableSet s<VAR>t : Set G<VAR>ht : MeasurableSet t<VAR>h1 : ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ν' t<VAR>h2 : μ' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = μ' t<GOAL>μ' s * ν' t = ν' s * μ' t
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>h : Surjective ⇑f<VAR>K L : Subgroup N<GOAL>comap f K = comap f L → K = L
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>R : Type u_1<VAR>inst✝ : SMul R α<VAR>x : R<VAR>a₀ a₁ : α<GOAL>x • ![a₀, a₁] = ![x • a₀, x • a₁]
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i✝ : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>l : Line α ι<VAR>x : α<VAR>i : ι<VAR>h : l.idxFun i = none<GOAL>(fun x i => (l.idxFun i).getD x) x i = x
<VAR>n k m : ℕ<GOAL>(n * k).dist (m * k) = n.dist m * k
<VAR>ι : Type u_1<VAR>κ✝¹ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>κ✝ : Type u_6<VAR>κ : Type u_7<VAR>s : Finset ι<VAR>t : ι → Set κ<VAR>f : κ → β<VAR>h : (↑s).PairwiseDisjoint t<VAR>x : κ<GOAL>(⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>I✝ J : Box ι<VAR>π : TaggedPrepartition I✝<VAR>inst✝² : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>inst✝¹ : CompleteSpace E<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>hc : ContinuousOn f (Box.Icc I)<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>Integrable I l f μ.toBoxAdditive.toSMul
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>I✝ J : Box ι<VAR>π : TaggedPrepartition I✝<VAR>inst✝² : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>inst✝¹ : CompleteSpace E<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>hc : ContinuousOn f (Box.Icc I)<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>I✝ J : Box ι<VAR>π : TaggedPrepartition I✝<VAR>inst✝² : Fintype ι<VAR>l : IntegrationParams<VAR>f✝ g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>inst✝¹ : CompleteSpace E<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>hc : ContinuousOn f (Box.Icc I)<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>F : ℍ[R,c₁,c₂] →ₐ[R] A<VAR>x✝ : ℍ[R,c₁,c₂]<GOAL>(algebraMap R A) x✝.re + x✝.imI • F { re := 0, imI := 1, imJ := 0, imK := 0 } + x✝.imJ • F { re := 0, imI := 0, imJ := 1, imK := 0 } + x✝.imK • F { re := 0, imI := 0, imJ := 0, imK := 1 } = F x✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>F : ℍ[R,c₁,c₂] →ₐ[R] A<VAR>x✝ : ℍ[R,c₁,c₂]<GOAL>F ((algebraMap R ℍ[R,c₁,c₂]) x✝.re) + x✝.imI • F { re := 0, imI := 1, imJ := 0, imK := 0 } + x✝.imJ • F { re := 0, imI := 0, imJ := 1, imK := 0 } + x✝.imK • F { re := 0, imI := 0, imJ := 0, imK := 1 } = F x✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>F : ℍ[R,c₁,c₂] →ₐ[R] A<VAR>x✝ : ℍ[R,c₁,c₂]<GOAL>F { re := x✝.re + 0 + 0 + 0, imI := 0 + x✝.imI • 1 + 0 + 0, imJ := 0 + 0 + x✝.imJ • 1 + 0, imK := 0 + 0 + 0 + x✝.imK • 1 } = F x✝
<VAR>α✝ : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α✝ × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α✝ → β<VAR>x y : FreeGroup α✝<VAR>α : Type u_1<GOAL>Subgroup.closure (Set.range of) = ⊤
<VAR>α✝ : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α✝ × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α✝ → β<VAR>x y : FreeGroup α✝<VAR>α : Type u_1<GOAL>(MonoidHom.id (FreeGroup α)).range = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a✝ : α<GOAL>a✝ ∈ s.val.toFinset ↔ a✝ ∈ s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C✝ C' C'' C : VariableChange R<GOAL>id.comp C = C
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>closedBall 1 δ / s = cthickening δ s⁻¹
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹¹ : CommSemiring R✝<VAR>inst✝¹⁰ : NonUnitalRing A✝<VAR>inst✝⁹ : Module R✝ A✝<VAR>inst✝⁸ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁷ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Semifield R<VAR>inst✝⁵ : Semifield S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : SpectrumRestricts a f<GOAL>f '' spectrum S a = spectrum R a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : CompactlySupportedContinuousMapClass F α β<VAR>G : Type u_5<VAR>inst✝² : FunLike G α β<VAR>inst✝¹ : ContinuousMapClass G α β<VAR>inst✝ : CompactSpace α<VAR>f : G<GOAL>HasCompactSupport ⇑f
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : ι) → Semiring (A i)<VAR>inst✝⁴ : Algebra R' R<VAR>inst✝³ : (i : ι) → Algebra R (A i)<VAR>inst✝² : (i : ι) → Algebra R' (A i)<VAR>inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)<VAR>r : R'<VAR>i : ι<VAR>inst✝ : DecidableEq ι<GOAL>r • (tprod R) 1 = (tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁷ : CommSemiring R'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : ι) → Semiring (A i)<VAR>inst✝⁴ : Algebra R' R<VAR>inst✝³ : (i : ι) → Algebra R (A i)<VAR>inst✝² : (i : ι) → Algebra R' (A i)<VAR>inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)<VAR>r : R'<VAR>i : ι<VAR>inst✝ : DecidableEq ι<VAR>this : Pi.mulSingle i ((algebraMap R' (A i)) r) = update (fun i => 1) i (r • 1)<GOAL>r • (tprod R) 1 = (tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))
<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>a : E<GOAL>Inseparable a 1 ↔ ‖a‖ = 0
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i✝ : ι<VAR>a✝ : β i✝<VAR>a b : (i : ι) → β i<VAR>h : a < b<VAR>i : ι<VAR>hi : i ∈ {i | a i ≠ b i}<VAR>hl : ∀ x ∈ {i | a i ≠ b i}, ¬x < i<VAR>j : ι<VAR>hj : (fun x x_1 => x < x_1) j i<GOAL>toLex a j = toLex b j
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i✝ : ι<VAR>a✝ : β i✝<VAR>a b : (i : ι) → β i<VAR>h : a < b<VAR>i : ι<VAR>hi : i ∈ {i | a i ≠ b i}<VAR>j : ι<VAR>hj : (fun x x_1 => x < x_1) j i<VAR>hl : toLex a j ≠ toLex b j<GOAL>∃ x ∈ {i | a i ≠ b i}, x < i
<VAR>α✝ : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : AddCommGroup β<VAR>a : FreeAbelianGroup α<VAR>f g : α → β<GOAL>(lift (f + g)) a = (lift f) a + (lift g) a
<VAR>α✝ : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : AddCommGroup β<VAR>a : FreeAbelianGroup α<VAR>f g : α → β<GOAL>(lift (f + g)) 0 = (lift f) 0 + (lift g) 0
<VAR>α✝ : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : AddCommGroup β<VAR>a : FreeAbelianGroup α<VAR>f g : α → β<GOAL>∀ (x : α), (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x)
<VAR>α✝ : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : AddCommGroup β<VAR>a : FreeAbelianGroup α<VAR>f g : α → β<GOAL>∀ (x : α), (lift (f + g)) (of x) = (lift f) (of x) + (lift g) (of x) → (lift (f + g)) (-of x) = (lift f) (-of x) + (lift g) (-of x)
<VAR>α✝ : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : AddCommGroup β<VAR>a : FreeAbelianGroup α<VAR>f g : α → β<GOAL>∀ (x y : FreeAbelianGroup α), (lift (f + g)) x = (lift f) x + (lift g) x → (lift (f + g)) y = (lift f) y + (lift g) y → (lift (f + g)) (x + y) = (lift f) (x + y) + (lift g) (x + y)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddZeroClass G<VAR>inst✝¹ : Add H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<GOAL>f a = f 0 + b
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>hn : ¬G.Adj s t<GOAL>(G.replaceVertex s t).edgeFinset = G.edgeFinset \ G.incidenceFinset t ∪ image (fun x => s(x, t)) (G.neighborFinset s)