ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>a✝ : c ≠ 0<VAR>heq : a ^ 4 + b ^ 4 = c ^ 4<GOAL>False
<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>a✝ : c ≠ 0<VAR>heq : a ^ 4 + b ^ 4 = c ^ 4<GOAL>a ^ 4 + b ^ 4 = (c ^ 2) ^ 2
<VAR>α : Sort u<VAR>β β' : Sort v<VAR>h' : α → β = β'<GOAL>((x : α) → (fun x => β) x) = (α → β')
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : Monoid A<VAR>inst✝⁹ : Monoid B<VAR>inst✝⁸ : Monoid C<VAR>inst✝⁷ : Monoid D<VAR>inst✝⁶ : CommGroup E<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace C<VAR>inst✝² : TopologicalSpace D<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalGroup E<GOAL>Set.range toContinuousMap = {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : Monoid A<VAR>inst✝⁹ : Monoid B<VAR>inst✝⁸ : Monoid C<VAR>inst✝⁷ : Monoid D<VAR>inst✝⁶ : CommGroup E<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace C<VAR>inst✝² : TopologicalSpace D<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalGroup E<GOAL>{f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y} ⊆ Set.range toContinuousMap
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : Monoid A<VAR>inst✝⁹ : Monoid B<VAR>inst✝⁸ : Monoid C<VAR>inst✝⁷ : Monoid D<VAR>inst✝⁶ : CommGroup E<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace C<VAR>inst✝² : TopologicalSpace D<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalGroup E<VAR>f : C(A, B)<VAR>h1 : f 1 = 1<VAR>hmul : ∀ (x y : A), f (x * y) = f x * f y<GOAL>f ∈ Set.range toContinuousMap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>borel ℝ = generateFrom (⋃ a, {Iic ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>generateFrom (range fun a => Ioi ↑a) = generateFrom (range fun a => Iic ↑a)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>s : Ideal R<VAR>hs : s ≠ ⊥<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<GOAL>∃ n, s = span {ϖ ^ n}
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>s : Ideal R<VAR>hs : s ≠ ⊥<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>gen_ne_zero : generator s ≠ 0<GOAL>∃ n, s = span {ϖ ^ n}
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>s : Ideal R<VAR>hs : s ≠ ⊥<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>gen_ne_zero : generator s ≠ 0<VAR>n : ℕ<VAR>u : Rˣ<VAR>hnu : generator s * ↑u = ϖ ^ n<GOAL>∃ n, s = span {ϖ ^ n}
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>s : Ideal R<VAR>hs : s ≠ ⊥<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>gen_ne_zero : generator s ≠ 0<VAR>n : ℕ<VAR>u : Rˣ<VAR>hnu : generator s * ↑u = ϖ ^ n<GOAL>s = span {ϖ ^ n}
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>s : Ideal R<VAR>hs : s ≠ ⊥<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>gen_ne_zero : generator s ≠ 0<VAR>n : ℕ<VAR>u : Rˣ<VAR>hnu : generator s * ↑u = ϖ ^ n<VAR>this : span {generator s} = s<GOAL>s = span {ϖ ^ n}
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>s : Ideal R<VAR>hs : s ≠ ⊥<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>gen_ne_zero : generator s ≠ 0<VAR>n : ℕ<VAR>u : Rˣ<VAR>hnu : generator s * ↑u = ϖ ^ n<VAR>this : span {generator s} = s<GOAL>Associated (generator s) (generator s * ↑u)
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>q : ℕ<VAR>hqa : q ∈ a.primeFactorsList<VAR>hqb : q ∈ b.primeFactorsList<GOAL>False
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>q : ℕ<VAR>hqa : q ∈ a.primeFactorsList<VAR>hqb : q ∈ b.primeFactorsList<GOAL>Prime 1
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>q : ℕ<VAR>hqa : q ∈ a.primeFactorsList<VAR>hqb : q ∈ b.primeFactorsList<GOAL>Prime q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → Tropical (WithTop R)<GOAL>untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrder R<VAR>f : S → Tropical (WithTop R)<GOAL>untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' ↑∅)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → Tropical (WithTop R)<VAR>h : s.Nonempty<GOAL>untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>Z : LocallyRingedSpace<VAR>g : Y ⟶ Z<VAR>x : ↑X.toTopCat<GOAL>residueFieldMap (f ≫ g) x = residueFieldMap g (f.val.base x) ≫ residueFieldMap f x
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>Z : LocallyRingedSpace<VAR>g : Y ⟶ Z<VAR>x : ↑X.toTopCat<GOAL>LocalRing.ResidueField.map (Hom.stalkMap (f ≫ g) x) = LocalRing.ResidueField.map (Hom.stalkMap g (f.val.base x)) ≫ LocalRing.ResidueField.map (Hom.stalkMap f x)
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>Z : LocallyRingedSpace<VAR>g : Y ⟶ Z<VAR>x : ↑X.toTopCat<GOAL>LocalRing.ResidueField.map (Hom.stalkMap g (f.val.base x) ≫ Hom.stalkMap f x) = LocalRing.ResidueField.map (Hom.stalkMap g (f.val.base x)) ≫ LocalRing.ResidueField.map (Hom.stalkMap f x)
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>Z : LocallyRingedSpace<VAR>g : Y ⟶ Z<VAR>x : ↑X.toTopCat<VAR>this : IsLocalRingHom (Hom.stalkMap g (f.val.base x))<GOAL>LocalRing.ResidueField.map (Hom.stalkMap g (f.val.base x) ≫ Hom.stalkMap f x) = LocalRing.ResidueField.map (Hom.stalkMap g (f.val.base x)) ≫ LocalRing.ResidueField.map (Hom.stalkMap f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ht : t ∈ 𝓝[s] x<GOAL>DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>i.cycleRange (i.succAbove j) = j.succ
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h : j.castSucc < i<GOAL>i.cycleRange (i.succAbove j) = j.succ
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h : j.castSucc ≥ i<GOAL>i.cycleRange (i.succAbove j) = j.succ
<VAR>u : XgcdType<GOAL>u.bp = u.ap ↔ u.ap = u.bp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<GOAL>rightLim f x ≤ leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y = ⊥<GOAL>rightLim f x ≤ leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y ≠ ⊥<GOAL>rightLim f x ≤ leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>h' : 𝓝[<] y ≠ ⊥<VAR>a : α<VAR>xa : x < a<VAR>ay : a < y<GOAL>rightLim f x ≤ leftLim f y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝³ : Category.{max v u, w} D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : Preadditive D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>x✝ : Cᵒᵖ<GOAL>(J.plusMap 0).app x✝ = NatTrans.app 0 x✝
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝³ : Category.{max v u, w} D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : Preadditive D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>x✝ : Cᵒᵖ<VAR>S : (J.Cover (unop x✝))ᵒᵖ<GOAL>colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap 0).app x✝ = colimit.ι (J.diagram P (unop x✝)) S ≫ NatTrans.app 0 x✝
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>inst✝ : CountableInterFilter l<VAR>hs : IsLindelof s<GOAL>Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)
<VAR>a b : Cardinal.{u_1}<VAR>ha : ℵ₀ ≤ a<VAR>hb : b ≤ a<GOAL>a + b = a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : Mono g<VAR>h : f ≫ g = 0<GOAL>f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : Mono g<VAR>h✝ : f ≫ g = 0<VAR>h : f = 0<GOAL>f = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>f : ι → α<VAR>g : ι' → α<GOAL>(⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>T =O[atTop] asympBound g a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>hf : _root_.Embedding f<VAR>s : Set α<VAR>x : α<GOAL>map f (𝓝[s] x) = 𝓝[f '' s] f x
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>R : Type u_2<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : Finite Mˣ<VAR>χ : MulChar M R<GOAL>0 < orderOf χ
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>R : Type u_2<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : Finite Mˣ<VAR>χ : MulChar M R<VAR>val✝ : Fintype Mˣ<GOAL>0 < orderOf χ
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>R : Type u_2<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : Finite Mˣ<VAR>χ : MulChar M R<VAR>val✝ : Fintype Mˣ<GOAL>IsOfFinOrder χ
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>M' : Type u_3<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : Fintype ι<VAR>e : Basis ι R M✝<VAR>A : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Module A M✝<VAR>κ : Type u_6<VAR>inst✝³ : Fintype κ<VAR>𝕜 : Type u_7<VAR>inst✝² : Field 𝕜<VAR>M : Type u_8<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module 𝕜 M<VAR>h : FiniteDimensional.finrank 𝕜 M = 0<VAR>f : M →ₗ[𝕜] M<GOAL>LinearMap.det f = 1
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) = (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>(∃ u, u • s₂ • m₁ = u • s₁ • m₂) ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>t : Set R<VAR>ht : span t = ⊤<VAR>H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG<GOAL>I.FG
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>t : Set R<VAR>ht : span t = ⊤<VAR>H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG<GOAL>Module.Finite R ↥I
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>t : Set R<VAR>ht : span t = ⊤<VAR>H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG<VAR>k : (g : ↑t) → ↥I →ₗ[R] ↥(map (algebraMap R (Localization.Away ↑g)) I) := fun g => Algebra.idealMap (Localization.Away ↑g) I<GOAL>Module.Finite R ↥I
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s t : Set E<VAR>c c' : ℝ≥0<VAR>hf : ApproximatesLinearOn f f' s c<GOAL>LipschitzWith (‖f'‖₊ + c) (s.restrict f)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>k : αˣ<VAR>h : IsUnit A.det<GOAL>k⁻¹ • A⁻¹ * k • A = 1
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<GOAL>↑((selfAdjointPart ℝ) a) = 2⁻¹ • (a + star a)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>s ⊆ interior s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hn : n ≤ firstDiff x y<GOAL>cylinder x n = cylinder y n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hn : n ≤ firstDiff x y<GOAL>x ∈ cylinder y n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hn : n ≤ firstDiff x y<VAR>i : ℕ<VAR>hi : i < n<GOAL>x i = y i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f<VAR>a : Ordinal.{max u v}<GOAL>a < o.bsup f → succ a < o.bsup f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ sup (o.familyOfBFamily f)<VAR>a : Ordinal.{max u v}<GOAL>a < sup (o.familyOfBFamily f) → succ a < sup (o.familyOfBFamily f)
<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✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : DecidableEq ι<VAR>f : ι → α<VAR>p : Finset ι → Prop<VAR>h0 : p ∅<VAR>step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)<VAR>s : Finset ι<VAR>ihs : ∀ t ⊂ s, p t<GOAL>p s
<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✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : DecidableEq ι<VAR>f : ι → α<VAR>p : Finset ι → Prop<VAR>h0 : p ∅<VAR>step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)<VAR>s : Finset ι<VAR>ihs : ∀ t ⊂ s, p t<VAR>hne : image f s = ∅<GOAL>p s
<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✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : DecidableEq ι<VAR>f : ι → α<VAR>p : Finset ι → Prop<VAR>h0 : p ∅<VAR>step : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)<VAR>s : Finset ι<VAR>ihs : ∀ t ⊂ s, p t<VAR>hne : (image f s).Nonempty<GOAL>p s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : ℚ<GOAL>⌈↑x⌉ = ⌈x⌉
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(blimsup u f fun x => True) = limsup u f
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>h : Pairwise (Disjoint on fun i => (φ i).vars)<GOAL>(∑ i ∈ t, φ i).vars = t.biUnion fun i => (φ i).vars
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f✝ : β → γ<VAR>x : t β<VAR>η : ApplicativeTransformation F G<VAR>f : α → F β<VAR>x✝ : t α<GOAL>traverse ((fun {α} => η.app α) ∘ f) x✝ = ((fun {α} => η.app α) ∘ traverse f) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a : Associates α<GOAL>IsUnit a ↔ a = ⊥
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<GOAL>Set.range ⇑(ιMulti R n) ⊆ ↑(⋀[R]^n M)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<GOAL>∀ (y : Fin n → M), (ιMulti R n) y ∈ ↑(⋀[R]^n M)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>v : Fin n → M<GOAL>(ιMulti R n) v ∈ ↑(⋀[R]^n M)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>v : Fin n → M<GOAL>(List.ofFn fun i => (ι R) (v i)).prod ∈ ↑(⋀[R]^n M)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>v : Fin n → M<GOAL>(List.ofFn fun i => (ι R) (v i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>v : Fin n → M<GOAL>∃ f, (List.ofFn fun i => ↑(f i)).prod = (List.ofFn fun i => (ι R) (v i)).prod
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : StrictOrderedRing A<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.ble 1 n = true<GOAL>e ≠ 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : StrictOrderedRing A<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.ble 1 n = true<GOAL>-↑n ≠ 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : StrictOrderedRing A<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.ble 1 n = true<GOAL>¬↑n = 0
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℕ<VAR>inst✝ : StrictOrderedRing A<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.ble 1 n = true<GOAL>0 < ↑n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<GOAL>∃ n, 2⁻¹ ^ n < a
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>n : ℕ<VAR>hn : (↑n)⁻¹ < a<GOAL>∃ n, 2⁻¹ ^ n < a
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>n : ℕ<VAR>hn : (↑n)⁻¹ < a<GOAL>2⁻¹ ^ n < (↑n)⁻¹
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>n : ℕ<VAR>hn : (↑n)⁻¹ < a<GOAL>↑n < 2 ^ n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>n : ℕ<VAR>hn : (↑n)⁻¹ < a<GOAL>n < 2 ^ n
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<VAR>hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)<VAR>c : index K<GOAL>↑(((stdBasis K).repr ((commMap K) x)) c) = (matrixToStdBasis K *ᵥ x ∘ ⇑(indexEquiv K)) c
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<VAR>hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)<VAR>c : index K<GOAL>↑(((stdBasis K).repr (fun w => (x (↑w).embedding).re, fun w => x (↑w).embedding)) c) = ∑ x_1 : { w // w.IsReal }, fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap) c (Sum.inl x_1) * x (↑x_1).embedding + ∑ x_1 : { w // w.IsComplex }, (fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap) c (Sum.inr (x_1, 0)) * x (↑x_1).embedding + fromBlocks 1 0 0 ((blockDiagonal fun x => !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap) c (Sum.inr (x_1, 1)) * x (ComplexEmbedding.conjugate (↑x_1).embedding))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>hsymm : Symmetric p<VAR>hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c<VAR>a b c : α<VAR>pab : p a b<VAR>pbc : p b c<VAR>pac : p a c<VAR>hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c<GOAL>f a c = f a b * f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>hsymm : Symmetric p<VAR>hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c<VAR>a b c : α<VAR>pab : p a b<VAR>pbc : p b c<VAR>pac : p a c<VAR>hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c<VAR>rbc : r b c<GOAL>f a c = f a b * f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Monoid β<VAR>p r : α → α → Prop<VAR>inst✝ : IsTotal α r<VAR>f : α → α → β<VAR>hsymm : Symmetric p<VAR>hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1<VAR>hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c<VAR>a b c : α<VAR>pab : p a b<VAR>pbc : p b c<VAR>pac : p a c<VAR>hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c<VAR>rcb : r c b<GOAL>f a c = f a b * f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulWithZero α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosReflectLT α β<VAR>h : 0 < a • b<VAR>hb : 0 ≤ b<GOAL>0 • b < a • b