ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>x y : E<GOAL>‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : IsCofilteredOrEmpty J<GOAL>InitiallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)<GOAL>InitiallySmall J
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>s : Set J<VAR>hs : Small.{v, u} ↑s<VAR>hs' : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)<GOAL>InitiallySmall J
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>h : s₁.Equivalent s₂<GOAL>s₁.length = s₂.length
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ : M<VAR>f : M → M'<VAR>g : M → M''<VAR>x : M<VAR>hf : MDifferentiableAt I I' f x<VAR>hg : MDifferentiableAt I I'' g x<GOAL>mfderiv I (I'.prod I'') (fun x => (f x, g x)) x = (mfderiv I I' f x).prod (mfderiv I I'' g x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasLineDerivAt 𝕜 f f' x v<VAR>c : 𝕜<GOAL>HasLineDerivAt 𝕜 f (c • f') x (c • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>h : HasLineDerivWithinAt 𝕜 f f' univ x v<GOAL>HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>count a s ≤ count a (fold max 0 (map (fun a => count a s) s) • s.dedup)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>count a s ≤ fold max 0 (map (fun a => count a s) s) * count a s.dedup
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>H.relindex ⊤ = H.index
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : 𝓞 K<VAR>w : InfinitePlace K<VAR>h₁ : x ≠ 0<VAR>h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1<VAR>h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1<GOAL>Algebra.adjoin ℚ {↑x} = ⊤
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : 𝓞 K<VAR>w : InfinitePlace K<VAR>h₁ : x ≠ 0<VAR>h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1<VAR>h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1<GOAL>ℚ⟮↑x⟯.toSubalgebra = ⊤
<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✝ : LinearOrderedField R<VAR>A : Matrix m n R<VAR>x : n → R<GOAL>x ∈ LinearMap.ker (Aᵀ * A).mulVecLin ↔ x ∈ LinearMap.ker A.mulVecLin
<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✝ : LinearOrderedField R<VAR>A : Matrix m n R<VAR>x : n → R<GOAL>Aᵀ *ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>a✝ : Nontrivial R<GOAL>IsOpen {x | IsUnit x}
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>a✝ : Nontrivial R<GOAL>∀ x ∈ {x | IsUnit x}, ∃ ε > 0, Metric.ball x ε ⊆ {x | IsUnit x}
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>a✝ : Nontrivial R<VAR>x : Rˣ<GOAL>∃ ε > 0, Metric.ball (↑x) ε ⊆ {x | IsUnit x}
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>a✝ : Nontrivial R<VAR>x : Rˣ<VAR>y : R<VAR>hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹<GOAL>y ∈ {x | IsUnit x}
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>a✝ : Nontrivial R<VAR>x : Rˣ<VAR>y : R<VAR>hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹<GOAL>y ∈ {x | IsUnit x}
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝ : ∀ (i : ι), IsTrichotomous (β i) s<VAR>wf : WellFounded r<VAR>a b : (i : ι) → β i<GOAL>Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝ : ∀ (i : ι), IsTrichotomous (β i) s<VAR>wf : WellFounded r<VAR>a b : (i : ι) → β i<VAR>hab : a = b<GOAL>Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝ : ∀ (i : ι), IsTrichotomous (β i) s<VAR>wf : WellFounded r<VAR>a b : (i : ι) → β i<VAR>hab : a ≠ b<GOAL>Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : Filter α<VAR>s : Set α<GOAL>Disjoint (𝓟 s) f ↔ sᶜ ∈ f
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>n : ℤ<GOAL>bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>bernoulliFourierCoeff k 0 = -↑k ! / (2 * ↑π * I * ↑0) ^ k
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>bernoulliFourierCoeff 1 n = -↑1! / (2 * ↑π * I * ↑n) ^ 1
<VAR>k✝ : ℕ<VAR>hk✝ : k✝ ≠ 0<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>k : ℕ<VAR>hk : 1 ≤ k<VAR>h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k<GOAL>bernoulliFourierCoeff (k + 1) n = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
<VAR>α β : Type u<VAR>c : Cardinal.{?u.229352}<VAR>f : α → β<VAR>s : Set β<VAR>h : Injective f<GOAL>#↑(f ⁻¹' s) ≤ #↑s
<VAR>α β : Type u<VAR>c : Cardinal.{?u.229352}<VAR>f : α → β<VAR>s : Set β<VAR>h : Injective f<GOAL>lift.{u, u} #↑(f ⁻¹' s) ≤ lift.{u, u} #↑s
<VAR>x✝ y✝ z✝ w x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hw : w ≠ 0<VAR>h : y + z = w<GOAL>x ^ w = x ^ y * x ^ z
<VAR>x✝ y✝ z✝ w x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hw : w ≠ 0<VAR>h : y + z = w<GOAL>y + z ≠ 0
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<VAR>hp✝ : x * x - Pell.d a1 * y * y = 1<VAR>hp : 0 - Pell.d a1 * y * y = 1<GOAL>1 ≤ { re := ↑0, im := ↑y }
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<VAR>hp✝ : x * x - Pell.d a1 * y * y = 1<VAR>hp : 0 = 1<GOAL>1 ≤ { re := ↑0, im := ↑y }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>f ^ n ∈ 𝒜 (m * n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>f ^ n ∈ 𝒜 (n * m)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>a ∈ carrier f_deg q ↔ HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>(HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ^ m ∈ q.asIdeal) = (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ^ m = HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>HomogeneousLocalization.val (HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ^ m) = (HomogeneousLocalization.mk { deg := m * (n * m), num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ (n * m), ⋯⟩, den_mem := ⋯ }).val
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>Localization.mk (a ^ m) (⟨f ^ n, ⋯⟩ ^ m) = Localization.mk (a ^ m) ⟨(f ^ n) ^ m, ⋯⟩
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x ≤ 1<GOAL>0 ≤ x.negMulLog
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w✝ : σ → M<VAR>n : M<VAR>φ✝ ψ : MvPolynomial σ R<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>m : M<GOAL>(weightedHomogeneousComponent w m) φ ∈ weightedHomogeneousSubmodule R w m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w✝ : σ → M<VAR>n : M<VAR>φ✝ ψ : MvPolynomial σ R<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>m : M<GOAL>IsWeightedHomogeneous w ((weightedHomogeneousComponent w m) φ) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>x : α<GOAL>(insert x s).encard ≤ s.encard + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>x : α<GOAL>(s ∪ {x}).encard ≤ s.encard + {x}.encard
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>a : ↥(𝒜 0)<GOAL>↑((projZeroRingHom' 𝒜) ↑a) = ↑a
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<GOAL>map₂ f p q = span R (image2 (fun m n => (f m) n) ↑p ↑q)
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<VAR>ι : Type u_3<VAR>b : Basis ι K V<GOAL>Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>ι : Type u_3<VAR>h : Infinite ι<VAR>b : Basis ι K V<GOAL>Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>ι : Type u_3<VAR>h : Infinite ι<VAR>b : Basis ι K V<VAR>e : (V →ₗ[K] K) ≃ₗ[K] ι → K<GOAL>Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>ι : Type u_3<VAR>h : Infinite ι<VAR>b : Basis ι K V<VAR>e : (V →ₗ[K] K) ≃ₗ[K] ι → K<GOAL>Module.rank K (ι → K) = #(ι → K)
<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>f✝ f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f' : α → γ → δ'<VAR>g' : β → δ' → ε<VAR>h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)<GOAL>image2 f s (image2 g t u) = image2 g' t (image2 f' s u)
<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>f✝ f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f' : α → γ → δ'<VAR>g' : β → δ' → ε<VAR>h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)<GOAL>image2 (fun a b => f b a) (image2 g t u) s = image2 g' t (image2 (fun a b => f' b a) u s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<GOAL>(p.bindOnSupport fun a x => pure a) = p
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>M : Matrix ι ι ℝ<VAR>hM : M.det ≠ 0<GOAL>Measure.map (⇑(toLin' M)) volume = ofReal |M.det⁻¹| • volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>M : Matrix ι ι ℝ<VAR>hM : M.det ≠ 0<GOAL>∀ (D : ι → ℝ), (Matrix.diagonal D).det ≠ 0 → Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = ofReal |(Matrix.diagonal D).det⁻¹| • volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>M : Matrix ι ι ℝ<VAR>hM : M.det ≠ 0<GOAL>∀ (t : TransvectionStruct ι ℝ), Measure.map (⇑(toLin' t.toMatrix)) volume = ofReal |t.toMatrix.det⁻¹| • volume
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>M : Matrix ι ι ℝ<VAR>hM : M.det ≠ 0<GOAL>∀ (A B : Matrix ι ι ℝ), A.det ≠ 0 → B.det ≠ 0 → Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume → Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume → Measure.map (⇑(toLin' (A * B))) volume = ofReal |(A * B).det⁻¹| • volume
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>X₁ X₂ : C<VAR>inst✝¹ : HasBinaryProduct X₁ X₂<VAR>inst✝ : PreservesLimit (pair X₁ X₂) (forget C)<VAR>x : (forget C).obj X₁ × (forget C).obj X₂<GOAL>prod.snd ((prodEquiv X₁ X₂).symm x) = x.2
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>X₁ X₂ : C<VAR>inst✝¹ : HasBinaryProduct X₁ X₂<VAR>inst✝ : PreservesLimit (pair X₁ X₂) (forget C)<VAR>y : (forget C).obj (X₁ ⨯ X₂)<GOAL>prod.snd ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).2
<VAR>x y : ℝ<VAR>a b : Cauchy abs<GOAL>({ cauchy := a } - { cauchy := b }).cauchy = { cauchy := a }.cauchy - { cauchy := b }.cauchy
<VAR>x y : ℝ<VAR>a b : Cauchy abs<GOAL>({ cauchy := a } - { cauchy := b }).cauchy = ({ cauchy := a } + -{ cauchy := b }).cauchy
<VAR>m n✝ n : ℕ<VAR>u : (ZMod n)ˣ<GOAL>↑u * (↑u)⁻¹ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : Ring β<VAR>abv : β → α<VAR>inst✝² : IsAbsoluteValue abv<VAR>G : Type u_3<VAR>inst✝¹ : SMul G β<VAR>inst✝ : IsScalarTower G β β<VAR>f1 f2 : CauSeq β abv<VAR>c : G<VAR>hf : f1 ≈ f2<GOAL>c • f1 ≈ c • f2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>p : α → Bool<VAR>a : List α<VAR>l : List (List α)<GOAL>countP p (a :: l).join = (map (countP p) (a :: l)).sum
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u v u' v' : V<VAR>p✝ : G.Walk u v<VAR>p : G.Walk u u<VAR>hinj : Injective ⇑f<GOAL>(Walk.map f p).IsCycle ↔ p.IsCycle
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>finj : Injective f<VAR>a : α<VAR>l : List α<VAR>this : (fun x => a == x) = fun x => f a == f x<GOAL>map f (l.erase a) = (map f l).erase (f a)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>finj : Injective f<VAR>a : α<VAR>l : List α<VAR>this : (fun x => a == x) = fun x => f a == f x<GOAL>map f (eraseP (fun x => f a == f x) l) = map f (eraseP ((fun x => f a == x) ∘ f) l)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>hmn : m ≤ n<GOAL>hitting u s n m ω = m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>i : ι<VAR>ω : Ω<VAR>m : ι<VAR>hmn : m ≤ m<GOAL>hitting u s m m ω = m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>hmn : m ≤ n<VAR>h : m < n<GOAL>hitting u s n m ω = m
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.9360, u_1} C<VAR>A✝ B✝ X✝ Y✝ : C<VAR>f✝ : A✝ ⟶ X✝<VAR>i✝ : A✝ ⟶ B✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>g✝ : B✝ ⟶ Y✝<VAR>A B X Y : Cᵒᵖ<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>p.unop ≫ l.l.unop = g.unop
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.9360, u_1} C<VAR>A✝ B✝ X✝ Y✝ : C<VAR>f✝ : A✝ ⟶ X✝<VAR>i✝ : A✝ ⟶ B✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>g✝ : B✝ ⟶ Y✝<VAR>A B X Y : Cᵒᵖ<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<VAR>l : sq.LiftStruct<GOAL>l.l.unop ≫ i.unop = f.unop
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>a : Matrix n n 𝕜<VAR>ha : a.IsHermitian<VAR>x : ℝ<GOAL>x ∈ spectrum ℝ a ↔ x ∈ Set.range ha.eigenvalues
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>a : Matrix n n 𝕜<VAR>ha : a.IsHermitian<VAR>x : ℝ<GOAL>↑x ∈ Set.range (RCLike.ofReal ∘ ha.eigenvalues) ↔ x ∈ Set.range ha.eigenvalues
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x : ↑C<VAR>l : List (LocallyConstant ↑C ℤ)<GOAL>l.prod x = (List.map (⇑(LocallyConstant.evalMonoidHom x)) l).prod
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x : ↑C<VAR>l : List (LocallyConstant ↑C ℤ)<GOAL>l.prod x = (LocallyConstant.evalMonoidHom x) l.prod
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>x y : R<VAR>S : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>hf : Surjective ⇑f<GOAL>(ker f).IsRadical ↔ IsReduced S
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>x y : R<VAR>S : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>hf : Surjective ⇑f<GOAL>(ker f).IsRadical ↔ ∀ (x : R), (∃ n, x ^ n ∈ ker f) → x ∈ ker f
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>h : I ⊔ K = ⊤<GOAL>I ⊔ J * K = I ⊔ J
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>h : I ⊔ K = ⊤<GOAL>I ⊔ K * J = I ⊔ J
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : ¬p x = true<GOAL>takeWhile p (x :: l) = []
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F<VAR>X A : C<VAR>inst✝¹ : Nonempty ↑(F.obj X)<VAR>inst✝ : IsConnected A<VAR>f : X ⟶ A<GOAL>Function.Surjective (F.map f)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F<VAR>X A : C<VAR>inst✝¹ : Nonempty ↑(F.obj X)<VAR>inst✝ : IsConnected A<VAR>f : X ⟶ A<VAR>this : Epi f<GOAL>Function.Surjective (F.map f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>s : Set X<GOAL>Dense s ↔ ∀ (x : X), f x ∈ closure (f '' s)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>a b : α<VAR>h0 : f 0 = 0<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>ha0 : ¬a = 0<VAR>hb0 : ¬b = 0<VAR>hf1 : ¬f 1 = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) = f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ^ Multiset.count p (normalizedFactors a)) * f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ^ Multiset.count p (normalizedFactors b))