ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : LocallyConnectedSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>h : OpenEmbedding f<GOAL>LocallyConnectedSpace β
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : LocallyConnectedSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>h : OpenEmbedding f<VAR>x : β<GOAL>(𝓝 x).HasBasis ((fun x s => (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x) ((fun x s => f ⁻¹' s) x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : LocallyConnectedSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>h : OpenEmbedding f<VAR>x : β<GOAL>(Filter.comap f (𝓝 (f x))).HasBasis ((fun x s => (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x) ((fun x s => f ⁻¹' s) x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : E), (fun x => ⟪c, f x⟫_𝕜) =ᶠ[ae μ] 0<VAR>s : ℕ → E := denseSeq E<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : E), (fun x => ⟪c, f x⟫_𝕜) =ᶠ[ae μ] 0<VAR>s : ℕ → E := denseSeq E<VAR>hs : DenseRange s<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : E), (fun x => ⟪c, f x⟫_𝕜) =ᶠ[ae μ] 0<VAR>s : ℕ → E := denseSeq E<VAR>hs : DenseRange s<VAR>hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : E), (fun x => ⟪c, f x⟫_𝕜) =ᶠ[ae μ] 0<VAR>s : ℕ → E := denseSeq E<VAR>hs : DenseRange s<VAR>hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0<VAR>x : α<VAR>hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0<GOAL>f x = 0 x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : E), (fun x => ⟪c, f x⟫_𝕜) =ᶠ[ae μ] 0<VAR>s : ℕ → E := denseSeq E<VAR>hs : DenseRange s<VAR>hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0<VAR>x : α<VAR>hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0<GOAL>⟪f x, f x⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : SecondCountableTopology E<VAR>f : α → E<VAR>hf : ∀ (c : E), (fun x => ⟪c, f x⟫_𝕜) =ᶠ[ae μ] 0<VAR>s : ℕ → E := denseSeq E<VAR>hs : DenseRange s<VAR>hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0<VAR>x : α<VAR>hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0<VAR>h_closed : IsClosed {c | ⟪c, f x⟫_𝕜 = 0}<GOAL>⟪f x, f x⟫_𝕜 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : Nontrivial R<VAR>hq : q.Monic<VAR>h : p /ₘ q = 0<GOAL>p.degree < q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : Nontrivial R<VAR>hq : q.Monic<VAR>h : p /ₘ q = 0<VAR>this : p %ₘ q + q * (p /ₘ q) = p<GOAL>p.degree < q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : Nontrivial R<VAR>hq : q.Monic<VAR>h : p.degree < q.degree<GOAL>p /ₘ q = 0
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>m : M<VAR>_hm : m ∈ p<VAR>n : N<VAR>hn : n ∈ ⊥<GOAL>(f m) n ∈ ⊥
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>m : M<VAR>_hm : m ∈ p<VAR>n : N<VAR>hn : n = 0<GOAL>(f m) n ∈ ⊥
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>m : M<VAR>_hm : m ∈ p<VAR>n : N<VAR>hn : n = 0<GOAL>0 ∈ ⊥
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hy : 0 < y<VAR>hz : z < 0<GOAL>x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ≤ x ↔ ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>((∀ (i : LeftMoves 0), moveLeft 0 i ⧏ x) ∧ ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j) ↔ ∀ (j : x.RightMoves), 0 ⧏ x.moveRight j
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<GOAL>dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l t₁ t₂ : List α<VAR>p : t₁ ~ t₂<VAR>a : α<VAR>x✝ : a ∈ l<GOAL>elem a t₁ = elem a t₂
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>(cs.leftInvSeq ω).prod = (cs.wordProd ω)⁻¹
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>(List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse<GOAL>(List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse<GOAL>(cs.rightInvSeq ω.reverse).prod = cs.wordProd ω
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse<GOAL>(cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>this : List.map (fun x => x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse<GOAL>(cs.rightInvSeq ω.reverse).prod = (cs.wordProd ω.reverse)⁻¹
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>hf : Function.Injective ⇑f<GOAL>OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a c : α<VAR>n✝ n : ℤ<GOAL>toIcoMod hp a (a + n • p) = a
<VAR>r : ℝ<GOAL>r.sign = 0 ↔ r = 0
<VAR>r : ℝ<VAR>h : r.sign = 0<GOAL>r = 0
<VAR>r : ℝ<VAR>h : r.sign = 0<VAR>hn : r < 0<GOAL>r = 0
<VAR>h : sign 0 = 0<GOAL>0 = 0
<VAR>r : ℝ<VAR>h : r.sign = 0<VAR>hp : 0 < r<GOAL>r = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : DecidableEq σ<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<GOAL>(coeff R n) (φ.invOfUnit u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (φ.invOfUnit u) else 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>s : Set X<GOAL>⋃ x ∈ s, closure {x} = s ↔ IsLowerSet s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p q : R[X]<VAR>inst✝³ : CommRing T<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>n : ℕ<GOAL>(X ^ n).aroots S = n • {0}
<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✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x y : n → α<VAR>e : m ≃ n<GOAL>x ∘ ⇑e ⬝ᵥ y ∘ ⇑e = x ⬝ᵥ y
<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✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>x y : n → α<VAR>e : m ≃ n<GOAL>x ⬝ᵥ (y ∘ ⇑e) ∘ ⇑e.symm = x ⬝ᵥ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : β → ℝ≥0<VAR>r : ℝ≥0<VAR>hgf : ∀ (b : β), g b ≤ f b<VAR>hfr : HasSum f r<GOAL>∑' (b : β), ↑(g b) ≤ ↑r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : β → ℝ≥0<VAR>r : ℝ≥0<VAR>hgf : ∀ (b : β), g b ≤ f b<VAR>hfr : HasSum f r<VAR>b : β<GOAL>↑(g b) ≤ ↑(f b)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>s : Set ℝ<GOAL>(Measure.map (fun x => x * a) volume) s = ofReal |a⁻¹| * volume s
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>s : Set ℝ<GOAL>(ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * volume s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁.isSubperm l₂ = true ↔ l₁ <+~ l₂
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n✝ : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>n : ℕ<GOAL>(∏ _i ∈ Finset.range n, φ).IsHomogeneous (m * n)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n✝ : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>n : ℕ<GOAL>(∏ _i ∈ Finset.range n, φ).IsHomogeneous (∑ _i ∈ Finset.range n, m)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι✝ : Type u_4<VAR>s✝ : Finset ι✝<VAR>w✝ w₁ w₂ : ι✝ → k<VAR>p✝ : ι✝ → V<VAR>ι : Type u_5<VAR>p : ι → V<VAR>s : Finset ι<VAR>w : ι → k<VAR>hw : ∑ i ∈ s, w i = 0<GOAL>((s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0) ↔ ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(GradedAlgebra.ι Q) m * (GradedAlgebra.ι Q) m = (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(DirectSum.of (fun i => ↥(evenOdd Q i)) (1 + 1)) (GradedMonoid.GMul.mul ⟨(ι Q) m, ⋯⟩ ⟨(ι Q) m, ⋯⟩) = (DirectSum.of (fun i => ↥(evenOdd Q i)) 0) (DirectSum.GAlgebra.toFun (Q m))
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'' : DifferentiableOn ℝ (deriv f) (interior D)<VAR>hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x<GOAL>DifferentiableOn ℝ (deriv f) (interior (interior D))
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'' : DifferentiableOn ℝ (deriv f) (interior D)<VAR>hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x<GOAL>∀ x ∈ interior (interior D), 0 ≤ deriv (deriv f) x
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f.Disjoint g<VAR>x : α<GOAL>f⁻¹ x = x ∨ g x = x
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f.Disjoint g<VAR>x : α<GOAL>f x = x ∨ g x = x
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : HasContDiffBump E<VAR>inst✝⁷ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : IsLocallyFiniteMeasure μ<VAR>inst✝³ : μ.IsOpenPosMeasure<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : CompleteSpace X<VAR>z : X<GOAL>∫ (x : E), f.normed μ x • z ∂μ = z
<VAR>N✝ : ℕ<VAR>N : ℕ+<VAR>A : SL(2, ℤ)<VAR>hA : A ∈ Gamma ↑N<GOAL>A ∈ Gamma1 ↑N
<VAR>N✝ : ℕ<VAR>N : ℕ+<VAR>A : SL(2, ℤ)<VAR>hA : ↑(↑A 0 0) = 1 ∧ ↑(↑A 0 1) = 0 ∧ ↑(↑A 1 0) = 0 ∧ ↑(↑A 1 1) = 1<GOAL>↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<GOAL>0 ∉ σ a ↔ IsUnit a
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>p : X → Prop<GOAL>(∀ᶠ (x : X) in residual X, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>p : X → Prop<GOAL>(∃ t, (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>inst✝¹¹ : TopologicalSpace H<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>G : Type u_7<VAR>inst✝⁹ : TopologicalSpace G<VAR>G' : Type u_8<VAR>inst✝⁸ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>M' : Type u_10<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : ChartedSpace H' M'<VAR>N : Type u_11<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace G N<VAR>N' : Type u_12<VAR>inst✝¹ : TopologicalSpace N'<VAR>inst✝ : ChartedSpace G' N'<VAR>n : ℕ∞<VAR>α : Sort u_13<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : α → M<GOAL>range (⇑h ∘ f) = ⇑h.symm ⁻¹' range f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>T : Finset ι<VAR>hT : T ⊆ S<VAR>i : ι<VAR>hi : i ∈ S<VAR>hiT : i ∉ T<GOAL>Disjoint ((fun i => torsionBySet R M ↑(p i)) i) (T.sup fun i => torsionBySet R M ↑(p i))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>T : Finset ι<VAR>hT : T ⊆ S<VAR>i : ι<VAR>hi : i ∈ S<VAR>hiT : i ∉ T<GOAL>(fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>T : Finset ι<VAR>hT : T ⊆ S<VAR>i : ι<VAR>hi : i ∈ S<VAR>hiT : i ∉ T<VAR>this : torsionBySet R M ↑(OrderDual.ofDual (OrderDual.toDual (p i) ⊓ OrderDual.toDual (⨅ i ∈ T, p i))) = torsionBySet R M ↑(OrderDual.ofDual (OrderDual.toDual (p i))) ⊓ torsionBySet R M ↑(OrderDual.ofDual (OrderDual.toDual (⨅ i ∈ T, p i)))<GOAL>(fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>T : Finset ι<VAR>hT : T ⊆ S<VAR>i : ι<VAR>hi : i ∈ S<VAR>hiT : i ∉ T<VAR>this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)<GOAL>torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>ι : Type u_3<VAR>p : ι → Ideal R<VAR>S : Finset ι<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>T : Finset ι<VAR>hT : T ⊆ S<VAR>i : ι<VAR>hi : i ∈ S<VAR>hiT : i ∉ T<VAR>this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)<GOAL>∀ i_1 ∈ T, p i ⊔ p i_1 = ⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ g, ‖↑g - f‖ < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w✝ : A.SeparatesPoints<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ ↑A.toSubsemiring<GOAL>∃ g, ‖↑g - f‖ < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w✝ : A.SeparatesPoints<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring<GOAL>∃ g, ‖↑g - f‖ < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w✝ : A.SeparatesPoints<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring<VAR>g : C(X, ℝ)<VAR>H : g ∈ Metric.ball f ε<VAR>m : g ∈ ↑A.toSubsemiring<GOAL>∃ g, ‖↑g - f‖ < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w✝ : A.SeparatesPoints<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring<VAR>g : C(X, ℝ)<VAR>H : ‖g - f‖ < ε<VAR>m : g ∈ ↑A.toSubsemiring<GOAL>∃ g, ‖↑g - f‖ < ε
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : 𝕜<VAR>v : E<VAR>T : E →ₗ[𝕜] E<VAR>h : v ∈ eigenspace T μ<GOAL>⟪v, T v⟫_𝕜 = μ * ↑‖v‖ ^ 2
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<GOAL>A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>this : A * (A.adjugate * A.adjugate.adjugate) = A * A.det ^ (Fintype.card n - 1) • 1<GOAL>A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s✝ t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>ι : Sort u_3<VAR>s : ι → Set X<VAR>P : X → Prop<GOAL>(∀ᶠ (x : X) in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ (i : ι), ∀ᶠ (x : X) in 𝓝ˢ (s i), P x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ U, IsOpen U ∧ U ∩ s = {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<VAR>U : Set X<VAR>hU_nhds : U ∈ 𝓝 x<VAR>hU_inter : U ∩ s = {x}<GOAL>∃ U, IsOpen U ∧ U ∩ s = {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<VAR>U : Set X<VAR>hU_nhds : U ∈ 𝓝 x<VAR>hU_inter : U ∩ s = {x}<VAR>t : Set X<VAR>ht_sub : t ⊆ U<VAR>ht_open : IsOpen t<VAR>ht_x : x ∈ t<GOAL>∃ U, IsOpen U ∧ U ∩ s = {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<VAR>U : Set X<VAR>hU_nhds : U ∈ 𝓝 x<VAR>hU_inter : U ∩ s = {x}<VAR>t : Set X<VAR>ht_sub : t ⊆ U<VAR>ht_open : IsOpen t<VAR>ht_x : x ∈ t<GOAL>t ∩ s ⊆ {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<VAR>U : Set X<VAR>hU_nhds : U ∈ 𝓝 x<VAR>hU_inter : U ∩ s = {x}<VAR>t : Set X<VAR>ht_sub : t ⊆ U<VAR>ht_open : IsOpen t<VAR>ht_x : x ∈ t<GOAL>{x} ⊆ t ∩ s
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(E.map φ).j = φ E.j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>t : Finset β<VAR>x : β<GOAL>x ∈ s.biUnion f ∩ t ↔ x ∈ s.biUnion fun x => f x ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>t : Finset β<VAR>x : β<GOAL>(∃ a ∈ s, x ∈ f a) ∧ x ∈ t ↔ ∃ a ∈ s, x ∈ f a ∧ x ∈ t
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G : C ⥤ D<VAR>hG : CompatiblePreserving K G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>h : x.Compatible<VAR>Z₁ Z₂ W : D<VAR>g₁ : W ⟶ Z₁<VAR>g₂ : W ⟶ Z₂<VAR>X₁ : C<VAR>f₁ : X₁ ⟶ Z<VAR>h₁ : Z₁ ⟶ G.obj X₁<VAR>hf₁ : T f₁<VAR>H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)<VAR>X₂ : C<VAR>f₂ : X₂ ⟶ Z<VAR>h₂ : Z₂ ⟶ G.obj X₂<VAR>hf₂ : T f₂<VAR>H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)<VAR>eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂<GOAL>ℱ.val.map (g₁ ≫ h₁).op (x f₁ hf₁) = ℱ.val.map (g₂ ≫ h₂).op (x f₂ hf₂)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>A : Type u₃<VAR>inst✝ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G : C ⥤ D<VAR>hG : CompatiblePreserving K G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>h : x.Compatible<VAR>Z₁ Z₂ W : D<VAR>g₁ : W ⟶ Z₁<VAR>g₂ : W ⟶ Z₂<VAR>X₁ : C<VAR>f₁ : X₁ ⟶ Z<VAR>h₁ : Z₁ ⟶ G.obj X₁<VAR>hf₁ : T f₁<VAR>H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)<VAR>X₂ : C<VAR>f₂ : X₂ ⟶ Z<VAR>h₂ : Z₂ ⟶ G.obj X₂<VAR>hf₂ : T f₂<VAR>H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)<VAR>eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂<GOAL>(g₁ ≫ h₁) ≫ G.map f₁ = (g₂ ≫ h₂) ≫ G.map f₂
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e₁ e₂ : Basis ι R M<GOAL>SameRay R e₁.det e₂.det ↔ SameRay R (e₁.det ⇑e₂ • e₂.det) e₂.det
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<VAR>inst✝ : StrongRankCondition R<GOAL>Module.rank R ℍ[R,c₁,c₂] = 4
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<VAR>inst✝ : StrongRankCondition R<GOAL>↑4 = 4