ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧ HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>(∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x))) ∧ HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) (κ a) ↔ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧ HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>(∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x))) ↔ ∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) (κ a) ↔ HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<VAR>s : Set α<VAR>hm : m.Nonempty<GOAL>(restrict s) (sInf m) = sInf (⇑(restrict s) '' m)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : DivisionSemiring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module Rᵐᵒᵖ M<VAR>inst✝¹ : Module R M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x⁻¹⁻¹ = 1 * x⁻¹⁻¹
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : DivisionSemiring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module Rᵐᵒᵖ M<VAR>inst✝¹ : Module R M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>1 * x⁻¹⁻¹ = x * x⁻¹ * x⁻¹⁻¹
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : DivisionSemiring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module Rᵐᵒᵖ M<VAR>inst✝¹ : Module R M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x * x⁻¹ * x⁻¹⁻¹ = x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : DivisionSemiring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module Rᵐᵒᵖ M<VAR>inst✝¹ : Module R M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x⁻¹.fst ≠ 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : DivisionSemiring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module Rᵐᵒᵖ M<VAR>inst✝¹ : Module R M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x.fst⁻¹ ≠ 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<VAR>hg : AnalyticAt 𝕜 g z₀<GOAL>(∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ g z
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<GOAL>ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>ℵ₀ < univ.{u, v}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{max (u + 1) v}<VAR>h : c < univ.{u, v}<GOAL>2 ^ c < univ.{u, v}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h : lift.{max (u + 1) v, u} c < univ.{u, v}<GOAL>2 ^ lift.{max (u + 1) v, u} c < univ.{u, v}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h : lift.{max (u + 1) v, u} c < univ.{u, v}<GOAL>lift.{max (u + 1) v, u} (2 ^ c) < univ.{u, v}
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasInjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<GOAL>(injectiveResolutions C).map f ≫ J.iso.hom = I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasInjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<GOAL>Homotopy (desc f (injectiveResolution Y) (injectiveResolution X) ≫ ((injectiveResolution Y).homotopyEquiv J).hom) (((injectiveResolution X).homotopyEquiv I).hom ≫ φ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0<VAR>hf : AEStronglyMeasurable f (μ.restrict t)<GOAL>∫ (x : X) in t, f x ∂μ = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0<VAR>hf : AEStronglyMeasurable f (μ.restrict t)<VAR>this : ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0<GOAL>∫ (x : X) in t, f x ∂μ = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0<VAR>hf : AEStronglyMeasurable f (μ.restrict t)<VAR>this : ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Free R M'<VAR>inst✝ : Module.Free R M₁<GOAL>Module.rank R (M × M') = lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M')
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : IsTerminal X<VAR>f : X ⟶ Y<GOAL>Mono f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>t : IsTerminal X<VAR>f : X ⟶ Y<VAR>this : IsSplitMono f<GOAL>Mono f
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>a₁✝ a₂✝ : M ≃[L] N<VAR>h : a₁✝.toEmbedding = a₂✝.toEmbedding<GOAL>a₁✝ = a₂✝
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>a₁✝ a₂✝ : M ≃[L] N<VAR>h : a₁✝.toEmbedding = a₂✝.toEmbedding<GOAL>(fun f => ⇑f) a₁✝ = (fun f => ⇑f) a₂✝
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesColimit F G<VAR>inst✝³ : HasColimit F<VAR>inst✝² : PreservesColimitsOfShape J G<VAR>inst✝¹ : HasColimitsOfShape J D<VAR>inst✝ : HasColimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<GOAL>(colim ⋙ G).map f ≫ ((fun F => preservesColimitIso G F) Y✝).hom = ((fun F => preservesColimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ colim).map f
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesColimit F G<VAR>inst✝³ : HasColimit F<VAR>inst✝² : PreservesColimitsOfShape J G<VAR>inst✝¹ : HasColimitsOfShape J D<VAR>inst✝ : HasColimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<GOAL>((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f = ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesColimit F G<VAR>inst✝³ : HasColimit F<VAR>inst✝² : PreservesColimitsOfShape J G<VAR>inst✝¹ : HasColimitsOfShape J D<VAR>inst✝ : HasColimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<GOAL>∀ (j : J), colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫ ((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f = colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫ ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesColimit F G<VAR>inst✝³ : HasColimit F<VAR>inst✝² : PreservesColimitsOfShape J G<VAR>inst✝¹ : HasColimitsOfShape J D<VAR>inst✝ : HasColimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) = (whiskerRight f G).app j ≫ colimit.ι (Y✝ ⋙ G) j ≫ (preservesColimitIso G Y✝).inv
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesColimit F G<VAR>inst✝³ : HasColimit F<VAR>inst✝² : PreservesColimitsOfShape J G<VAR>inst✝¹ : HasColimitsOfShape J D<VAR>inst✝ : HasColimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>G.map (colimit.ι X✝ j ≫ colimMap f) = G.map (f.app j ≫ colimit.ι Y✝ j)
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S T : Subsemigroup M<GOAL>∀ {x : M}, x ∈ T → x ∈ S ⊔ T
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S T : Subsemigroup M<VAR>this : T ≤ S ⊔ T<GOAL>∀ {x : M}, x ∈ T → x ∈ S ⊔ T
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<GOAL>(fun N => ↑(rothNumberNat N)) =o[atTop] fun N => ↑N
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<GOAL>∀ ⦃c : ℝ⦄, 0 < c → ∃ a, ∀ b ≥ a, ↑(rothNumberNat b) ≤ c * ↑b
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n✝ : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : n ≥ cornersTheoremBound (ε / 3)<GOAL>↑(rothNumberNat n) ≤ ε * ↑n
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n✝ : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : n ≥ cornersTheoremBound (ε / 3)<VAR>A : Finset ℕ<VAR>hs₁ : A ⊆ range n<VAR>hs₂ : A.card = rothNumberNat n<VAR>hs₃ : ThreeAPFree ↑A<GOAL>↑(rothNumberNat n) ≤ ε * ↑n
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n✝ : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : n ≥ cornersTheoremBound (ε / 3)<VAR>A : Finset ℕ<VAR>hs₁ : A ⊆ range n<VAR>hs₂ : A.card = rothNumberNat n<VAR>hs₃ : ThreeAPFree ↑A<GOAL>¬ε * ↑n < ↑A.card
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Γ : Type u_4<VAR>inst✝⁶ : Group Γ<VAR>T : Type u_5<VAR>inst✝⁵ : TopologicalSpace T<VAR>inst✝⁴ : MulAction Γ T<VAR>G₀ : Type u_6<VAR>inst✝³ : GroupWithZero G₀<VAR>inst✝² : MulAction G₀ α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>s : Set α<VAR>x : α<VAR>hs : s ∈ 𝓝 x<VAR>hc : c ≠ 0<GOAL>c • s ∈ 𝓝 (c • x)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Γ : Type u_4<VAR>inst✝⁶ : Group Γ<VAR>T : Type u_5<VAR>inst✝⁵ : TopologicalSpace T<VAR>inst✝⁴ : MulAction Γ T<VAR>G₀ : Type u_6<VAR>inst✝³ : GroupWithZero G₀<VAR>inst✝² : MulAction G₀ α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>s : Set α<VAR>x : α<VAR>hs : ∃ t ⊆ s, IsOpen t ∧ x ∈ t<VAR>hc : c ≠ 0<GOAL>∃ t ⊆ c • s, IsOpen t ∧ c • x ∈ t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Γ : Type u_4<VAR>inst✝⁶ : Group Γ<VAR>T : Type u_5<VAR>inst✝⁵ : TopologicalSpace T<VAR>inst✝⁴ : MulAction Γ T<VAR>G₀ : Type u_6<VAR>inst✝³ : GroupWithZero G₀<VAR>inst✝² : MulAction G₀ α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : ContinuousConstSMul G₀ α<VAR>c : G₀<VAR>s : Set α<VAR>x : α<VAR>hc : c ≠ 0<VAR>U : Set α<VAR>hs' : U ⊆ s<VAR>hU : IsOpen U<VAR>hU' : x ∈ U<GOAL>∃ t ⊆ c • s, IsOpen t ∧ c • x ∈ t
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>fγ : (a : α) × (β a → γ) → γ<VAR>fγ_injective : Function.Injective fγ<VAR>a₁ : α<VAR>f₁ : β a₁ → WType β<VAR>a₂ : α<VAR>f₂ : β a₂ → WType β<VAR>h : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₂ f₂)<GOAL>mk a₁ f₁ = mk a₂ f₂
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>fγ : (a : α) × (β a → γ) → γ<VAR>fγ_injective : Function.Injective fγ<VAR>a₁ : α<VAR>f₁ f₂ : β a₁ → WType β<VAR>h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)<VAR>h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)<GOAL>mk a₁ f₁ = mk a₁ f₂
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>fγ : (a : α) × (β a → γ) → γ<VAR>fγ_injective : Function.Injective fγ<VAR>a₁ : α<VAR>f₁ f₂ : β a₁ → WType β<VAR>h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)<VAR>h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)<VAR>x : β a₁<GOAL>f₁ x = f₂ x
<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<GOAL>qrSign m n = qrSign n m
<VAR>α : Type u<VAR>inst✝ : Nonempty α<GOAL>#(List α) = max #α ℵ₀
<VAR>α : Type u<VAR>inst✝ : Nonempty α<VAR>h✝ : Finite α<GOAL>#(List α) = max #α ℵ₀
<VAR>α : Type u<VAR>inst✝ : Nonempty α<VAR>h✝ : Infinite α<GOAL>#(List α) = max #α ℵ₀
<VAR>f : Bool → Bool → Bool<VAR>x y n : ℕ<VAR>hx : x < 2 ^ n<VAR>hy : y < 2 ^ n<GOAL>bitwise f x y < 2 ^ n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n : ℕ<VAR>S✝ : ComposableArrows C n<VAR>S : ComposableArrows C (n + 2)<VAR>hS : S.Exact<GOAL>S.δlast.Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n : ℕ<VAR>S✝ : ComposableArrows C n<VAR>S : ComposableArrows C (n + 2)<VAR>hS : S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact<GOAL>S.δlast.Exact
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>I : Set ι<VAR>hI : I.Countable<VAR>f : ι → Set X<VAR>hf : ∀ i ∈ I, IsOpen (f i)<GOAL>∀ t ∈ f '' I, IsOpen t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝ : TopologicalSpace X<VAR>I : Set ι<VAR>hI : I.Countable<VAR>f : ι → Set X<VAR>hf : ∀ i ∈ I, IsOpen (f i)<GOAL>⋂ i ∈ I, f i = ⋂₀ (f '' I)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<GOAL>baseChange A (span R s) = span A (⇑((TensorProduct.mk R A M) 1) '' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<GOAL>span A (⇑((TensorProduct.mk R A M) 1) '' ↑(span R s)) = span A (⇑((TensorProduct.mk R A M) 1) '' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<GOAL>⇑((TensorProduct.mk R A M) 1) '' ↑(span R s) ⊆ ↑(span A (⇑((TensorProduct.mk R A M) 1) '' s))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ span R s<GOAL>((TensorProduct.mk R A M) 1) m ∈ ↑(span A (⇑((TensorProduct.mk R A M) 1) '' s))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ span R s<GOAL>∀ x ∈ s, 1 ⊗ₜ[R] x ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ span R s<GOAL>1 ⊗ₜ[R] 0 ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ span R s<GOAL>∀ (x y : M), 1 ⊗ₜ[R] x ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s) → 1 ⊗ₜ[R] y ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s) → 1 ⊗ₜ[R] (x + y) ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>p : Submodule R M<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ span R s<GOAL>∀ (a : R) (x : M), 1 ⊗ₜ[R] x ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s) → 1 ⊗ₜ[R] (a • x) ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
<GOAL>-π < π / 2 ∧ π / 2 ≤ π
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : Fintype ↑G.edgeSet<VAR>hG : G.IsTree<GOAL>G.edgeFinset.card + 1 = Fintype.card V
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : Fintype ↑G.edgeSet<VAR>hG : G.IsTree<VAR>this : Nonempty V<GOAL>G.edgeFinset.card + 1 = Fintype.card V
<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>ι : Type u_11<VAR>t : Set ι<VAR>s : ι → Set β<VAR>w : ⋃ i ∈ t, s i = ⊤<VAR>x : β<GOAL>∃ i ∈ t, x ∈ s i
<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>ι : Type u_11<VAR>t : Set ι<VAR>s : ι → Set β<VAR>w : ⋃ i ∈ t, s i = ⊤<VAR>x : β<VAR>p : x ∈ ⊤<GOAL>∃ i ∈ t, x ∈ s i
<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>ι : Type u_11<VAR>t : Set ι<VAR>s : ι → Set β<VAR>w : ⋃ i ∈ t, s i = ⊤<VAR>x : β<VAR>p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i<GOAL>∃ i ∈ t, x ∈ s i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s✝ s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>g : γ → β<VAR>s : Finset γ<GOAL>(image g s).gcd f = s.gcd (f ∘ g)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>s t : Set α<VAR>a b : α<GOAL>∀ (x : Set α), InfClosed ((fun s => {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ s ∧ t.inf' ht id = a}) x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>s t✝ : Set α<VAR>a b : α<VAR>s₁ s₂ : Set α<VAR>hs : s₁ ≤ s₂<VAR>h₂ : InfClosed s₂<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>hts : ↑t ⊆ s₁<GOAL>t.inf' ht id ∈ s₂
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>E : EllipticCurve R<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>j : F<VAR>inst✝ : DecidableEq F<VAR>h0 : j ≠ 0<VAR>h1728 : j ≠ 1728<GOAL>ofJ j = ofJ' j
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>h : IsProperMap f<GOAL>IsClosedMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>h : IsProperMap f<GOAL>∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>F : Type u_2<VAR>E : Type u_3<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<GOAL>Module.rank F ↥⊤ = Module.rank F ↥⊤
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>F : Type u_2<VAR>E : Type u_3<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<GOAL>Module.rank F ↥⊤ = Module.rank F ↥(Subalgebra.toSubmodule ⊤)
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>E : Set α<VAR>hδ : 0 ≤ δ<GOAL>cthickening δ E = ⋃ x ∈ closure E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>hδ : 0 ≤ δ<GOAL>cthickening δ ∅ = ⋃ x ∈ closure ∅, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>E : Set α<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<GOAL>cthickening δ E = ⋃ x ∈ closure E, closedBall x δ