ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>r : MonoidAlgebra k G<VAR>m : RestrictScalars k (MonoidAlgebra k G) M<GOAL>((ofModule M).asAlgebraHom r) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>r : MonoidAlgebra k G<VAR>m : RestrictScalars k (MonoidAlgebra k G) M<GOAL>∀ (g : G), ((ofModule M).asAlgebraHom ((of k G) g)) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm ((of k G) g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>r : MonoidAlgebra k G<VAR>m : RestrictScalars k (MonoidAlgebra k G) M<GOAL>∀ (f g : MonoidAlgebra k G), ((ofModule M).asAlgebraHom f) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) → ((ofModule M).asAlgebraHom g) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) → ((ofModule M).asAlgebraHom (f + g)) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm ((f + g) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>r : MonoidAlgebra k G<VAR>m : RestrictScalars k (MonoidAlgebra k G) M<GOAL>∀ (r : k) (f : MonoidAlgebra k G), ((ofModule M).asAlgebraHom f) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) → ((ofModule M).asAlgebraHom (r • f)) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm ((r • f) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : (i : ι) → DecidableEq (α i)<VAR>inst✝² : (i : ι) → PartialOrder (α i)<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Icc (f i) (g i)).card - 2
<VAR>n : ℕ<GOAL>antidiagonal n = image (fun i => (i, n - i)) (range (n + 1))
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module A M₁<VAR>inst✝⁴ : SMulCommClass R A M₁<VAR>inst✝³ : SMulCommClass A R M₁<VAR>inst✝² : IsScalarTower R A M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Invertible 2<VAR>Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)<VAR>h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)<GOAL>Q₁ = Q₂
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module A M₁<VAR>inst✝⁴ : SMulCommClass R A M₁<VAR>inst✝³ : SMulCommClass A R M₁<VAR>inst✝² : IsScalarTower R A M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Invertible 2<VAR>Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)<VAR>h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)<GOAL>Q₁ = Q₂
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : AddCommGroup M₂<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module A M₁<VAR>inst✝⁴ : SMulCommClass R A M₁<VAR>inst✝³ : SMulCommClass A R M₁<VAR>inst✝² : IsScalarTower R A M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Invertible 2<VAR>Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)<VAR>h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)<VAR>x : A ⊗[R] M₂<GOAL>Q₁ x = Q₂ x
<VAR>p : ℕ<GOAL>↑(mersenne p) = 0
<VAR>p : ℕ<GOAL>(2 ^ p - 1).minFac ∣ 2 ^ p - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>i : δ<GOAL>Measurable ⋯.mp
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>(b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c
<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>f : α → β → γ<VAR>g : γ → δ<GOAL>g '' image2 f ↑s ↑t = image2 (fun a b => g (f a b)) ↑s ↑t
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>hsc : sᶜ.Finite<GOAL>Finite α
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>hsc : sᶜ.Finite<GOAL>(s ∪ sᶜ).Finite
<VAR>r : ℝ<GOAL>r.toNNReal < 1 ↔ r < 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a z✝ : α<GOAL>↑(toIcoMod hp a z✝) = ↑z✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a z✝ : α<GOAL>-toIcoDiv hp a z✝ • p ∈ AddSubgroup.zmultiples p
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y z : V<VAR>h₂ : ‖z - y‖ = ‖z + y‖<VAR>k : ℝ<VAR>hk_ne_one : k ≠ 1<VAR>hk : x + y = k • (x - y)<VAR>r : ℝ := (k - 1)⁻¹ * (k + 1)<GOAL>‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y z : V<VAR>h₂ : ‖z - y‖ = ‖z + y‖<VAR>k : ℝ<VAR>hk_ne_one : k ≠ 1<VAR>hk : x + y = k • (x - y)<VAR>r : ℝ := (k - 1)⁻¹ * (k + 1)<VAR>hxy : x = r • y<GOAL>‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y z : V<VAR>h₂ : ‖z - y‖ = ‖z + y‖<VAR>k : ℝ<VAR>hk_ne_one : k ≠ 1<VAR>hk : x + y = k • (x - y)<VAR>r : ℝ := (k - 1)⁻¹ * (k + 1)<VAR>hxy : x = r • y<VAR>hzy : ⟪z, y⟫_ℝ = 0<GOAL>‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y z : V<VAR>h₂ : ‖z - y‖ = ‖z + y‖<VAR>k : ℝ<VAR>hk_ne_one : k ≠ 1<VAR>hk : x + y = k • (x - y)<VAR>r : ℝ := (k - 1)⁻¹ * (k + 1)<VAR>hxy : x = r • y<VAR>hzy : ⟪z, y⟫_ℝ = 0<VAR>hzx : ⟪z, x⟫_ℝ = 0<GOAL>‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Semiring α<VAR>m✝ n✝ m n : ℕ<GOAL>↑(m ^ (n + 1)) = ↑m ^ (n + 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>(f.extend I).target = ↑I '' f.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable β<VAR>f : α →. β<VAR>h : Partrec f<VAR>n : α<VAR>x✝ : Unit<GOAL>x✝ ∈ Part.map (fun b => ()) (f n) ↔ x✝ ∈ Part.assert ((fun a => (f a).Dom) n) fun x => Part.some ()
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>n : ℕ<VAR>hk0 : 1 ≠ 0<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<VAR>hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<VAR>hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs<VAR>p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<VAR>hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs<VAR>p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac<VAR>hprime : Fact (Prime p)<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<VAR>hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs<VAR>p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac<VAR>hprime : Fact (Prime p)<VAR>hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<VAR>hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs<VAR>p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac<VAR>hprime : Fact (Prime p)<VAR>hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)<VAR>hpb : ¬p ∣ b<GOAL>∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<VAR>hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs<VAR>p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac<VAR>hprime : Fact (Prime p)<VAR>hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)<VAR>hpb : ¬p ∣ b<VAR>habs : p ≤ n<GOAL>False
<VAR>k n : ℕ<VAR>hk0 : k ≠ 0<VAR>hk1 : 1 < k<VAR>b : ℕ := k * n !<VAR>hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs<VAR>p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac<VAR>hprime : Fact (Prime p)<VAR>hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)<VAR>hpb : ¬p ∣ b<GOAL>p ≡ 1 [MOD k]
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>c : E<VAR>x : α<GOAL>‖⟪f x, c⟫_𝕜‖ ≤ ?m.10083 * ‖f x‖
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>c : E<VAR>x : α<GOAL>‖⟪f x, c⟫_𝕜‖ ≤ ‖f x‖ * ?m.10603
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PredOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<GOAL>⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PredOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>IsOpen {a}
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PredOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)<GOAL>IsOpen {a}
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PredOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)<VAR>this : TopologicalSpace α := Preorder.topology α<GOAL>IsOpen (Iio (succ a) ∩ Ioi (pred a))
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PredOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)<VAR>this : TopologicalSpace α := Preorder.topology α<GOAL>IsOpen (Iio (succ a))
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : PredOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)<VAR>this : TopologicalSpace α := Preorder.topology α<GOAL>IsOpen (Ioi (pred a))
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>F : Filter R<GOAL>Cauchy F ↔ F.NeBot ∧ ∀ (γ : Γ₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < ↑γ
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>F : Filter R<GOAL>(F.NeBot ∧ ∀ U ∈ RingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔ F.NeBot ∧ ∀ (γ : Γ₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < ↑γ
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>F : Filter R<GOAL>(∀ U ∈ RingFilterBasis.toAddGroupFilterBasis, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔ ∀ (γ : Γ₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < ↑γ
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>F : Filter R<GOAL>(∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup i)) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔ ∀ (γ : Γ₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < ↑γ
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ LiftPropWithinAt P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) → ContinuousWithinAt (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>h : ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<GOAL>ContinuousWithinAt (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>h : ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<VAR>h1 : ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e.symm.symm x)<GOAL>ContinuousWithinAt (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>h : ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<VAR>h1 : ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e.symm.symm x)<VAR>this : ContinuousAt (↑f) ((g ∘ ↑e.symm) (↑e x))<GOAL>ContinuousWithinAt (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Finset ℝ≥0∞<VAR>hs : ∀ (x : α), ↑f x ≠ 0 → μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s<GOAL>f.lintegral μ = ∑ x ∈ s, x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Finset ℝ≥0∞<VAR>hs : ∀ (x : α), ↑f x ≠ 0 → μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s<GOAL>∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ : a * μ (↑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Finset ℝ≥0∞<VAR>hs : ∀ (x : α), ↑f x ≠ 0 → μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s<GOAL>∀ (a₁ : ℝ≥0∞) (h₁₁ : a₁ ∈ f.range) (h₁₂ : a₁ * μ (↑f ⁻¹' {a₁}) ≠ 0) (a₂ : ℝ≥0∞) (h₂₁ : a₂ ∈ f.range) (h₂₂ : a₂ * μ (↑f ⁻¹' {a₂}) ≠ 0), (fun r x x => r) a₁ h₁₁ h₁₂ = (fun r x x => r) a₂ h₂₁ h₂₂ → a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Finset ℝ≥0∞<VAR>hs : ∀ (x : α), ↑f x ≠ 0 → μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s<GOAL>∀ b ∈ s, b * μ (↑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (h₁ : a ∈ f.range) (h₂ : a * μ (↑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Finset ℝ≥0∞<VAR>hs : ∀ (x : α), ↑f x ≠ 0 → μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s<GOAL>∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ : a * μ (↑f ⁻¹' {a}) ≠ 0), a * μ (↑f ⁻¹' {a}) = (fun r x x => r) a h₁ h₂ * μ (↑f ⁻¹' {(fun r x x => r) a h₁ h₂})
<VAR>n p : ℕ<GOAL>p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫ (x : γ), κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<GOAL>∃ f, ∀ (x y : 𝕎 k), (x * y).coeff (n + 1) = x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) + f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k<VAR>hf : ∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)<GOAL>∃ f, ∀ (x y : 𝕎 k), (x * y).coeff (n + 1) = x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) + f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k<VAR>hf : ∀ (x y : 𝕎 k), f (truncateFun (n + 1) x) (truncateFun (n + 1) y) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)<GOAL>∀ (x y : 𝕎 k), (x * y).coeff (n + 1) = x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) + f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Vector α n<VAR>i : Fin n<GOAL>(a ::ᵥ v).get i.succ = v.get i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a✝ b : R<VAR>hx : AlgebraicIndependent R x<VAR>a : A<GOAL>(AlgebraicIndependent R fun o => o.elim a x) ↔ ¬_root_.IsAlgebraic (↥(adjoin R (range x))) a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a✝ b : R<VAR>hx : AlgebraicIndependent R x<VAR>a : A<GOAL>Injective (⇑↑(Polynomial.aeval a) ∘ ⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) ↔ Injective ⇑(Polynomial.aeval a)
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<GOAL>n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>n_pos : 0 < n<GOAL>n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>n_pos : 0 < n<VAR>n2_pos : 1 ≤ 2 * n<GOAL>n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>n_pos : 0 < n<VAR>n2_pos : 1 ≤ 2 * n<VAR>S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))<VAR>f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x<GOAL>n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)