ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLattice α✝<VAR>α : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>f : Filter α<VAR>inst✝ : f.NeBot<VAR>b : β<GOAL>limsup (fun x => b) f = b
<GOAL>HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)
<VAR>this : HasDerivAt Gamma ↑(-√π * (γ + 2 * Real.log 2)) ↑(1 / 2)<GOAL>HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)
<GOAL>∀ (m : ℕ), ↑(1 / 2) ≠ -↑m
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<VAR>h : (l :: L).any isEmpty = true<GOAL>(l :: L).sections = []
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<VAR>h : l.isEmpty = true ∨ L.any isEmpty = true<GOAL>(l :: L).sections = []
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑(pos p).bit1 = ↑(pos p) + ↑(pos p) + 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑p.bit1 = ↑p + ↑p + 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑(neg p).bit1 = ↑(neg p) + ↑(neg p) + 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>-↑(Num.casesOn p.pred' 1 bit1) = -↑p + -↑p + 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<VAR>e : p.pred' = Num.zero<VAR>ep : p = Num.zero.succ'<GOAL>-↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p a : PosNum<VAR>e : p.pred' = Num.pos a<VAR>ep : p = (Num.pos a).succ'<GOAL>-↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<GOAL>ψ ≠ 1 ↔ ψ 1 ≠ 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<GOAL>(∃ x, ψ x ≠ 1) ↔ ψ 1 ≠ 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<GOAL>(∃ x, ψ x ≠ 1) → ψ 1 ≠ 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<GOAL>ψ 1 = 1 → ∀ (x : ZMod n), ψ x = 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<VAR>h₁ : ψ 1 = 1<VAR>a : ZMod n<GOAL>ψ a = 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<VAR>h₁ : ψ 1 = 1<VAR>a : ZMod n<VAR>ha₁ : a = a.val • 1<GOAL>ψ a = 1
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Group M<VAR>a b : M<VAR>ha : a ∈ S.centralizer<VAR>g : M<VAR>hg : g ∈ S<GOAL>g * a⁻¹ = a⁻¹ * g
<VAR>n : ℕ<VAR>θ : [n + 1] ⟶ [n]<VAR>inst✝ : Epi θ<GOAL>∃ i, θ = σ i
<VAR>n : ℕ<VAR>θ : [n + 1] ⟶ [n]<VAR>inst✝ : Epi θ<VAR>i : Fin (n + 1)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = σ i ≫ θ'<GOAL>∃ i, θ = σ i
<VAR>n : ℕ<VAR>θ : [n + 1] ⟶ [n]<VAR>inst✝ : Epi θ<VAR>i : Fin (n + 1)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = σ i ≫ θ'<GOAL>θ = σ i
<VAR>n : ℕ<VAR>θ : [n + 1] ⟶ [n]<VAR>inst✝ : Epi θ<VAR>i : Fin (n + 1)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = σ i ≫ θ'<VAR>this : Epi (σ i ≫ θ')<GOAL>θ = σ i
<VAR>n : ℕ<VAR>θ : [n + 1] ⟶ [n]<VAR>inst✝ : Epi θ<VAR>i : Fin (n + 1)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = σ i ≫ θ'<VAR>this✝ : Epi (σ i ≫ θ')<VAR>this : Epi θ'<GOAL>θ = σ i
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>hq : q.natDegree ≠ 0<VAR>P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r<VAR>key1 : ∀ {r : F[X]}, Irreducible r → P r<VAR>key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)<GOAL>Splits (algebraMap F (p.comp q).SplittingField) p
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>gaussianReal μ v ≪ ℙ
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>ℙ.withDensity (gaussianPDF μ v) ≪ ℙ
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<GOAL>((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<VAR>h✝ : Subsingleton R<GOAL>((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<VAR>h✝ : Nontrivial R<GOAL>((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<VAR>h✝ : Nontrivial R<GOAL>(aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly = 0
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<VAR>h✝ : Nontrivial R<GOAL>∀ (q : R[X]), q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree → q = 0 ∨ (aeval h.gen) q ≠ 0
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<VAR>h✝ : Nontrivial R<VAR>q : R[X]<VAR>hq : q.degree < ((leftMulMatrix h.basis) h.gen).charpoly.degree<VAR>h0 : ¬q = 0<GOAL>(aeval h.gen) q ≠ 0
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<VAR>h✝ : Nontrivial R<VAR>q : R[X]<VAR>hq : q.degree < ↑h.dim<VAR>h0 : ¬q = 0<GOAL>(aeval h.gen) q ≠ 0
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>n : Type v<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>N : Type w<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>S : Type u_1<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>h : PowerBasis R S<VAR>h✝ : Nontrivial R<VAR>q : R[X]<VAR>h0 : ¬q = 0<VAR>hq : (aeval h.gen) q = 0<GOAL>↑h.dim ≤ q.degree
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommMonoidWithZero R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : ZeroLEOneClass R<VAR>inst✝ : PosMulMono R<VAR>f g : ι → R<VAR>s t : Finset ι<VAR>h0 : ∀ i ∈ s, 0 ≤ f i<VAR>h1 : ∀ i ∈ s, f i ≤ 1<GOAL>∏ i ∈ s, f i ≤ 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommMonoidWithZero R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : ZeroLEOneClass R<VAR>inst✝ : PosMulMono R<VAR>f g : ι → R<VAR>s t : Finset ι<VAR>h0 : ∀ i ∈ s, 0 ≤ f i<VAR>h1 : ∀ i ∈ s, f i ≤ 1<GOAL>∏ i ∈ s, 1 = 1
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>S : Set L<VAR>hS : ∀ x ∈ S, IsIntegral K x<GOAL>Algebra.IsAlgebraic K ↥(adjoin K S)
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>S : Set L<VAR>hS : ∀ x ∈ S, IsIntegral K x<GOAL>Algebra.IsAlgebraic K ↥(⨆ i, K⟮↑i⟯)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a * b⁻¹ < c ↔ a < c * b
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>τ π : Ω → ℕ<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>i : ℕ<VAR>ω : Ω<GOAL>ω ∈ {ω | (τ + π) ω ≤ i} ↔ ω ∈ ⋃ k, ⋃ (_ : k ≤ i), {ω | π ω = k} ∩ {ω | τ ω + k ≤ i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>τ π : Ω → ℕ<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>i : ℕ<VAR>ω : Ω<GOAL>τ ω + π ω ≤ i ↔ ∃ i_1 ≤ i, π ω = i_1 ∧ τ ω + i_1 ≤ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<GOAL>#↑{o' | o' < o} = Cardinal.lift.{u + 1, u} o.card
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : CompleteLattice α<VAR>inst✝² : CompleteLattice β<VAR>inst✝¹ : CompleteLattice γ<VAR>inst✝ : CompleteLattice δ<VAR>g : CompleteLatticeHom β γ<VAR>f₁ f₂ : CompleteLatticeHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : Nonempty Y<VAR>f : LocallyConstant X Y<GOAL>∃ y, f = const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : Nonempty Y<VAR>f : LocallyConstant X Y<VAR>x : X<GOAL>∃ y, f = const X y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : Nonempty Y<VAR>f : LocallyConstant X Y<VAR>hX : ¬Nonempty X<GOAL>∃ y, f = const X y
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f f₁ : E → F<VAR>f' f₀' f₁' : F<VAR>s t : Set E<VAR>x v : E<GOAL>HasLineDerivAt 𝕜 f f' x v ↔ (fun t => f (x + t • v) - f x - t • f') =o[𝓝 0] fun t => t
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P✝ P : R[X]<VAR>N : ℕ<VAR>hN : P.natDegree ≤ N<GOAL>IsNilpotent (reflect N P) ↔ IsNilpotent P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P✝ P : R[X]<VAR>N : ℕ<VAR>hN : P.natDegree ≤ N<GOAL>(∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P✝ P : R[X]<VAR>N : ℕ<VAR>hN : P.natDegree ≤ N<VAR>h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)<VAR>i : ℕ<VAR>hi : i ≤ N<GOAL>IsNilpotent (P.coeff i)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P✝ P : R[X]<VAR>N : ℕ<VAR>hN : P.natDegree ≤ N<VAR>h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)<VAR>i : ℕ<VAR>hi : N < i<GOAL>IsNilpotent (P.coeff i)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P✝ P : R[X]<VAR>N : ℕ<VAR>hN : P.natDegree ≤ N<VAR>h : ∀ (i : ℕ), IsNilpotent (P.coeff i)<VAR>i : ℕ<VAR>hi : i ≤ N<GOAL>IsNilpotent ((reflect N P).coeff i)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P✝ P : R[X]<VAR>N : ℕ<VAR>hN : P.natDegree ≤ N<VAR>h : ∀ (i : ℕ), IsNilpotent (P.coeff i)<VAR>i : ℕ<VAR>hi : N < i<GOAL>IsNilpotent ((reflect N P).coeff i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>a b x y x' y' : R<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x - x') (y - y')
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<GOAL>s.WellFoundedOn r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f✝ : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s<GOAL>s.WellFoundedOn r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f✝ : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s<VAR>h : s.WellFoundedOn r<GOAL>WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f✝ : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f : (fun a b => r ↑a ↑b) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s<VAR>h : s.WellFoundedOn r<GOAL>∀ (s_1 : Set α), s_1.Nonempty → ∃ m ∈ s_1, ∀ x ∈ s_1, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l✝ : E →L[𝕜] 𝕜<VAR>A B : Set E<VAR>X : Finset E<VAR>x w : E<VAR>l : E →L[𝕜] 𝕜<VAR>hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B<VAR>hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<GOAL>∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, l_1 y ≤ l_1 x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f d : ℕ → α<VAR>hdisj : Pairwise (Disjoint on d)<VAR>hsups : partialSups d = partialSups f<VAR>n : ℕ<GOAL>d (n + 1) = disjointed f (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f d : ℕ → α<VAR>hdisj : Pairwise (Disjoint on d)<VAR>hsups : partialSups d = partialSups f<VAR>n : ℕ<GOAL>d n.succ = (partialSups d) n.succ \ (partialSups d) n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f d : ℕ → α<VAR>hdisj : Pairwise (Disjoint on d)<VAR>hsups : partialSups d = partialSups f<VAR>n : ℕ<GOAL>Disjoint ((partialSups d) n) (d (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f d : ℕ → α<VAR>hdisj : Pairwise (Disjoint on d)<VAR>hsups : partialSups d = partialSups f<VAR>n : ℕ<GOAL>∀ m ≤ n, Disjoint ((partialSups d) m) (d n.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f d : ℕ → α<VAR>hdisj : Pairwise (Disjoint on d)<VAR>hsups : partialSups d = partialSups f<VAR>n m : ℕ<VAR>ih : m ≤ n → Disjoint ((partialSups d) m) (d n.succ)<VAR>hm : m + 1 ≤ n<GOAL>Disjoint ((partialSups d) (m + 1)) (d n.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f d : ℕ → α<VAR>hdisj : Pairwise (Disjoint on d)<VAR>hsups : partialSups d = partialSups f<VAR>n m : ℕ<VAR>ih : m ≤ n → Disjoint ((partialSups d) m) (d n.succ)<VAR>hm : m + 1 ≤ n<GOAL>Disjoint ((partialSups d) m) (d n.succ) ∧ Disjoint (d (m + 1)) (d n.succ)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (i : α), f i ≠ ⊤<GOAL>Summable (ENNReal.toNNReal ∘ f)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>sepDegree F ↥⊥ = 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)<GOAL>sepDegree F ↥⊥ = 1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<VAR>hα' : weightSpace M α ≠ ⊥<VAR>e : (chainTop α β).IsZero<GOAL>weightSpace M α = ⊥
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>s : Cone F.unop<VAR>m : s.pt ⟶ (coneUnopOfCocone c).pt<VAR>w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j<GOAL>m = (fun s => (hc.desc (coconeOfConeUnop s)).unop) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>s : Cone F.unop<VAR>m : s.pt ⟶ (coneUnopOfCocone c).pt<VAR>w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j<VAR>j : Jᵒᵖ<GOAL>(c.ι.app j ≫ m.op).unop = (c.ι.app j ≫ ((fun s => (hc.desc (coconeOfConeUnop s)).unop) s).op).unop
<VAR>X✝ X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>e : X ≅ Y<VAR>y : ↑Y.toTopCat<GOAL>Hom.stalkMap e.hom (e.inv.val.base y) ≫ Hom.stalkMap e.inv y = Y.presheaf.stalkSpecializes ⋯
<VAR>X✝ X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>e : X ≅ Y<VAR>y : ↑Y.toTopCat<GOAL>Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 Y) y = Y.presheaf.stalkSpecializes ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>m : M<VAR>x : ExteriorAlgebra R M<GOAL>(((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m * x) 0) 0 = (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i => (f (i + 1)).curryLeft m) x 0) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>m : M<VAR>x : ExteriorAlgebra R M<GOAL>(((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) (((LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) f)) x 0) 0 = (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i => (f (i + 1)).curryLeft m) x 0) 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : Ring R₂<VAR>inst✝⁹ : Ring R₃<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup 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>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<GOAL>ker f = ⊥ ↔ Injective ⇑f
<VAR>α : Type u<VAR>x : Tree α<GOAL>0 < x.numLeaves
<VAR>α : Type u<VAR>x : Tree α<GOAL>0 < x.numNodes + 1
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Tendsto f l (𝓝 C)<VAR>hg : Tendsto g l atTop<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<GOAL>∫ (x : ℝ) in Ioi a, f' x = m - f a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Surreal<GOAL>BddBelow (Set.range f)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Subtype Numeric<GOAL>BddBelow (Set.range fun i => ⟦f i⟧)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Subtype Numeric<VAR>g : ι → PGame := Subtype.val ∘ f<GOAL>BddBelow (Set.range fun i => ⟦f i⟧)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → Subtype Numeric<VAR>g : ι → PGame := Subtype.val ∘ f<VAR>hg : ∀ (i : ι), (g i).Numeric<GOAL>BddBelow (Set.range fun i => ⟦f i⟧)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>g : ι → PGame<VAR>hg : ∀ (i : ι), (g i).Numeric<VAR>x : PGame := PGame.mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x => (g ((equivShrink ι).symm x.fst)).moveRight x.snd<GOAL>BddBelow (Set.range fun i => mk (g i) ⋯)
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>g : ι → PGame<VAR>hg : ∀ (i : ι), (g i).Numeric<VAR>x : PGame := PGame.mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x => (g ((equivShrink ι).symm x.fst)).moveRight x.snd<VAR>i : ι<GOAL>mk x ⋯ ≤ mk (g i) ⋯
<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>g : ι → PGame<VAR>hg : ∀ (i : ι), (g i).Numeric<VAR>x : PGame := PGame.mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x => (g ((equivShrink ι).symm x.fst)).moveRight x.snd<VAR>i : ι<GOAL>(∀ (i_1 : x.LeftMoves), x.moveLeft i_1 ⧏ g ((equivShrink ι).symm ((equivShrink ι) i))) ∧ ∀ (j : (g ((equivShrink ι).symm ((equivShrink ι) i))).RightMoves), x ⧏ (g ((equivShrink ι).symm ((equivShrink ι) i))).moveRight j
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>E.variableChange WeierstrassCurve.VariableChange.id = E
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>E : EllipticCurve R<VAR>C : WeierstrassCurve.VariableChange R<GOAL>{ toWeierstrassCurve := E.toWeierstrassCurve, Δ' := WeierstrassCurve.VariableChange.id.u⁻¹ ^ 12 * E.Δ', coe_Δ' := ⋯ } = E
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m✝ n✝ : ℤ<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>m n : ℤ<VAR>h : m ≤ n<GOAL>a ^ m * a ^ (n - m) = a ^ n
<VAR>n : Int<VAR>d a : Nat<VAR>a0 : a ≠ 0<GOAL>mkRat (↑a * n) (a * d) = mkRat n d
<VAR>R : Type u_2<VAR>K : Type ?u.43539<VAR>L : Type ?u.43542<VAR>S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>T : Type u_1<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : IsDomain T<VAR>inst✝ : DecidableEq T<VAR>x : S<VAR>σ₁ σ₂ : S →ₐ[R] T<GOAL>eval₂ (↑σ₁) (σ₂ x) (minpolyDiv R x) = if σ₁ x = σ₂ x then σ₁ ((aeval x) (derivative (minpoly R x))) else 0
<VAR>R : Type u_2<VAR>K : Type ?u.43539<VAR>L : Type ?u.43542<VAR>S : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra K L<VAR>x✝ : S<VAR>hx : IsIntegral R x✝<VAR>T : Type u_1<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : IsDomain T<VAR>inst✝ : DecidableEq T<VAR>x : S<VAR>σ₁ σ₂ : S →ₐ[R] T<GOAL>eval₂ ((↑σ₁).comp (algebraMap R S)) (σ₂ x) (minpoly R x) = 0
<VAR>ι : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α✝ : ι → Type u_4<VAR>β✝ : ι → Type u_5<VAR>γ : ι → Type u_6<VAR>x y : (i : ι) → α✝ i<VAR>i : ι<VAR>M : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>inst✝ : SMul M β<VAR>r : M<VAR>f : ι → α<VAR>g : ι → β<VAR>e : α → β<GOAL>extend f (r • g) (r • e) = r • extend f g e
<VAR>ι : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α✝ : ι → Type u_4<VAR>β✝ : ι → Type u_5<VAR>γ : ι → Type u_6<VAR>x✝ y : (i : ι) → α✝ i<VAR>i : ι<VAR>M : Type u_7<VAR>α : Type u_8<VAR>β : Type u_9<VAR>inst✝ : SMul M β<VAR>r : M<VAR>f : ι → α<VAR>g : ι → β<VAR>e : α → β<VAR>x : α<GOAL>extend f (r • g) (r • e) x = (r • extend f g e) x