ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x✝ : R<GOAL>x✝ ∈ a • S ↔ x✝ ∈ comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x✝ : R<GOAL>x✝ ∈ map (MulSemiringAction.toRingHom M R a) S ↔ x✝ ∈ map (MulSemiringAction.toRingEquiv M R a) S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>ht : t.Nonempty<VAR>i : α<GOAL>i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>C : Set α<VAR>x : α<VAR>U : Set α<VAR>h_acc : AccPt x (𝓟 C)<VAR>hU : U ∈ 𝓝 x<GOAL>AccPt x (𝓟 (U ∩ C))
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>C : Set α<VAR>x : α<VAR>U : Set α<VAR>h_acc : AccPt x (𝓟 C)<VAR>hU : U ∈ 𝓝 x<VAR>this : 𝓝[≠] x ≤ 𝓟 U<GOAL>AccPt x (𝓟 (U ∩ C))
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>C : Set α<VAR>x : α<VAR>U : Set α<VAR>h_acc : AccPt x (𝓟 C)<VAR>hU : U ∈ 𝓝 x<VAR>this : 𝓝[≠] x ≤ 𝓟 U<GOAL>(𝓝[≠] x ⊓ 𝓟 C).NeBot
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : TopologicalSpace M''<VAR>G : StructureGroupoid H<VAR>inst✝³ : ChartedSpace H M'<VAR>inst✝² : ChartedSpace H M''<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Opens M := { carrier := e.source, is_open' := ⋯ }<VAR>t : Opens H := { carrier := e.target, is_open' := ⋯ }<VAR>c' : PartialHomeomorph (↥t) H<VAR>hc' : c' ∈ atlas H ↥t<GOAL>e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ maximalAtlas (↥s) G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : TopologicalSpace M''<VAR>G : StructureGroupoid H<VAR>inst✝³ : ChartedSpace H M'<VAR>inst✝² : ChartedSpace H M''<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Opens M := { carrier := e.source, is_open' := ⋯ }<VAR>t : Opens H := { carrier := e.target, is_open' := ⋯ }<VAR>c' : PartialHomeomorph (↥t) H<VAR>hc' : c' ∈ atlas H ↥t<VAR>this : Nonempty ↥t<GOAL>e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ maximalAtlas (↥s) G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : TopologicalSpace M''<VAR>G : StructureGroupoid H<VAR>inst✝³ : ChartedSpace H M'<VAR>inst✝² : ChartedSpace H M''<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Opens M := { carrier := e.source, is_open' := ⋯ }<VAR>t : Opens H := { carrier := e.target, is_open' := ⋯ }<VAR>c' : PartialHomeomorph (↥t) H<VAR>hc'✝ : c' ∈ atlas H ↥t<VAR>this : Nonempty ↥t<VAR>x : ↥t<VAR>hc' : c' = (chartAt H ↑x).subtypeRestr this<GOAL>e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ maximalAtlas (↥s) G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : TopologicalSpace M''<VAR>G : StructureGroupoid H<VAR>inst✝³ : ChartedSpace H M'<VAR>inst✝² : ChartedSpace H M''<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Opens M := { carrier := e.source, is_open' := ⋯ }<VAR>t : Opens H := { carrier := e.target, is_open' := ⋯ }<VAR>c' : PartialHomeomorph (↥t) H<VAR>hc'✝ : c' ∈ atlas H ↥t<VAR>this : Nonempty ↥t<VAR>x : ↥t<VAR>hc' : c' = (chartAt H ↑x).subtypeRestr this<GOAL>e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ (PartialHomeomorph.refl H).subtypeRestr this ∈ maximalAtlas (↥s) G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : TopologicalSpace M''<VAR>G : StructureGroupoid H<VAR>inst✝³ : ChartedSpace H M'<VAR>inst✝² : ChartedSpace H M''<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Opens M := { carrier := e.source, is_open' := ⋯ }<VAR>t : Opens H := { carrier := e.target, is_open' := ⋯ }<VAR>c' : PartialHomeomorph (↥t) H<VAR>hc'✝ : c' ∈ atlas H ↥t<VAR>this : Nonempty ↥t<VAR>x : ↥t<VAR>hc' : c' = (chartAt H ↑x).subtypeRestr this<GOAL>e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : TopologicalSpace M''<VAR>G : StructureGroupoid H<VAR>inst✝³ : ChartedSpace H M'<VAR>inst✝² : ChartedSpace H M''<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Opens M := { carrier := e.source, is_open' := ⋯ }<VAR>t : Opens H := { carrier := e.target, is_open' := ⋯ }<VAR>c' : PartialHomeomorph (↥t) H<VAR>hc'✝ : c' ∈ atlas H ↥t<VAR>this : Nonempty ↥t<VAR>x : ↥t<VAR>hc' : c' = (chartAt H ↑x).subtypeRestr this<VAR>goal : PartialHomeomorph (↑e.source) H := e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this<GOAL>e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : TopologicalSpace M''<VAR>G : StructureGroupoid H<VAR>inst✝³ : ChartedSpace H M'<VAR>inst✝² : ChartedSpace H M''<VAR>e : PartialHomeomorph M H<VAR>he : e ∈ atlas H M<VAR>hs : Nonempty ↑e.source<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : ClosedUnderRestriction G<VAR>s : Opens M := { carrier := e.source, is_open' := ⋯ }<VAR>t : Opens H := { carrier := e.target, is_open' := ⋯ }<VAR>c' : PartialHomeomorph (↥t) H<VAR>hc'✝ : c' ∈ atlas H ↥t<VAR>this✝ : Nonempty ↥t<VAR>x : ↥t<VAR>hc' : c' = (chartAt H ↑x).subtypeRestr this✝<VAR>goal : PartialHomeomorph (↑e.source) H := e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this✝<VAR>this : goal ≈ e.subtypeRestr hs<GOAL>e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this✝ ∈ maximalAtlas (↥s) G
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>G : Comonad C<VAR>A B : G.Coalgebra<VAR>h : A.A ≅ B.A<VAR>w : autoParam (A.a ≫ G.map h.hom = h.hom ≫ B.a) _auto✝<GOAL>B.a ≫ G.map h.inv = h.inv ≫ A.a
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>G : Comonad C<VAR>A B : G.Coalgebra<VAR>h : A.A ≅ B.A<VAR>w : autoParam (A.a ≫ G.map h.hom = h.hom ≫ B.a) _auto✝<GOAL>A.a ≫ G.map (h.hom ≫ h.inv) = A.a
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>r : R<GOAL>(X ^ n - C r).leadingCoeff = 1
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<VAR>A : 0 < μ (u ∩ s)<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<VAR>A : 0 < μ (u ∩ s)<VAR>B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>x : α<VAR>hx : x ∈ μ.everywherePosSubset s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[μ.everywherePosSubset s] x<VAR>u : Set α<VAR>u_mem : u ∈ 𝓝 x<VAR>hu : u ∩ μ.everywherePosSubset s ⊆ n<VAR>A : 0 < μ (u ∩ μ.everywherePosSubset s)<VAR>B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s<GOAL>0 < μ n
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → Zero (N a)<VAR>f✝ g✝ f g : Π₀ (a : α), N a<VAR>h : f = g<GOAL>f.neLocus f = ∅
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>b ^ (2 * p) - 1 - (b ^ 2 - 1) = b ^ (2 * p) - (1 + (b ^ 2 - 1))
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>b ^ (2 * p) - (1 + (b ^ 2 - 1)) = b ^ (2 * p) - (1 + b ^ 2 - 1)
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>b ^ (2 * p) - (1 + b ^ 2 - 1) = b ^ (2 * p) - b ^ 2
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>b ^ (2 * p) - b ^ 2 = b ^ (p * 2) - b ^ 2
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>b ^ (p * 2) - b ^ 2 = (b ^ p) ^ 2 - b ^ 2
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>(b ^ p) ^ 2 - b ^ 2 = (b ^ p + b) * (b ^ p - b)
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>(b ^ p + b) * (b ^ p - b) = (b ^ p - b) * (b ^ p + b)
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>(b ^ p - b) * (b ^ p + b) = (b ^ (p - 1 + 1) - b) * (b ^ p + b)
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>(b ^ (p - 1 + 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>(b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)
<VAR>b p : ℕ<VAR>hb : 0 < b<VAR>hp : 1 ≤ p<VAR>hi_bsquared : 1 ≤ b ^ 2<GOAL>(b * b ^ (p - 1) - b * 1) * (b ^ p + b) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x : 𝓞 K<GOAL>(x - 1) * (x - ↑η) * (x - ↑η ^ 2) = x ^ 3 - 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>D : Matrix n n α<GOAL>IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<GOAL>sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>H : ∀ (i : ι), μ i ⟂ₘ ν<GOAL>sum μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>s : ι → Set α<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsν : ∀ (i : ι), ν (s i)ᶜ = 0<GOAL>sum μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>s : ι → Set α<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsν : ∀ (i : ι), ν (s i)ᶜ = 0<GOAL>(sum μ) (⋂ i, s i) = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>ι : Type u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>s : ι → Set α<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>hsμ : ∀ (i : ι), (μ i) (s i) = 0<VAR>hsν : ∀ (i : ι), ν (s i)ᶜ = 0<GOAL>ν (⋂ i, s i)ᶜ = 0
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν✝<VAR>inst✝ : SFinite μ<VAR>ν : Measure β<GOAL>Measure.prod 0 ν = 0
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν✝ ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν✝<VAR>inst✝ : SFinite μ<VAR>ν : Measure β<GOAL>(bind 0 fun x => map (Prod.mk x) ν) = 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<GOAL>Nonempty (IsInitial X) ↔ IsEmpty ↑(F.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<GOAL>Nonempty (IsInitial (F.obj X)) ↔ IsEmpty ↑(F.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>this✝ : PreservesFiniteColimits (forget FintypeCat)<VAR>this : ReflectsColimit (empty FintypeCat) (forget FintypeCat)<GOAL>Nonempty (IsInitial (F.obj X)) ↔ IsEmpty ↑(F.obj X)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hA : A.PosDef<VAR>inst✝ : Invertible A<GOAL>(fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hA : A.PosDef<VAR>inst✝ : Invertible A<GOAL>((D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → 𝕜), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x) ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef
<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✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a : E<VAR>n : ℕ<VAR>ih : ‖a ^ n‖ ≤ ↑n * ‖a‖<GOAL>‖a ^ (n + 1)‖ ≤ ↑(n + 1) * ‖a‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>α : Type u_4<VAR>l : Filter α<VAR>g₁ : α → F<VAR>g₂ : α → ↥(LinearMap.ker f')<VAR>h₁ : Tendsto g₁ l (𝓝 (f a))<VAR>h₂ : Tendsto g₂ l (𝓝 0)<GOAL>Tendsto (fun t => implicitFunction f f' hf hf' (g₁ t) (g₂ t)) l (𝓝 a)
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>α : Type u_4<VAR>l : Filter α<VAR>g₁ : α → F<VAR>g₂ : α → ↥(LinearMap.ker f')<VAR>h₁ : Tendsto g₁ l (𝓝 (f a))<VAR>h₂ : Tendsto g₂ l (𝓝 0)<GOAL>Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (↑(implicitToPartialHomeomorph f f' hf hf') a))
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>α : Type u_4<VAR>l : Filter α<VAR>g₁ : α → F<VAR>g₂ : α → ↥(LinearMap.ker f')<VAR>h₁ : Tendsto g₁ l (𝓝 (f a))<VAR>h₂ : Tendsto g₂ l (𝓝 0)<GOAL>Tendsto (fun t => (g₁ t, g₂ t)) l (𝓝 (f a, 0))
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>IntegrableOn (fun t => t ^ a) (Ioi c) volume
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x<GOAL>IntegrableOn (fun t => t ^ a) (Ioi c) volume
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<VAR>hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x<VAR>ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))<GOAL>IntegrableOn (fun t => t ^ a) (Ioi c) volume
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>b c : α<GOAL>gcd (0 * b) (0 * c) = normalize 0 * gcd b c
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x / t)) ↔ {x | p x} ∈ Filter.map (fun t_1 => t_1 / t) (ae μ)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y : PresheafedSpace C<VAR>α : X ⟶ Y<VAR>x x' : ↑↑X<VAR>h : x = x'<GOAL>Hom.stalkMap α x ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Hom.stalkMap α x'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>hab : 0 ≤ a • b<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>hab : 0 ≤ a • b<GOAL>(0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>hab : 0 ≤ a • b<VAR>ab : 0 ≤ a → b < 0<VAR>nab : a ≤ 0 → 0 < b<GOAL>a • b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>hab : 0 ≤ a • b<VAR>ab : 0 ≤ a → b < 0<VAR>nab : a ≤ 0 → 0 < b<VAR>ha : 0 < a<GOAL>a • b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>b : β<VAR>hab : 0 ≤ 0 • b<VAR>ab : 0 ≤ 0 → b < 0<VAR>nab : 0 ≤ 0 → 0 < b<GOAL>0 • b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<VAR>hab : 0 ≤ a • b<VAR>ab : 0 ≤ a → b < 0<VAR>nab : a ≤ 0 → 0 < b<VAR>ha : a < 0<GOAL>a • b < 0
<VAR>P : PartENat → Prop<GOAL>∀ (a : PartENat), P ⊤ → (∀ (n : ℕ), P ↑n) → P a
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : SeminormedAddCommGroup β<VAR>inst✝² : NormedSpace 𝕜 β<VAR>inst✝¹ : NormedRing γ<VAR>inst✝ : NormedAlgebra 𝕜 γ<VAR>f g : α →ᵇ γ<VAR>x : α<VAR>c k : 𝕜<VAR>a : α<GOAL>((algebraMap 𝕜 (α →ᵇ γ)) k) a = k • 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g σ : Perm α<GOAL>σ⁻¹.support = σ.support
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<GOAL>{ toQuot := Quot.mk (Rel r) 0 } = RingQuot.zero r
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : a < b * c<GOAL>b⁻¹ * a < c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : a < c * b<GOAL>a * b⁻¹ < c
<VAR>α : Type u_1<VAR>inst✝ : Infinite α<VAR>s t : Set α<VAR>hs : #↑s < #α<VAR>ht : #↑t < #α<GOAL>#↑sᶜ = #↑tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n✝ : ℕ<VAR>inst✝ : DecidableEq α<VAR>X Y : Finset α<VAR>n : ℕ<VAR>hXY : 2 * n < (X ∪ Y).card<GOAL>∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n✝ : ℕ<VAR>inst✝ : DecidableEq α<VAR>X Y : Finset α<VAR>n : ℕ<VAR>hXY : 2 * n < (X ∪ Y).card<VAR>h₁ : (X ∩ (Y \ X)).card = 0<GOAL>∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n✝ : ℕ<VAR>inst✝ : DecidableEq α<VAR>X Y : Finset α<VAR>n : ℕ<VAR>hXY : 2 * n < (X ∪ Y).card<VAR>h₁ : (X ∩ (Y \ X)).card = 0<VAR>h₂ : (X ∪ Y).card = X.card + (Y \ X).card<GOAL>∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n✝ : ℕ<VAR>inst✝ : DecidableEq α<VAR>X Y : Finset α<VAR>n : ℕ<VAR>hXY : n + n < X.card + (Y \ X).card<VAR>h₁ : (X ∩ (Y \ X)).card = 0<VAR>h₂ : (X ∪ Y).card = X.card + (Y \ X).card<GOAL>∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n✝ : ℕ<VAR>inst✝ : DecidableEq α<VAR>X Y : Finset α<VAR>n : ℕ<VAR>hXY : n + n < X.card + (Y \ X).card<VAR>h₁ : (X ∩ (Y \ X)).card = 0<VAR>h₂ : (X ∪ Y).card = X.card + (Y \ X).card<VAR>h : n < X.card<GOAL>∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)