ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι✝ : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : IsDomain R<VAR>inst✝¹⁰ : IsPrincipalIdealRing R<VAR>inst✝⁹ : IsDomain S<VAR>inst✝⁸ : Finite ι✝<VAR>F : Type u_4<VAR>inst✝⁷ : CommRing F<VAR>inst✝⁶ : Algebra F R<VAR>inst✝⁵ : Algebra F S<VAR>inst✝⁴ : IsScalarTower F R S<VAR>b✝ : Basis ι✝ R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>ι : Type u_5<VAR>inst✝³ : Fintype ι<VAR>b : Basis ι R S<VAR>inst✝² : Nontrivial F<VAR>inst✝¹ : ∀ (i : ι), Module.Free F (R ⧸ span {smithCoeffs b I hI i})<VAR>inst✝ : ∀ (i : ι), Module.Finite F (R ⧸ span {smithCoeffs b I hI i})<GOAL>FiniteDimensional.finrank F (S ⧸ I) = ∑ i : ι, FiniteDimensional.finrank F (R ⧸ span {smithCoeffs b I hI i})
<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>n : Nat<GOAL>(if { byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len (c :: m) } then n else if h : { data := l ++ c :: m ++ r }.atEnd { byteIdx := utf8Len l } = true then n else let_fun this := ⋯; { data := l ++ c :: m ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (n + 1)) = n + (c :: m).length
<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>n : Nat<GOAL>(if h : { data := l ++ c :: m ++ r }.atEnd { byteIdx := utf8Len l } = true then n else let_fun this := ⋯; { data := l ++ c :: m ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (n + 1)) = n + (c :: m).length
<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>n : Nat<GOAL>(if h : c :: m ++ r = [] then n else { data := l ++ (c :: m ++ r) }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ (c :: m ++ r) }.next { byteIdx := utf8Len l }) (n + 1)) = n + (c :: m).length
<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>n : Nat<GOAL>(if h : False then n else { data := l ++ c :: (m ++ r) }.offsetOfPosAux { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } { byteIdx := utf8Len l + c.utf8Size } (n + 1)) = n + (c :: m).length
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<GOAL>TendstoLocallyUniformly F f p ↔ ∀ (x : α), Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : StrictOrderedSemiring R<VAR>a x y : R<VAR>n✝ m : ℕ<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<VAR>n : ℕ<GOAL>a ^ (n + 1) < a ^ n
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMinOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x > x_1) (Ici a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasProd (f ∘ Subtype.val) a₁<GOAL>HasProd f (a₁ * (a₂ / a₁)) ↔ HasProd f a₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>⌊a + 1⌋ = ⌊a⌋ + 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>h₁ : 0 < a<VAR>h₂ : 0 < b<GOAL>a - b < a
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>h₁ : 0 < a<VAR>h₂ : 0 < b<VAR>h : a - b = a<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>h₁ : b < a<VAR>h₂ : 0 < b<VAR>h : a - b = a<GOAL>False
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : Fin 2 → V<GOAL>LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>⇑h '' closure s = closure (⇑h '' s)
<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>n : σ<GOAL>eval₂ f g (X n) = g n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>(s ∪ t).encard = s.encard + t.encard
<VAR>x y : ℝ≥0<GOAL>sqrt x = 0 ↔ x = 0
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module ℝ W<VAR>L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ<VAR>μ : Measure V<VAR>f : V → E<VAR>w : W<GOAL>VectorFourier.fourierIntegral 𝐞 μ L f w = ∫ (v : V), Complex.exp (↑(-2 * π * (L v) w) * Complex.I) • f v ∂μ
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>↑(n - m) + ↑m = ↑n
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a.succ ≠ last (n + 1)<GOAL>b < a.succ.castPred ha ↔ b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<GOAL>card α = 1 ↔ ∃ x, ∀ (y : α), y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<GOAL>Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ t ∩ s' ×ˢ t' ↔ (x, y) ∈ (s ∩ s') ×ˢ (t ∩ t')
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : IsNormal f<VAR>a : Ordinal.{u_1}<GOAL>f a ≤ a ↔ ∃ o, derivFamily (fun x => f) o = a
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : IsNormal f<VAR>a : Ordinal.{u_1}<GOAL>f a ≤ a ↔ Unit → f a ≤ a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(∑ i ∈ range n, ↑p ^ i * wittMul p i ^ p ^ (n - i)).vars ⊆ univ ×ˢ range n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>((range n).biUnion fun i => (↑p ^ i * wittMul p i ^ p ^ (n - i)).vars) ⊆ univ ×ˢ range n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>∀ x ∈ range n, (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n x : ℕ<VAR>hx : x ∈ range n<GOAL>(↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n x : ℕ<VAR>hx : x ∈ range n<GOAL>(↑p ^ x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n x : ℕ<VAR>hx : x ∈ range n<GOAL>(↑p ^ x).vars ⊆ univ ×ˢ range n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n x : ℕ<VAR>hx : x ∈ range n<GOAL>(wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n
<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>p₁ p₂ : P<VAR>Q : AffineSubspace k P<GOAL>Q = ⊥ ∨ (↑Q).Nonempty
<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>p₁ p₂ : P<VAR>Q : AffineSubspace k P<GOAL>Q = ⊥ ∨ Q ≠ ⊥
<GOAL>((ofComplex.comp toComplex).toLinearMap ∘ₗ ι Q) 1 = ((AlgHom.id ℝ (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) 1
<GOAL>ofComplex (toComplex ((ι Q) 1)) = (ι Q) 1
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<GOAL>(((Equiv.symm τ).trans (g x)).trans τ) ∞ = ∞
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<GOAL>τ ((g x) ((Equiv.symm τ) ∞)) = ∞
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<GOAL>τ (fromCoset ⟨x • ↑⟨↑(MonoidHom.range f), ⋯⟩, ⋯⟩) = ∞
<VAR>α : Type u_1<VAR>r : Setoid α<VAR>a w✝ : α<VAR>ha : a ∈ {x | r.Rel x w✝}<VAR>x : α<GOAL>x ∈ {x | r.Rel x w✝} ↔ x ∈ {x | r.Rel x a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<GOAL>limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<GOAL>limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<VAR>aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)<GOAL>limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<VAR>aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)<GOAL>limsup (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (limsup xs F)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι : Type u_5<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>b : ℝ≥0∞<VAR>b_ne_top : b ≠ ⊤<VAR>xs : ι → ℝ≥0∞<VAR>le_b : ∀ᶠ (i : ι) in F, xs i ≤ b<VAR>aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)<VAR>aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)<VAR>key : b.truncateToReal (limsup xs F) = limsup (b.truncateToReal ∘ xs) F<GOAL>limsup (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (limsup xs F)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<VAR>b : γ<GOAL>((p.bind f).bind g) b = (p.bind fun a => (f a).bind g) b
<VAR>b : ℕ<VAR>hb : (b / 2).beq 0 = false<GOAL>jacobiSymNat 0 b = 0
<VAR>b : ℕ<VAR>hb : (b / 2).beq 0 = false<GOAL>1 < b
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsLocalMinOn f (Icc a b) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<GOAL>c ∈ {x | (fun x => f a ≤ f x) x}
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsLocalMinOn f (Icc a b) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<GOAL>f a ≤ f c
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<GOAL>f a ≤ f c
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>hc : a ∈ Icc a b<GOAL>f a ≤ f a
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<VAR>a_lt_c : a < c<GOAL>f a ≤ f c
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<VAR>a_lt_c : a < c<VAR>H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y<GOAL>f a ≤ f c
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<VAR>a_lt_c : a < c<VAR>H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y<VAR>H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c<GOAL>f a ≤ f c
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<VAR>a_lt_c : a < c<VAR>H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y<VAR>H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c<VAR>y : ℝ<VAR>hfy : f a ≤ f y<VAR>hy_ac : y ∈ Ioc a c<GOAL>f a ≤ f c
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<VAR>a_lt_c : a < c<VAR>H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y<VAR>H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c<VAR>ya yc : ℝ<VAR>ya₀ : 0 ≤ ya<VAR>yc₀ : 0 < yc<VAR>yac : ya + yc = 1<VAR>hfy : f a ≤ f (ya * a + yc * c)<VAR>hy_ac : ya * a + yc * c ∈ Ioc a c<GOAL>f a ≤ f c
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : ContinuousSMul ℝ E<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module ℝ β<VAR>inst✝ : OrderedSMul ℝ β<VAR>s : Set E<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsMinFilter f (𝓝[≥] a) a<VAR>h_conv : ConvexOn ℝ (Icc a b) f<VAR>c : ℝ<VAR>hc : c ∈ Icc a b<VAR>a_lt_c : a < c<VAR>H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y<VAR>H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c<VAR>ya yc : ℝ<VAR>ya₀ : 0 ≤ ya<VAR>yc₀ : 0 < yc<VAR>yac : ya + yc = 1<VAR>hfy : f a ≤ f (ya * a + yc * c)<VAR>hy_ac : ya * a + yc * c ∈ Ioc a c<GOAL>ya • f a + yc • f a ≤ ya • f a + yc • f c
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : K<GOAL>(commMap K) ((canonicalEmbedding K) x) = (mixedEmbedding K) x
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : K<GOAL>(fun w => ((↑w).embedding x).re) = (Pi.ringHom fun w => embedding_of_isReal ⋯) x ∧ (fun w => (↑w).embedding x) = (Pi.ringHom fun w => (↑w).embedding) x
<VAR>y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0∞<GOAL>(x ^ y) ^ y⁻¹ = x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<GOAL>W_ R 0 = X 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>γ' : Path y z<VAR>t : ↑I<GOAL>(if ↑t ≤ 1 / 2 then γ.extend (2 * ↑t) else γ'.extend (2 * ↑t - 1)) = if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b : α<GOAL>a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>k a : ℕ<VAR>ha : a ∈ filter p (range (nth p (k + 1)))<GOAL>a ∈ insert (nth p k) (filter p (range (nth p k)))
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>k a : ℕ<VAR>ha : a < nth p (k + 1) ∧ p a<GOAL>a = nth p k ∨ a < nth p k ∧ p a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulZeroClass α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>hs : s.Nonempty<GOAL>0 ⊆ s • 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>f : α → β<VAR>S : Multiset (Multiset α)<GOAL>map f S.join = (map (map f) S).join
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hs : IsClosed s<GOAL>mk ⁻¹' (mk '' s) = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hs : IsClosed s<GOAL>mk ⁻¹' (mk '' s) ⊆ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hs : IsClosed s<VAR>x y : X<VAR>hys : y ∈ s<VAR>hxy : mk y = mk x<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>z : (forget CommRingCat).obj (CommRingCat.of (A⁰_ f))<GOAL>(awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ x) z = (HomogeneousLocalization.mapId 𝒜 ⋯ ≫ (Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv) z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>z : (forget CommRingCat).obj (CommRingCat.of (A⁰_ f))<GOAL>(Proj.stalkIso' 𝒜 ↑x).toEquiv ((awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ x) z) = (HomogeneousLocalization.mapId 𝒜 ⋯) z
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>m : (i : Fin n.succ) → Ei i<GOAL>f.curryRight.uncurryRight m = f m
<VAR>a : Rat<GOAL>a.num /. ↑a.den = a
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>x✝ y : R<VAR>n : ℕ<VAR>S : Type u_3<VAR>inst✝ : MonoidWithZero S<VAR>x : S<VAR>N : ℕ<VAR>hN : x ^ N = 0<GOAL>IsNilpotent (x ^ n.succ)
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>x✝ y : R<VAR>n : ℕ<VAR>S : Type u_3<VAR>inst✝ : MonoidWithZero S<VAR>x : S<VAR>N : ℕ<VAR>hN : x ^ N = 0<GOAL>(x ^ n.succ) ^ N = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : HasBinaryCoproduct X Y<GOAL>coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl 0 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y < 1 ↔ x = y
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : X → ℝ<VAR>c : Continuous f<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : X → ℝ<VAR>c : Continuous f<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>g : ↥A<VAR>b : ‖↑g - { toFun := f, continuous_toFun := c }‖ < ε<GOAL>∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>f : X → ℝ<VAR>c : Continuous f<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>g : ↥A<VAR>b : ‖↑g - { toFun := f, continuous_toFun := c }‖ < ε<GOAL>∀ (x : X), ‖↑g x - f x‖ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : One β<VAR>x : β<GOAL>x ∈ SimpleFunc.range 1 ↔ x ∈ {1}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>m : ↥N<VAR>i : Fin n<GOAL>(⇑(snf.bM.repr ↑m) ∘ ⇑snf.f) i = (snf.a • ⇑(snf.bN.repr m)) i
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : ZMod (p ^ m)<GOAL>((truncate hm).comp (zmodEquivTrunc p m).toRingHom) x = (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : ZMod (p ^ m)<GOAL>((zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))) x = (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<GOAL>𝓝 1 = toFilterBasis.filter
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<GOAL>map (fun y => y) toFilterBasis.filter = toFilterBasis.filter
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a b c d : α<GOAL>a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c