ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ : Set (α → M)<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α ≃ β<GOAL>(fun g => g ∘ ⇑f.symm) ⁻¹' s = (fun g => g ∘ ⇑f) '' s
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ : Set (α → M)<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α ≃ β<GOAL>Function.LeftInverse (fun g => g ∘ ⇑f.symm) fun g => g ∘ ⇑f
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ : Set (α → M)<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α ≃ β<GOAL>Function.RightInverse (fun g => g ∘ ⇑f.symm) fun g => g ∘ ⇑f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>e : ι ≃ ι₂<VAR>f : (i : ι) → s i<GOAL>(lift { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s e), map_add' := ⋯, map_smul' := ⋯ }) ((tprod R) f) = (tprod R) fun i => f (e.symm i)
<VAR>m n k : ℕ<GOAL>k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors
<VAR>m n k : ℕ<GOAL>(∃ x x_1, (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : Measure α<VAR>a b : α<VAR>inst✝ : NoAtoms μ<GOAL>μ {b} ≠ ⊤
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m : ℤ<VAR>n : ℕ<VAR>x : 𝕜<VAR>k : ℕ<GOAL>deriv^[k] (fun x => x ^ n) x = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m : ℤ<VAR>n : ℕ<VAR>x : 𝕜<VAR>k : ℕ<GOAL>(∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m : ℤ<VAR>n : ℕ<VAR>x : 𝕜<VAR>k : ℕ<VAR>hkn : k ≤ n<GOAL>(∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m : ℤ<VAR>n : ℕ<VAR>x : 𝕜<VAR>k : ℕ<VAR>hnk : n < k<GOAL>(∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : TopologicalSpace G₀<VAR>inst✝ : HasContinuousInv₀ G₀<VAR>x : G₀<VAR>hx : x ≠ 0<GOAL>𝓝 x⁻¹ = (𝓝 x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : TopologicalSpace G₀<VAR>inst✝ : HasContinuousInv₀ G₀<VAR>x : G₀<VAR>hx : x ≠ 0<GOAL>(𝓝 x⁻¹)⁻¹ ≤ 𝓝 x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>v : Basis ι R M<VAR>Q : QuadraticMap R M N<VAR>w : ι → R<GOAL>(Q.basisRepr v) w = Q (∑ i : ι, w i • v i)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>v : Basis ι R M<VAR>Q : QuadraticMap R M N<VAR>w : ι → R<GOAL>(Q.basisRepr v) w = Q (v.equivFun.symm w)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⋙ G ⟶ H ⋙ R₂<VAR>c : C<GOAL>G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c) = adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((𝟭 C).obj c))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⋙ G ⟶ H ⋙ R₂<VAR>c : C<GOAL>G.map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) = adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((𝟭 C).obj c))
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : KleisliCat m<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) = { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : KleisliCat m<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝<GOAL>{ obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t = ({ obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g) t
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : KleisliCat m<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝<GOAL>{ obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t = joinM (g <$> f t)
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : KleisliCat m<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝<GOAL>(f ≫ g) t = f t >>= g
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>this✝ : _root_.Monad (ofTypeMonad m).obj := let_fun this := inferInstance; this<VAR>this : LawfulMonad (ofTypeMonad m).obj := let_fun this := inferInstance; this<GOAL>{ obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) = { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>this✝ : _root_.Monad (ofTypeMonad m).obj := let_fun this := inferInstance; this<VAR>this : LawfulMonad (ofTypeMonad m).obj := let_fun this := inferInstance; this<VAR>t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝<GOAL>{ obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t = ({ obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g) t
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>this✝ : _root_.Monad (ofTypeMonad m).obj := let_fun this := inferInstance; this<VAR>this : LawfulMonad (ofTypeMonad m).obj := let_fun this := inferInstance; this<VAR>t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝<GOAL>joinM (g <$> f t) = (f ≫ g) t
<VAR>m : Type u → Type u<VAR>inst✝¹ : _root_.Monad m<VAR>inst✝ : LawfulMonad m<VAR>X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>this✝ : _root_.Monad (ofTypeMonad m).obj := let_fun this := inferInstance; this<VAR>this : LawfulMonad (ofTypeMonad m).obj := let_fun this := inferInstance; this<VAR>t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝<GOAL>f t >>= g = (f ≫ g) t
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝ : (i : I) → Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) → C i<VAR>f : X ≅ Y<VAR>i : I<GOAL>f.hom i ≫ f.inv i = 𝟙 (X i)
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝ : (i : I) → Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) → C i<VAR>f : X ≅ Y<VAR>i : I<GOAL>f.inv i ≫ f.hom i = 𝟙 (Y i)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → CommRing (G i)<VAR>f✝ : (i j : ι) → i ≤ j → G i → G j<VAR>f'✝ : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝⁴ : CommRing P<VAR>g✝ : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f✝ i j hij x) = (g✝ i) x<VAR>f : (i j : ι) → i ≤ j → G i →+* G j<VAR>G' : ι → Type v'<VAR>inst✝³ : (i : ι) → CommRing (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+* G' j<VAR>G'' : ι → Type v''<VAR>inst✝² : (i : ι) → CommRing (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃+* G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)<VAR>i : ι<VAR>g : G' i<GOAL>(congr e he).symm ((of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) g) = (of G (fun x x_1 h => ⇑(f x x_1 h)) i) ((e i).symm g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R N<GOAL>map e.flip.symm p.dualAnnihilator = (map e p).dualCoannihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R N<VAR>this : IsReflexive R N<GOAL>map e.flip.symm p.dualAnnihilator = (map e p).dualCoannihilator
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h0 : q ≠ 0<VAR>hl : q.natDegree < p.natDegree<VAR>hcontra : p ∣ q<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝² : SecondCountableTopology E<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)<GOAL>Measurable fun p => lineDeriv 𝕜 f p.1 p.2
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝² : SecondCountableTopology E<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)<VAR>this : Continuous (Function.uncurry g)<GOAL>Measurable fun p => lineDeriv 𝕜 f p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<GOAL>l.reduceOption.length ≤ l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<GOAL>l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.57189, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>(fun i j => homotopyCofiber.d φ i j) i j ≫ (fun i j => homotopyCofiber.d φ i j) j k = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.57189, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>homotopyCofiber.inlX φ j i hij ≫ (fun i j => homotopyCofiber.d φ i j) i j ≫ (fun i j => homotopyCofiber.d φ i j) j k = homotopyCofiber.inlX φ j i hij ≫ 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.57189, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>homotopyCofiber.inrX φ i ≫ (fun i j => homotopyCofiber.d φ i j) i j ≫ (fun i j => homotopyCofiber.d φ i j) j k = homotopyCofiber.inrX φ i ≫ 0
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>hurwitzZeta (↑x) (-(2 * ↑k)) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>k : ℕ<VAR>hk : k.succ ≠ 0<GOAL>hurwitzZetaEven (↑x) (-(2 * ↑k.succ)) = 0
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < (1 - r) * (b - a)<GOAL>f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a b ≤ slope f ((lineMap a b) r) b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < (1 - r) * (b - a)<GOAL>f ((lineMap b a) (1 - r)) ≤ (lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f ((lineMap b a) (1 - r)) b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>f : k → E<VAR>a b r' : k<VAR>h : 0 < r' * (b - a)<GOAL>f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>f : k → E<VAR>a b r' : k<VAR>h : 0 < r' * (b - a)<GOAL>f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔ (b - a)⁻¹ • (f b - f a) ≤ (b - (r' * (a - b) + b))⁻¹ • (f b - f (r' * (a - b) + b))
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>f : k → E<VAR>a b r' : k<VAR>h : 0 < r' * (b - a)<GOAL>b - a ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>a : α<VAR>z : Sym2 α<VAR>ha : a ∈ z<VAR>hb : Mem.other ha ∈ z<GOAL>Mem.other hb = a
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>N : Type u_3<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : Module R N<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommMonoid P<VAR>inst✝⁸ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>f : M₂ →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>g₁ g₂ : M [⋀^ι]→ₗ[R] N<VAR>h : (fun g => g.compLinearMap f) g₁ = (fun g => g.compLinearMap f) g₂<VAR>x : ι → M<GOAL>g₁ x = g₂ x
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_4} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>X : C<VAR>this : HasShift D A := HasShift.induced F A s i<GOAL>(shiftFunctorZero D A).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<GOAL>ringChar F = 2 ↔ Fintype.card F % 2 = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>h : Fintype.card F = ringChar F ^ ↑n<GOAL>ringChar F = 2 ↔ Fintype.card F % 2 = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>h : Fintype.card F = ringChar F ^ ↑n<GOAL>ringChar F = 2 ↔ ringChar F = 2 ∧ ↑n ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(C a * p).natDegree = p.natDegree
<VAR>n : ℤ<GOAL>(n + 1).negOnePow = -n.negOnePow
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ Subgroup.center G
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S✝<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>IsOpen (Set.range ⇑(comap (algebraMap R S)))
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S✝<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>IsOpen ↑(basicOpen r)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i : Fin n<VAR>y : α i.castSucc<VAR>z : α (last n)<VAR>j : Fin n<GOAL>init (update q (last n) z) j = init q j
<VAR>δ : ℕ → ℝ<VAR>x : UnitAddCircle<GOAL>x ∈ addWellApproximable UnitAddCircle δ ↔ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite
<VAR>δ : ℕ → ℝ<VAR>x : UnitAddCircle<GOAL>{n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}.Infinite ↔ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}.Infinite
<VAR>δ : ℕ → ℝ<VAR>x : UnitAddCircle<VAR>n : ℕ<VAR>hn : n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}<GOAL>n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}
<VAR>δ : ℕ → ℝ<VAR>x : UnitAddCircle<VAR>n : ℕ<VAR>hn : n ∈ {n | ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ n}<GOAL>n ∈ {n | 0 < n ∧ x ∈ approxAddOrderOf UnitAddCircle n (δ n)}
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>H : ∃ f, LinearIndependent R f<GOAL>↑n ≤ Module.rank R M
<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✝ : (C × D)ᵒᵖ<VAR>X : C<VAR>Y : D<GOAL>(𝟙 (op X) ≫ 𝟙 (op X), 𝟙 (op Y) ≫ 𝟙 (op Y)) = (𝟙 (op X), 𝟙 (op Y))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>mapFun (⇑f) (x - y) = mapFun (⇑f) x - mapFun (⇑f) y
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>x : L<VAR>hx : x ∈ ↑(Ideal.span {(algebraMap S L) a})<GOAL>x ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>x' : L<VAR>hx : (algebraMap S L) a * x' ∈ ↑(Ideal.span {(algebraMap S L) a})<GOAL>(algebraMap S L) a * x' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<GOAL>(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹² : IsDomain R<VAR>inst✝¹¹ : IsDomain S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : Algebra R L<VAR>inst✝⁶ : Algebra S L<VAR>inst✝⁵ : IsIntegralClosure S R L<VAR>inst✝⁴ : IsFractionRing S L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsScalarTower R S L<VAR>inst✝¹ : IsScalarTower R K L<VAR>a : S<VAR>b : Set S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)<VAR>y' : S<VAR>z' : ↥S⁰<VAR>hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})<VAR>y : S<VAR>z : R<VAR>hz0 : z ≠ 0<VAR>yz_eq : z • y' = ↑z' * y<GOAL>(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))