ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<GOAL>(C r * p).smeval x = r • p.smeval x
<VAR>α β : Type u<VAR>s : Set Cardinal.{v}<GOAL>lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
<VAR>α β : Type u<GOAL>lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)
<VAR>α β : Type u<VAR>s : Set Cardinal.{v}<VAR>hs : s.Nonempty<GOAL>lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x y : L<GOAL>((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥↑(weightSpace M ⇑χ) • (χ x * χ y)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : Module.Free R M<VAR>inst✝¹⁰ : Module.Finite R M<VAR>inst✝⁹ : Module.Free R L<VAR>inst✝⁸ : Module.Finite R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module K M<VAR>inst✝⁴ : LieModule K L M<VAR>inst✝³ : FiniteDimensional K M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : LinearWeights K L M<VAR>inst✝ : IsTriangularizable K L M<VAR>x y : L<VAR>hxy : ∀ (χ : Weight K L M), MapsTo ⇑((toEnd K L M) x ∘ₗ (toEnd K L M) y) ↑(weightSpace M ⇑χ) ↑(weightSpace M ⇑χ)<GOAL>((traceForm K L M) x) y = ∑ χ : Weight K L M, finrank K ↥↑(weightSpace M ⇑χ) • (χ x * χ y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>ht : IsPreirreducible t<VAR>f : Y → X<VAR>hf : OpenEmbedding f<VAR>U V : Set Y<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>x : Y<VAR>hx : x ∈ f ⁻¹' t<VAR>hx' : x ∈ U<VAR>y : Y<VAR>hy : y ∈ f ⁻¹' t<VAR>hy' : y ∈ V<GOAL>(f ⁻¹' t ∩ (U ∩ V)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>ht : IsPreirreducible t<VAR>f : Y → X<VAR>hf : OpenEmbedding f<VAR>U V : Set Y<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>x : Y<VAR>hx : x ∈ f ⁻¹' t<VAR>hx' : x ∈ U<VAR>y✝ : Y<VAR>hy : y✝ ∈ f ⁻¹' t<VAR>hy' : y✝ ∈ V<VAR>y : Y<VAR>h₂ : y ∈ U<VAR>h₁ : f y ∈ t<VAR>y' : Y<VAR>h₃ : y' ∈ V<VAR>h₄ : f y' = f y<GOAL>(f ⁻¹' t ∩ (U ∩ V)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>ht : IsPreirreducible t<VAR>f : Y → X<VAR>hf : OpenEmbedding f<VAR>U V : Set Y<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>x : Y<VAR>hx : x ∈ f ⁻¹' t<VAR>hx' : x ∈ U<VAR>y✝ : Y<VAR>hy : y✝ ∈ f ⁻¹' t<VAR>hy' : y✝ ∈ V<VAR>y : Y<VAR>h₂ : y ∈ U<VAR>h₁ : f y ∈ t<VAR>h₃ : y ∈ V<VAR>h₄ : f y = f y<GOAL>(f ⁻¹' t ∩ (U ∩ V)).Nonempty
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : SummableFamily Γ R α<VAR>f : α ↪ β<VAR>a : α<VAR>b : β<VAR>g : Γ<GOAL>(s.embDomain f).hsum.coeff g = s.hsum.coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : SummableFamily Γ R α<VAR>f : α ↪ β<VAR>a : α<VAR>b : β<VAR>g : Γ<GOAL>(∑ᶠ (i : β), if h : i ∈ Set.range ⇑f then (s (Classical.choose ⋯)).coeff g else 0) = ∑ᶠ (i : α), (s i).coeff g
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w u v : V<VAR>p : G.Walk v u<VAR>h : G.Adj u v<GOAL>(cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w u v : V<VAR>p : G.Walk v u<VAR>h : G.Adj u v<GOAL>(s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w u v : V<VAR>p : G.Walk v u<VAR>h : G.Adj u v<VAR>this : p.support.Nodup → p.edges.Nodup<GOAL>(s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : E → F<VAR>C : ℝ≥0<GOAL>LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : AddMonoid γ<VAR>P : (α →ₛ γ) → Prop<VAR>h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))<VAR>h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)<VAR>f : α →ₛ γ<VAR>s : Finset γ<VAR>h : f.range \ {0} = s<GOAL>P f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : AddMonoid γ<VAR>P : (α →ₛ γ) → Prop<VAR>h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))<VAR>h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)<VAR>f : α →ₛ γ<VAR>s : Finset γ<VAR>h : range ↑f \ {0} = ↑s<GOAL>P f
<VAR>α : Type u<VAR>C : List α → Sort u_1<VAR>h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>ofFnRec h (ofFn f) = h n f
<VAR>α : Type u<VAR>C : List α → Sort u_1<VAR>h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)<VAR>n : ℕ<VAR>f : Fin n → α<VAR>this : Function.RightInverse ⇑equivSigmaTuple.symm ⇑equivSigmaTuple<GOAL>ofFnRec h (ofFn f) = h n f
<VAR>α : Type u<VAR>C : List α → Sort u_1<VAR>h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)<VAR>n : ℕ<VAR>f : Fin n → α<VAR>this : Function.RightInverse (fun f => ofFn f.snd) fun l => ⟨l.length, l.get⟩<GOAL>ofFnRec h (ofFn f) = h n f
<VAR>α : Type u<VAR>C : List α → Sort u_1<VAR>h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)<VAR>n : ℕ<VAR>f : Fin n → α<VAR>this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => ⟨l.length, l.get⟩<VAR>this : cast ⋯ (h ⟨(ofFn ⟨n, f⟩.snd).length, (ofFn ⟨n, f⟩.snd).get⟩.fst ⟨(ofFn ⟨n, f⟩.snd).length, (ofFn ⟨n, f⟩.snd).get⟩.snd) = h ⟨n, f⟩.fst ⟨n, f⟩.snd<GOAL>ofFnRec h (ofFn f) = h n f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure ≠ univ<GOAL>‖S.normedMk‖ = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure ≠ univ<GOAL>1 ≤ ‖S.normedMk‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure ≠ univ<VAR>x : M<VAR>hx : 0 < ‖↑x‖<GOAL>1 ≤ ‖S.normedMk‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure ≠ univ<VAR>x : M<VAR>hx : 0 < ‖↑x‖<GOAL>‖↑x‖ ≤ ‖S.normedMk‖ * ‖↑x‖
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>dt t : ℝ<VAR>ht : t ∈ {t | t + dt ∈ s}<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (γ ∘ fun x => x + dt) t (ContinuousLinearMap.smulRight 1 (v ((γ ∘ fun x => x + dt) t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>dt t : ℝ<VAR>ht : t ∈ {t | t + dt ∈ s}<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (γ ∘ fun x => x + dt) t ((ContinuousLinearMap.smulRight 1 (v (γ (t + dt)))).comp (ContinuousLinearMap.id ℝ ℝ))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>dt t : ℝ<VAR>ht : t ∈ {t | t + dt ∈ s}<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) (fun x => x + dt) t (ContinuousLinearMap.id ℝ ℝ)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>dt t : ℝ<VAR>ht : t ∈ {t | t + dt ∈ s}<GOAL>HasFDerivWithinAt (writtenInExtChartAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) t fun x => x + dt) (ContinuousLinearMap.id ℝ ℝ) (range ↑𝓘(ℝ, ℝ)) (↑(extChartAt 𝓘(ℝ, ℝ) t) t)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>dt t : ℝ<VAR>ht : t ∈ {t | t + dt ∈ s}<GOAL>HasFDerivAt (fun x => x + dt) (ContinuousLinearMap.id ℝ ℝ) t
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O F<VAR>hv : v.Integers O<VAR>x : O<VAR>hvx : v ((algebraMap O F) x) = 1<GOAL>IsUnit x
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O F<VAR>hv : v.Integers O<VAR>x : O<VAR>hvx : v ((algebraMap O F) x) = 1<GOAL>(algebraMap O F) x ≠ 0
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Monoid M<VAR>s : Set M<GOAL>centralizer s.centralizer.centralizer = centralizer s
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Monoid M<VAR>s : Set M<GOAL>↑(centralizer s.centralizer.centralizer) = ↑(centralizer s)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<VAR>i : IsZero X<GOAL>IsZero Y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<VAR>i : IsZero X<VAR>hf : f = 0<GOAL>IsZero Y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>i : IsZero X<VAR>inst✝ : Epi 0<GOAL>IsZero Y
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x : R<GOAL>lcm 0 x = 0
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hs : MeasurableSet s<VAR>hu : IsUniform X s ℙ μ<GOAL>(fun x => s.indicator ((μ s)⁻¹ • 1) x) =ᶠ[ae μ] pdf X ℙ μ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>k : ℕ<VAR>kpos : 0 < k<VAR>x : ℕ<GOAL>(f.ppow (k + 1)) x = ((f.ppow k).pmul f) x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>k : ℕ<VAR>kpos : 0 < k<VAR>x : ℕ<GOAL>f x ^ k * f x = ((f.ppow k).pmul f) x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f✝ f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>f : (i : ι) → Filter (α i)<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>i : ι<GOAL>map (eval i) (pi f) = f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f✝ f₁ f₂ : (i : ι) → Filter (α i)<VAR>s✝ : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>f : (i : ι) → Filter (α i)<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : s ∈ map (eval i) (pi f)<GOAL>s ∈ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f✝ f₁ f₂ : (i : ι) → Filter (α i)<VAR>s✝ : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>f : (i : ι) → Filter (α i)<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : s ∈ map (eval i) (pi f)<VAR>I : Set ι<VAR>hIf : I.Finite<VAR>t : (i : ι) → Set (α i)<VAR>htf : ∀ (i : ι), t i ∈ f i<VAR>hI : I.pi t ⊆ eval i ⁻¹' s<GOAL>s ∈ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f✝ f₁ f₂ : (i : ι) → Filter (α i)<VAR>s✝ : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>f : (i : ι) → Filter (α i)<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : s ∈ map (eval i) (pi f)<VAR>I : Set ι<VAR>hIf : I.Finite<VAR>t : (i : ι) → Set (α i)<VAR>htf : ∀ (i : ι), t i ∈ f i<VAR>hI : eval i '' I.pi t ⊆ s<GOAL>s ∈ f i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f✝ f₁ f₂ : (i : ι) → Filter (α i)<VAR>s✝ : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>f : (i : ι) → Filter (α i)<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : s ∈ map (eval i) (pi f)<VAR>I : Set ι<VAR>hIf : I.Finite<VAR>t : (i : ι) → Set (α i)<VAR>htf : ∀ (i : ι), t i ∈ f i<VAR>hI : eval i '' I.pi t ⊆ s<GOAL>(I.pi t).Nonempty
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n m : ℕ<VAR>i : [m] ⟶ [n]<VAR>hi : Mono i<VAR>h₁ : [m].len ≠ n<VAR>h₂ : ¬Isδ₀ i<GOAL>PInfty.f n ≫ X.map i.op = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n m : ℕ<VAR>i : [m] ⟶ [n]<VAR>hi : Mono i<VAR>h₁ : [m].len ≠ n<VAR>h₂ : ¬Isδ₀ i<VAR>k : ℕ<VAR>hk : [n].len = [m].len + k + 1<GOAL>PInfty.f n ≫ X.map i.op = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n m : ℕ<VAR>i : [m] ⟶ [n]<VAR>hi : Mono i<VAR>h₁ : [m].len ≠ n<VAR>h₂ : ¬Isδ₀ i<VAR>k : ℕ<VAR>hk : n = m + k + 1<GOAL>PInfty.f n ≫ X.map i.op = 0
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype n'<VAR>v : n' → α<VAR>A : Fin m → n' → α<VAR>B : Matrix n' o' α<VAR>i : Fin m.succ<VAR>j : o'<GOAL>∀ (i : Fin m), (of (vecCons v A) * B) i.succ j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i.succ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>h : G.IsNClique n s<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsClique ↑(map f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>h : G.IsNClique n s<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsClique (⇑f '' ↑s)
<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>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>s : Finset ι<VAR>w : ι → k<VAR>h : ∑ i ∈ s, w i = 0<VAR>p : ι → P<VAR>v : V<GOAL>(s.weightedVSub (v +ᵥ p)) w = (s.weightedVSub p) w
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : TruncatedWittVector p m (ZMod p)<GOAL>(zmodEquivTrunc p n).symm ((truncate hm) x) = (ZMod.castHom ⋯ (ZMod (p ^ n))) ((zmodEquivTrunc p m).symm x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : TruncatedWittVector p m (ZMod p)<GOAL>(zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) = (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) ((zmodEquivTrunc p m).symm x))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : TruncatedWittVector p m (ZMod p)<GOAL>(zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) = (truncate hm) ((zmodEquivTrunc p m) ((zmodEquivTrunc p m).symm x))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Subsingleton R<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Nontrivial R<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Nontrivial R<VAR>a✝ : Nontrivial S<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Nontrivial R<VAR>a✝ : Nontrivial S<VAR>this✝ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra<VAR>this : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := Algebra.toSMul<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Nontrivial R<VAR>a✝ : Nontrivial S<VAR>this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra<VAR>this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := Algebra.toSMul<VAR>this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Nontrivial R<VAR>a✝ : Nontrivial S<VAR>this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra<VAR>this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := Algebra.toSMul<VAR>this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin ↥A ↑B)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Nontrivial R<VAR>a✝ : Nontrivial S<VAR>this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra<VAR>this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := Algebra.toSMul<VAR>this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥(restrictScalars R (Algebra.adjoin ↥A ↑B))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<VAR>h✝ : Nontrivial R<VAR>a✝ : Nontrivial S<VAR>this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra<VAR>this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := Algebra.toSMul<VAR>this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)<GOAL>Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin R (↑A ∪ ↑B))
<VAR>α : Type u_1<VAR>inst✝¹ : Neg α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : α<GOAL>(equivShrink α) (-x) = -(equivShrink α) x
<VAR>α : Type u_1<VAR>inst✝¹ : Neg α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : α<GOAL>(equivShrink α) (-x) = (equivShrink α).symm.symm (-(equivShrink α).symm ((equivShrink α) x))
<VAR>α : Type u<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b c : α<GOAL>a⁻¹ < a ↔ 1 < a
<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 n' : ℤ<VAR>hn' : n + a = n'<VAR>x : R<VAR>p q : ℤ<VAR>hpq : p + n' = q<GOAL>((x • γ).leftShift a n' hn').v p q hpq = x • (γ.leftShift a n' hn').v p q hpq
<VAR>n : ℕ<VAR>IH : n.multichoose 1 = n<GOAL>(n + 1).multichoose 1 = n + 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<GOAL>Injective ⇑(castHom ⋯ R)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<GOAL>∀ (a : ZMod n), (castHom ⋯ R) a = 0 → a = 0
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<VAR>x : ZMod n<GOAL>(castHom ⋯ R) x = 0 → x = 0
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<VAR>k : ℤ<GOAL>(castHom ⋯ R) ↑k = 0 → ↑k = 0
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<VAR>k : ℤ<GOAL>↑n ∣ k → ↑n ∣ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hg : ∀ (b : δ), IsLUB (range fun i => f i b) (g b)<GOAL>Measurable g