ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R ↥M₁<VAR>N' : Submodule R ↥N₁<VAR>left✝¹ : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))<VAR>hM : Submodule.map M₁.subtype M' ≤ M₁<VAR>hN : Submodule.map N₁.subtype N' ≤ N₁<GOAL>s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<VAR>M' : Submodule R ↥M₁<VAR>N' : Submodule R ↥N₁<VAR>left✝¹ : Module.Finite R ↥M'<VAR>left✝ : Module.Finite R ↥N'<VAR>hM : Submodule.map M₁.subtype M' ≤ M₁<VAR>hN : Submodule.map N₁.subtype N' ≤ N₁<VAR>h : s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN) ∘ₗ map (M₁.subtype.submoduleMap M') (N₁.subtype.submoduleMap N')))<GOAL>s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))
<VAR>n : ℕ<VAR>a : Fin n<VAR>x : ℕ<GOAL>x ∈ map valEmbedding (Ioi a) ↔ x ∈ Ioc (↑a) (n - 1)
<VAR>n : ℕ<VAR>a : Fin n<VAR>x : ℕ<GOAL>(∃ a_1, a < a_1 ∧ valEmbedding a_1 = x) ↔ ↑a < x ∧ x ≤ n - 1
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallyUnramified R S<GOAL>FormallyUnramified Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallyUnramified R S<VAR>this : FormallyUnramified S Sₘ<GOAL>FormallyUnramified Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallyUnramified R S<VAR>this✝ : FormallyUnramified S Sₘ<VAR>this : FormallyUnramified R Sₘ<GOAL>FormallyUnramified Rₘ Sₘ
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>s : S<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff i ((truncate n) (liftFun f s)) = TruncatedWittVector.coeff i ((f n) s)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>s : S<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff (Fin.last ↑i) ((f (↑i + 1)) s) = TruncatedWittVector.coeff i ((f n) s)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>s : S<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff (Fin.castLE ⋯ (Fin.last ↑i)) ((f n) s) = TruncatedWittVector.coeff i ((f n) s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableRel f.SameCycle<VAR>inst✝ : DecidableRel g.SameCycle<VAR>h : f.SameCycle x y<VAR>z : α<GOAL>(f.cycleOf x) z = (f.cycleOf y) z
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableRel f.SameCycle<VAR>inst✝ : DecidableRel g.SameCycle<VAR>h : f.SameCycle x y<VAR>z : α<GOAL>(if f.SameCycle x z then f z else z) = (f.cycleOf y) z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>Q : QuadraticForm R M<VAR>inst✝ : Invertible 2<VAR>m : M<VAR>h : IsUnit ((ι Q) m)<GOAL>IsUnit (Q m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>Q : QuadraticForm R M<VAR>inst✝ : Invertible 2<VAR>m : M<VAR>h : IsUnit ((ι Q) m)<VAR>val✝ : Invertible ((ι Q) m)<GOAL>IsUnit (Q m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>Q : QuadraticForm R M<VAR>inst✝ : Invertible 2<VAR>m : M<VAR>h : IsUnit ((ι Q) m)<VAR>val✝ : Invertible ((ι Q) m)<VAR>this : Invertible (Q m) := invertibleOfInvertibleι Q m<GOAL>IsUnit (Q m)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>v w : V<GOAL>s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addLeftEmbedding c) (Ico a b) = Ico (c + a) (c + b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addLeftEmbedding c) '' Set.Ico a b = Set.Ico (c + a) (c + b)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>a : R<VAR>x y : M<GOAL>polar (⇑Q) (a • x) y = a • polar (⇑Q) x y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>a : R<VAR>x y : M<VAR>B : BilinMap R M N<VAR>h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y<GOAL>polar (⇑Q) (a • x) y = a • polar (⇑Q) x y
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Filter α<VAR>s : Set α<VAR>a✝ : α<VAR>m : α → β<VAR>f : Filter β<VAR>a : α<GOAL>a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Filter α<VAR>s : Set α<VAR>a✝ : α<VAR>m : α → β<VAR>f : Filter β<VAR>a : α<GOAL>(∀ y ∈ f, ∀ (x : Set α), m ⁻¹' y ⊆ x → a ∈ x) ↔ ∀ s ∈ f, m a ∈ s
<VAR>f : Type u₀ → Type u₁<VAR>inst✝¹ : Applicative f<VAR>inst✝ : LawfulApplicative f<VAR>α β : Type u₀<VAR>h : ∀ (γ : Type u₀), Injective pure<VAR>e₁ e₂ : α ≃ β<VAR>H : mapEquiv f e₁ = mapEquiv f e₂<VAR>x : α<GOAL>pure (e₁ x) = pure (e₂ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hc : 0 ≤ c<VAR>x : α<GOAL>x ∈ {x | (fun x => ‖0‖ ≤ c * ‖g' x‖) x}
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<GOAL>Finset.image Prod.fst m.toEnumFinset = m.toFinset
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>n : ℤ<GOAL>1 < normSq ↑(T ^ n • z)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>n : ℤ<VAR>hz₁ : 1 < z.re * z.re + z.im * z.im<GOAL>1 < normSq ↑(T ^ n • z)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>n : ℤ<VAR>hz₁ : 1 < z.re * z.re + z.im * z.im<VAR>hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n<GOAL>1 < normSq ↑(T ^ n • z)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>n : ℤ<VAR>hz₁ : 1 < z.re * z.re + z.im * z.im<VAR>hzn : 0 ≤ ↑n * (2 * z.re) + ↑n * ↑n<VAR>this : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im<GOAL>1 < normSq ↑(T ^ n • z)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : QuasiErgodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s =ᶠ[ae μ] s<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : QuasiErgodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s =ᶠ[ae μ] s<VAR>t : Set α<VAR>h₀ : MeasurableSet t<VAR>h₁ : t =ᶠ[ae μ] s<VAR>h₂ : f ⁻¹' t = t<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
<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>h : ¬IsUnit A.det<GOAL>A⁻¹.det = Ring.inverse A.det
<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>h : ¬IsUnit A.det<VAR>h✝ : IsEmpty n<GOAL>A⁻¹.det = Ring.inverse A.det
<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>h : ¬IsUnit A.det<VAR>h✝ : Nonempty n<GOAL>A⁻¹.det = Ring.inverse A.det
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<GOAL>¬Odd n ↔ n % 2 = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>c : k<GOAL>∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>c : k<GOAL>∑ x ∈ s, (c • weightedVSubVSubWeights k j i) x + ∑ x ∈ s, affineCombinationSingleWeights k i x = 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>𝕜' : Type u_3<VAR>inst✝⁵ : NontriviallyNormedField 𝕜'<VAR>inst✝⁴ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝³ : NormedSpace 𝕜' E<VAR>inst✝² : IsScalarTower 𝕜 𝕜' E<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>p' : E → FormalMultilinearSeries 𝕜' E F<VAR>h : HasFTaylorSeriesUpToOn n f p' s<VAR>m : ℕ<VAR>hm : ↑m < n<VAR>x : E<VAR>hx : x ∈ s<GOAL>HasFDerivWithinAt (fun x => FormalMultilinearSeries.restrictScalars 𝕜 (p' x) m) (FormalMultilinearSeries.restrictScalars 𝕜 (p' x) m.succ).curryLeft s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>g : Set (Set α)<VAR>hc : 2 < c<GOAL>IsGreatest {f | CardinalInterFilter f c ∧ g ⊆ f.sets} (cardinalGenerate g hc)
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>g : Set (Set α)<VAR>hc : 2 < c<GOAL>cardinalGenerate g hc ∈ upperBounds {f | CardinalInterFilter f c ∧ g ⊆ f.sets}
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>g : Set (Set α)<VAR>hc : 2 < c<VAR>f : Filter α<VAR>fct : CardinalInterFilter f c<VAR>hf : g ⊆ f.sets<GOAL>f ≤ cardinalGenerate g hc
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>s s₁ s₂ t t₁ t₂ u : Set X<GOAL>SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u
<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 K S<VAR>x : S<VAR>h : IsIntegral K x<GOAL>LinearIndependent K fun i => x ^ ↑i
<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 K S<VAR>x : S<VAR>h : IsIntegral K x<VAR>g : Fin (minpoly K x).natDegree → K<VAR>hg : ∑ i : Fin (minpoly K x).natDegree, g i • x ^ ↑i = 0<VAR>i : Fin (minpoly K x).natDegree<GOAL>g i = 0
<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 K S<VAR>x : S<VAR>h : IsIntegral K x<VAR>g : Fin (minpoly K x).natDegree → K<VAR>i : Fin (minpoly K x).natDegree<VAR>hg : (aeval x) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial ↑x_1) (g x_1)) = 0<GOAL>g i = 0
<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 K S<VAR>x : S<VAR>h : IsIntegral K x<VAR>g : Fin (minpoly K x).natDegree → K<VAR>i : Fin (minpoly K x).natDegree<VAR>hg : (aeval x) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial ↑x_1) (g x_1)) = 0<GOAL>(∑ x_1 : Fin (minpoly K x).natDegree, (monomial ↑x_1) (g x_1)).degree < (minpoly K x).degree
<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 K S<VAR>x : S<VAR>h : IsIntegral K x<VAR>g : Fin (minpoly K x).natDegree → K<VAR>i : Fin (minpoly K x).natDegree<VAR>hg : (aeval x) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial ↑x_1) (g x_1)) = 0<VAR>hn0 : ¬g i = 0<VAR>h0 : ∑ x_1 : Fin (minpoly K x).natDegree, (monomial ↑x_1) (g x_1) = 0<GOAL>g i = 0
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<VAR>f : R[X]<GOAL>(expand R p) f = map (↑(frobeniusEquiv R p).symm) f ^ p
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹⁴ : Semiring R<VAR>inst✝¹³ : Semiring R₂<VAR>inst✝¹² : Semiring R₃<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R₂ M₂<VAR>inst✝⁶ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>p✝ p' : Submodule R M<VAR>q q' : Submodule R₂ M₂<VAR>x : M<VAR>inst✝⁴ : RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>inst✝¹ : RingHomSurjective σ₂₃<VAR>inst✝ : RingHomSurjective σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>p : Submodule R M<GOAL>↑(map (g.comp f) p) = ↑(map g (map f p))
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<GOAL>(α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom = W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<GOAL>(W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom) ≫ (α_ (W ⊗ X) Y Z).inv = (W ◁ (α_ X Y Z).inv ≫ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv) ≫ (α_ (W ⊗ X) Y Z).inv
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommMonoidWithZero R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : PosMulStrictMono R<VAR>inst✝ : Nontrivial R<VAR>f g : ι → R<VAR>s t : Finset ι<VAR>hf : ∀ i ∈ s, 0 < f i<VAR>hfg : ∀ i ∈ s, f i < g i<VAR>h_ne : s.Nonempty<GOAL>∏ i ∈ s, f i < ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommMonoidWithZero R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : PosMulStrictMono R<VAR>inst✝ : Nontrivial R<VAR>f g : ι → R<VAR>s t : Finset ι<VAR>hf : ∀ i ∈ s, 0 < f i<VAR>hfg : ∀ i ∈ s, f i < g i<VAR>h_ne : s.Nonempty<GOAL>∃ i ∈ s, f i < g i
<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>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>inst✝³ : CommMonoid α₁<VAR>inst✝² : CommMonoid α₂<VAR>inst✝¹ : CommMonoid β₁<VAR>inst✝ : CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanIso n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanIso n A₂ B₂ f₂<VAR>s t : Multiset (α₁ × α₂)<VAR>hsA : ∀ ⦃x : α₁ × α₂⦄, x ∈ s → x ∈ A₁ ×ˢ A₂<VAR>htA : ∀ ⦃x : α₁ × α₂⦄, x ∈ t → x ∈ A₁ ×ˢ A₂<VAR>hs : card s = n<VAR>ht : card t = n<GOAL>(map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod ↔ s.prod = t.prod
<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>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>inst✝³ : CommMonoid α₁<VAR>inst✝² : CommMonoid α₂<VAR>inst✝¹ : CommMonoid β₁<VAR>inst✝ : CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanIso n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanIso n A₂ B₂ f₂<VAR>s t : Multiset (α₁ × α₂)<VAR>hs : card s = n<VAR>ht : card t = n<VAR>hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂<VAR>htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂<GOAL>(map (Prod.map f₁ f₂) s).prod = (map (Prod.map f₁ f₂) t).prod ↔ s.prod = t.prod
<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>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>inst✝³ : CommMonoid α₁<VAR>inst✝² : CommMonoid α₂<VAR>inst✝¹ : CommMonoid β₁<VAR>inst✝ : CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanIso n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanIso n A₂ B₂ f₂<VAR>s t : Multiset (α₁ × α₂)<VAR>hs : card s = n<VAR>ht : card t = n<VAR>hsA : (∀ (a : α₁) (b : α₂), (a, b) ∈ s → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ s → b ∈ A₂<VAR>htA : (∀ (a : α₁) (b : α₂), (a, b) ∈ t → a ∈ A₁) ∧ ∀ (a : α₁) (b : α₂), (a, b) ∈ t → b ∈ A₂<GOAL>(map (fun x => f₁ x.1) s).prod = (map (fun x => f₁ x.1) t).prod ∧ (map (fun x => f₂ x.2) s).prod = (map (fun x => f₂ x.2) t).prod ↔ (map Prod.fst s).prod = (map Prod.fst t).prod ∧ (map Prod.snd s).prod = (map Prod.snd t).prod
<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>i : ι✝<VAR>a : α✝<VAR>f✝ g✝ : ι✝ → α✝<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : CommSemiring α<VAR>f g : ι → α<GOAL>∏ a : ι, (f a + g a) = ∑ t : Finset ι, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>σ : Type u_1<VAR>i : σ<VAR>x : MvPolynomial σ R<GOAL>(mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • (D R (MvPolynomial σ R)) (MvPolynomial.X i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>σ : Type u_1<VAR>i : σ<VAR>x : MvPolynomial σ R<GOAL>(mvPolynomialBasis R σ).repr ((mvPolynomialBasis R σ).repr.symm (Finsupp.single i x)) = (mvPolynomialBasis R σ).repr (x • (D R (MvPolynomial σ R)) (MvPolynomial.X i))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Icc a b)<VAR>hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)<VAR>x : ℝ<VAR>hx : x ∈ Icc a b<GOAL>f x ≤ B x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>B B' : ℝ → ℝ<VAR>ha : f a ≤ B a<VAR>hB : ContinuousOn B (Icc a b)<VAR>hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r<VAR>Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)<VAR>x : ℝ<VAR>hx : x ∈ Icc a b<VAR>this : ContinuousWithinAt (fun r => B x + r * (x - a)) (Ioi 0) 0<GOAL>f x ≤ B x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<GOAL>∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, n ≤ a}, ⊤ ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<GOAL>∀ (b : α), (∀ (x : α), x ≤ b) → b = ⊤
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 ≤ (a * a₁⁻¹).y
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<GOAL>Tendsto (fun g => |(↑g • z).re|) cofinite atTop
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<GOAL>Tendsto (fun g => (↑g • z).re) cofinite (cocompact ℝ)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0<GOAL>Tendsto (fun g => (↑g • z).re) cofinite (cocompact ℝ)