ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ inst✝ : Semiring R<VAR>x : α → R<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ih : ∀ (hc : (↑s).Pairwise fun i j => Commute (x i) (x j)) (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯<VAR>hc : (↑(insert a s)).Pairwise fun i j => Commute (x i) (x j)<GOAL>∀ (n : ℕ), (insert a s).sum x ^ n = ∑ k : { x // x ∈ (insert a s).sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ inst✝ : Semiring R<VAR>x : α → R<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ih : ∀ (hc : (↑s).Pairwise fun i j => Commute (x i) (x j)) (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯<VAR>hc : (↑(insert a s)).Pairwise fun i j => Commute (x i) (x j)<VAR>n : ℕ<GOAL>(insert a s).sum x ^ n = ∑ k : { x // x ∈ (insert a s).sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ inst✝ : Semiring R<VAR>x : α → R<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hc : (↑(insert a s)).Pairwise fun i j => Commute (x i) (x j)<VAR>n : ℕ<VAR>ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯<GOAL>(insert a s).sum x ^ n = ∑ k : { x // x ∈ (insert a s).sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ inst✝ : Semiring R<VAR>x : α → R<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hc : (↑(insert a s)).Pairwise fun i j => Commute (x i) (x j)<VAR>n : ℕ<VAR>ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯<GOAL>∑ i : Fin (n + 1), x a ^ ↑i * (∑ i ∈ s, x i) ^ (n - ↑i) * ↑(n.choose ↑i) = ∑ k : { x // x ∈ (insert a s).sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ inst✝ : Semiring R<VAR>x : α → R<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>hc : (↑(insert a s)).Pairwise fun i j => Commute (x i) (x j)<VAR>n : ℕ<VAR>ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯<GOAL>∀ i ∈ s, Commute (x a) (x i)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝² : HasBinaryProduct X Y<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<GOAL>IsPullback prod.fst prod.snd 0 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<GOAL>sᶜ ∈ μ.cofinite ↔ μ s < ⊤
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>mapFun (⇑f) 1 = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a p q : ℤ<VAR>hpq : p + n = q<GOAL>((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a + γ₂.shift a).v p q hpq
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<GOAL>legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<GOAL>¬IsSquare ↑↑a ↔ ¬IsSquare ↑a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>𝕜 : Type u_3<VAR>inst✝⁶ : CommSemiring 𝕜<VAR>A : Type u_4<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : TopologicalSemiring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : ContinuousStar A<VAR>inst✝ : Algebra 𝕜 A<VAR>f : X ≃ₜ Y<VAR>g : C(Y, A)<GOAL>(ContinuousMap.compStarAlgHom' 𝕜 A f.symm.toContinuousMap) ((ContinuousMap.compStarAlgHom' 𝕜 A f.toContinuousMap) g) = g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>𝕜 : Type u_3<VAR>inst✝⁶ : CommSemiring 𝕜<VAR>A : Type u_4<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : TopologicalSemiring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : ContinuousStar A<VAR>inst✝ : Algebra 𝕜 A<VAR>f : X ≃ₜ Y<VAR>g : C(X, A)<GOAL>(ContinuousMap.compStarAlgHom' 𝕜 A f.toContinuousMap) ((ContinuousMap.compStarAlgHom' 𝕜 A f.symm.toContinuousMap) g) = g
<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>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>L : Type u_6<VAR>inst✝ : RCLike L<VAR>r : L<VAR>f : α → L<GOAL>∫ (a : α), f a / r ∂μ = (∫ (a : α), f a ∂μ) / r
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>R : ℝ<VAR>z w : ℂ<VAR>hw : w ∈ ball z R<GOAL>Continuous fun θ => (circleMap z R θ - w)⁻¹
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>R : ℝ<VAR>z w : ℂ<VAR>hw : w ∈ ball z R<VAR>this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0<GOAL>Continuous fun θ => (circleMap z R θ - w)⁻¹
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph = g.graph<VAR>x : E<GOAL>x ∈ f.domain ↔ x ∈ g.domain
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedSemifield α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c : α<GOAL>(a - b) / c = a / c - b / c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>b : β<VAR>x : α<GOAL>x ∈ ⇑e ⁻¹' Ici b ↔ x ∈ Ici (e.symm b)
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a✝ b✝ a b : α<GOAL>Chain R a [b] ↔ R a b
<VAR>Ω✝ : Type u_1<VAR>inst✝⁶ : TopologicalSpace Ω✝<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>δs : ℕ → ℝ<VAR>δs_pos : ∀ (n : ℕ), 0 < δs n<VAR>δs_lim : Tendsto δs atTop (𝓝 0)<GOAL>Tendsto (fun n => ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F))
<VAR>Ω✝ : Type u_1<VAR>inst✝⁶ : TopologicalSpace Ω✝<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>δs : ℕ → ℝ<VAR>δs_pos : ∀ (n : ℕ), 0 < δs n<VAR>δs_lim : Tendsto δs atTop (𝓝 0)<GOAL>Tendsto (fun n ω => (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x => 1))
<VAR>Ω✝ : Type u_1<VAR>inst✝⁶ : TopologicalSpace Ω✝<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>δs : ℕ → ℝ<VAR>δs_pos : ∀ (n : ℕ), 0 < δs n<VAR>δs_lim : Tendsto δs atTop (𝓝 0)<VAR>key : Tendsto (fun n => ⇑(thickenedIndicator ⋯ F)) atTop (𝓝 ((closure F).indicator fun x => 1))<GOAL>Tendsto (fun n ω => (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x => 1))
<VAR>n : ℕ<GOAL>sqrt ↑n = ↑n.sqrt
<VAR>q₁ q₂ : ℚ<GOAL>(q₁ + q₂).den ∣ q₁.den * q₂.den
<VAR>q₁ q₂ : ℚ<GOAL>{ num := (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) / ↑((q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den)), den := q₁.den * q₂.den / (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den ∣ q₁.den * q₂.den
<VAR>q₁ q₂ : ℚ<GOAL>(q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>H : Type w<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type v'<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>H' : Type w'<VAR>inst✝ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<GOAL>{ toFun := fun x => (↑I x.1, ↑I' x.2), invFun := fun x => (↑I.symm x.1, ↑I'.symm x.2), source := {x | x.1 ∈ I.source ∧ x.2 ∈ I'.source}, target := __src✝.target, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.source = univ
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>A : Type u₃<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>f : L →ₗ⁅R⁆ A<VAR>x : L<GOAL>((lift R) f) ((ι R) x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>s.diag ∪ s.offDiag = s ×ˢ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>s.diag ∪ s.offDiag = filter (fun a => a.1 = a.2) (s ×ˢ s) ∪ filter (fun a => ¬a.1 = a.2) (s ×ˢ s)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x : α<VAR>i : m<GOAL>v ⬝ᵥ Pi.single i x = v i * x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x : α<VAR>i : m<VAR>this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0<GOAL>v ⬝ᵥ Pi.single i x = v i * x
<VAR>k : Type u_1<VAR>inst✝⁵ : Field k<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>F : Type u_3<VAR>inst✝³ : Field F<VAR>inst✝² : NumberField K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsAlgebraic k K<VAR>w : InfinitePlace k<VAR>this : Algebra k ℂ := w.embedding.toAlgebra<GOAL>(fun x => x.comap (algebraMap k K)) (mk IsAlgClosed.lift.toRingHom) = w
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>b : ↥B<GOAL>t⁻¹ * of ↑b = of ↑(φ.symm b) * t⁻¹
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>b : ↥B<GOAL>t⁻¹ * of ↑b = t⁻¹ * of ↑b * t * t⁻¹
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : NonAssocRing α<VAR>a✝ b : α<VAR>n✝ : ℤ<VAR>a : α<VAR>n : ℤ<GOAL>n • a = a * ↑n
<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>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>s : Set ((a : ι) → π a)<GOAL>IsOpen s ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
<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>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>s : Set ((a : ι) → π a)<GOAL>(∀ x ∈ s, 𝓝 x ≤ 𝓟 s) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
<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>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>s : Set ((a : ι) → π a)<GOAL>(∀ x ∈ s, ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ x i ∈ t_1) ∧ (↑I).pi t ⊆ s) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
<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>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>s : Set ((a : ι) → π a)<VAR>a : (a : ι) → π a<VAR>x✝ : a ∈ s<GOAL>(∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) → ∃ I u, (∀ a_2 ∈ I, IsOpen (u a_2) ∧ a a_2 ∈ u a_2) ∧ (↑I).pi u ⊆ s
<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>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>s : Set ((a : ι) → π a)<VAR>a : (a : ι) → π a<VAR>x✝ : a ∈ s<GOAL>(∃ I u, (∀ a_1 ∈ I, IsOpen (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s) → ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38879, u_1} C<VAR>P : Karoubi C<GOAL>P.p = { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p ≫ P.p ≫ P.p
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<GOAL>QuasiCompact f ↔ CompactSpace ↑↑X.toPresheafedSpace
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>A : Set G<VAR>hA : μ.outerMeasure A ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<GOAL>∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>A : Set G<VAR>hA : μ.outerMeasure A ≠ ⊤<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>U : Set G<VAR>hU : IsOpen U<VAR>h2U : A ⊆ U<VAR>h3U : (inducedOuterMeasure (fun s₁ hs₁ => μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯) U ≤ (inducedOuterMeasure (fun s₁ hs₁ => μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯) A + ↑ε<GOAL>∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>m✝ : OuterMeasure α<VAR>β : Type u_3<VAR>f : α → β<VAR>m : OuterMeasure β<VAR>s : Set β<GOAL>f '' (f ⁻¹' s) = Subtype.val '' (Subtype.val ⁻¹' s)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>S : Set (LieSubalgebra R L)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>S : Set (LieSubalgebra R L)<GOAL>⋂ p ∈ {x | ∃ s ∈ S, s.toSubmodule = x}, ↑p = ⋂ s ∈ S, ↑s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝ : Archimedean 𝕜<GOAL>⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝ : Archimedean 𝕜<GOAL>(fun x => Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) = fun x => Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>inst✝ : Archimedean 𝕜<VAR>x : 𝕜<GOAL>Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : HasInitial C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>to P ≫ f = to Q
<VAR>α : Type u_1<VAR>s₁ : Set α → Prop<VAR>has_empty✝¹ : s₁ ∅<VAR>has_compl✝¹ : ∀ {a : Set α}, s₁ a → s₁ aᶜ<VAR>has_iUnion_nat✝¹ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ i, f i)<VAR>s₂ : Set α → Prop<VAR>has_empty✝ : s₂ ∅<VAR>has_compl✝ : ∀ {a : Set α}, s₂ a → s₂ aᶜ<VAR>has_iUnion_nat✝ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₂ (f i)) → s₂ (⋃ i, f i)<VAR>h : ∀ (s : Set α), { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ }.Has s ↔ { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }.Has s<GOAL>{ Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } = { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }
<VAR>α : Type u_1<VAR>s₁ : Set α → Prop<VAR>has_empty✝¹ : s₁ ∅<VAR>has_compl✝¹ : ∀ {a : Set α}, s₁ a → s₁ aᶜ<VAR>has_iUnion_nat✝¹ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ i, f i)<VAR>s₂ : Set α → Prop<VAR>has_empty✝ : s₂ ∅<VAR>has_compl✝ : ∀ {a : Set α}, s₂ a → s₂ aᶜ<VAR>has_iUnion_nat✝ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₂ (f i)) → s₂ (⋃ i, f i)<VAR>h : ∀ (s : Set α), { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ }.Has s ↔ { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }.Has s<VAR>this : s₁ = s₂<GOAL>{ Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } = { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : m<VAR>j : n<GOAL>(toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : m<VAR>j : n<GOAL>∀ b ∈ Finset.univ, b ≠ j → (if b = j then 1 else 0) • v₁ b = 0
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : m<VAR>j : n<GOAL>j ∉ Finset.univ → (if j = j then 1 else 0) • v₁ j = 0
<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✝⁹ : TopologicalSpace G<VAR>μ : Measure G<VAR>inst✝⁸ : μ.IsHaarMeasure<VAR>inst✝⁷ : BorelSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>H : Type u_4<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : BorelSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TopologicalGroup H<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>h_surj : Surjective ⇑f<VAR>h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)<VAR>K : Set H<VAR>hK : IsCompact K<GOAL>(map (⇑f) μ) K < ⊤
<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✝⁹ : TopologicalSpace G<VAR>μ : Measure G<VAR>inst✝⁸ : μ.IsHaarMeasure<VAR>inst✝⁷ : BorelSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>H : Type u_4<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : BorelSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : TopologicalGroup H<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>h_surj : Surjective ⇑f<VAR>h_prop : Tendsto (⇑f) (cocompact G) (cocompact H)<VAR>K : Set H<VAR>hK : IsCompact K<GOAL>μ (⇑f ⁻¹' K) < ⊤
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>r : R<GOAL>0 ≤ r * star r
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ioi a) (Ioi (a + d))
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d x✝ : M<VAR>h : x✝ ∈ Ioi (a + d)<GOAL>x✝ ∈ (fun x => x + d) '' Ioi a
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c✝ d c : M<VAR>h : a + d + c ∈ Ioi (a + d)<GOAL>a + d + c ∈ (fun x => x + d) '' Ioi a
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c✝ d c : M<VAR>h : a < a + c<GOAL>a + d + c ∈ (fun x => x + d) '' Ioi a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a✝ b : α<VAR>s✝ s : Set α<VAR>h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t<VAR>a : α<VAR>ha : a ∈ s<GOAL>Disjoint a (sSup (s \ {a}))
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a✝ b : α<VAR>s✝ s : Set α<VAR>h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t<VAR>a : α<VAR>ha : a ∈ s<GOAL>∀ (i : Finset α), ⨆ (_ : ↑i ⊆ s \ {a}), a ⊓ i.sup id = ⊥
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a✝ b : α<VAR>s✝ s : Set α<VAR>h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t<VAR>a : α<VAR>ha : a ∈ s<VAR>t : Finset α<GOAL>⨆ (_ : ↑t ⊆ s \ {a}), a ⊓ t.sup id = ⊥
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a✝ b : α<VAR>s✝ s : Set α<VAR>h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t<VAR>a : α<VAR>ha : a ∈ s<VAR>t : Finset α<GOAL>↑t ⊆ s \ {a} → a ⊓ sSup ↑t = ⊥
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a b : G<VAR>n m : ℤ<GOAL>a * b ^ n * b ^ m = a * b ^ (n + m)
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>p : ℝ<GOAL>ENNReal.ofReal p < 1 ↔ p < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : NoMaxOrder α<VAR>inst✝ : DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : NoMaxOrder α<VAR>inst✝ : DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>(∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : M<VAR>hab : a ≤ b<VAR>k : ℕ<GOAL>a ^ (k + 1) ≤ b ^ (k + 1)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : M<VAR>hab : a ≤ b<VAR>k : ℕ<GOAL>a ^ k * a ≤ b ^ k * b