ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X ⊕ Y → Z<GOAL>IsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b)
<VAR>h : LSeriesSummable (fun n => ↑(μ n)) 1<GOAL>False
<VAR>h : LSeriesSummable (fun n => ↑(μ n)) 1<GOAL>Summable fun b => -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) b)
<VAR>h : LSeriesSummable (fun n => ↑(μ n)) 1<GOAL>Summable (-fun i => ↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) i))
<VAR>h : LSeriesSummable (fun n => ↑(μ n)) 1<VAR>n : ℕ<GOAL>{n | Nat.Prime n}.indicator (term (fun n => ↑(μ n)) 1) n = (-fun i => ↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) i)) n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β →ₛ F<VAR>hf_int : Integrable (↑f) μ<GOAL>∫ (x : β), ↑f x ∂μ = ∫ (x : β), ↑f x ∂μ.trim hm
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β →ₛ F<VAR>hf_int : Integrable (↑f) μ<VAR>hf : StronglyMeasurable ↑f<GOAL>∫ (x : β), ↑f x ∂μ = ∫ (x : β), ↑f x ∂μ.trim hm
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β →ₛ F<VAR>hf_int : Integrable (↑f) μ<VAR>hf : StronglyMeasurable ↑f<VAR>hf_int_m : Integrable (↑f) (μ.trim hm)<GOAL>∫ (x : β), ↑f x ∂μ = ∫ (x : β), ↑f x ∂μ.trim hm
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β →ₛ F<VAR>hf_int : Integrable (↑f) μ<VAR>hf : StronglyMeasurable ↑f<VAR>hf_int_m : Integrable (↑f) (μ.trim hm)<GOAL>∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • x = ∑ x ∈ f.range, ((μ.trim hm) (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β →ₛ F<VAR>hf_int : Integrable (↑f) μ<VAR>hf : StronglyMeasurable ↑f<VAR>hf_int_m : Integrable (↑f) (μ.trim hm)<VAR>x : F<GOAL>μ (↑f ⁻¹' {x}) = (μ.trim hm) (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l✝ : List α<VAR>f : β → α<VAR>b : β<VAR>l : List β<GOAL>Pairwise R (map f (b :: l)) ↔ Pairwise (fun a b => R (f a) (f b)) (b :: l)
<VAR>r n : ℕ<GOAL>n.choose r ≤ n.choose (n / 2)
<VAR>r n : ℕ<VAR>b : r ≤ n<GOAL>n.choose r ≤ n.choose (n / 2)
<VAR>r n : ℕ<VAR>b : r > n<GOAL>n.choose r ≤ n.choose (n / 2)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t✝ s t : Set α<GOAL>(s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁵ : Category.{v'', u''} D<VAR>F : C ⥤ D<VAR>inst✝⁴ : Adhesive D<VAR>H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g<VAR>H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>inst✝³ : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape WalkingSpan F<VAR>inst✝ : ReflectsColimitsOfShape WalkingSpan F<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hf : Mono f<VAR>H : IsPushout f g h i<GOAL>H.IsVanKampen
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁵ : Category.{v'', u''} D<VAR>F : C ⥤ D<VAR>inst✝⁴ : Adhesive D<VAR>H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g<VAR>H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>inst✝³ : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape WalkingSpan F<VAR>inst✝ : ReflectsColimitsOfShape WalkingSpan F<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hf : Mono f<VAR>H : IsPushout f g h i<GOAL>IsVanKampenColimit (PushoutCocone.mk h i ⋯)
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁵ : Category.{v'', u''} D<VAR>F : C ⥤ D<VAR>inst✝⁴ : Adhesive D<VAR>H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g<VAR>H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>inst✝³ : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape WalkingSpan F<VAR>inst✝ : ReflectsColimitsOfShape WalkingSpan F<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hf : Mono f<VAR>H : IsPushout f g h i<GOAL>IsVanKampenColimit (F.mapCocone (PushoutCocone.mk h i ⋯))
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁵ : Category.{v'', u''} D<VAR>F : C ⥤ D<VAR>inst✝⁴ : Adhesive D<VAR>H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g<VAR>H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>inst✝³ : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape WalkingSpan F<VAR>inst✝ : ReflectsColimitsOfShape WalkingSpan F<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hf : Mono f<VAR>H : IsPushout f g h i<GOAL>IsVanKampenColimit ((Cocones.precompose (diagramIsoSpan (span f g ⋙ F)).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯)))
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁵ : Category.{v'', u''} D<VAR>F : C ⥤ D<VAR>inst✝⁴ : Adhesive D<VAR>H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g<VAR>H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>inst✝³ : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape WalkingSpan F<VAR>inst✝ : ReflectsColimitsOfShape WalkingSpan F<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hf : Mono f<VAR>H : IsPushout f g h i<GOAL>IsVanKampenColimit (PushoutCocone.mk ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.left) ((F.mapCocone (PushoutCocone.mk h i ⋯)).ι.app WalkingSpan.right) ⋯)
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁵ : Category.{v'', u''} D<VAR>F : C ⥤ D<VAR>inst✝⁴ : Adhesive D<VAR>H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Mono f], HasPullback f g<VAR>H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>inst✝³ : PreservesLimitsOfShape WalkingCospan F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape WalkingSpan F<VAR>inst✝ : ReflectsColimitsOfShape WalkingSpan F<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hf : Mono f<VAR>H : IsPushout f g h i<GOAL>⋯.IsVanKampen
<VAR>n✝ : ℕ<VAR>c : Composition n✝<VAR>n i : ℕ<GOAL>(ones n).sizeUpTo i = min i n
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : Countable E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasurableSet {x | f x = g x}
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : Countable E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}<GOAL>MeasurableSet {x | f x = g x}
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : Countable E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}<GOAL>MeasurableSet (⋃ j, {x | f x = j} ∩ {x | g x = j})
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : Countable E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}<VAR>j : E<GOAL>MeasurableSet {x | f x = j}
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : Countable E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>this : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j}<VAR>j : E<GOAL>MeasurableSet {x | g x = j}
<VAR>R : Type uR<VAR>S : Type uS<VAR>A✝ : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : Semiring A✝<VAR>inst✝⁹ : Algebra R A✝<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>b✝ : Basis ι R M<VAR>inst✝⁶ : Fintype ι<VAR>ι' : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : DecidableEq ι'<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>b : Basis ι R M<VAR>b' : Basis ι' R N<VAR>ij : ι × ι'<GOAL>baseChange A ((b'.linearMap b) ij) = ((basis A b').linearMap (basis A b)) ij
<VAR>R : Type uR<VAR>S : Type uS<VAR>A✝ : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : Semiring A✝<VAR>inst✝⁹ : Algebra R A✝<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>b✝ : Basis ι R M<VAR>inst✝⁶ : Fintype ι<VAR>ι' : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : DecidableEq ι'<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>b : Basis ι R M<VAR>b' : Basis ι' R N<VAR>ij : ι × ι'<GOAL>∀ (i : ι'), (baseChange A ((b'.linearMap b) ij)) ((basis A b') i) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') i)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A✝ : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : Semiring A✝<VAR>inst✝⁹ : Algebra R A✝<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>b✝ : Basis ι R M<VAR>inst✝⁶ : Fintype ι<VAR>ι' : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : DecidableEq ι'<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>b : Basis ι R M<VAR>b' : Basis ι' R N<VAR>ij : ι × ι'<VAR>k : ι'<GOAL>(baseChange A ((b'.linearMap b) ij)) ((basis A b') k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A✝ : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : Semiring A✝<VAR>inst✝⁹ : Algebra R A✝<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>b✝ : Basis ι R M<VAR>inst✝⁶ : Fintype ι<VAR>ι' : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : DecidableEq ι'<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>b : Basis ι R M<VAR>b' : Basis ι' R N<VAR>ij : ι × ι'<VAR>k : ι'<GOAL>1 ⊗ₜ[R] ((b'.linearMap b) ij) (b' k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A✝ : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : Semiring A✝<VAR>inst✝⁹ : Algebra R A✝<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>b✝ : Basis ι R M<VAR>inst✝⁶ : Fintype ι<VAR>ι' : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : DecidableEq ι'<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>b : Basis ι R M<VAR>b' : Basis ι' R N<VAR>ij : ι × ι'<VAR>k : ι'<GOAL>(1 ⊗ₜ[R] if ij.2 = k then b ij.1 else 0) = if ij.2 = k then 1 ⊗ₜ[R] b ij.1 else 0
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : (pos a * b).natSize ≤ n.succ<GOAL>↑(gcdAux n.succ (pos a) b) = (↑(pos a)).gcd ↑b
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : (pos a * b).natSize ≤ n.succ<GOAL>↑(gcdAux n (b % pos a) (pos a)) = (↑a).gcd ↑b
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : (pos a * b).natSize ≤ n.succ<GOAL>(↑b % ↑(pos a)).gcd ↑(pos a) = (↑b % ↑a).gcd ↑a
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : (pos a * b).natSize ≤ n.succ<GOAL>b % pos a ≤ pos a
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : (pos a * b).natSize ≤ n.succ<GOAL>(b % pos a * pos a).natSize ≤ n
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * ↑b < 2 ^ n.succ<GOAL>↑(b % pos a) * ↑(pos a) < 2 ^ n
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * ↑b < 2 ^ n.succ<GOAL>↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2<GOAL>↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2<GOAL>↑(pos a) * (↑b % ↑(pos a)) * 2 ≤ ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a)))
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2<GOAL>↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑b % ↑(pos a)) ≤ ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑(pos a) * (↑b / ↑(pos a)))
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2<GOAL>↑a ≤ ↑(pos a) * (↑b / ↑(pos a))
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2<GOAL>1 ≤ ↑b / ↑a
<VAR>n : ℕ<VAR>a : PosNum<VAR>b : Num<VAR>ab : pos a ≤ b<VAR>h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2<GOAL>↑a ≤ ↑b
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<GOAL>CotangentSpace.map (Hom.id P) = LinearMap.id
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<GOAL>∀ (i : P.vars), (CotangentSpace.map (Hom.id P)) (P.cotangentSpaceBasis i) = LinearMap.id (P.cotangentSpaceBasis i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>i : P.vars<GOAL>(CotangentSpace.map (Hom.id P)) (P.cotangentSpaceBasis i) = LinearMap.id (P.cotangentSpaceBasis i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>i : P.vars<GOAL>1 ⊗ₜ[P.Ring] (D R P.Ring) ((Hom.id P).val i) = LinearMap.id (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i))
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>s : Set α<VAR>M : Type w'<VAR>inst✝² : Nonempty M<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : M ⊨ T<VAR>h : lift.{w', w} #↑s ≤ lift.{w, w'} #M<VAR>this : Inhabited M<GOAL>((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>s : Set α<VAR>M : Type w'<VAR>inst✝² : Nonempty M<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : M ⊨ T<VAR>h : Nonempty (↑s ↪ M)<VAR>this : Inhabited M<GOAL>((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>s : Set α<VAR>M : Type w'<VAR>inst✝² : Nonempty M<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : M ⊨ T<VAR>h : Nonempty (↑s ↪ M)<VAR>this✝ : Inhabited M<VAR>this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)<GOAL>((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' T : L.Theory<VAR>s : Set α<VAR>M : Type w'<VAR>inst✝² : Nonempty M<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : M ⊨ T<VAR>h : Nonempty (↑s ↪ M)<VAR>this✝¹ : Inhabited M<VAR>this✝ : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)<VAR>this : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s<GOAL>((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : NullMeasurableSet s μ<GOAL>∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>x : α<VAR>hfx : f x = x<VAR>n : ℕ<GOAL>(f ^ (n + 1)) x = x
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>L : x.LeftMoves ≃ y.LeftMoves<VAR>R : x.RightMoves ≃ y.RightMoves<VAR>hl : ∀ (i : x.LeftMoves), x.moveLeft i ≈ y.moveLeft (L i)<VAR>hr : ∀ (j : x.RightMoves), x.moveRight j ≈ y.moveRight (R j)<GOAL>x ≈ y