ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>α₁ : Type u<VAR>α₂ : Type v<VAR>β₁ : Type w<VAR>β₂ : Type x<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>m₁ : α₁ → β₁<VAR>m₂ : α₂ → β₂<VAR>s : Set (β₁ × β₂)<VAR>hs : (fun p => (m₁ p.1, m₂ p.2)) ⁻¹' s ∈ f₁ ×ˢ f₂<VAR>s₁ : Set α₁<VAR>hs₁ : s₁ ∈ f₁<VAR>s₂ : Set α₂<VAR>hs₂ : s₂ ∈ f₂<VAR>h : s₁ ×ˢ s₂ ⊆ (fun p => (m₁ p.1, m₂ p.2)) ⁻¹' s<GOAL>(m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>s : Set α<VAR>h : q.s ⊆ s<GOAL>s ∪ q.s = s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<GOAL>x = ↑(unitCoeff hx) * ↑p ^ x.valuation.natAbs
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<GOAL>(fun a => ↑a) x = (fun a => ↑a) (↑(unitCoeff hx) * ↑p ^ x.valuation.natAbs)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>hx : x ≠ 0<VAR>repr : ↑x = ↑↑(unitCoeff hx) * ↑p ^ x.valuation<GOAL>↑p ^ x.valuation.natAbs = ↑p ^ x.valuation
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<GOAL>0 ∈ lifts 0
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<GOAL>(List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) 0).sum = 0
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<GOAL>[].sum = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>s ∈ coclosedCompact X ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<GOAL>LiftRel R s t.think ↔ LiftRel R s t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<GOAL>Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.think.destruct ↔ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝¹ : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n k : ℕ<VAR>hn : ∀ (m : ℕ), n + k ≤ m → p m = 0<VAR>x✝ : ℕ<VAR>hm : n ≤ x✝<GOAL>n + k ≤ k + x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝¹ : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n k : ℕ<VAR>hn : ∀ (m : ℕ), n + k ≤ m → p m = 0<VAR>x✝ : ℕ<VAR>hm : n ≤ x✝<GOAL>k + n ≤ k + x✝
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<VAR>h : a ≠ 0<VAR>g : G₀<GOAL>(fun g => a * g) (a⁻¹ * g) = g
<VAR>t : ↑I<GOAL>1 / 2 ≤ ↑(σ t) ↔ ↑t ≤ 1 / 2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : LinearWeights R L M<VAR>χ✝ : L → R<VAR>inst✝ : IsNoetherian R M<VAR>χ : Weight R L M<GOAL>∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : LinearWeights R L M<VAR>χ✝ : L → R<VAR>inst✝ : IsNoetherian R M<VAR>χ : Weight R L M<VAR>hχ : Nontrivial ↥↑(shiftedWeightSpace R L M ⇑χ)<GOAL>∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : LinearWeights R L M<VAR>χ✝ : L → R<VAR>inst✝ : IsNoetherian R M<VAR>χ : Weight R L M<VAR>hχ : Nontrivial ↥↑(shiftedWeightSpace R L M ⇑χ)<VAR>m : M<VAR>property✝ : m ∈ ↑(shiftedWeightSpace R L M ⇑χ)<VAR>hm₁ : ⟨m, property✝⟩ ∈ ↑(maxTrivSubmodule R L ↥↑(shiftedWeightSpace R L M ⇑χ))<VAR>hm₂ : ⟨⟨m, property✝⟩, hm₁⟩ ≠ 0<GOAL>∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : LinearWeights R L M<VAR>χ✝ : L → R<VAR>inst✝ : IsNoetherian R M<VAR>χ : Weight R L M<VAR>hχ : Nontrivial ↥↑(shiftedWeightSpace R L M ⇑χ)<VAR>m : M<VAR>property✝ : m ∈ ↑(shiftedWeightSpace R L M ⇑χ)<VAR>hm₁✝ : ⟨m, property✝⟩ ∈ ↑(maxTrivSubmodule R L ↥↑(shiftedWeightSpace R L M ⇑χ))<VAR>hm₂ : ⟨⟨m, property✝⟩, hm₁✝⟩ ≠ 0<VAR>hm₁ : ∀ (x : L), ⁅x, m⁆ = χ x • m<GOAL>∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.snd (𝒰.map j ≫ f) g = pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g
<VAR>R : 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>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hst : s =ᶠ[ae μ] t<GOAL>s.indicator f =ᶠ[ae μ] t.indicator f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>se : SplitEpi f<VAR>F : C ⥤ D<GOAL>F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)
<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<VAR>inst✝ : Semiring T<VAR>s : A → A → Prop<GOAL>Function.Surjective ⇑(mkAlgHom S s)
<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<VAR>inst✝ : Semiring T<VAR>s : A → A → Prop<GOAL>Function.Surjective fun x => { toQuot := Quot.mk (Rel s) x }
<VAR>n : ℕ<VAR>l : List ℕ<VAR>h₁ : l.prod = n<VAR>h₂ : ∀ p ∈ l, Prime p<GOAL>l ~ n.primeFactorsList
<VAR>n : ℕ<VAR>l : List ℕ<VAR>h₁ : l.prod = n<VAR>h₂ : ∀ p ∈ l, Prime p<GOAL>l.prod = n.primeFactorsList.prod
<VAR>n : ℕ<VAR>l : List ℕ<VAR>h₁ : l.prod = n<VAR>h₂ : ∀ p ∈ l, Prime p<GOAL>∀ p ∈ l, _root_.Prime p
<VAR>n : ℕ<VAR>l : List ℕ<VAR>h₁ : l.prod = n<VAR>h₂ : ∀ p ∈ l, Prime p<GOAL>∀ p ∈ n.primeFactorsList, _root_.Prime p
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : (ZMod p)ˣ<GOAL>a ^ (p - 1) = 1
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>Tendsto (fun x => rexp (f x)) l atTop ↔ Tendsto f l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f : α → β<VAR>p : α → Prop<GOAL>EventuallyConst p l ↔ (p =ᶠ[l] fun x => False) ∨ p =ᶠ[l] fun x => True
<VAR>D : GlueData<VAR>x y : ↑(∐ D.U)<VAR>h : (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv) x = (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv) y<GOAL>EqvGen (Types.CoequalizerRel ⇑D.diagram.fstSigmaMap ⇑D.diagram.sndSigmaMap) x y
<VAR>D : GlueData<VAR>x y : ↑(∐ D.U)<VAR>h : (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 x = (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 y<GOAL>EqvGen (Types.CoequalizerRel ⇑D.diagram.fstSigmaMap ⇑D.diagram.sndSigmaMap) x y
<VAR>D : GlueData<VAR>x y : ↑(∐ D.U)<VAR>h : (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 x = (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 y<VAR>diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat<GOAL>EqvGen (Types.CoequalizerRel ⇑D.diagram.fstSigmaMap ⇑D.diagram.sndSigmaMap) x y
<VAR>D : GlueData<VAR>x y : ↑(∐ D.U)<VAR>h : (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 x = (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 y<VAR>diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat<VAR>this : colimit.ι diagram one x = colimit.ι diagram one y<GOAL>EqvGen (Types.CoequalizerRel ⇑D.diagram.fstSigmaMap ⇑D.diagram.sndSigmaMap) x y
<VAR>D : GlueData<VAR>x y : ↑(∐ D.U)<VAR>h : (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 x = (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 y<VAR>diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat<VAR>this✝ : colimit.ι diagram one x = colimit.ι diagram one y<VAR>this : (colimit.ι diagram one ≫ colim.map (diagramIsoParallelPair diagram).hom ≫ (colimit.isoColimitCocone (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))).hom) x = (colimit.ι diagram one ≫ colim.map (diagramIsoParallelPair diagram).hom ≫ (colimit.isoColimitCocone (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right))).hom) y<GOAL>EqvGen (Types.CoequalizerRel ⇑D.diagram.fstSigmaMap ⇑D.diagram.sndSigmaMap) x y
<VAR>D : GlueData<VAR>x y : ↑(∐ D.U)<VAR>h : (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 x = (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap).1 y<VAR>diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat<VAR>this✝ : colimit.ι diagram one x = colimit.ι diagram one y<VAR>this : (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right)).cocone.ι.app one x = (Types.coequalizerColimit (diagram.map WalkingParallelPairHom.left) (diagram.map WalkingParallelPairHom.right)).cocone.ι.app one y<GOAL>EqvGen (Types.CoequalizerRel ⇑D.diagram.fstSigmaMap ⇑D.diagram.sndSigmaMap) x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n✝ : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (a * g)<VAR>h_inv : ∀ (a : G), P a → P (a * g⁻¹)<VAR>n : ℤ<GOAL>P (g ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (a * g)<VAR>h_inv : ∀ (a : G), P a → P (a * g⁻¹)<GOAL>P (g ^ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n✝ : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (a * g)<VAR>h_inv : ∀ (a : G), P a → P (a * g⁻¹)<VAR>n : ℕ<VAR>ih : P (g ^ ↑n)<GOAL>P (g ^ (↑n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n✝ : ℤ<VAR>g : G<VAR>P : G → Prop<VAR>h_one : P 1<VAR>h_mul : ∀ (a : G), P a → P (a * g)<VAR>h_inv : ∀ (a : G), P a → P (a * g⁻¹)<VAR>n : ℕ<VAR>ih : P (g ^ (-↑n))<GOAL>P (g ^ (-↑n - 1))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝³ : CommRing A<VAR>S : Submonoid A<VAR>hS✝ : S ≤ A⁰<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>hS : S ≤ A⁰<VAR>s : ↥S<GOAL>IsUnit ((algebraMap A K) ↑s)
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<GOAL>ListBlank.modifyNth (fun a => (a.1, f a.2)) n (addBottom L) = addBottom (ListBlank.modifyNth f n L)
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n✝ : ℕ<GOAL>ListBlank.cons (true, L.head) (ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)) = ListBlank.cons (true, L.head) (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail))
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n✝ : ℕ<GOAL>ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail) = ListBlank.modifyNth (fun a => (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n✝ : ℕ<GOAL>∀ (x : (k : K) → Option (Γ k)), { f := Prod.mk false, map_pt' := ⋯ }.f (f x) = (({ f := Prod.mk false, map_pt' := ⋯ }.f x).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x).2)
<VAR>r p : ℝ≥0<VAR>h : p ≠ 0<GOAL>r ≤ p⁻¹ ↔ r * p ≤ 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hf : Function.Surjective ⇑f<VAR>tG : IsTorsion G<VAR>h : H<VAR>g : G<VAR>hg : f g = h<GOAL>IsOfFinOrder (f g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<VAR>hg : ContDiffAt ℝ n g x<VAR>hne : f x ≠ g x<GOAL>ContDiffAt ℝ n (fun y => ‖f y - g y‖) x
<VAR>x y : ℂ<GOAL>sinh (x + y) = sinh x * cosh y + cosh x * sinh y
<VAR>x y : ℂ<GOAL>(cexp x - cexp (-x)) * (cexp y + cexp (-y)) + (cexp x + cexp (-x)) * (cexp y - cexp (-y)) = 2 * (cexp x * cexp y - cexp (-x) * cexp (-y))
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : ι → ℙ K V<VAR>u v : ℙ K V<GOAL>Independent ![u, v] ↔ u ≠ v
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))<VAR>this : NumberField K<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))<VAR>this : NumberField K<GOAL>(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ 2 ^ k - 1)) = (algebraMap ℤ ℚ) ((-2) ^ 2 ^ k)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition n<VAR>i : Fin (l.splitWrtComposition c).length<GOAL>(l.splitWrtComposition c).get i = drop (c.sizeUpTo ↑i) (take (c.sizeUpTo (↑i + 1)) l)
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>T : Type u_2<VAR>inst✝ : Category.{?u.3840, u_2} T<VAR>X✝ Y✝ : HomologicalComplex (T ⥤ V) c<VAR>f : X✝ ⟶ Y✝<VAR>t t' : T<VAR>g : t ⟶ t'<VAR>i : ι<GOAL>(((fun C => C.asFunctor) X✝).map g ≫ (fun t => { f := fun i => (f.f i).app t, comm' := ⋯ }) t').f i = ((fun t => { f := fun i => (f.f i).app t, comm' := ⋯ }) t ≫ ((fun C => C.asFunctor) Y✝).map g).f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : α<VAR>ab : b ∈ pure a<VAR>c : α<VAR>ac : c ∈ pure a<GOAL>b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : α<VAR>ab : b = a<VAR>c : α<VAR>ac : c = a<GOAL>b = c
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>ι : Type u_1<VAR>m : ι → ↥M<VAR>hm : LinearIndependent R m<GOAL>LinearMap.ker (mulLeftMap N m) = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>ι : Type u_1<VAR>m : ι → ↥M<VAR>hm : LinearIndependent R m<GOAL>Function.Injective ⇑(mulLeftMap N m)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>ι : Type u_1<VAR>m : ι → ↥M<VAR>hm : LinearIndependent R m<GOAL>Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.total ι (↥M) R m)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥N<VAR>ι : Type u_1<VAR>m : ι → ↥M<VAR>hm : Function.Injective ⇑(Finsupp.total ι (↥M) R m)<GOAL>Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.total ι (↥M) R m)))
<VAR>x y z : ℝ<VAR>f g : ℝ → ℝ<VAR>f' g' : ℝ<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<VAR>h : 0 < f x<GOAL>HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x)) x
<VAR>x y z : ℝ<VAR>f g : ℝ → ℝ<VAR>f' g' : ℝ<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<VAR>h : 0 < f x<GOAL>f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x) = ((((fun x => (f x, g x)) x).2 * ((fun x => (f x, g x)) x).1 ^ (((fun x => (f x, g x)) x).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (((fun x => (f x, g x)) x).1 ^ ((fun x => (f x, g x)) x).2 * log ((fun x => (f x, g x)) x).1) • ContinuousLinearMap.snd ℝ ℝ ℝ) (f', g')
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>l : Filter X<GOAL>l ×ˢ 𝓝ˢ K = ⨆ y ∈ K, l ×ˢ 𝓝 y
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>f : β → α<GOAL>(∃ C, ∀ ⦃x : α⦄, x ∈ range f → ∀ ⦃y : α⦄, y ∈ range f → dist x y ≤ C) ↔ ∃ C, ∀ (x y : β), dist (f x) (f y) ≤ C
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁴ : CommRing R₁<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>M : Matrix ι ι R₁<VAR>b : Basis ι R₁ M₁<GOAL>((toLinearMap₂ b b) M).SeparatingLeft ↔ M.Nondegenerate
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NormedDivisionRing α<VAR>a : α<GOAL>(𝓝[≠] 0)⁻¹ = cobounded α
<VAR>n m : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<GOAL>p.predAbove i.rev = (p.rev.predAbove i).rev
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<GOAL>IsNoetherianRing A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>I : Ideal A<GOAL>Submodule.FG I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>I : Ideal A<VAR>hI : ¬I = ⊥<GOAL>Submodule.FG I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>I : Ideal A<VAR>hI✝ : ¬I = ⊥<VAR>hI : ↑I ≠ 0<GOAL>Submodule.FG I
<VAR>R✝ : Type u<VAR>a✝ b : R✝<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q : R✝[X]<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>a : R[ℕ]<GOAL>{ toFinsupp := -a } = Polynomial.neg { toFinsupp := a }
<VAR>E : Type u_1<VAR>inst✝ : SeminormedGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<VAR>hs : IsBounded s<VAR>ht : IsBounded t<VAR>Rs : ℝ<VAR>hRs : ∀ x ∈ s, ‖x‖ ≤ Rs<VAR>Rt : ℝ<VAR>hRt : ∀ x ∈ t, ‖x‖ ≤ Rt<GOAL>IsBounded (s * t)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<VAR>hs : IsBounded s<VAR>ht : IsBounded t<VAR>Rs : ℝ<VAR>hRs : ∀ x ∈ s, ‖x‖ ≤ Rs<VAR>Rt : ℝ<VAR>hRt : ∀ x ∈ t, ‖x‖ ≤ Rt<GOAL>∀ x ∈ s * t, ‖x‖ ≤ Rs + Rt
<VAR>E : Type u_1<VAR>inst✝ : SeminormedGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x✝ y✝ : E<VAR>hs : IsBounded s<VAR>ht : IsBounded t<VAR>Rs : ℝ<VAR>hRs : ∀ x ∈ s, ‖x‖ ≤ Rs<VAR>Rt : ℝ<VAR>hRt : ∀ x ∈ t, ‖x‖ ≤ Rt<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ t<GOAL>‖(fun x x_1 => x * x_1) x y‖ ≤ Rs + Rt
<VAR>p a b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>padicValNat p (a ^ n) = n * padicValNat p a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<GOAL>∑ a ∈ s.toFinset, count a s = card s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝¹ : Encodable α<VAR>inst✝ : Inhabited α<VAR>x : α<GOAL>(fun n => (decode n).iget) (encode x) = x