ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<GOAL>∀ (c_1 : 𝕜), c • x ∈ c_1 • s → ↑‖c‖₊ * egauge 𝕜 s x ≤ ↑‖c_1‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y✝ : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<VAR>a : 𝕜<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : (fun x => a • x) y = c • x<GOAL>↑‖c‖₊ * egauge 𝕜 s x ≤ ↑‖a‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y✝ : E<VAR>r : ℝ≥0∞<VAR>s : Set E<VAR>x : E<VAR>a : 𝕜<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : (fun x => a • x) y = 0 • x<GOAL>↑‖0‖₊ * egauge 𝕜 s x ≤ ↑‖a‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y✝ : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<VAR>a : 𝕜<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : (fun x => a • x) y = c • x<VAR>hc : c ≠ 0<GOAL>↑‖c‖₊ * egauge 𝕜 s x ≤ ↑‖a‖₊
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ : S₁ ⟶ S₂<VAR>φ₂ : S₂ ⟶ S₃<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>h₃ : S₃.LeftHomologyData<VAR>γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂<VAR>γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃<GOAL>cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>h : IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)<GOAL>IntervalIntegrable f volume a b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : StrictOrderedSemiring R<VAR>a x y : R<VAR>n m : ℕ<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<VAR>hn : 1 < n<GOAL>a ^ n < a
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : Integrable (fun x => rexp (f x)) μ<VAR>g : α → ℝ<GOAL>(μ.tilted f).tilted g = μ.tilted (f + g)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : Fintype ↑G.edgeSet<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsEulerian<VAR>e : Sym2 V<GOAL>e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeFinset
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>rk : α → ℕ<VAR>s : Set α<GOAL>s.PartiallyWellOrderedOn r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>rk : α → ℕ<VAR>s : Set α<GOAL>(∃ x, IsBadSeq r s x) ↔ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x y : α<GOAL>dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))
<VAR>K : Type u_1<VAR>R : 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✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ✝ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>x : L<VAR>χ : L → R<GOAL>LieSubmodule.map (weightSpaceOf M (χ x) x).incl (weightSpace (↥↑(weightSpaceOf M (χ x) x)) χ) = weightSpace M χ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>edist (f n) a ≤ C * r ^ n / (1 - r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ : L[[α]].Sentence<GOAL>{p | φ ∈ p} = Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ : L[[α]].Sentence<GOAL>{p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅
<VAR>m✝ n✝ m n : ℕ<GOAL>IsUnit ↑m ↔ m.Coprime n
<VAR>m✝ n✝ m n : ℕ<VAR>H : IsUnit ↑m<GOAL>m.Coprime n
<VAR>m✝ n✝ m n : ℕ<VAR>H : IsUnit ↑m<VAR>H' : (↑H.unit).val.Coprime n<GOAL>m.Coprime n
<VAR>m✝ n✝ m n : ℕ<VAR>H : IsUnit ↑m<VAR>H' : (m % n).gcd n = 1<GOAL>m.Coprime n
<VAR>m✝ n✝ m n : ℕ<VAR>H : IsUnit ↑m<VAR>H' : (m % n).gcd n = 1<GOAL>n.gcd m = (m % n).gcd n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_6<VAR>A B C : Matrix m n α<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>v : m → α<VAR>w : n → α<GOAL>v ᵥ* A ⊙ B ⬝ᵥ w = (diagonal v * A * (B * diagonal w)ᵀ).trace
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_6<VAR>A B C : Matrix m n α<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R α<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>v : m → α<VAR>w : n → α<GOAL>v ᵥ* A ⊙ B ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v * A) ⊙ (B * diagonal w)) x y
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w : Fin 3 → R<GOAL>u ⬝ᵥ (crossProduct v) w = det ![u, v, w]
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>u v w : Fin 3 → R<GOAL>u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 + u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 + u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 = ![u, v, w] 0 0 * ![u, v, w] 1 1 * ![u, v, w] 2 2 - ![u, v, w] 0 0 * ![u, v, w] 1 2 * ![u, v, w] 2 1 - ![u, v, w] 0 1 * ![u, v, w] 1 0 * ![u, v, w] 2 2 + ![u, v, w] 0 1 * ![u, v, w] 1 2 * ![u, v, w] 2 0 + ![u, v, w] 0 2 * ![u, v, w] 1 0 * ![u, v, w] 2 1 - ![u, v, w] 0 2 * ![u, v, w] 1 1 * ![u, v, w] 2 0
<VAR>α : Type u<VAR>inst✝⁴ : DecidableEq α<VAR>β : Type v<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Fintype β<VAR>e : Perm α<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<GOAL>sign (e.extendDomain f) = sign e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>ht : autoParam t.Finite _auto✝<GOAL>s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>lift b.fst b.snd ≫ desc b.inl b.inr = 𝟙 b.pt
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>desc b.inl b.inr ≫ lift b.fst b.snd = 𝟙 (X ⊞ Y)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>n : ℕ<GOAL>(opRingEquiv R) (op (C r * X ^ n)) = C (op r) * X ^ n
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(bind₁ 0) (wittPolynomial p R n) = 0
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>∑ i ∈ range n, x ^ i / ↑i ! ≤ CauSeq.lim ⟨fun n => (↑(exp' ↑x) n).re, ⋯⟩
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<VAR>n j : ℕ<VAR>hj : j ≥ n<GOAL>↑(const _root_.abs (∑ i ∈ range n, x ^ i / ↑i !)) j ≤ ↑⟨fun n => (↑(exp' ↑x) n).re, ⋯⟩ j
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<VAR>n j : ℕ<VAR>hj : j ≥ n<GOAL>∑ i ∈ range n, x ^ i / ↑i ! ≤ ∑ i ∈ range j, (↑x ^ i / ↑i !).re
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<VAR>n j : ℕ<VAR>hj : j ≥ n<GOAL>∑ i ∈ range n, x ^ i / ↑i ! ≤ ∑ i ∈ range j, x ^ i / ↑i !
<VAR>x✝³ y x : ℝ<VAR>hx : 0 ≤ x<VAR>n j : ℕ<VAR>hj : j ≥ n<VAR>x✝² : ℕ<VAR>x✝¹ : x✝² ∈ range j<VAR>x✝ : x✝² ∉ range n<GOAL>0 ≤ x ^ x✝² / ↑x✝²!
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>CauSeq.lim ⟨fun n => (↑(exp' ↑x) n).re, ⋯⟩ = rexp x
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u v : U<VAR>g : Lex (Γ' × Γ)<GOAL>((of R).symm ((fun u => (of R) (A.compHahnSeries B u).ofIterate) (u + v))).coeff g = ((of R).symm ((fun u => (of R) (A.compHahnSeries B u).ofIterate) u + (fun u => (of R) (A.compHahnSeries B u).ofIterate) v)).coeff g
<VAR>Γ✝ : Type u_1<VAR>inst✝¹⁴ : PartialOrder Γ✝<VAR>R✝ : Type u_2<VAR>V✝ : Type u_3<VAR>W✝ : Type u_4<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : AddCommGroup V✝<VAR>inst✝¹¹ : Module R✝ V✝<VAR>inst✝¹⁰ : AddCommGroup W✝<VAR>inst✝⁹ : Module R✝ W✝<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>inst✝⁸ : OrderedCancelAddCommMonoid Γ<VAR>inst✝⁷ : OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>inst✝⁵ : AddCommGroup U<VAR>inst✝⁴ : Module R U<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>r : R<VAR>x : U<VAR>g : Lex (Γ' × Γ)<GOAL>((of R).symm ({ toFun := fun u => (of R) (A.compHahnSeries B u).ofIterate, map_add' := ⋯ }.toFun (r • x))).coeff g = ((of R).symm ((RingHom.id R) r • { toFun := fun u => (of R) (A.compHahnSeries B u).ofIterate, map_add' := ⋯ }.toFun x)).coeff g
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>E : Type u_2<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>f = (p.prodEquivOfIsCompl (ker f) ⋯).conj (id.prodMap 0)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>E : Type u_2<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] E<VAR>h : IsProj p f<GOAL>f = (↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0) ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯).symm
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>hdiv : p ∣ k<GOAL>IsPrimitiveRoot (ζ ^ p) (k / p)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>hdiv : p ∣ k<GOAL>orderOf (ζ ^ p) = k / p
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>x₀ : X<VAR>hA : EquicontinuousAt (u ∘ Subtype.val) x₀<VAR>hu : Continuous u<GOAL>EquicontinuousAt (u ∘ Subtype.val) x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → X → α<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀<VAR>hu : Continuous u<GOAL>EquicontinuousWithinAt (u ∘ Subtype.val) univ x₀
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j : J<GOAL>1 = M.mk F ⟨j, 1⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j : J<GOAL>∃ k f g, (F.map f) ⟨⋯.some, 1⟩.snd = (F.map g) ⟨j, 1⟩.snd
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>hf : Martingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f j ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>hf : Martingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f i ω ∂μ = ∫ (x : Ω) in s, (μ[f j|↑ℱ i]) x ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>hf : Martingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : Ω) ∂μ, x ∈ s → f i x = (μ[f j|↑ℱ i]) x
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{u_14, u_1} C₁<VAR>inst✝⁵ : Category.{u_13, u_2} C₂<VAR>inst✝⁴ : Category.{u_12, u_3} C₃<VAR>inst✝³ : Category.{u_11, u_4} C₄<VAR>inst✝² : Category.{?u.63581, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.63585, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>Y : C₄<VAR>j : J<VAR>inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j), ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ'<GOAL>φ = φ'
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁶ : Category.{u_14, u_1} C₁<VAR>inst✝⁵ : Category.{u_13, u_2} C₂<VAR>inst✝⁴ : Category.{u_12, u_3} C₃<VAR>inst✝³ : Category.{u_11, u_4} C₄<VAR>inst✝² : Category.{?u.63581, u_5} C₁₂<VAR>inst✝¹ : Category.{?u.63585, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>p : I₁ × I₂ × I₃ → J<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>Y : C₄<VAR>j : J<VAR>inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p<VAR>φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j), ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ'<GOAL>∀ (i : I₁ × I₂ × I₃) (hij : p i = j), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p i j hij ≫ φ = ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p i j hij ≫ φ'
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>Subsingleton α ∨ Nontrivial α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>Nontrivial α ∨ ¬Nontrivial α
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>u v : ℙ K V<VAR>h : u.submodule = v.submodule<GOAL>u = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : ℙ K V<VAR>u : V<VAR>hu : u ≠ 0<VAR>h : (mk K u hu).submodule = v.submodule<GOAL>mk K u hu = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>u : V<VAR>hu : u ≠ 0<VAR>v : V<VAR>hv : v ≠ 0<VAR>h : (mk K u hu).submodule = (mk K v hv).submodule<GOAL>mk K u hu = mk K v hv
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>u : V<VAR>hu : u ≠ 0<VAR>v : V<VAR>hv : v ≠ 0<VAR>h : ∃ z, z • u = v<GOAL>mk K u hu = mk K v hv
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (regionBetween f g s)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 < a_1} ∩ {a_1 | a_1 < g a.1}})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G✝ H : SimpleGraph α<VAR>n : ℕ<VAR>a b c : α<VAR>s✝ : Finset α<VAR>G : SimpleGraph α<VAR>s : Finset α<GOAL>s ∈ G.cliqueSet 1 ↔ s ∈ Set.range singleton
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ✝ : R →+* A<VAR>C : VariableChange R<VAR>φ : R →+* A<VAR>hφ : Function.Injective ⇑φ<VAR>x✝¹ x✝ : VariableChange R<VAR>h✝ : map φ x✝¹ = map φ x✝<VAR>h : (Units.map ↑φ) x✝¹.u = (Units.map ↑φ) x✝.u<VAR>left✝¹ : φ x✝¹.r = φ x✝.r<VAR>left✝ : φ x✝¹.s = φ x✝.s<VAR>right✝ : φ x✝¹.t = φ x✝.t<GOAL>x✝¹ = x✝
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ✝ : R →+* A<VAR>C : VariableChange R<VAR>φ : R →+* A<VAR>hφ : Function.Injective ⇑φ<VAR>x✝¹ x✝ : VariableChange R<VAR>h✝ : map φ x✝¹ = map φ x✝<VAR>left✝¹ : φ x✝¹.r = φ x✝.r<VAR>left✝ : φ x✝¹.s = φ x✝.s<VAR>right✝ : φ x✝¹.t = φ x✝.t<VAR>h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u<GOAL>x✝¹ = x✝
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∑ t ∈ filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k), f t = ∑ A ∈ powersetCard k univ, ∑ j ∈ A, f (A, j)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∀ (p : Finset σ × σ), p ∈ filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k) ↔ p.1 ∈ powersetCard k univ ∧ p.2 ∈ p.1
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f : ι → Ω → ℝ<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f j ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f : ι → Ω → ℝ<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (x : Ω) in s, (μ[f j|↑ℱ i]) x ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f : ι → Ω → ℝ<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>μ[f j|↑ℱ i] ≤ᶠ[ae μ] f i
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>mabs a = mabs b ↔ a = b ∨ a = b⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : mabs a = mabs b<GOAL>a = b ∨ a = b⁻¹
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>s t : Submodule R M<GOAL>Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<VAR>s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<GOAL>x ∈ corootSpace α ↔ x ∈ Submodule.span R s
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<VAR>s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<GOAL>⇑H.subtype '' s = {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<VAR>s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<VAR>u : L<GOAL>u ∈ ⇑H.subtype '' s ↔ u ∈ {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>α : ↥H → R<VAR>x : ↥H<VAR>s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}<VAR>u : L<GOAL>(∃ (x : u ∈ H), ⟨u, ⋯⟩ ∈ {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}) ↔ ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u