ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>t : |2⁻¹| = 2⁻¹<VAR>z : |∑ x ∈ range 34, (1 / 2) ^ (x + 1) / (↑x + 1) + log (1 / 2)| ≤ 1 / 17179869184<GOAL>|log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
<VAR>t : |2⁻¹| = 2⁻¹<VAR>z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184<GOAL>|log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
<VAR>t : |2⁻¹| = 2⁻¹<VAR>z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184<GOAL>|∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1) - 287209 / 414355| ≤ 1 / 10 ^ 10 - 1 / 2 ^ 34
<VAR>t : |2⁻¹| = 2⁻¹<VAR>z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184<GOAL>|∑ x ∈ range 0, 2⁻¹ ^ (x + 1) / (↑x + 1) + 2⁻¹ ^ (0 + 1) / (↑0 + 1) + 2⁻¹ ^ (1 + 1) / (↑1 + 1) + 2⁻¹ ^ (2 + 1) / (↑2 + 1) + 2⁻¹ ^ (3 + 1) / (↑3 + 1) + 2⁻¹ ^ (4 + 1) / (↑4 + 1) + 2⁻¹ ^ (5 + 1) / (↑5 + 1) + 2⁻¹ ^ (6 + 1) / (↑6 + 1) + 2⁻¹ ^ (7 + 1) / (↑7 + 1) + 2⁻¹ ^ (8 + 1) / (↑8 + 1) + 2⁻¹ ^ (9 + 1) / (↑9 + 1) + 2⁻¹ ^ (10 + 1) / (↑10 + 1) + 2⁻¹ ^ (11 + 1) / (↑11 + 1) + 2⁻¹ ^ (12 + 1) / (↑12 + 1) + 2⁻¹ ^ (13 + 1) / (↑13 + 1) + 2⁻¹ ^ (14 + 1) / (↑14 + 1) + 2⁻¹ ^ (15 + 1) / (↑15 + 1) + 2⁻¹ ^ (16 + 1) / (↑16 + 1) + 2⁻¹ ^ (17 + 1) / (↑17 + 1) + 2⁻¹ ^ (18 + 1) / (↑18 + 1) + 2⁻¹ ^ (19 + 1) / (↑19 + 1) + 2⁻¹ ^ (20 + 1) / (↑20 + 1) + 2⁻¹ ^ (21 + 1) / (↑21 + 1) + 2⁻¹ ^ (22 + 1) / (↑22 + 1) + 2⁻¹ ^ (23 + 1) / (↑23 + 1) + 2⁻¹ ^ (24 + 1) / (↑24 + 1) + 2⁻¹ ^ (25 + 1) / (↑25 + 1) + 2⁻¹ ^ (26 + 1) / (↑26 + 1) + 2⁻¹ ^ (27 + 1) / (↑27 + 1) + 2⁻¹ ^ (28 + 1) / (↑28 + 1) + 2⁻¹ ^ (29 + 1) / (↑29 + 1) + 2⁻¹ ^ (30 + 1) / (↑30 + 1) + 2⁻¹ ^ (31 + 1) / (↑31 + 1) + 2⁻¹ ^ (32 + 1) / (↑32 + 1) + 2⁻¹ ^ (33 + 1) / (↑33 + 1) - 287209 / 414355| ≤ 1 / 10 ^ 10 - 1 / 2 ^ 34
<VAR>t : |2⁻¹| = 2⁻¹<VAR>z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184<GOAL>|30417026706710207 / 51397301678363663775930777600| ≤ 7011591 / 167772160000000000
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a✝ b✝ : α<VAR>inst✝ : IsTrans α R<VAR>a b : α<VAR>l : List α<VAR>h : R a b<VAR>hb : Chain R b l<GOAL>∀ (a' : α), a' ∈ b :: l → R a a'
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a✝ b✝ : α<VAR>inst✝ : IsTrans α R<VAR>a b : α<VAR>l : List α<VAR>h : R a b<VAR>hb : Chain R b l<GOAL>∀ (a_1 : α), a_1 ∈ l → R a a_1
<VAR>A : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝² : Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>X✝ Y✝ : A ⥤ B × C<VAR>α : X✝ ⟶ Y✝<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) X✝).1.map f ≫ (fun X => (α.app X).1) Y = (fun X => (α.app X).1) X ≫ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) Y✝).1.map f
<VAR>A : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝² : Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>X✝ Y✝ : A ⥤ B × C<VAR>α : X✝ ⟶ Y✝<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) X✝).2.map f ≫ (fun X => (α.app X).2) Y = (fun X => (α.app X).2) X ≫ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) Y✝).2.map f
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>hd : HasDerivAt d d' x<VAR>hx : d x ≠ 0<GOAL>HasDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivWithinAt c c' univ x<VAR>hd : HasDerivWithinAt d d' univ x<VAR>hx : d x ≠ 0<GOAL>HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) univ x
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<GOAL>(s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty
<VAR>x y : ℤ<GOAL>(toComplex { re := x, im := y }).im = ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a b c : M<VAR>m n✝ n : ℕ<VAR>h : a * b = 1<GOAL>a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a b c : M<VAR>m n✝ n : ℕ<VAR>h : a * b = 1<GOAL>a ^ n * a * (b * b ^ n) = a ^ n * (a * b) * b ^ n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>g h : M<VAR>Hg : g ∈ Set.center M<VAR>u : Mˣ<VAR>hu : SemiconjBy (↑u) g h<GOAL>g = h
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x<VAR>x : E<VAR>hx : p x ≠ 0<GOAL>q x ≤ C * p x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x<VAR>x : E<VAR>hx : p x ≠ 0<VAR>δ : 𝕜<VAR>hδ : δ ≠ 0<VAR>δxle : p (δ • x) < ε<VAR>leδx : ε / ‖c‖ ≤ p (δ • x)<GOAL>q x ≤ C * p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>hg : Measurable g<VAR>a✝¹ : γ<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((comap 0 g hg) a✝¹) s✝ = (0 a✝¹) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>hg : Measurable g<VAR>a✝¹ : γ<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>(0 (g a✝¹)) s✝ = (0 a✝¹) s✝
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>H : FermatLastTheoremForThreeGen hζ<GOAL>FermatLastTheoremFor 3
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>H : FermatLastTheoremForThreeGen hζ<VAR>a b c : ℤ<VAR>hc : c ≠ 0<VAR>ha : ¬3 ∣ a<VAR>hb : ¬3 ∣ b<VAR>x✝ : 3 ∣ c<VAR>hcoprime : IsCoprime a b<VAR>h : a ^ 3 + b ^ 3 = c ^ 3<VAR>x : ℤ<VAR>hx : c = 3 * x<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>i' : ι'<GOAL>(b.repr ≪≫ₗ Finsupp.domLCongr e).symm (Finsupp.single i' 1) = b.repr.symm (Finsupp.single (e.symm i') 1)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t : Finset α<GOAL>∀ (i : (α × α) × α × α), i ∈ filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t) ↔ (Equiv.prodProdProdComm α α α α) i ∈ filter (fun x => match x with | ((a, b), c, d) => a * b = c * d) ((s ×ˢ t) ×ˢ s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s✝ : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Multiset α<VAR>x✝ : β<GOAL>x✝ ∈ map f s.toFinset ↔ x✝ ∈ (Multiset.map (⇑f) s).toFinset
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<GOAL>eval x (p * X) = eval x p * x
<VAR>G : Type u_1<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝¹ : μ.IsHaarMeasure<VAR>inst✝ : μ'.IsHaarMeasure<VAR>H : μ'.haarScalarFactor μ = 0<GOAL>False
<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<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝ : NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>ContinuousAt Inv.inv x ↔ x ≠ 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : ReflectsLimit (cospan h i) F<VAR>e : f ≫ h = g ≫ i<VAR>H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt ≅ H.cone.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : ReflectsLimit (cospan h i) F<VAR>e : f ≫ h = g ≫ i<VAR>H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).π.app WalkingCospan.left = ?refine_1.hom ≫ H.cone.π.app WalkingCospan.left
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : ReflectsLimit (cospan h i) F<VAR>e : f ≫ h = g ≫ i<VAR>H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).π.app WalkingCospan.right = ?refine_1.hom ≫ H.cone.π.app WalkingCospan.right
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hGG' : G ≤ G'<VAR>v✝ : V<VAR>hv : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts<GOAL>∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>hGG' : G ≤ G'<VAR>v✝ : V<VAR>hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts<VAR>w✝ : V<VAR>hv : w✝ ∈ M.verts<VAR>hv' : (Hom.ofLE hGG') w✝ = v✝<GOAL>∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w✝¹ : V<VAR>h : M.IsMatching<VAR>hGG' : G ≤ G'<VAR>v✝ : V<VAR>hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts<VAR>w✝ : V<VAR>hv : w✝ ∈ M.verts<VAR>hv' : (Hom.ofLE hGG') w✝ = v✝<VAR>w : V<VAR>hw : (fun w => M.Adj w✝ w) w ∧ ∀ (y : V), (fun w => M.Adj w✝ w) y → y = w<GOAL>∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w✝¹ : V<VAR>h : M.IsMatching<VAR>hGG' : G ≤ G'<VAR>v✝ : V<VAR>hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts<VAR>w✝ : V<VAR>hv : w✝ ∈ M.verts<VAR>hv' : (Hom.ofLE hGG') w✝ = v✝<VAR>w : V<VAR>hw : (fun w => M.Adj w✝ w) w ∧ ∀ (y : V), (fun w => M.Adj w✝ w) y → y = w<GOAL>(fun w => (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w) w ∧ ∀ (y : V), (fun w => (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w) y → y = w
<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>inst✝² : MeasurableSpace α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSpace β<VAR>f : β → α<VAR>h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})<VAR>s : Set α<VAR>x✝ : MeasurableSet s<GOAL>MeasurableSet (f ⁻¹' s)
<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>inst✝² : MeasurableSpace α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSpace β<VAR>f : β → α<VAR>h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})<VAR>s : Set α<VAR>x✝ : MeasurableSet s<GOAL>MeasurableSet (⋃ y ∈ s, f ⁻¹' {y})
<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>inst✝² : MeasurableSpace α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSpace β<VAR>f : β → α<VAR>h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})<VAR>s : Set α<VAR>x✝ : MeasurableSet s<VAR>y : α<VAR>hy : y ∈ s<GOAL>MeasurableSet (f ⁻¹' {y})
<VAR>a b m n p : ℕ<GOAL>0 < a.factorizationLCMRight b
<VAR>a b m n p : ℕ<GOAL>a.factorizationLCMRight b ≠ 0
<VAR>a b m n p : ℕ<GOAL>∀ i ∈ (a.lcm b).factorization.support, (if b.factorization i ≤ a.factorization i then 1 else i ^ (a.lcm b).factorization i) ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : InvolutiveInv α<VAR>f g : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>s⁻¹ ∈ f⁻¹
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁✝ x₂✝ y y₁✝ y₂✝ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>I : Ideal A<VAR>x₁ x₂ y₁ y₂ : A<VAR>hxy₁ : x₁ ≡ y₁ [SMOD I]<VAR>hxy₂ : x₂ ≡ y₂ [SMOD I]<GOAL>x₁ * x₂ ≡ y₁ * y₂ [SMOD I]
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁✝ x₂✝ y y₁✝ y₂✝ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>I : Ideal A<VAR>x₁ x₂ y₁ y₂ : A<VAR>hxy₁ : (Ideal.Quotient.mk I) x₁ = (Ideal.Quotient.mk I) y₁<VAR>hxy₂ : (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₂<GOAL>(Ideal.Quotient.mk I) x₁ * (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₁ * (Ideal.Quotient.mk I) y₂
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(coeff A (n + 1)) (bernoulliPowerSeries A * (exp A - 1)) = (coeff A (n + 1)) X
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(algebraMap ℚ A) (bernoulli (n + 1) / ((↑n + 1) * ↑n !)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) + (algebraMap ℚ A) (∑ x ∈ antidiagonal n, bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = if n + 1 = 1 then 1 else 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(algebraMap ℚ A) (bernoulli (n + 1 + 1) / ((↑(n + 1) + 1) * ↑(n + 1)!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) + (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = if n + 1 + 1 = 1 then 1 else 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(algebraMap ℚ A) (bernoulli (n + 1 + 1) / ((↑(n + 1) + 1) * ↑(n + 1)!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) + (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<GOAL>(algebraMap ℚ A) (bernoulli (n + 1 + 1) / ((↑(n + 1) + 1) * ↑(n + 1)!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) + (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>hite2 : (if n.succ = 0 then 1 else 0) = 0<GOAL>(algebraMap ℚ A) (bernoulli (n + 1 + 1) / ((↑(n + 1) + 1) * ↑(n + 1)!)) * ((algebraMap ℚ A) (↑0 + 1)⁻¹ - 1) + (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>hite2 : (if n.succ = 0 then 1 else 0) = 0<GOAL>(algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>hite2 : (if n.succ = 0 then 1 else 0) = 0<GOAL>(algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) = (algebraMap ℚ A) (∑ i ∈ antidiagonal n.succ, ↑((i.1 + i.2).choose i.2) / (↑i.2 + 1) * bernoulli i.1 / ↑n.succ !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>hite2 : (if n.succ = 0 then 1 else 0) = 0<VAR>x : ℕ × ℕ<VAR>h : x ∈ antidiagonal n.succ<GOAL>bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n.succ ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>hite2 : (if n.succ = 0 then 1 else 0) = 0<VAR>x : ℕ × ℕ<VAR>h : x.1 + x.2 = n.succ<GOAL>bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n.succ ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>hite2 : (if n.succ = 0 then 1 else 0) = 0<VAR>x : ℕ × ℕ<VAR>h : x.1 + x.2 = n.succ<GOAL>bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑(x.1 + x.2)! = ↑(x.1 + x.2)! / ↑(x.1! * x.2!) / (↑x.2 + 1) * bernoulli x.1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>hfact : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>hite2 : (if n.succ = 0 then 1 else 0) = 0<VAR>x : ℕ × ℕ<VAR>h : x.1 + x.2 = n.succ<GOAL>(↑x.2! * (↑x.2 + 1) = (↑x.2 + 1) * ↑x.2! ∨ (x.1 + x.2)! = 0) ∨ bernoulli x.1 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>⊥.IsNClique n s ↔ n ≤ 1 ∧ s.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>(↑s).Subsingleton ∧ s.card = n ↔ n ≤ 1 ∧ s.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>s.card = n → ((↑s).Subsingleton ↔ n ≤ 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s : Finset α<VAR>a b c : α<GOAL>(↑s).Subsingleton ↔ s.card ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ≃ β<VAR>I : Set β<GOAL>(M.mapEquiv f).Indep I ↔ M.Indep (⇑f.symm '' I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ≃ β<VAR>I : Set β<GOAL>(∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f.symm '' I)
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>φ : M ↪ₑ[L] N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>φ (funMap f x) = funMap f (⇑φ ∘ x)
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>φ : M ↪ₑ[L] N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<VAR>h : (Formula.graph f).Realize (⇑φ ∘ Fin.cons (funMap f x) x) ↔ (Formula.graph f).Realize (Fin.cons (funMap f x) x)<GOAL>φ (funMap f x) = funMap f (⇑φ ∘ x)
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>φ : M ↪ₑ[L] N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<VAR>h : funMap f (⇑φ ∘ x) = φ (funMap f x) ↔ funMap f x = funMap f x<GOAL>φ (funMap f x) = funMap f (⇑φ ∘ x)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Infinite F<VAR>E : Type u_2<VAR>inst✝ : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>f g : F[X]<VAR>sf : Multiset E := (Polynomial.map ϕ f).roots<VAR>sg : Multiset E := (Polynomial.map ϕ g).roots<VAR>s : Finset E := (sf.bind fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg).toFinset<GOAL>∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Infinite F<VAR>E : Type u_2<VAR>inst✝ : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>f g : F[X]<VAR>sf : Multiset E := (Polynomial.map ϕ f).roots<VAR>sg : Multiset E := (Polynomial.map ϕ g).roots<VAR>s : Finset E := (sf.bind fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg).toFinset<VAR>s' : Finset F := s.preimage ⇑ϕ ⋯<GOAL>∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Infinite F<VAR>E : Type u_2<VAR>inst✝ : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>f g : F[X]<VAR>sf : Multiset E := (Polynomial.map ϕ f).roots<VAR>sg : Multiset E := (Polynomial.map ϕ g).roots<VAR>s : Finset E := (sf.bind fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg).toFinset<VAR>s' : Finset F := s.preimage ⇑ϕ ⋯<VAR>c : F<VAR>hc : c ∉ s'<GOAL>∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Infinite F<VAR>E : Type u_2<VAR>inst✝ : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>f g : F[X]<VAR>sf : Multiset E := (Polynomial.map ϕ f).roots<VAR>sg : Multiset E := (Polynomial.map ϕ g).roots<VAR>s : Finset E := (sf.bind fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg).toFinset<VAR>s' : Finset F := s.preimage ⇑ϕ ⋯<VAR>c : F<VAR>hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = ϕ c<GOAL>∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p k : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>cyclotomic (p ^ (k + 1)) R * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>heI : e ∉ I<GOAL>M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>heI : e ∉ I<GOAL>M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : IsEmpty β<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<VAR>hs : (g '' (f '' s)ᶜ)ᶜ = s<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<VAR>hs : (g '' (f '' s)ᶜ)ᶜ = s<VAR>hns : g '' (f '' s)ᶜ = sᶜ<GOAL>∃ h, Bijective h