ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²⁵ : Semiring R₁<VAR>inst✝²⁴ : Semiring R₂<VAR>inst✝²³ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>inst✝²² : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝²¹ : RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>inst✝²⁰ : RingHomInvPair σ₂₃ σ₃₂<VAR>inst✝¹⁹ : RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>inst✝¹⁸ : RingHomInvPair σ₁₃ σ₃₁<VAR>inst✝¹⁷ : RingHomInvPair σ₃₁ σ₁₃<VAR>inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹⁵ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M₁<VAR>inst✝¹³ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹² : TopologicalSpace M'₁<VAR>inst✝¹¹ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace M₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝⁸ : TopologicalSpace M₃<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁶ : TopologicalSpace M₄<VAR>inst✝⁵ : AddCommMonoid M₄<VAR>inst✝⁴ : Module R₁ M₁<VAR>inst✝³ : Module R₁ M'₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>inst✝ : TopologicalSpace R₁<VAR>f g : R₁ ≃L[R₁] M₁<VAR>h : f 1 = g 1<VAR>x : R₁<GOAL>f (x * 1) = g (x * 1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X X' : SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : MorphComponents X n Z<VAR>g : X' ⟶ X<VAR>h : Z ⟶ Z'<GOAL>(id X n).φ = 𝟙 (X _[n + 1])
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X X' : SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : MorphComponents X n Z<VAR>g : X' ⟶ X<VAR>h : Z ⟶ Z'<GOAL>PInfty.f (n + 1) ≫ (id X n).a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev = (P (n + 1)).f (n + 1) + (Q (n + 1)).f (n + 1)
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : L.Structure N<VAR>S : ι →o L.Substructure M<GOAL>(liftInclusion S).toHom.range = ⨆ i, S i
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n : ℕ<VAR>hpos : 0 < n<GOAL>Irreducible (cyclotomic n ℤ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n : ℕ<VAR>hpos : 0 < n<GOAL>Irreducible (minpoly ℤ (cexp (2 * ↑Real.pi * I / ↑n)))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n : ℕ<VAR>hpos : 0 < n<GOAL>IsIntegral ℤ (cexp (2 * ↑Real.pi * I / ↑n))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype m<VAR>M : Matrix m n α<VAR>i✝ : l<VAR>j✝ : n<GOAL>(0 * M) i✝ j✝ = 0 i✝ j✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<VAR>x : β<VAR>hx : x ∈ image f s.support<GOAL>x ∈ (mapDomain f s).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<VAR>x : β<VAR>hx : ∃ a, ¬s a = 0 ∧ f a = x<GOAL>x ∈ (mapDomain f s).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<VAR>hx_w : α<VAR>hx_h_left : ¬s hx_w = 0<GOAL>f hx_w ∈ (mapDomain f s).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<VAR>hx_w : α<VAR>hx_h_left : ¬s hx_w = 0<GOAL>¬(mapDomain f s) (f hx_w) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<VAR>hx_w : α<VAR>hx_h_left : ¬s hx_w = 0<GOAL>¬s hx_w = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<VAR>hx_w : α<VAR>hx_h_left : ¬s hx_w = 0<GOAL>hx_w ∈ ↑s.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : α →₀ M<VAR>hf : Set.InjOn f ↑s.support<VAR>hx_w : α<VAR>hx_h_left : ¬s hx_w = 0<GOAL>↑s.support ⊆ ↑s.support
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<GOAL>cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<GOAL>cyclotomic' n K = (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic<GOAL>cyclotomic' n K = (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic<GOAL>0 + (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K = cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K ∧ degree 0 < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic<GOAL>(∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K = cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K ∧ ⊥ < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic<GOAL>⊥ < (∏ i ∈ n.properDivisors, cyclotomic' i K).degree
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic<GOAL>(∏ i ∈ n.properDivisors, cyclotomic' i K).degree ≠ ⊥
<VAR>K✝ : Type u_1<VAR>inst✝² : Field K✝<VAR>K : Type u_2<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h✝ : IsPrimitiveRoot ζ n<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic<VAR>h : (∏ i ∈ n.properDivisors, cyclotomic' i K).degree = ⊥<GOAL>False
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : 𝕜<GOAL>projectiveSeminormAux (List.map (fun y => (a * y.1, y.2)) p) = ‖a‖ * projectiveSeminormAux p
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : 𝕜<GOAL>(List.map ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) p).sum = ‖a‖ * (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : 𝕜<GOAL>(List.map ((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) p).sum = (List.map ((fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : 𝕜<VAR>x : 𝕜 × ((i : ι) → E i)<GOAL>((fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ∘ fun y => (a * y.1, y.2)) x = ((fun x => ‖a‖ • x) ∘ fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>a : 𝕜<VAR>x : 𝕜 × ((i : ι) → E i)<GOAL>‖a‖ * ‖x.1‖ * ∏ x_1 : ι, ‖x.2 x_1‖ = ‖a‖ * (‖x.1‖ * ∏ x_1 : ι, ‖x.2 x_1‖)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<GOAL>F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<GOAL>F.IsSheafPairwiseIntersections ↔ F.IsSheafPreservesLimitPairwiseIntersections
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ Prod.mk a '' t
<VAR>a b : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 3<VAR>hb : b % 4 = 3<VAR>hr : jacobiSymNat b a = r<GOAL>jacobiSymNat a b = -r
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x<GOAL>∀ x ∈ interior (interior D), 0 < deriv (deriv f) x
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : Lattice α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>toSemilatticeSup✝¹ : SemilatticeSup α<VAR>toInf✝¹ : Inf α<VAR>inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>toSemilatticeSup✝ : SemilatticeSup α<VAR>toInf✝ : Inf α<VAR>inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : Lattice α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>toSemilatticeSup✝ : SemilatticeSup α<VAR>toInf✝¹ : Inf α<VAR>inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>toInf✝ : Inf α<VAR>inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : Lattice α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>toSemilatticeSup✝ : SemilatticeSup α<VAR>toInf✝ : Inf α<VAR>inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter β<GOAL>map f (comap f G ⊓ F) = G ⊓ map f F
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>-(⁅y, ⁅z, x⁆⁆ - ⁅z, ⁅y, x⁆⁆) + ⁅y, ⁅z, x⁆⁆ + -⁅z, ⁅y, x⁆⁆ = 0
<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 α<GOAL>f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → DecidableEq (α i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Ioo a b).card = ∏ i : ι, (Icc (a i) (b i)).card - 2
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n : ℕ<GOAL>Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n✝ n : ℕ<GOAL>Stream'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) n = IntFractPair.stream v n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this : DecidableEq L := Classical.decEq L<GOAL>∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance<GOAL>∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance<VAR>s' : Finset L := IsNoetherian.finsetBasisIndex K L<VAR>bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L<GOAL>∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance<VAR>s' : Finset L := IsNoetherian.finsetBasisIndex K L<VAR>bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L<VAR>y : A<VAR>hy : y ≠ 0<VAR>his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)<GOAL>∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance<VAR>s' : Finset L := IsNoetherian.finsetBasisIndex K L<VAR>bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L<VAR>y : A<VAR>hy : y ≠ 0<VAR>his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)<VAR>hy' : (algebraMap A L) y ≠ 0<GOAL>∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance<VAR>s' : Finset L := IsNoetherian.finsetBasisIndex K L<VAR>bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L<VAR>y : A<VAR>hy : y ≠ 0<VAR>his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)<VAR>hy' : (algebraMap A L) y ≠ 0<GOAL>Function.LeftInverse (fun x => ((algebraMap A L) y)⁻¹ * x) { toFun := fun x => (algebraMap A L) y * x, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance<VAR>s' : Finset L := IsNoetherian.finsetBasisIndex K L<VAR>bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L<VAR>y : A<VAR>hy : y ≠ 0<VAR>his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)<VAR>hy' : (algebraMap A L) y ≠ 0<GOAL>Function.RightInverse (fun x => ((algebraMap A L) y)⁻¹ * x) { toFun := fun x => (algebraMap A L) y * x, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>this : IsNoetherian K L := IsNoetherian.iff_fg.mpr inferInstance<VAR>s' : Finset L := IsNoetherian.finsetBasisIndex K L<VAR>bs' : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K L } K L := IsNoetherian.finsetBasis K L<VAR>y : A<VAR>hy : y ≠ 0<VAR>his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)<VAR>hy' : (algebraMap A L) y ≠ 0<GOAL>∀ (x : { x // x ∈ s' }), IsIntegral A ((bs'.map (let __src := (lmul K L) ((algebraMap A L) y); { toFun := fun x => (algebraMap A L) y * x, map_add' := ⋯, map_smul' := ⋯, invFun := fun x => ((algebraMap A L) y)⁻¹ * x, left_inv := ⋯, right_inv := ⋯ })) x)