ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α✝ : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>x y : G<VAR>i : ℤ<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>hx : x ∈ zpowers y<VAR>a : α<VAR>hs : y • a = a<GOAL>x • a = a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α✝ : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>y : G<VAR>i : ℤ<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>hs : y • a = a<VAR>k : ℤ<VAR>hx : y ^ k ∈ zpowers y<GOAL>y ^ k • a = a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α✝ : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>y : G<VAR>i : ℤ<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>hs : y • a = a<VAR>k : ℤ<VAR>hx : y ^ k ∈ zpowers y<GOAL>(MulAction.toPerm y ^ k) a = a
<VAR>a b c d m n : ℤ<VAR>p : ℤ → Prop<VAR>i : ℤ<VAR>hz : p 0<VAR>hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)<VAR>hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)<GOAL>p i
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.6722<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>fderivWithin 𝕜 (fun y => c + f y) s x = fderivWithin 𝕜 f s x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Semifield S<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra S A<VAR>inst✝² : IsScalarTower R S A<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSpace S<VAR>a : A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>h_cpct : CompactSpace ↑(spectrum S a)<GOAL>CompactSpace ↑(spectrum R a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Semifield S<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra S A<VAR>inst✝² : IsScalarTower R S A<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSpace S<VAR>a : A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>h_cpct : IsCompact (spectrum S a)<GOAL>IsCompact (spectrum R a)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - 1 * W.Ψ₃ ^ 3 * 1) * W.Ψ₃ * 1 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<GOAL>((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.total R R) b) ∘ₗ algEquivMatrix'.symm.toLinearMap) 1 = (PiToModule.fromEnd R b) 1
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<GOAL>((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.total R R) b)) 1 = (PiToModule.fromEnd R b) 1
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>A ↓∩ ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, A ↓∩ B = x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>A ↓∩ ⋂₀ S = ⋂ x ∈ S, A ↓∩ x
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ ↑n
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ n
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ (-↑(n + 1))
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ (n + 1)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>p✝ : α✝ → Prop<VAR>f✝ : (a : α✝) → p✝ a → β✝<VAR>x✝ : Option α✝<VAR>α : Type u_5<VAR>β γ : Type u_6<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>g : β → Option γ<VAR>H : ∀ (a : α), a ∈ x → p a<GOAL>pmap f x H >>= g = x.pbind fun a h => g (f a ⋯)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>φ : L[[α]].Sentence<VAR>hf : Formula.not φ ∈ p<VAR>ht : φ ∈ p<GOAL>False
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>φ : L[[α]].Sentence<VAR>hf : Formula.not φ ∈ p<VAR>ht : φ ∈ p<VAR>h : ¬{φ, Formula.not φ}.IsSatisfiable<GOAL>False
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>φ : L[[α]].Sentence<VAR>hf : Formula.not φ ∈ p<VAR>ht : φ ∈ p<VAR>h : ¬{φ, Formula.not φ}.IsSatisfiable<GOAL>{φ, Formula.not φ} ⊆ ↑p
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>φ : L[[α]].Sentence<VAR>hf : Formula.not φ ∈ p<VAR>ht : φ ∈ p<VAR>h : ¬{φ, Formula.not φ}.IsSatisfiable<GOAL>φ ∈ ↑p ∧ Formula.not φ ∈ ↑p
<VAR>R : Type<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R[X] K<VAR>inst✝ : IsFractionRing R[X] K<VAR>f g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>c d : R[X]<VAR>hcd : c * g₁ + d * g₂ = 1<GOAL>∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
<VAR>R : Type<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R[X] K<VAR>inst✝ : IsFractionRing R[X] K<VAR>f g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>c d : R[X]<VAR>hcd : c * g₁ + d * g₂ = 1<GOAL>↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
<VAR>R : Type<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R[X] K<VAR>inst✝ : IsFractionRing R[X] K<VAR>f g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>c d : R[X]<VAR>hcd : c * g₁ + d * g₂ = 1<VAR>hg₁' : ↑g₁ ≠ 0<GOAL>↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
<VAR>R : Type<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R[X] K<VAR>inst✝ : IsFractionRing R[X] K<VAR>f g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>c d : R[X]<VAR>hcd : c * g₁ + d * g₂ = 1<VAR>hg₁' : ↑g₁ ≠ 0<VAR>hg₂' : ↑g₂ ≠ 0<GOAL>↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
<VAR>R : Type<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R[X] K<VAR>inst✝ : IsFractionRing R[X] K<VAR>f g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>c d : R[X]<VAR>hcd : c * g₁ + d * g₂ = 1<VAR>hg₁' : ↑g₁ ≠ 0<VAR>hg₂' : ↑g₂ ≠ 0<VAR>hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c<GOAL>↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
<VAR>R : Type<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R[X] K<VAR>inst✝ : IsFractionRing R[X] K<VAR>f g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>c d : R[X]<VAR>hcd : c * g₁ + d * g₂ = 1<VAR>hg₁' : ↑g₁ ≠ 0<VAR>hg₂' : ↑g₂ ≠ 0<VAR>hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c<VAR>hfd : f * d %ₘ g₁ + g₁ * (f * d /ₘ g₁) = f * d<GOAL>↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂
<VAR>R : Type<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R[X] K<VAR>inst✝ : IsFractionRing R[X] K<VAR>f g₁ g₂ : R[X]<VAR>hg₁ : g₁.Monic<VAR>hg₂ : g₂.Monic<VAR>c d : R[X]<VAR>hcd : c * g₁ + d * g₂ = 1<VAR>hg₁' : ↑g₁ ≠ 0<VAR>hg₂' : ↑g₂ ≠ 0<VAR>hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c<VAR>hfd : f * d %ₘ g₁ + g₁ * (f * d /ₘ g₁) = f * d<GOAL>f = ((f * d /ₘ g₁ + f * c /ₘ g₂) * g₁ + f * d %ₘ g₁) * g₂ + f * c %ₘ g₂ * g₁
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ f : Perm α<VAR>h : f.IsThreeCycle<GOAL>f⁻¹.IsThreeCycle
<VAR>f✝ g f g₁ g₂ : CircleDeg1Lift<VAR>h : Semiconj ⇑f ⇑g₁ ⇑g₂<GOAL>dist (g₁ 0) (f (g₁ 0) - f 0) + dist (f (g₁ 0) - f 0) (g₂ 0) = dist (f 0 + g₁ 0) (f (g₁ 0)) + dist (g₂ 0 + f 0) (g₂ (f 0))
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<GOAL>∫ (v : V), cexp (-b * ↑‖v‖ ^ 2) = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<GOAL>⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⇔ b = ⊥ ↔ IsCompl a b
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<VAR>P : Set X → Prop := IsCompact<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>k : Set X<VAR>k_comp : IsCompact k<VAR>k_closed : IsClosed k<VAR>sk : s ⊆ interior k<VAR>kt : k ⊆ tᶜ<VAR>P : Set X → Prop := IsCompact<VAR>c : Urysohns.CU P := { C := k, U := tᶜ, P_C := k_comp, closed_C := k_closed, open_U := ⋯, subset := kt, hP := ⋯ }<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>K : IntermediateField F E<VAR>S : Set E<GOAL>restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)
<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>m : ℕ<VAR>f : α → ℕ<VAR>h₁ : ∀ x ∈ s, f x = m<GOAL>∑ x ∈ s, f x = s.card * m
<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>m : ℕ<VAR>f : α → ℕ<VAR>h₁ : ∀ x ∈ s, f x = m<GOAL>∑ x ∈ s, f x = ∑ _x ∈ s, m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t
<GOAL>#Cardinal.{u} = univ.{u, u + 1}
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<GOAL>P.StableUnderBaseChange
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<GOAL>(sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).StableUnderBaseChange
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<VAR>this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).IsLocal := HasAffineProperty.isLocal_affineProperty P<GOAL>(sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).StableUnderBaseChange
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<VAR>this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).IsLocal := HasAffineProperty.isLocal_affineProperty P<GOAL>∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => Q) g → sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => Q) (pullback.fst f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<VAR>this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).IsLocal := HasAffineProperty.isLocal_affineProperty P<VAR>X Y S : Scheme<VAR>inst✝¹ : IsAffine S<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => Q) g<GOAL>sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => Q) (pullback.fst f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<VAR>this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).IsLocal := HasAffineProperty.isLocal_affineProperty P<VAR>X Y S : Scheme<VAR>inst✝¹ : IsAffine S<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P g<GOAL>P (pullback.fst f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<VAR>this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).IsLocal := HasAffineProperty.isLocal_affineProperty P<VAR>X S : Scheme<VAR>inst✝¹ : IsAffine S<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ S<VAR>Y : Scheme<VAR>g : Y ⟶ S<VAR>H : P g<VAR>hX : IsAffine Y<GOAL>P (pullback.fst f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<VAR>this : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q).IsLocal := HasAffineProperty.isLocal_affineProperty P<VAR>X S : Scheme<VAR>inst✝¹ : IsAffine S<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ S<VAR>Y : Scheme<VAR>g : Y ⟶ S<VAR>H : Q (Scheme.Hom.app g ⊤)<VAR>hX : IsAffine Y<GOAL>Q (Scheme.Hom.app (pullback.fst f g) ⊤)
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>(⊤ * a).toReal = 0
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>ha : a < a'<VAR>hb : b < b'<VAR>h₀✝ : 0 ≤ r<VAR>h₁ : r ≤ 1<VAR>h₀ : 0 < r<GOAL>(lineMap a b) r < (lineMap a' b') r
<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>E' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>v : E'<GOAL>‖(toSesqForm f) v‖ ≤ ‖f‖ * ‖v‖
<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>E' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>v : E'<VAR>x : E<GOAL>‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖
<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>E' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>v : E'<VAR>x : E<VAR>h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖<GOAL>‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖
<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>E' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace 𝕜 E'<VAR>f : E →L[𝕜] E'<VAR>v : E'<VAR>x : E<VAR>h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖<VAR>h₂ : ‖⟪v, f x⟫_𝕜‖ ≤ ‖v‖ * ‖f x‖<GOAL>‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : LinearOrder R<VAR>g : α → R<VAR>F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}<GOAL>{t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}.Countable
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : LinearOrder R<VAR>g : α → R<VAR>F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}<GOAL>{t | μ {a | t ≤ g a} ≠ μ {a | t < g a}} ⊆ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : LinearOrder R<VAR>g : α → R<VAR>F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}<VAR>t : R<VAR>ht : t ∈ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}<GOAL>t ∈ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : LinearOrder R<VAR>g : α → R<VAR>F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}<VAR>t : R<VAR>ht : t ∈ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}<VAR>this : μ {a | t < g a} < μ {a | t ≤ g a}<GOAL>t ∈ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing T<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>F : Type u_6<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : Nontrivial S<VAR>pb : PowerBasis K S<VAR>hf : Splits (algebraMap K F) (minpoly K pb.gen)<GOAL>(algebraMap K F) ((Algebra.trace K S) pb.gen) = ((minpoly K pb.gen).aroots F).sum
<VAR>R : Type u₁<VAR>inst✝¹ : CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(coeff R p (n + 1)) (f ^ p) = (coeff R p n) f
<VAR>R : Type u₁<VAR>inst✝¹ : CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(coeff R p (n + 1)) f ^ p = (coeff R p n) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : α → Fin n<GOAL>(Primrec fun a => ↑(f a)) ↔ Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : α → Fin n<VAR>this : Primcodable { a // id a < n } := Primcodable.subtype ⋯<GOAL>(Primrec fun a => ↑(f a)) ↔ Primrec f
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>N₁ N₂ : ℕ<VAR>hN₁ : N ≤ N₁<VAR>hN₁' : f N₁ ω < a<VAR>hN₂ : N₁ ≤ N₂<VAR>hN₂' : b < f N₂ ω<GOAL>upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>N₁ N₂ : ℕ<VAR>hN₁ : N ≤ N₁<VAR>hN₁' : f N₁ ω < a<VAR>hN₂ : N₁ ≤ N₂<VAR>hN₂' : b < f N₂ ω<GOAL>(upcrossingsBefore a b f N ω).succ ∈ {n | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>N₁ N₂ : ℕ<VAR>hN₁ : N ≤ N₁<VAR>hN₁' : f N₁ ω < a<VAR>hN₂ : N₁ ≤ N₂<VAR>hN₂' : b < f N₂ ω<GOAL>∃ j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>N₁ N₂ : ℕ<VAR>hN₁ : N ≤ N₁<VAR>hN₁' : f N₁ ω < a<VAR>hN₂ : N₁ ≤ N₂<VAR>hN₂' : b < f N₂ ω<GOAL>lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N₂
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>N₁ N₂ : ℕ<VAR>hN₁ : N ≤ N₁<VAR>hN₁' : f N₁ ω < a<VAR>hN₂ : N₁ ≤ N₂<VAR>hN₂' : b < f N₂ ω<GOAL>∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>N₁ N₂ : ℕ<VAR>hN₁ : N ≤ N₁<VAR>hN₁' : f N₁ ω < a<VAR>hN₂ : N₁ ≤ N₂<VAR>hN₂' : b < f N₂ ω<GOAL>upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>f : M → ι<VAR>i : ι<VAR>a : R[M]<GOAL>a ∈ gradeBy R f i ↔ ↑a.support ⊆ f ⁻¹' {i}