ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<VAR>n : ℕ<GOAL>(match decode n with | some y => ↑y | none => default) ∈ insert default s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>comap (fun x => (id x.1, id x.2)) (𝓤 α) = 𝓤 α
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>k j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>f : ⟨j₁, x⟩.fst ⟶ k<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>g : ⟨j₂, y⟩.fst ⟶ k<GOAL>M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ = M.mk F ⟨k, (F.map f) ⟨j₁, x⟩.snd * (F.map g) ⟨j₂, y⟩.snd⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>k j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>f : ⟨j₁, x⟩.fst ⟶ k<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>g : ⟨j₂, y⟩.fst ⟶ k<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : k ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β<GOAL>M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ = M.mk F ⟨k, (F.map f) ⟨j₁, x⟩.snd * (F.map g) ⟨j₂, y⟩.snd⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>k j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>f : ⟨j₁, x⟩.fst ⟶ k<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>g : ⟨j₂, y⟩.fst ⟶ k<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : k ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β<GOAL>∃ k_1 f_1 g_1, (F.map f_1) ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₁, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₂, y⟩.snd⟩.snd = (F.map g_1) ⟨k, (F.map f) ⟨j₁, x⟩.snd * (F.map g) ⟨j₂, y⟩.snd⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>k j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>f : ⟨j₁, x⟩.fst ⟶ k<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>g : ⟨j₂, y⟩.fst ⟶ k<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : k ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β<GOAL>(F.map α) ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₁, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₂, y⟩.snd⟩.snd = (F.map β) ⟨k, (F.map f) ⟨j₁, x⟩.snd * (F.map g) ⟨j₂, y⟩.snd⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>k j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>f : ⟨j₁, x⟩.fst ⟶ k<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>g : ⟨j₂, y⟩.fst ⟶ k<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : k ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β<GOAL>(F.map α) ((F.map (IsFiltered.leftToMax j₁ j₂)) x * (F.map (IsFiltered.rightToMax j₁ j₂)) y) = (F.map β) ((F.map f) x * (F.map g) y)
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>k j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>f : ⟨j₁, x⟩.fst ⟶ k<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>g : ⟨j₂, y⟩.fst ⟶ k<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : k ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β<GOAL>(F.map α) ((F.map (IsFiltered.leftToMax j₁ j₂)) x) * (F.map α) ((F.map (IsFiltered.rightToMax j₁ j₂)) y) = (F.map β) ((F.map f) x) * (F.map β) ((F.map g) y)
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>k j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>f : ⟨j₁, x⟩.fst ⟶ k<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>g : ⟨j₂, y⟩.fst ⟶ k<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : k ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β<GOAL>(F.map (IsFiltered.leftToMax j₁ j₂) ≫ F.map α) x * (F.map (IsFiltered.rightToMax j₁ j₂) ≫ F.map α) y = (F.map f ≫ F.map β) x * (F.map g ≫ F.map β) y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>IsIso (toSpec 𝒜 f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>this : IsIso (toSpec 𝒜 f).val.base<GOAL>IsIso (toSpec 𝒜 f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>this✝ : IsIso (toSpec 𝒜 f).val.base<VAR>this : ∀ (x : ↑(Proj.restrict ⋯).toTopCat), IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)<GOAL>IsIso (toSpec 𝒜 f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>this✝¹ : IsIso (toSpec 𝒜 f).val.base<VAR>this✝ : ∀ (x : ↑(Proj.restrict ⋯).toTopCat), IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)<VAR>this : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f)<GOAL>IsIso (toSpec 𝒜 f)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<GOAL>sigmaImp ⟨n, φ⟩ ⟨n, ψ⟩ = ⟨n, φ ⟹ ψ⟩
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasLimits C<VAR>inst✝⁴ : HasColimits C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms<VAR>inst✝¹ : PreservesLimits (CategoryTheory.forget C)<VAR>inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.base<VAR>H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f x)<VAR>U : Opens ↑↑X.toPresheafedSpace<GOAL>IsIso (f.c.app (op (⋯.functor.obj U)))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasLimits C<VAR>inst✝⁴ : HasColimits C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms<VAR>inst✝¹ : PreservesLimits (CategoryTheory.forget C)<VAR>inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.base<VAR>H : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (PresheafedSpace.Hom.stalkMap f x)<VAR>U : Opens ↑↑X.toPresheafedSpace<GOAL>∀ (x : ↥(⋯.functor.obj U)), IsIso ((TopCat.Presheaf.stalkFunctor C ↑x).map (let_fun this := { val := f.c }; this).val)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasLimits C<VAR>inst✝⁴ : HasColimits C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms<VAR>inst✝¹ : PreservesLimits (CategoryTheory.forget C)<VAR>inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.base<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>y : ↑↑X.toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>H : IsIso ((TopCat.Presheaf.stalkFunctor C (f.base y)).map f.c ≫ TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)<GOAL>IsIso ((TopCat.Presheaf.stalkFunctor C ↑⟨f.base y, ⋯⟩).map (let_fun this := { val := f.c }; this).val)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasLimits C<VAR>inst✝⁴ : HasColimits C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms<VAR>inst✝¹ : PreservesLimits (CategoryTheory.forget C)<VAR>inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.base<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>y : ↑↑X.toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>H : IsIso ((TopCat.Presheaf.stalkFunctor C (f.base y)).map f.c ≫ TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)<VAR>H' : IsIso (TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)<GOAL>IsIso ((TopCat.Presheaf.stalkFunctor C ↑⟨f.base y, ⋯⟩).map (let_fun this := { val := f.c }; this).val)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasLimits C<VAR>inst✝⁴ : HasColimits C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : (CategoryTheory.forget C).ReflectsIsomorphisms<VAR>inst✝¹ : PreservesLimits (CategoryTheory.forget C)<VAR>inst✝ : PreservesFilteredColimits (CategoryTheory.forget C)<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.base<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>y : ↑↑X.toPresheafedSpace<VAR>hy : y ∈ ↑U<VAR>H : IsIso ((TopCat.Presheaf.stalkFunctor C (f.base y)).map f.c ≫ TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)<VAR>H' : IsIso (TopCat.Presheaf.stalkPushforward C f.base X.presheaf y)<VAR>this : IsIso (((TopCat.Presheaf.stalkFunctor C (f.base y)).map f.c ≫ TopCat.Presheaf.stalkPushforward C f.base X.presheaf y) ≫ inv (TopCat.Presheaf.stalkPushforward C f.base X.presheaf y))<GOAL>IsIso ((TopCat.Presheaf.stalkFunctor C ↑⟨f.base y, ⋯⟩).map (let_fun this := { val := f.c }; this).val)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<GOAL>F.IsSheaf ↔ F.IsSheafPairwiseIntersections
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>|a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>|a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r✝ r₁ r₂ r : ℝ<GOAL>ENNReal.ofReal r ≤ ↑‖r‖₊
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r✝ r₁ r₂ r : ℝ<VAR>hr : 0 ≤ r<GOAL>ENNReal.ofReal r ≤ ↑‖r‖₊
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r✝ r₁ r₂ r : ℝ<VAR>hr : r ≤ 0<GOAL>ENNReal.ofReal r ≤ ↑‖r‖₊
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>init n (-x) = init n (-init n x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>n : ℕ := card α<VAR>hn : n = card α<VAR>ha : 1 = card α<VAR>_h : card α ≤ 1<VAR>a b : α<GOAL>a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>n : ℕ := card α<VAR>hn : n = card α<VAR>ha : 1 = card α<VAR>_h : card α ≤ 1<VAR>a b x : α<VAR>hx : ∀ (y : α), y = x<GOAL>a = b
<VAR>R : Type u_1<VAR>inst✝ : AddCommGroup R<VAR>f g : ℕ → R<GOAL>(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
<VAR>R : Type u_1<VAR>inst✝ : AddCommGroup R<VAR>f g : ℕ → R<VAR>f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }<GOAL>(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
<VAR>R : Type u_1<VAR>inst✝ : AddCommGroup R<VAR>f g : ℕ → R<VAR>f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }<VAR>g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }<GOAL>(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<GOAL>r = 0
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<GOAL>Ideal.span {r} = ⊥
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<GOAL>∀ (J : Ideal R) (hJ : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) (Ideal.span {r}) = ⊥
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<VAR>J : Ideal R<VAR>hJ : J.IsMaximal<GOAL>Submodule.map (Algebra.linearMap R (Localization.AtPrime J)) (Ideal.span {r}) = ⊥
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<VAR>J : Ideal R<VAR>hJ : J.IsMaximal<GOAL>∀ x ∈ ⇑(Algebra.linearMap R (Localization.AtPrime J)) '' {r}, x = 0
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<VAR>J : Ideal R<VAR>hJ : J.IsMaximal<VAR>w✝ : R<VAR>h' : w✝ ∈ {r}<GOAL>(Algebra.linearMap R (Localization.AtPrime J)) w✝ = 0
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<VAR>J : Ideal R<VAR>hJ : J.IsMaximal<VAR>h' : r ∈ {r}<GOAL>(Algebra.linearMap R (Localization.AtPrime J)) r = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>x : X<GOAL>map (⇑h.symm) (𝓝 (h x)) = 𝓝 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>h : IsBoundedLinearMap 𝕜 f<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>_root_.fderivWithin 𝕜 f s x = h.toContinuousLinearMap
<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>h : IsBoundedLinearMap 𝕜 f<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>_root_.fderiv 𝕜 f x = h.toContinuousLinearMap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α ≃o β<VAR>s : Set β<VAR>x : α<GOAL>IsLUB (⇑f ⁻¹' s) x ↔ IsLUB s (f x)
<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 : OpenEmbedding f<VAR>s : Set β<VAR>x : α<GOAL>map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x
<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 : OpenEmbedding f<VAR>s : Set β<VAR>x : α<GOAL>𝓝[s ∩ range f] f x = 𝓝[s] f x
<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 : OpenEmbedding f<VAR>s : Set β<VAR>x : α<GOAL>s ∩ range f ∩ range f = s ∩ range f
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(baseChange W B).toAffine.polynomial = Polynomial.map (mapRingHom ↑f) (baseChange W A).toAffine.polynomial
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>0 < log x ↔ 1 < x
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>log 1 < log x ↔ 1 < x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>f : β → α<VAR>f_cont : Continuous f<GOAL>AnalyticSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>f : β → α<VAR>f_cont : Continuous f<VAR>h✝ : IsEmpty β<GOAL>AnalyticSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>f : β → α<VAR>f_cont : Continuous f<VAR>h✝ : Nonempty β<GOAL>AnalyticSet (range f)
<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>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<GOAL>S.Solution'_descent.multiplicity < S.multiplicity
<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>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<GOAL>S.multiplicity.pred < S.multiplicity
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ γ : Type<VAR>s : σ<VAR>f : α → β → σ × σ → (σ × σ) × γ<VAR>h : ∀ (x : α) (y : β) (s : σ), let s' := (f x y (s, s)).1; s'.1 = s'.2<GOAL>∃ R, R (s, s) s ∧ ∀ {s : σ × σ} {q : σ} (a : α) (b : β), R s q → R (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧ (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ γ : Type<VAR>s : σ<VAR>f : α → β → σ × σ → (σ × σ) × γ<VAR>h : ∀ (x : α) (y : β) (s : σ), let s' := (f x y (s, s)).1; s'.1 = s'.2<GOAL>(match (s, s) with | (s₁, s₂) => s₂ = s ∧ s₁ = s) ∧ ∀ {s : σ × σ} {q : σ} (a : α) (b : β), (match s with | (s₁, s₂) => s₂ = q ∧ s₁ = q) → (match (f a b s).1 with | (s₁, s₂) => s₂ = ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧ s₁ = ((f a b (q, q)).1.1, (f a b (q, q)).2).1) ∧ (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∃ n, p n<VAR>n : ℕ<GOAL>n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_in_E : x ∈ E<GOAL>x ∈ (thickening δ (thickening δ E)ᶜ)ᶜ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_in_E : x ∈ E<GOAL>ENNReal.ofReal δ ≤ infEdist x {x | infEdist x E < ENNReal.ofReal δ}ᶜ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_in_E : x ∈ E<VAR>y : α<VAR>hy : y ∈ {x | infEdist x E < ENNReal.ofReal δ}ᶜ<GOAL>ENNReal.ofReal δ ≤ edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_in_E : x ∈ E<VAR>y : α<VAR>hy : ENNReal.ofReal δ ≤ infEdist y E<GOAL>ENNReal.ofReal δ ≤ edist x y
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f : V →ₗ[K] V<VAR>hinj : Injective ⇑f<GOAL>Surjective ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f : V →ₗ[K] V<VAR>hinj : Injective ⇑f<VAR>h : Module.rank K ↥(range f) = Module.rank K V<GOAL>Surjective ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f : V →ₗ[K] V<VAR>hinj : Injective ⇑f<VAR>h : finrank K ↥(range f) = finrank K V<GOAL>Surjective ⇑f
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Exponentiable A<VAR>A₁ A₂ A₃ : C<VAR>inst✝² : Exponentiable A₁<VAR>inst✝¹ : Exponentiable A₂<VAR>inst✝ : Exponentiable A₃<VAR>f : A₁ ⟶ A₂<VAR>g : A₂ ⟶ A₃<GOAL>pre (f ≫ g) = pre g ≫ pre f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L₁<VAR>inst✝² : LieRing L₂<VAR>inst✝¹ : LieAlgebra R L₁<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>h₁ : Surjective ⇑f<VAR>h₂ : IsLieAbelian L₁<VAR>u v : L₁<GOAL>⁅f u, f v⁆ = 0
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → E<VAR>x y : k<GOAL>slope (-f) x y = (-slope f) x y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>x x' : S<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) (x * x') = ((pb.basis.constr A) fun i => y ^ ↑i) x * ((pb.basis.constr A) fun i => y ^ ↑i) x'