ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>h : 0 ∈ Set.Ioo 0 1<GOAL>False
<VAR>m n : ℤ<GOAL>bitwise and m n = m.land n
<VAR>m n : ℕ<GOAL>↑(Nat.bitwise (fun x y => !x && y) m n) = -[m+1].land (ofNat n)
<VAR>m n : ℕ<GOAL>-[Nat.bitwise (fun x y => !(!x && !y)) m n+1] = -[m+1].land -[n+1]
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>comap (↑(opLinearEquiv R).symm) 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ → δ<VAR>hg : Continuous (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>↑(comp₂ g hg f₁ f₂) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β → γ → δ<VAR>hg : Continuous (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m : WithBot ℕ<VAR>p : R[X]<VAR>h_deg_le : p.degree ≤ m<VAR>coeff_ne_zero : p.coeff (WithBot.unbot' 0 m) ≠ 0<GOAL>p.degree = m
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>h_deg_le : p.degree ≤ ⊥<VAR>coeff_ne_zero : p.coeff (WithBot.unbot' 0 ⊥) ≠ 0<GOAL>p.degree = ⊥
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m : WithBot ℕ<VAR>p : R[X]<VAR>h_deg_le : p.degree ≤ m<VAR>coeff_ne_zero : p.coeff (WithBot.unbot' 0 m) ≠ 0<VAR>hh : m ≠ ⊥<GOAL>p.degree = m
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<GOAL>mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧<GOAL>mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>this : mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr ((P F).wMk a f' f)⟧<GOAL>Setoid.r (wrepr ((P F).wMk a f' f)) ((P F).wMk a f' f)
<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>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>σ : Subalgebra R S<VAR>hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ<VAR>τ : Set T<VAR>t : T<VAR>ht : t ∈ adjoin S τ<GOAL>∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
<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>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>σ : Subalgebra R S<VAR>hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ<VAR>τ : Set T<VAR>t : T<VAR>ht : t ∈ adjoin S τ<GOAL>∀ x ∈ τ, ∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
<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>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>σ : Subalgebra R S<VAR>hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ<VAR>τ : Set T<VAR>t : T<VAR>ht : t ∈ adjoin S τ<GOAL>∀ (r : S), ∃ s ∈ σ, IsUnit s ∧ s • (algebraMap S T) r ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
<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>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>σ : Subalgebra R S<VAR>hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ<VAR>τ : Set T<VAR>t : T<VAR>ht : t ∈ adjoin S τ<GOAL>∀ (x y : T), (∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) → (∃ s ∈ σ, IsUnit s ∧ s • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) → ∃ s ∈ σ, IsUnit s ∧ s • (x + y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
<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>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>σ : Subalgebra R S<VAR>hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ<VAR>τ : Set T<VAR>t : T<VAR>ht : t ∈ adjoin S τ<GOAL>∀ (x y : T), (∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) → (∃ s ∈ σ, IsUnit s ∧ s • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) → ∃ s ∈ σ, IsUnit s ∧ s • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α<VAR>inst✝³ : UniformSpace β<VAR>inst✝² : LocallyCompactSpace α<VAR>inst✝¹ : CompactSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β → γ<VAR>x : α<VAR>U : Set α<VAR>hxU : U ∈ 𝓝 x<VAR>h : ContinuousOn (↿f) (U ×ˢ univ)<GOAL>TendstoUniformly f (f x) (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α<VAR>inst✝³ : UniformSpace β<VAR>inst✝² : LocallyCompactSpace α<VAR>inst✝¹ : CompactSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β → γ<VAR>x : α<VAR>U : Set α<VAR>hxU : U ∈ 𝓝 x<VAR>h : ContinuousOn (↿f) (U ×ˢ univ)<VAR>K : Set α<VAR>hxK : K ∈ 𝓝 x<VAR>hKU : K ⊆ U<VAR>hK : IsCompact K<GOAL>TendstoUniformly f (f x) (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : UniformSpace α<VAR>inst✝³ : UniformSpace β<VAR>inst✝² : LocallyCompactSpace α<VAR>inst✝¹ : CompactSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β → γ<VAR>x : α<VAR>U : Set α<VAR>hxU : U ∈ 𝓝 x<VAR>h : ContinuousOn (↿f) (U ×ˢ univ)<VAR>K : Set α<VAR>hxK : K ∈ 𝓝 x<VAR>hKU : K ⊆ U<VAR>hK : IsCompact K<VAR>this : UniformContinuousOn (↿f) (K ×ˢ univ)<GOAL>TendstoUniformly f (f x) (𝓝 x)
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<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>f : E' → F'<VAR>hf : ContDiff 𝕂 1 f<VAR>x : E'<GOAL>∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<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>f : E' → F'<VAR>hf✝ : ContDiff 𝕂 1 f<VAR>x : E'<VAR>K : ℝ≥0<VAR>t : Set E'<VAR>ht : t ∈ 𝓝 ?m.51584<VAR>hf : LipschitzOnWith K f t<GOAL>∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(Λ n)) s = -deriv (L 1) s / L 1 s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>x✝ : n ≠ 0<GOAL>↑(Λ n) = ((fun n => 1 ↑n) * fun n => ↑(Λ n)) n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>(closure s).Nonempty ↔ s.Nonempty
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : A ⊗[R] Matrix n n R<GOAL>invFun R A n ((toFunAlgHom R A n) M) = M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>hs₁ : IsChain r s<VAR>hs₂ : ¬IsMaxChain r s<GOAL>SuperChain r s (SuccChain r s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>hs₁ : IsChain r s<VAR>hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x<GOAL>SuperChain r s (SuccChain r s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t✝ : Set α<VAR>a b x y : α<VAR>hs₁ : IsChain r s<VAR>hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x<VAR>t : Set α<VAR>ht : IsChain r t<VAR>hst : s ⊆ t ∧ ¬s = t<GOAL>SuperChain r s (SuccChain r s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a✝ a₁ a₂ b✝ b₁ b₂ c d x a b : α<GOAL>Ι a b = Ι b a
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype o<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Field R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>A : Matrix m n R<VAR>x : n → R<GOAL>x ∈ LinearMap.ker (Aᴴ * A).mulVecLin ↔ x ∈ LinearMap.ker A.mulVecLin
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : LocallyCompactSpace H<GOAL>LocallyCompactSpace M
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : LocallyCompactSpace H<VAR>this : ∀ (x : M), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑(chartAt H x) x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target) fun s => ↑(chartAt H x).symm '' s<GOAL>LocallyCompactSpace M
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : LocallyCompactSpace H<VAR>this : ∀ (x : M), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑(chartAt H x) x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target) fun s => ↑(chartAt H x).symm '' s<GOAL>∀ (x : M) (i : Set H), i ∈ 𝓝 (↑(chartAt H x) x) ∧ IsCompact i ∧ i ⊆ (chartAt H x).target → IsCompact (↑(chartAt H x).symm '' i)
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : LocallyCompactSpace H<VAR>this : ∀ (x : M), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (↑(chartAt H x) x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target) fun s => ↑(chartAt H x).symm '' s<VAR>x : M<VAR>s : Set H<VAR>left✝ : s ∈ 𝓝 (↑(chartAt H x) x)<VAR>h₂ : IsCompact s<VAR>h₃ : s ⊆ (chartAt H x).target<GOAL>IsCompact (↑(chartAt H x).symm '' s)
<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>f g : ℝ → E<VAR>f' g' : E<VAR>x : ℝ<GOAL>HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun t => ⟪f t, g t⟫_𝕜) (⟪f x, g'⟫_𝕜 + ⟪f', g x⟫_𝕜) x
<VAR>α : Type u_1<VAR>inst✝³ : AddMonoidWithOne α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 2
<VAR>α : Type u_1<VAR>inst✝³ : AddMonoidWithOne α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 1 + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Finset α<GOAL>Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝²⁶ : CommSemiring S<VAR>inst✝²⁵ : Semiring R<VAR>inst✝²⁴ : CommSemiring R'<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Algebra S R<VAR>inst✝²¹ : Algebra S R'<VAR>inst✝²⁰ : Module S M<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁷ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹⁶ : IsScalarTower S R M<VAR>inst✝¹⁵ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝¹⁴ : Module R' M<VAR>inst✝¹³ : Module R'ᵐᵒᵖ M<VAR>inst✝¹² : IsCentralScalar R' M<VAR>inst✝¹¹ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra S A<VAR>inst✝⁸ : Algebra R' A<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R' N<VAR>inst✝⁵ : Module R'ᵐᵒᵖ N<VAR>inst✝⁴ : IsCentralScalar R' N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R' P<VAR>inst✝¹ : Module R'ᵐᵒᵖ P<VAR>inst✝ : IsCentralScalar R' P<VAR>f : M →ₗ[R'] N<VAR>g : N →ₗ[R'] P<GOAL>map (g ∘ₗ f) = (map g).comp (map f)
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝²⁶ : CommSemiring S<VAR>inst✝²⁵ : Semiring R<VAR>inst✝²⁴ : CommSemiring R'<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Algebra S R<VAR>inst✝²¹ : Algebra S R'<VAR>inst✝²⁰ : Module S M<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁷ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹⁶ : IsScalarTower S R M<VAR>inst✝¹⁵ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝¹⁴ : Module R' M<VAR>inst✝¹³ : Module R'ᵐᵒᵖ M<VAR>inst✝¹² : IsCentralScalar R' M<VAR>inst✝¹¹ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra S A<VAR>inst✝⁸ : Algebra R' A<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R' N<VAR>inst✝⁵ : Module R'ᵐᵒᵖ N<VAR>inst✝⁴ : IsCentralScalar R' N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R' P<VAR>inst✝¹ : Module R'ᵐᵒᵖ P<VAR>inst✝ : IsCentralScalar R' P<VAR>f : M →ₗ[R'] N<VAR>g : N →ₗ[R'] P<GOAL>∀ (m : M), (map (g ∘ₗ f)) (inr m) = ((map g).comp (map f)) (inr m)
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this : ω ^ e.repr ≤ (e.oadd n a).repr<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ ω ≤ (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<GOAL>∀ b' < ω, (ω ^ e.repr * ↑↑n + a.repr) ^ b' ≤ (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<VAR>this : (e.oadd n a).repr < ω ^ succ e.repr<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<VAR>this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr<GOAL>(ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<VAR>this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr<GOAL>(ω ^ succ e.repr) ^ b ≤ (ω ^ e.repr) ^ ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<VAR>this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr<GOAL>ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<VAR>this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr<GOAL>succ e.repr * b ≤ e.repr * ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h✝ : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<VAR>this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr<VAR>h : ω ≤ e.repr<GOAL>succ e.repr * b ≤ e.repr * ω
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>e0 : e.repr ≠ 0<VAR>n : ℕ+<VAR>h✝ : a.repr < ω ^ e.repr<VAR>No : (e.oadd n a).NF<VAR>this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr<VAR>b : Ordinal.{0}<VAR>l : b < ω<VAR>this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr<VAR>h : e.repr < ω<GOAL>succ e.repr * b ≤ e.repr * ω
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>aeSeqSet hf p ⊆ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>{x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}ᶜ ⊆ toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x✝ : α<VAR>hx : x✝ ∈ aeSeqSet hf p<VAR>i : ι<VAR>x : α<VAR>h : x ∈ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}<GOAL>x ∈ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}
<VAR>R : Type u_1<VAR>inst✝² : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝¹ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>inst✝ : NoZeroDivisors S<GOAL>ψ.Even ∨ ψ.Odd
<VAR>R : Type u_1<VAR>inst✝² : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝¹ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>inst✝ : NoZeroDivisors S<GOAL>ψ (-1) ^ 2 = 1
<VAR>a b c d m n : ℤ<VAR>h : a * b ∣ c<GOAL>b ∣ c / a
<VAR>b c d m n : ℤ<VAR>h : 0 * b ∣ c<GOAL>b ∣ c / 0
<VAR>a b c d m n : ℤ<VAR>h : a * b ∣ c<VAR>ha : a ≠ 0<GOAL>b ∣ c / a
<VAR>n : ℕ<GOAL>0 < fib n ↔ 0 < n
<VAR>L : Language<VAR>L' : Language<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<GOAL>(Language.mk₂ c f₁ f₂ r₁ r₂).card = lift.{v, u} #c + lift.{v, u} #f₁ + lift.{v, u} #f₂ + lift.{u, v} #r₁ + lift.{u, v} #r₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s✝ t u : Set α<VAR>a b : α<VAR>s : Set ι<VAR>h : InjOn f s<GOAL>(f '' s).Pairwise r ↔ s.Pairwise (r on f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g✝ : G<VAR>x✝ y z : α<VAR>s : Set α<VAR>g : β →ᵈ γ<VAR>f₁ f₂ : α →ᵈ β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>x : α<GOAL>g (f₁ x) = g (f₂ x)
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>d : K<GOAL>J / spanSingleton R₁⁰ d = spanSingleton R₁⁰ d⁻¹ * J
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>d : K<GOAL>J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>d : K<VAR>hd : ¬d = 0<GOAL>J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>d : K<VAR>hd : ¬d = 0<VAR>h_spand : spanSingleton R₁⁰ d ≠ 0<GOAL>J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>d : K<VAR>hd : ¬d = 0<VAR>h_spand : spanSingleton R₁⁰ d ≠ 0<GOAL>J / spanSingleton R₁⁰ d ≤ 1 / spanSingleton R₁⁰ d * J
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>d : K<VAR>hd : ¬d = 0<VAR>h_spand : spanSingleton R₁⁰ d ≠ 0<GOAL>1 / spanSingleton R₁⁰ d * J ≤ J / spanSingleton R₁⁰ d
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>c d : D<VAR>f : c ⟶ d<GOAL>f ∈ (im φ hφ).arrows c d ↔ ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>c d : D<VAR>f : c ⟶ d<VAR>x✝⁴ x✝³ : C<VAR>x✝² : x✝⁴ ⟶ x✝³<VAR>x✝¹ : φ.obj x✝⁴ = c<VAR>x✝ : φ.obj x✝³ = d<GOAL>f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝ ↔ ∃ (_ : x✝² ∈ ⊤.arrows x✝⁴ x✝³), f = eqToHom ⋯ ≫ φ.map x✝² ≫ eqToHom x✝
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p 0) x = x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))<GOAL>AEMeasurable f μ