ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x + y) y = ↑(Real.arctan (‖x‖ / ‖y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle y (x + y) = ↑(Real.arctan (‖x‖ / ‖y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle y (y + x) = ↑(Real.arctan (‖x‖ / ‖y‖))
<VAR>α : Type u_1<VAR>m n : Num<GOAL>m.cmp n = Ordering.eq ↔ m = n
<VAR>α : Type u_1<VAR>m n : Num<VAR>this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)<GOAL>m.cmp n = Ordering.eq ↔ m = n
<VAR>α : Type u_1<VAR>m n : Num<GOAL>Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m) → (m.cmp n = Ordering.eq ↔ m = n)
<VAR>n m : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ last n<GOAL>j < i.castPred hi ↔ j.castSucc < i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>↑(basicOpen 𝒜 (f ^ n)) = ↑(basicOpen 𝒜 f)
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>e : K ≌ J<VAR>s : Cone (e.functor ⋙ F)<VAR>k : K<GOAL>(((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).π.app k = (Iso.refl (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).pt).hom ≫ ((𝟭 (Cone (e.functor ⋙ F))).obj s).π.app k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : trace K L = 0<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : trace K L = 0<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>(traceMatrix K ⇑pb.basis).det = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : trace K L = 0<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>Nonempty (Fin pb.dim)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb✝ : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : trace K L = 0<VAR>pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L<GOAL>0 < finrank K L
<GOAL>Integrable (fun x => (1 + x ^ 2)⁻¹) volume
<GOAL>Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-2 / 2)) volume
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>I₀ : Set α<VAR>hI₀ : M.Indep I₀<GOAL>∃ I₀_1, M.Indep I₀_1 ∧ BijOn f I₀_1 (f '' I₀)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t✝ u : Finset α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>t : Finset β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.card ≤ s.card<GOAL>∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : HasDerivWithinAt f f' S x<GOAL>slope f x y < f'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ : Cocycle K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>δ n' (n' + 1) ((↑γ).rightShift a n' hn') = 0
<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>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<GOAL>HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') 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>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<VAR>this : HasStrictDerivAt (fun y => c y * d y) ((c x • smulRight 1 d' + (smulRight 1 c').smulRight (d x)) 1) x<GOAL>HasStrictDerivAt (fun y => c y * d y) (c' * d x + c x * d') x
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<GOAL>M.Basis B M.E ↔ M.Base B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<GOAL>M.Indep B → ((B ⊆ M.E ∧ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ M.E → B = J) ∧ M.E ⊆ M.E ↔ ∀ (I : Set α), M.Indep I → B ⊆ I → B = I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<GOAL>M.Indep B → ((B ⊆ M.E ∧ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ M.E → B = J) ↔ ∀ (I : Set α), M.Indep I → B ⊆ I → B = I)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>x✝ : ℕ<GOAL>x✝ ∈ Nat.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋₊ ⌈b⌉₊
<VAR>m n : ℕ<GOAL>pair m n < (max m n + 1) ^ 2
<VAR>m n : ℕ<GOAL>(if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁴ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝³ : G.IsCocontinuous J K<VAR>inst✝² : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Sheaf K A<GOAL>((G.sheafAdjunctionCocontinuous A J K).unit.app F).val = (G.op.ranAdjunction A).unit.app F.val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁴ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝³ : G.IsCocontinuous J K<VAR>inst✝² : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Sheaf K A<GOAL>(G.op.ranAdjunction A).unit.app ((sheafToPresheaf K A).obj F) ≫ G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm.hom.app F) ≫ (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm.hom.app ((G.sheafPushforwardContinuous A J K).obj F) = (G.op.ranAdjunction A).unit.app F.val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁴ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝³ : G.IsCocontinuous J K<VAR>inst✝² : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Sheaf K A<GOAL>(G.op.ranAdjunction A).unit.app F.val ≫ G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫ 𝟙 ((G.sheafPushforwardCocontinuous A J K).obj ((G.sheafPushforwardContinuous A J K).obj F)).val = (G.op.ranAdjunction A).unit.app F.val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁴ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝³ : G.IsCocontinuous J K<VAR>inst✝² : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Sheaf K A<GOAL>(G.op.ranAdjunction A).unit.app F.val ≫ 𝟙 (G.op.ran.obj (G.op ⋙ F.val)) ≫ 𝟙 ((G.sheafPushforwardCocontinuous A J K).obj ((G.sheafPushforwardContinuous A J K).obj F)).val = (G.op.ranAdjunction A).unit.app F.val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁴ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝³ : G.IsCocontinuous J K<VAR>inst✝² : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Sheaf K A<GOAL>(G.op.ranAdjunction A).unit.app F.val ≫ 𝟙 (G.op.ran.obj (G.op ⋙ F.val)) ≫ 𝟙 (G.op.ran.obj (G.op ⋙ F.val)) = (G.op.ranAdjunction A).unit.app F.val
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>inst✝ : HasKernels V<VAR>i j j' : ι<VAR>r : c.Rel i j<VAR>r' : c.Rel i j'<GOAL>kernelSubobject (C.d i j) = kernelSubobject (C.d i j')
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>inst✝ : HasKernels V<VAR>i j j' : ι<VAR>r : c.Rel i j<VAR>r' : c.Rel i j'<GOAL>kernelSubobject (C.d i j' ≫ eqToHom ⋯) = kernelSubobject (C.d i j')
<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 : Cardinal.{v}<VAR>hn : n < Module.rank R M<GOAL>∃ s, #↑s = n ∧ LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
<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 : Cardinal.{v}<VAR>hn : n < Module.rank R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hs' : n < #↑↑⟨s, hs⟩<GOAL>∃ s, #↑s = n ∧ LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
<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 : Cardinal.{v}<VAR>hn : n < Module.rank R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hs' : n < #↑↑⟨s, hs⟩<VAR>t : Set M<VAR>ht : t ⊆ ↑⟨s, hs⟩<VAR>ht' : #↑t = n<GOAL>∃ s, #↑s = n ∧ LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : DivisionMonoid G<VAR>inst✝³ : MeasurableMul G<VAR>inst✝² : MeasurableInv G<VAR>μ✝ μ : Measure G<VAR>inst✝¹ : μ.IsInvInvariant<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasurePreserving (fun t => g / t) μ μ
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : DivisionMonoid G<VAR>inst✝³ : MeasurableMul G<VAR>inst✝² : MeasurableInv G<VAR>μ✝ μ : Measure G<VAR>inst✝¹ : μ.IsInvInvariant<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>MeasurePreserving (fun t => g * t⁻¹) μ μ
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>i : ι<GOAL>(b.repr ↑(ceil b m)) i = ↑⌈(b.repr m) i⌉
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>eraseP p l <+ l
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Mul α<VAR>v : Fin n.succ → α<VAR>x : α<VAR>w : Fin n → α<GOAL>v ⬝ᵥ vecCons x w = vecHead v * x + vecTail v ⬝ᵥ w
<VAR>n : ℕ+<GOAL>n.gcd 1 = 1
<VAR>n : ℕ+<GOAL>gcd 1 n = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>f : { x // p x } → β<VAR>g : α → β<VAR>h : ∀ x ∈ s, g ↑x = f x<GOAL>∏ x ∈ map (Embedding.subtype fun x => p x) s, g x = ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>f : { x // p x } → β<VAR>g : α → β<VAR>h : ∀ x ∈ s, g ↑x = f x<GOAL>∏ x ∈ s, g ((Embedding.subtype fun x => p x) x) = ∏ x ∈ s, f x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : Tendsto (fun x => f ↑x) atTop (𝓝 0)<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'<VAR>x₀ : ℝ<VAR>hx₀ : 0 ≤ x₀<VAR>hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖<GOAL>∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : Tendsto (fun x => f ↑x) atTop (𝓝 0)<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'<VAR>x₀ : ℝ<VAR>hx₀ : 0 ≤ x₀<VAR>hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖<VAR>h : ‖f ↑x₀‖ ≤ C<GOAL>∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : Tendsto (fun x => f ↑x) atTop (𝓝 0)<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'<VAR>x₀ : ℝ<VAR>hx₀ : 0 ≤ x₀<VAR>hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖<VAR>h : C < ‖f ↑x₀‖<GOAL>∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : Subgroup G<VAR>hG : Group.IsNilpotent G<GOAL>Group.nilpotencyClass ↥H ≤ Group.nilpotencyClass G
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : Subgroup G<VAR>hG : Group.IsNilpotent G<GOAL>Nat.find ⋯ ≤ Nat.find ⋯
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : Subgroup G<VAR>hG : Group.IsNilpotent G<GOAL>∀ (n : ℕ), lowerCentralSeries G n = ⊥ → lowerCentralSeries (↥H) n = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : Subgroup G<VAR>hG✝ : Group.IsNilpotent G<VAR>n : ℕ<VAR>hG : lowerCentralSeries G n = ⊥<GOAL>lowerCentralSeries (↥H) n = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : Subgroup G<VAR>hG✝ : Group.IsNilpotent G<VAR>n : ℕ<VAR>hG : lowerCentralSeries G n = ⊥<VAR>this : map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n<GOAL>lowerCentralSeries (↥H) n = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>inst✝ : H✝.Normal<VAR>H : Subgroup G<VAR>hG✝ : Group.IsNilpotent G<VAR>n : ℕ<VAR>hG : lowerCentralSeries G n = ⊥<VAR>this : ∀ ⦃x : G⦄ (x_1 : ↥H), x_1 ∈ lowerCentralSeries (↥H) n ∧ H.subtype x_1 = x → x ∈ ⊥<GOAL>lowerCentralSeries (↥H) n = ⊥
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>x✝¹ x✝ : ℕ<GOAL>x✝ * b ^ (x✝¹ + 1) = b * (x✝ * b ^ x✝¹)
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>x✝¹ x✝ : ℕ<GOAL>x✝ * (b ^ x✝¹ * b) = b * (x✝ * b ^ x✝¹)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>(∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.ball 0 1
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∃ a, s ⊆ a • Metric.ball 0 1
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<GOAL>(∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>IsLieAbelian ↥↑I ↔ ⁅I, I⁆ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>IsLieAbelian ↥↑I ↔ ∀ (y : L) (x : ↥I) (x_1 : ↥I), ⁅↑x, ↑x_1⁆ = y → y = 0
<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>g : γ → δ<VAR>f' : α' → β' → δ<VAR>g₁ : α → α'<VAR>g₂ : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)<GOAL>g '' image2 f ↑s ↑t = image2 f' (g₁ '' ↑s) (g₂ '' ↑t)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>U V : Set α<VAR>this : Setoid α := orbitRel G α<VAR>f : α → Quotient (orbitRel G α) := Quotient.mk'<GOAL>Disjoint (f '' U) (f '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>U V : Set α<VAR>this : Setoid α := orbitRel G α<VAR>f : α → Quotient (orbitRel G α) := Quotient.mk'<VAR>h : Disjoint (f '' U) (f '' V)<VAR>a : α<VAR>a_in_U : a ∈ U<VAR>g : G<VAR>g_in_V : g • a ∈ V<GOAL>(fun m => m • g • a) g⁻¹ = a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>U V : Set α<VAR>this : Setoid α := orbitRel G α<VAR>f : α → Quotient (orbitRel G α) := Quotient.mk'<GOAL>(∀ x ∈ U, ∀ (g : G), g • x ∉ V) → Disjoint (f '' U) (f '' V)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>z : ℤ<GOAL>clog b (↑b ^ z) = z
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a b✝ c d : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a * b / a = b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>n ≤ 0 ↔ n = 0
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>dist z w ≤ dist ↑z ↑w / √(z.im * w.im)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>inj : Injective m<VAR>large : range m ∈ f<VAR>S : Set α<GOAL>S ∈ comap m f ↔ m '' S ∈ f
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>t : Set G<GOAL>μ' t = ((μ' s / ν' s) • ν') t
<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>x : H<VAR>s : Set H<GOAL>map (↑I.symm) (𝓝[↑I '' s] ↑I x) = 𝓝[s] x
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A✝ A B : ValuationSubring K<VAR>h : A.unitGroup = B.unitGroup<GOAL>A = B