ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : o → Matrix m n α<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>i✝ : m × o<VAR>j✝ : n × o<GOAL>(blockDiagonal M).map f i✝ j✝ = blockDiagonal (fun k => (M k).map f) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>M : o → Matrix m n α<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>i✝ : m × o<VAR>j✝ : n × o<GOAL>f (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>r : M<GOAL>r ∉ M⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.even.get n.succ = s.get (2 * n).succ.succ
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s : Stream' α<GOAL>s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>Integrable (fun x => x ^ s * rexp (-b * x ^ 2)) volume
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume ∧ IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>IntegrableOn ((fun x => x ^ s * rexp (-b * x ^ 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>IntegrableOn (fun x => (-x) ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>AEStronglyMeasurable (fun x => (-x) ^ s * rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>s : ℝ<VAR>hs : -1 < s<GOAL>∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>f : Filter α<VAR>g h : Set α → Filter β<GOAL>(f.lift fun x => g x ⊓ h x) = f.lift g ⊓ f.lift h
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c✝ d✝ : α<VAR>h : a ≤ b<VAR>δ c d : α<VAR>hdc : d ≤ c<GOAL>|↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c✝ d✝ : α<VAR>h : a ≤ b<VAR>δ c d : α<VAR>hdc : d ≤ c<GOAL>(fun a_1 => ↑a_1) (projIcc a b h c) - (fun a_1 => ↑a_1) (projIcc a b h d) ≤ c - d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c✝ d✝ : α<VAR>h : a ≤ b<VAR>δ c d : α<VAR>hdc : 0 ≤ c - d<GOAL>(fun a_1 => ↑a_1) (projIcc a b h c) - (fun a_1 => ↑a_1) (projIcc a b h d) ≤ c - d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c✝ d✝ : α<VAR>h : a ≤ b<VAR>δ c d : α<VAR>hdc : 0 ≤ c - d<GOAL>min b c - min b d ≤ c - d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c✝ d✝ : α<VAR>h : a ≤ b<VAR>δ c d : α<VAR>hdc : 0 ≤ c - d<GOAL>|b - b| ≤ c - d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c✝ d✝ : α<VAR>h : a ≤ b<VAR>δ c d : α<VAR>hdc : 0 ≤ c - d<GOAL>|c - d| ≤ c - d
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<GOAL>x ∈ ↑(nonZeroDivisorsRight M₀) ↔ x ∈ {x | x ≠ 0}
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<GOAL>(∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<VAR>h : ∀ (y : M₀), x = 0 ∨ y = 0 → y = 0<GOAL>x ≠ 0
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<VAR>h : x = 0<GOAL>∃ y, (x = 0 ∨ y = 0) ∧ y ≠ 0
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>n : Type w<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>a : R<VAR>Q : QuadraticMap R (n → R) R<GOAL>(a • Q).toMatrix' = a • Q.toMatrix'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝¹ : One F<VAR>inst✝ : NormOneClass F<VAR>_x : α<GOAL>0 ≤ ‖1‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝¹ : One F<VAR>inst✝ : NormOneClass F<GOAL>(∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖1‖ ≤ ‖f x‖) ↔ ∀ (n : ℕ), True → ∀ᶠ (x : α) in l, ‖f x‖ ∈ Ici ↑n
<VAR>V : Type u<VAR>inst✝² : Quiver V<VAR>V' : Type u'<VAR>inst✝¹ : Quiver V'<VAR>V'' : Type u''<VAR>inst✝ : Quiver V''<VAR>φ : V ⥤q V'<VAR>φ' : V' ⥤q V''<GOAL>lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')
<VAR>V : Type u<VAR>inst✝² : Quiver V<VAR>V' : Type u'<VAR>inst✝¹ : Quiver V'<VAR>V'' : Type u''<VAR>inst✝ : Quiver V''<VAR>φ : V ⥤q V'<VAR>φ' : V' ⥤q V''<GOAL>of V ⋙q (lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')).toPrefunctor = φ ⋙q φ' ⋙q of V''
<VAR>α β : DistLat<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget DistLat).obj α<GOAL>({ toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : DistLat<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget DistLat).obj β<GOAL>({ toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Ioc ↑a ↑b = Ioc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g✝ g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)<VAR>y : β<VAR>hy : y ∈ t<VAR>t' : Set β<VAR>g : ↑s → ↑t'<VAR>htt' : t ⊆ t'<VAR>hg : Surjective g<VAR>hfg : ∀ (x : ↑s), f ↑x = ↑(g x)<VAR>x : ↑s<VAR>hx : g x = ⟨y, ⋯⟩<GOAL>f ↑x = y
<VAR>A B : TopCat<VAR>x₀ : ↑(π.obj A)<VAR>x₁ : ↑(π.obj B)<GOAL>{ obj := fun g => { as := (g.1.as, g.2.as) }, map := fun {x y} p => match x, y, p with | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.map (𝟙 (x₀, x₁)) = 𝟙 ({ obj := fun g => { as := (g.1.as, g.2.as) }, map := fun {x y} p => match x, y, p with | (x₀, x₁), (y₀, y₁), (p₀, p₁) => Path.Homotopic.prod p₀ p₁ }.obj (x₀, x₁))
<VAR>A B : TopCat<VAR>x₀ : ↑(π.obj A)<VAR>x₁ : ↑(π.obj B)<GOAL>Path.Homotopic.prod (𝟙 x₀) (𝟙 x₁) = 𝟙 { as := (x₀.as, x₁.as) }
<VAR>a✝ b c d m✝ n✝ : ℤ<VAR>m n : ℕ<VAR>a : ℤ<VAR>h : ↑n = ↑m * a<GOAL>m ∣ n
<VAR>a✝ b c d m n✝ : ℤ<VAR>n : ℕ<VAR>a : ℤ<VAR>h : ↑n = ↑0 * a<GOAL>0 ∣ n
<VAR>a✝ b c d m✝ n✝ : ℤ<VAR>m n : ℕ<VAR>a : ℤ<VAR>h : ↑n = ↑m * a<VAR>hm : m > 0<GOAL>m ∣ n
<VAR>a✝ b c d m✝ n✝ : ℤ<VAR>m n : ℕ<VAR>a : ℤ<VAR>h : ↑n = ↑m * a<VAR>hm : m > 0<VAR>ha : 0 ≤ a<GOAL>m ∣ n
<VAR>a✝ b c d m✝ n : ℤ<VAR>m a : ℕ<GOAL>↑m ∣ ↑(m * a)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<GOAL>p.support.card ≤ p.natDegree + 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<GOAL>p.support.card ≤ (range (p.natDegree + 1)).card
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>f : OnePoint X → Y<VAR>x : X<GOAL>ContinuousAt f ↑x ↔ ContinuousAt (f ∘ some) x
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>f : OnePoint X → Y<VAR>x : X<GOAL>Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<GOAL>leRec refl le_succ_of_le ⋯ = refl
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<GOAL>a / b ≤ a / c ↔ c ≤ b
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>i : ι<GOAL>(mk s 0) i = 0 i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>i : ι<GOAL>(if H : i ∈ s then 0 ⟨i, H⟩ else 0) = 0 i
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>g : γ → δ<VAR>f' : β' → α → δ<VAR>g' : β → β'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a<GOAL>g '' image2 f ↑s ↑t = image2 f' (g' '' ↑t) ↑s
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>h : e.source = univ<VAR>h' : e.target = univ<VAR>x : X<GOAL>x ∈ univ
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>h : e.source = univ<VAR>h' : e.target = univ<VAR>x : Y<GOAL>x ∈ univ
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>h : e.source = univ<VAR>h' : e.target = univ<GOAL>Continuous { toFun := ↑e, invFun := ↑e.symm, left_inv := ⋯, right_inv := ⋯ }.toFun
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>h : e.source = univ<VAR>h' : e.target = univ<GOAL>Continuous { toFun := ↑e, invFun := ↑e.symm, left_inv := ⋯, right_inv := ⋯ }.invFun
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>1 ∈ s / t ↔ ¬Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → β<VAR>hf : Integrable f μ<VAR>h : Integrable (f + g) μ<GOAL>g = f + g + -f
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>hRA : FiniteType R A<VAR>f : A →ₐ[R] B<VAR>hf : Surjective ⇑f<GOAL>⊤.FG
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>hRA : FiniteType R A<VAR>f : A →ₐ[R] B<VAR>hf : Surjective ⇑f<GOAL>⊤ = Subalgebra.map f ⊤
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Iio a ↔ x ∈ Iio (r • a)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y < a, r * y = x) ↔ x < r * a
<VAR>c : ℝ<GOAL>IntegrableOn rexp (Iic c) volume
<VAR>c y : ℝ<VAR>x✝ : y ∈ Iic 0<GOAL>∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c
<VAR>c y : ℝ<VAR>x✝ : y ∈ Iic 0<GOAL>0 ≤ rexp (id y)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C a * X ^ 2 + C b * X + C c).leadingCoeff = a
<VAR>z : ℤ<GOAL>(↑z).sign = ↑z.sign
<VAR>z : ℤ<VAR>hn : z < 0<GOAL>(↑z).sign = ↑z.sign
<VAR>z : ℤ<VAR>hp : 0 < z<GOAL>(↑z).sign = ↑z.sign
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c ≠ 0<VAR>hd : d ≠ 0<GOAL>(a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<VAR>y✝ : α i.succ<VAR>z : α 0<VAR>inst✝ : (i : Fin (n + 1)) → Preorder (α i)<VAR>x₀ y₀ : α 0<VAR>x y : (i : Fin n) → α i.succ<GOAL>(∀ (i : Fin n), cons x₀ x i.succ ≤ cons y₀ y i.succ) ↔ x ≤ y
<VAR>n' : Type u_1<VAR>inst✝³ : DecidableEq n'<VAR>inst✝² : Fintype n'<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : StarRing R<VAR>A : M<VAR>n : ℕ<GOAL>(A ^ ↑n)ᴴ = Aᴴ ^ ↑n
<VAR>n' : Type u_1<VAR>inst✝³ : DecidableEq n'<VAR>inst✝² : Fintype n'<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : StarRing R<VAR>A : M<VAR>n : ℕ<GOAL>(A ^ -[n+1])ᴴ = Aᴴ ^ -[n+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>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i<GOAL>Supermartingale f 𝒢 μ
<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>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i<GOAL>Supermartingale (- -f) 𝒢 μ
<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>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i<VAR>i : ℕ<GOAL>(-f) i ≤ᶠ[ae μ] -μ[f (i + 1)|↑𝒢 i]
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ n ≠ 0<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : p = 0<VAR>hn0 : ¬n = 0<GOAL>(p ^ n).natDegree = n * p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ n ≠ 0<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : p = 0<VAR>hn0 : ¬n = 0<GOAL>natDegree 0 = n * natDegree 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ n ≠ 0<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hpn0 : p ^ n = 0<VAR>h1 : p.leadingCoeff ^ n ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : 0 ≠ 0<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hpn0 : p ^ n = 0<VAR>h1 : p.leadingCoeff ^ n ≠ 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ n ≠ 0<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hpn : p ^ n ≠ 0<GOAL>↑(p ^ n).natDegree = ↑(n * p.natDegree)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ n ≠ 0<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hpn : p ^ n ≠ 0<GOAL>n • ↑p.natDegree = ↑(n * p.natDegree)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s t : Finset α<GOAL>insert a s ∪ t = insert a (s ∪ t)
<VAR>n : ℕ<GOAL>(cycleRange 2).IsThreeCycle
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP (fun x => true) l = l.length
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>∀ (a : α), a ∈ l → true = true
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>x : M<GOAL>x ∈ ↑(lieSpan R L s) ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>x : M<GOAL>x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s : Set α<VAR>μ : Measure α<VAR>hm : m ≤ m0<GOAL>(μ.trim hm).toOuterMeasure = μ.trim
<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>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b<VAR>hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b<VAR>hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b<VAR>hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b<VAR>val✝¹ : α₁<VAR>val✝ : β₁<GOAL>sumLexLift f₁ f₂ g₁ g₂ (inl val✝¹) (inl val✝) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val✝¹) (inl val✝)
<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>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b<VAR>hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b<VAR>hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b<VAR>hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b<VAR>val✝¹ : α₁<VAR>val✝ : β₂<GOAL>sumLexLift f₁ f₂ g₁ g₂ (inl val✝¹) (inr val✝) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val✝¹) (inr val✝)
<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>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b<VAR>hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b<VAR>hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b<VAR>hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b<VAR>val✝¹ : α₂<VAR>val✝ : β₁<GOAL>sumLexLift f₁ f₂ g₁ g₂ (inr val✝¹) (inl val✝) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val✝¹) (inl val✝)
<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>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b<VAR>hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b<VAR>hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b<VAR>hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b<VAR>val✝¹ : α₂<VAR>val✝ : β₂<GOAL>sumLexLift f₁ f₂ g₁ g₂ (inr val✝¹) (inr val✝) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val✝¹) (inr val✝)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>xᶜ = y ↔ yᶜ = x
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hy : 0 < y<GOAL>x < logb b y ↔ b ^ x < y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>n : ℕ<GOAL>toMultiset (∑ i ∈ s, single i n) = n • s.val
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>coborder s = s ∪ (frontier s)ᶜ