ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 : E<GOAL>‖u‖ = ‖u * v / v‖
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<GOAL>typesGlue S hs α (eval S α s) = s
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<GOAL>∀ ⦃Y : Type u⦄ ⦃f : Y ⟶ α⦄, discretePresieve α f → S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<VAR>β : Type u<VAR>f : β ⟶ α<VAR>hf : discretePresieve α f<GOAL>S.map f.op (typesGlue S hs α (eval S α s)) = S.map f.op s
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<VAR>β : Type u<VAR>f : β ⟶ α<VAR>hf : discretePresieve α f<GOAL>S.map (↾fun x => PUnit.unit).op (eval S α s (f (Classical.choose hf))) = S.map f.op s
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<VAR>β : Type u<VAR>f : β ⟶ α<VAR>hf : discretePresieve α f<GOAL>S.map ((↾fun x => f (Classical.choose hf)).op ≫ (↾fun x => PUnit.unit).op) s = S.map f.op s
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<VAR>β : Type u<VAR>f : β ⟶ α<VAR>hf : discretePresieve α f<GOAL>S.map ((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)).op s = S.map f.op s
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<VAR>β : Type u<VAR>f : β ⟶ α<VAR>hf : discretePresieve α f<GOAL>((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) = f
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>s : S.obj (op α)<VAR>β : Type u<VAR>f : β ⟶ α<VAR>hf : discretePresieve α f<VAR>x : β<GOAL>((↾fun x => PUnit.unit) ≫ ↾fun x => f (Classical.choose hf)) x = f x
<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✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<GOAL>0 < measureUnivNNReal μ
<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✝ : IsFiniteMeasure μ<VAR>hμ : measureUnivNNReal μ ≤ 0<GOAL>μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Injective f<VAR>inst✝ : DecidablePred fun x => x ∈ range f<VAR>g : α → M<GOAL>(∏ᶠ (b : β), if h : b ∈ range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Injective f<VAR>inst✝ : DecidablePred fun x => x ∈ range f<VAR>g : α → M<GOAL>∏ᶠ (b : β) (h : b ∈ range f), g (Classical.choose h) = ∏ᶠ (a : α), g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Injective f<VAR>inst✝ : DecidablePred fun x => x ∈ range f<VAR>g : α → M<GOAL>∀ (a : α), (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a✝ b : α<VAR>s t : Set α<VAR>f : α → β<VAR>hf : Injective f<VAR>inst✝ : DecidablePred fun x => x ∈ range f<VAR>g : α → M<VAR>a : α<GOAL>(if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>Measure.map (fun x => x * a) volume = ofReal |a⁻¹| • volume
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>(∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝¹ t✝ : Set α<VAR>a b x : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s : Set α<VAR>t : Set β<GOAL>Subtype.val '' minimals (fun x x_1 => x ≤ x_1) univ = minimals (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝¹ t✝ : Set α<VAR>a b x : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s : Set α<VAR>t : Set β<GOAL>∀ ⦃a a' : { x // x ∈ s }⦄, a ∈ univ → a' ∈ univ → (a ≤ a' ↔ ↑a ≤ ↑a')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝¹ t✝ : Set α<VAR>a b x : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s : Set α<VAR>t : Set β<VAR>a✝² a'✝ : { x // x ∈ s }<VAR>a✝¹ : a✝² ∈ univ<VAR>a✝ : a'✝ ∈ univ<GOAL>a✝² ≤ a'✝ ↔ ↑a✝² ≤ ↑a'✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set (Set α)<GOAL>⋂₀ s = ⋂ i ∈ s, i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>h : {x | eval x p = eval x q}.Infinite<GOAL>p = q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>h : {x | eval x p = eval x q}.Infinite<GOAL>p - q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>h : {x | eval x p = eval x q}.Infinite<GOAL>{x | (p - q).IsRoot x}.Infinite
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<GOAL>Nonempty (Transversal φ)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>t : (i : ι) → Set (G i)<VAR>ht : ∀ (i : ι), t i ∈ rightTransversals ↑(φ i).range ∧ 1 ∈ t i<GOAL>Nonempty (Transversal φ)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>t : (i : ι) → Set (G i)<VAR>ht : ∀ (i : ι), t i ∈ rightTransversals ↑(φ i).range ∧ 1 ∈ t i<GOAL>Transversal φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b : α<VAR>s t : Finset α<VAR>a : α<GOAL>insert a (s ∩ t) = insert a s ∩ insert a t
<VAR>A✝ : Type u_1<VAR>inst✝⁷ : NormedRing A✝<VAR>inst✝⁶ : StarRing A✝<VAR>inst✝⁵ : CstarRing A✝<VAR>inst✝⁴ : CompleteSpace A✝<VAR>inst✝³ : NormedAlgebra ℂ A✝<VAR>inst✝² : StarModule ℂ A✝<VAR>A : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>a : A<VAR>ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>SpectrumRestricts (r • a) ⇑ContinuousMap.realToNNReal
<VAR>A✝ : Type u_1<VAR>inst✝⁷ : NormedRing A✝<VAR>inst✝⁶ : StarRing A✝<VAR>inst✝⁵ : CstarRing A✝<VAR>inst✝⁴ : CompleteSpace A✝<VAR>inst✝³ : NormedAlgebra ℂ A✝<VAR>inst✝² : StarModule ℂ A✝<VAR>A : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>a : A<VAR>ha : ∀ x ∈ σ ℝ a, 0 ≤ x<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>∀ x ∈ σ ℝ (r • a), 0 ≤ x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : FractionalIdeal S P<VAR>C : P → Prop<VAR>r : P<VAR>hr : r ∈ I * J<VAR>hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)<VAR>ha : ∀ (x y : P), C x → C y → C (x + y)<GOAL>C r
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : FractionalIdeal S P<VAR>C : P → Prop<VAR>r : P<VAR>hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)<VAR>ha : ∀ (x y : P), C x → C y → C (x + y)<VAR>hr : r ∈ ⟨↑I * ↑J, ⋯⟩<GOAL>C r
<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>x y : P<GOAL>Wbtw R x (midpoint R x y) y
<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>x y : P<GOAL>y = (pointReflection R (midpoint R x y)) x
<VAR>V : Type v<VAR>inst✝² : Category.{w, v} V<VAR>inst✝¹ : MonoidalCategory V<VAR>C✝ : Type u₁<VAR>inst✝ : EnrichedCategory V C✝<VAR>C : Type u₁<VAR>𝒞 : EnrichedCategory (Type v) C<VAR>D : Type u₂<VAR>𝒟 : EnrichedCategory (Type v) D<VAR>F : C ⥤ D<VAR>X : C<GOAL>(eId (Type v) X ≫ (fun X Y f => F.map f) X X) PUnit.unit = eId (Type v) ((fun X => F.obj X) X) PUnit.unit
<VAR>V : Type v<VAR>inst✝² : Category.{w, v} V<VAR>inst✝¹ : MonoidalCategory V<VAR>C✝ : Type u₁<VAR>inst✝ : EnrichedCategory V C✝<VAR>C : Type u₁<VAR>𝒞 : EnrichedCategory (Type v) C<VAR>D : Type u₂<VAR>𝒟 : EnrichedCategory (Type v) D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : EnrichedCategory.Hom X Y<VAR>g : EnrichedCategory.Hom Y Z<GOAL>(eComp (Type v) X Y Z ≫ (fun X Y f => F.map f) X Z) (f, g) = (((fun X Y f => F.map f) X Y ⊗ (fun X Y f => F.map f) Y Z) ≫ eComp (Type v) ((fun X => F.obj X) X) ((fun X => F.obj X) Y) ((fun X => F.obj X) Z)) (f, g)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>f : Derivation R A ↥I<GOAL>↑(f 1) + (algebraMap A B) 1 = 1
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>f : Derivation R A ↥I<VAR>x y : A<GOAL>{ toFun := fun x => ↑(f x) + (algebraMap A B) x, map_one' := ⋯ }.toFun (x * y) = { toFun := fun x => ↑(f x) + (algebraMap A B) x, map_one' := ⋯ }.toFun x * { toFun := fun x => ↑(f x) + (algebraMap A B) x, map_one' := ⋯ }.toFun y
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>f : Derivation R A ↥I<VAR>x y : A<VAR>this : ↑(f x) * ↑(f y) = 0<GOAL>{ toFun := fun x => ↑(f x) + (algebraMap A B) x, map_one' := ⋯ }.toFun (x * y) = { toFun := fun x => ↑(f x) + (algebraMap A B) x, map_one' := ⋯ }.toFun x * { toFun := fun x => ↑(f x) + (algebraMap A B) x, map_one' := ⋯ }.toFun y
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>f : Derivation R A ↥I<VAR>x y : A<VAR>this : ↑(f x) * ↑(f y) = 0<GOAL>(algebraMap A B) x * ↑(f y) + (algebraMap A B) y * ↑(f x) + (algebraMap A B) x * (algebraMap A B) y = 0 + (algebraMap A B) x * ↑(f y) + (↑(f x) * (algebraMap A B) y + (algebraMap A B) x * (algebraMap A B) y)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>f : Derivation R A ↥I<VAR>r : R<GOAL>(↑↑{ toFun := fun x => ↑(f x) + (algebraMap A B) x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap R A) r) = (algebraMap R B) r
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : CommRing k<VAR>inst✝² : Module k V<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b b₂ : AffineBasis ι k P<VAR>x : P<GOAL>b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : CommRing k<VAR>inst✝² : Module k V<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b b₂ : AffineBasis ι k P<VAR>x : P<VAR>hu : IsUnit (b.toMatrix ⇑b₂)<GOAL>b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : AffineSpace V P<VAR>inst✝³ : CommRing k<VAR>inst✝² : Module k V<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b b₂ : AffineBasis ι k P<VAR>x : P<VAR>hu : IsUnit (b.toMatrix ⇑b₂).det<GOAL>b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<VAR>i : ι<GOAL>(mk s (x + y)) i = (mk s x + mk s y) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<VAR>i : ι<GOAL>(if H : i ∈ s then (x + y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) + if H : i ∈ s then y ⟨i, H⟩ else 0
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝² : NormedLinearOrderedField K<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace K E<VAR>b : Basis ι K E<GOAL>span K ↑(span ℤ (Set.range ⇑b)) = ⊤
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<VAR>m₁ : M i<VAR>m₂ : M j<VAR>w : Word M<GOAL>⟨i, m₁⟩ ∈ (of m₂ • w).toList ↔ ⟨i, m₁⟩ ∈ w.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>u : αˣ<VAR>h : a * b * ↑u = 1<GOAL>a * (b * ↑u) = 1
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set (α × β)<VAR>p : α × β<GOAL>IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set (α × β)<VAR>p : α × β<VAR>H : IsLUB s p<VAR>a : α<VAR>ha : a ∈ upperBounds (Prod.fst '' s)<GOAL>p.1 ≤ a
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set (α × β)<VAR>p : α × β<VAR>H : IsLUB s p<VAR>a : β<VAR>ha : a ∈ upperBounds (Prod.snd '' s)<GOAL>p.2 ≤ a
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set (α × β)<VAR>p : α × β<VAR>H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2<GOAL>p ∈ upperBounds s
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set (α × β)<VAR>p : α × β<VAR>H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2<GOAL>p ∈ lowerBounds (upperBounds s)
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b r r' s t s' t' : R<VAR>p : EuclideanDomain.P a b (r, s, t)<VAR>p' : EuclideanDomain.P a b (r', s', t')<GOAL>EuclideanDomain.P a b (xgcdAux r s t r' s' t')
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ico a b, g' x ≤ φ x<GOAL>g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ico a b, g' x ≤ φ x<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ico a b, g' x ≤ φ x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>G' : ℝ → EReal<VAR>f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x<VAR>G'cont : LowerSemicontinuous G'<VAR>G'int : Integrable (fun x => (G' x).toReal) (volume.restrict (Icc a b))<VAR>G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤<VAR>hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal ∂volume < ∫ (x : ℝ) in Icc a b, φ x ∂volume + ε<GOAL>g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ico a b, g' x ≤ φ x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>G' : ℝ → EReal<VAR>f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x<VAR>G'cont : LowerSemicontinuous G'<VAR>G'int : Integrable (fun x => (G' x).toReal) (volume.restrict (Icc a b))<VAR>G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤<VAR>hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal ∂volume < ∫ (x : ℝ) in Icc a b, φ x ∂volume + ε<VAR>s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b<GOAL>g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ico a b, g' x ≤ φ x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>G' : ℝ → EReal<VAR>f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x<VAR>G'cont : LowerSemicontinuous G'<VAR>G'int : Integrable (fun x => (G' x).toReal) (volume.restrict (Icc a b))<VAR>G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤<VAR>hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal ∂volume < ∫ (x : ℝ) in Icc a b, φ x ∂volume + ε<VAR>s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b<VAR>s_closed : IsClosed s<GOAL>g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>this : Tendsto (fun r => μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>this : Tendsto (fun r => μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>r : ℝ<GOAL>μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t) = μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>this : Tendsto (fun r => μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>r : ℝ<GOAL>μ (toMeasurable μ s ∩ ({x} + r • t)) = μ (s ∩ ({x} + r • t))
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>this : Tendsto (fun r => μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>r : ℝ<GOAL>MeasurableSet ({x} + r • t)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h't : μ t ≠ 0<VAR>h''t : μ t ≠ ⊤<VAR>this : Tendsto (fun r => μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1)<VAR>r : ℝ<GOAL>MeasurableSet ((fun x_1 => -x + x_1) ⁻¹' (r • t))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<GOAL>TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) atTop s