ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<GOAL>homogeneousSubmodule σ R n = supported R R {d | d.degree = n}
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<GOAL>homogeneousSubmodule σ R n = supported R R {d | (weight 1) d = n}
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>g✝ : σ → S₁<VAR>inst✝ : Fintype σ<VAR>g : R →+* S₁<VAR>X : σ → S₁<VAR>f : MvPolynomial σ R<GOAL>eval₂ g X f = ∑ d ∈ f.support, g (coeff d f) * ∏ i : σ, X i ^ d i
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>g✝ : σ → S₁<VAR>inst✝ : Fintype σ<VAR>g : R →+* S₁<VAR>X : σ → S₁<VAR>f : MvPolynomial σ R<GOAL>∑ d ∈ f.support, g (coeff d f) * ∏ i ∈ d.support, X i ^ d i = ∑ x ∈ f.support, g (coeff x f) * x.prod fun a b => X a ^ 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✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>ε : ι → 𝕜<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>hε : Tendsto ε l (𝓝[≠] 0)<VAR>S : Set E<GOAL>∀ᶠ (n : ι) in l, ε n ≠ 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : Over P<VAR>hf : f.hom = 0<GOAL>biprod.fst ≫ f.hom = biprod.snd ≫ (Over.mk 0).hom
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>α' : Type u_1<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<VAR>s : σ'<VAR>x : List α<GOAL>((reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>n : ℕ<VAR>hn1 : n ≠ 0<VAR>hn2 : f ↑n ≠ 1<VAR>P : Set ℕ := {m | 0 < f ↑m ∧ f ↑m < 1}<GOAL>∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>n : ℕ<VAR>hn1 : n ≠ 0<VAR>hn2 : f ↑n ≠ 1<VAR>P : Set ℕ := {m | 0 < f ↑m ∧ f ↑m < 1}<VAR>hP : P.Nonempty<GOAL>∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>F₁.map (Hom.mk f) = eqToHom ⋯ ≫ F₂.map (Hom.mk f) ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>F₁.map ((Q W).map f.f) ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>(eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯) ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>this : IsIso ((Q W).map f.s)<GOAL>eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>this : IsIso ((Q W).map f.s)<GOAL>F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>this : IsIso ((Q W).map f.s)<GOAL>(eqToHom ⋯ ≫ (Q W ⋙ F₁).map f.s ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>this : IsIso ((Q W).map f.s)<GOAL>(eqToHom ⋯ ≫ F₁.map ((Q W).map f.s) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>this : IsIso ((Q W).map f.s)<GOAL>eqToHom ⋯ ≫ F₁.map (𝟙 ((Q W).obj Y)) = eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.87374, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F₁ F₂ : Localization W ⥤ E<VAR>h : Q W ⋙ F₁ = Q W ⋙ F₂<VAR>X Y : C<VAR>f : W.LeftFraction X Y<VAR>this : IsIso ((Q W).map f.s)<GOAL>eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<GOAL>(fun x => ((μ.tilted f).rnDeriv ν x).toReal) =ᶠ[ae ν] fun x => (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>x : α<VAR>hx : (μ.tilted f).rnDeriv ν x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x<GOAL>((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>x : α<VAR>hx : (μ.tilted f).rnDeriv ν x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x<GOAL>(ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>x : α<VAR>hx : (μ.tilted f).rnDeriv ν x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x<GOAL>0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ∨ (μ.rnDeriv ν x).toReal = 0
<VAR>n✝ : ℕ<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)
<VAR>n✝ : ℕ<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ x ∈ n.divisors, f ({ toFun := fun d => (d, n / d), inj' := ⋯ } x).1 ({ toFun := fun d => (d, n / d), inj' := ⋯ } x).2 = ∏ i ∈ n.divisors, f i (n / i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>(extChartAt (IB.prod 𝓘(𝕜, F)) x).target = ((extChartAt IB x.proj).target ∩ ↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>((extChartAt IB x.proj).prod (PartialEquiv.refl F)).target ∩ ↑((extChartAt IB x.proj).prod (PartialEquiv.refl F)).symm ⁻¹' (trivializationAt F E x.proj).baseSet ×ˢ univ = (extChartAt IB x.proj).target ×ˢ univ ∩ (↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ
<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✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>hpos : 0 < r<VAR>hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖<VAR>x y : E<VAR>hne : x ≠ y<GOAL>(fun x x_1 => r ≤ dist x x_1) x y
<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✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>hpos : 0 < r<VAR>hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖<VAR>x y : E<VAR>hne : x ≠ y<GOAL>r ≤ ‖x / y‖
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>f✝ f g : R[X]<VAR>I : Ideal R<GOAL>(quotEquivQuotMap f I).symm ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>{ ofColex := s } ≤ { ofColex := {a} } ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>(∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b✝ b : α<VAR>x✝ : b ∈ s<GOAL>¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i j✝ : Fin n✝<VAR>n : ℕ<VAR>j : Fin n<GOAL>succAbove 1 j.succ = j.succ.succ
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i j✝ : Fin n✝<VAR>n : ℕ<VAR>j : Fin n<VAR>this : (succ 0).succAbove j.succ = (succAbove 0 j).succ<GOAL>succAbove 1 j.succ = j.succ.succ
<VAR>n n✝ : ℕ<VAR>a✝ : Fin2 n✝<VAR>i_ih : ∀ {α : TypeVec.{u_1} n✝} {x y : α a✝}, ofRepeat (α.repeatEq a✝ (prod.mk a✝ x y)) ↔ x = y<VAR>α : TypeVec.{u_1} (n✝ + 1)<VAR>x y : α a✝.fs<GOAL>ofRepeat (α.repeatEq a✝.fs (prod.mk a✝.fs x y)) ↔ x = y
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<GOAL>∃ r < ↑n, x = ζ ^ r ∨ x = -ζ ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>r : ℕ<VAR>hr : x = (-ζ) ^ r<GOAL>∃ r < ↑n, x = ζ ^ r ∨ x = -ζ ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>r : ℕ<VAR>hr : x = (-ζ) ^ r<GOAL>x = ζ ^ (r % ↑n) ∨ x = -ζ ^ (r % ↑n)
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>r : ℕ<VAR>hr : x = (-ζ) ^ r<GOAL>(-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>n₀ : ℕ<GOAL>F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)) ↔ ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>n₀ : ℕ<GOAL>(∀ (i : ℕ), ⇑(single R i) '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))) ↔ ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>n₀ : ℕ<GOAL>Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)) ≤ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⇑(single R i) '' ↑(F.N i))
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>x ≤ 0 ↔ ∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>((∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0) ∧ ∀ (j : RightMoves 0), x ⧏ moveRight 0 j) ↔ ∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : CompleteLattice γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>l u : α → β → γ<VAR>l₁ u₁ : β → γ → α<VAR>l₂ u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (l₁ b) (swap u b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)<GOAL>sInf (image2 u s t) = u (sInf s) (sInf t)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : CommSemiring F<VAR>inst✝¹ : Semiring E<VAR>inst✝ : Algebra F E<VAR>b : F →ₗ[F] E<VAR>hb : Function.Injective ⇑b<VAR>x y : F<VAR>e : (algebraMap F E) x = (algebraMap F E) y<GOAL>b x = b y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a b c d : α<VAR>h : b ≠ 0<GOAL>(a + b) / b = a / b + 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹ : OrderedSemiring 𝕜<VAR>inst✝ : Fintype ι<VAR>f : ι → 𝕜<GOAL>f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f < g<VAR>gh : g ≈ h<GOAL>(h - f).Pos
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f < g<VAR>gh : g ≈ h<GOAL>h - f = g - f + -(g - h)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M✝ : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M✝<VAR>inst✝ : Module R M✝<VAR>inst : IsNoetherianRing R<VAR>I : Ideal R[X]<VAR>M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯<VAR>hm : M ∈ Set.range I.leadingCoeffNth<VAR>N : ℕ<VAR>HN : I.leadingCoeffNth N = M<VAR>s : Finset R[X]<VAR>hs : Submodule.span R ↑s = I.degreeLE ↑N<VAR>k : ℕ<VAR>h : N < k<VAR>x : R<VAR>hx : x ∈ I.leadingCoeffNth k<VAR>hxm : x ∉ M<VAR>this : IsNoetherian R R<GOAL>¬M < I.leadingCoeffNth k
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M✝ : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M✝<VAR>inst✝ : Module R M✝<VAR>inst : IsNoetherianRing R<VAR>I : Ideal R[X]<VAR>M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯<VAR>hm : M ∈ Set.range I.leadingCoeffNth<VAR>N : ℕ<VAR>HN : I.leadingCoeffNth N = M<VAR>s : Finset R[X]<VAR>hs : Submodule.span R ↑s = I.degreeLE ↑N<VAR>k : ℕ<VAR>h : N < k<VAR>x : R<VAR>hx : x ∈ I.leadingCoeffNth k<VAR>hxm : x ∉ M<VAR>this : IsNoetherian R R<GOAL>I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M✝ : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M✝<VAR>inst✝ : Module R M✝<VAR>inst : IsNoetherianRing R<VAR>I : Ideal R[X]<VAR>M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯<VAR>hm : M ∈ Set.range I.leadingCoeffNth<VAR>N : ℕ<VAR>HN : I.leadingCoeffNth N = M<VAR>s : Finset R[X]<VAR>hs : Submodule.span R ↑s = I.degreeLE ↑N<VAR>hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M<VAR>hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s<VAR>this : Submodule.span R[X] ↑s = Ideal.span ↑s<VAR>p : R[X]<VAR>hp : p ∈ I<VAR>k : ℕ<VAR>hn : p.natDegree = k<GOAL>p ∈ Ideal.span ↑s
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M✝ : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M✝<VAR>inst✝ : Module R M✝<VAR>inst : IsNoetherianRing R<VAR>I : Ideal R[X]<VAR>M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯<VAR>hm : M ∈ Set.range I.leadingCoeffNth<VAR>N : ℕ<VAR>HN : I.leadingCoeffNth N = M<VAR>s : Finset R[X]<VAR>hs : Submodule.span R ↑s = I.degreeLE ↑N<VAR>hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M<VAR>hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s<VAR>this : Submodule.span R[X] ↑s = Ideal.span ↑s<VAR>k : ℕ<VAR>ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s<VAR>p : R[X]<VAR>hp : p ∈ I<VAR>hn : p.natDegree = k<GOAL>p ∈ Ideal.span ↑s
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M✝ : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M✝<VAR>inst✝ : Module R M✝<VAR>inst : IsNoetherianRing R<VAR>I : Ideal R[X]<VAR>M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯<VAR>hm : M ∈ Set.range I.leadingCoeffNth<VAR>N : ℕ<VAR>HN : I.leadingCoeffNth N = M<VAR>s : Finset R[X]<VAR>hs : Submodule.span R ↑s = I.degreeLE ↑N<VAR>hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M<VAR>hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s<VAR>this : Submodule.span R[X] ↑s = Ideal.span ↑s<VAR>k : ℕ<VAR>ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s<VAR>p : R[X]<VAR>hp : p ∈ I<VAR>hn : p.natDegree = k<VAR>h : k ≤ N<GOAL>p ∈ Ideal.span ↑s
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M✝ : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M✝<VAR>inst✝ : Module R M✝<VAR>inst : IsNoetherianRing R<VAR>I : Ideal R[X]<VAR>M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯<VAR>hm : M ∈ Set.range I.leadingCoeffNth<VAR>N : ℕ<VAR>HN : I.leadingCoeffNth N = M<VAR>s : Finset R[X]<VAR>hs : Submodule.span R ↑s = I.degreeLE ↑N<VAR>hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M<VAR>hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s<VAR>this : Submodule.span R[X] ↑s = Ideal.span ↑s<VAR>k : ℕ<VAR>ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s<VAR>p : R[X]<VAR>hp : p ∈ I<VAR>hn : p.natDegree = k<VAR>h : N < k<GOAL>p ∈ Ideal.span ↑s
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝⁷ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x✝ : α<VAR>s t : Set α<VAR>y✝ z : β<VAR>γ : Type u_3<VAR>inst✝⁶ : LinearOrder γ<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : OrderTopology γ<VAR>δ : Type u_4<VAR>inst✝³ : LinearOrder δ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : OrderTopology δ<VAR>ι : Type u_5<VAR>inst✝ : TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>y : α<VAR>x : ι<VAR>hf : UpperSemicontinuousAt f (g x)<VAR>hg : ContinuousAt g x<VAR>hy : g x = y<GOAL>UpperSemicontinuousAt (fun x => f (g x)) x
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c a : α<VAR>u : αˣ<GOAL>a * (↑u * ↑u⁻¹) = a
<VAR>X : Type u_1<VAR>inst✝ : EMetricSpace X<VAR>s✝ t✝ : Set X<VAR>x y : X<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : Set X<VAR>t : ι → Set X<GOAL>IsMetricSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, IsMetricSeparated s (t i)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>f₁ g₁ f₂ g₂ : C ⟶ D<VAR>h₁ : Homotopy f₁ g₁<VAR>h₂ : Homotopy f₂ g₂<VAR>i j : ι<VAR>hij : ¬c.Rel j i<GOAL>(h₁.hom + h₂.hom) i j = 0