ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>f : ι → E<VAR>val✝ : Fintype ι<VAR>hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥<VAR>K : ℝ≥0<VAR>K0 : K > 0<VAR>hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))<VAR>this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)<VAR>g : ι → E<VAR>hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹<VAR>v u : ι → 𝕜<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>‖v i - u i‖ ≤ ‖v - u‖
<VAR>T : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} T<VAR>X : T<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : T ⥤ D<VAR>X✝ Y✝ : Over X<VAR>f : X✝ ⟶ Y✝<GOAL>F.map f.left ≫ ((fun Y => mk (F.map Y.hom)) Y✝).hom = ((fun Y => mk (F.map Y.hom)) X✝).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>hf : Tendsto f l atTop<VAR>b : β<VAR>hb : ∀ᶠ (x : β) in map f l, (fun x x_1 => x ≤ x_1) x b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>hf : Tendsto f l atTop<VAR>b : β<VAR>hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>hf : Tendsto f l atTop<VAR>b : β<VAR>hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b<VAR>b' : β<VAR>h : b < b'<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>hf : Tendsto f l atTop<VAR>b : β<VAR>hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b<VAR>b' : β<VAR>h : b < b'<VAR>hb' : ∀ᶠ (a : α) in l, b' ≤ f a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f✝ g : Filter α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>hf : Tendsto f l atTop<VAR>b : β<VAR>hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b<VAR>b' : β<VAR>h : b < b'<VAR>hb' : ∀ᶠ (a : α) in l, b' ≤ f a<VAR>this : {x | f x ≤ b} ∩ {x | b' ≤ f x} = ∅<GOAL>False
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed K<VAR>f : k →+* K<VAR>p : k[X]<VAR>h : p.Separable<GOAL>Splits f p
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed K<VAR>f : k →+* K<VAR>p : k[X]<VAR>h : p.Separable<GOAL>Splits f p ↔ Splits (RingHom.id K) (map f p)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ Type w<VAR>a : C<VAR>x : F.obj a<VAR>y : G.obj a<GOAL>Limits.prod.snd.app a (prodMk x y) = y
<VAR>ι : Sort u_1<VAR>f✝ f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>(⨆ i, f i) / a = ⨆ i, f i / a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>insert b (Ico a b) = Icc a b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Zero M<VAR>inst✝ : CommMonoid N<VAR>f : α →₀ M<VAR>g : α → M → N<VAR>n₁ n₂ : N<VAR>a : α<VAR>ha : a ∈ f.support<VAR>h : g a (f a) * n₁ = g a (f a) * n₂<GOAL>f.prod g * n₁ = f.prod g * n₂
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : IsSplitMono f<VAR>inst✝ : Epi f<GOAL>retraction f ≫ f = 𝟙 Y
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>q : ℕ<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(-1) ^ q = -1
<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✝² : NonUnitalSemiring α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>L : Matrix l m α<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>i✝ : l<VAR>j✝ : o<GOAL>(L * M * N) i✝ j✝ = (L * (M * N)) i✝ j✝
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq σ<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(∏ i ∈ s, f i).vars ⊆ s.biUnion fun i => (f i).vars
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<GOAL>φ.order + ψ.order ≤ (φ * ψ).order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<GOAL>∀ (i : ℕ), ↑i < φ.order + ψ.order → (coeff R i) (φ * ψ) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>hn : ↑n < φ.order + ψ.order<GOAL>(coeff R n) (φ * ψ) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>hn : ↑n < φ.order + ψ.order<GOAL>∀ x ∈ antidiagonal n, (coeff R x.1) φ * (coeff R x.2) ψ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>hn : ↑n < φ.order + ψ.order<VAR>i j : ℕ<VAR>hij : (i, j) ∈ antidiagonal n<VAR>hi : ¬↑i < φ.order<VAR>hj : ¬↑j < ψ.order<GOAL>(coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>hn : ↑n < φ.order + ψ.order<VAR>i j : ℕ<VAR>hij : (i, j) ∈ antidiagonal n<VAR>hi : φ.order ≤ ↑i<VAR>hj : ψ.order ≤ ↑j<GOAL>(coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>hn : ↑n < φ.order + ψ.order<VAR>i j : ℕ<VAR>hij : (i, j).1 + (i, j).2 = n<VAR>hi : φ.order ≤ ↑i<VAR>hj : ψ.order ≤ ↑j<GOAL>(coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>hn : ↑n < φ.order + ψ.order<VAR>i j : ℕ<VAR>hij : (i, j).1 + (i, j).2 = n<VAR>hi : φ.order ≤ ↑i<VAR>hj : ψ.order ≤ ↑j<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>hn : ↑n < φ.order + ψ.order<VAR>i j : ℕ<VAR>hij : (i, j).1 + (i, j).2 = n<VAR>hi : φ.order ≤ ↑i<VAR>hj : ψ.order ≤ ↑j<GOAL>↑n = ↑i + ↑j
<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>f : F[X]<GOAL>(map (algebraMap F E) f).natSepDegree = f.natSepDegree
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>n : ℕ<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>↑(cfcUnits f a hf' hf ha ^ n) = ↑(cfcUnits (fun x => f x ^ n) a ⋯ ⋯ ha)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hr : r ≠ 0<GOAL>LiouvilleWith p (x * ↑r)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hr : r ≠ 0<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>LiouvilleWith p (x * ↑r)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hr : r ≠ 0<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∀ (x_1 : ℕ), (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, x * ↑r ≠ ↑m / ↑(r.den • id x_1) ∧ |x * ↑r - ↑m / ↑(r.den • id x_1)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id x_1) ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>hr : r ≠ 0<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>_hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∃ m, x * ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x * ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>hr : r ≠ 0<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>_hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r<GOAL>∃ m, x * ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x * ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α✝<VAR>a b c✝ d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeInf α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>x y c : α<GOAL>c ≤ x ⊓ y ↔ c ≤ x ⊓ y
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α✝<VAR>a b c✝ d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeInf α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>x y c : α<GOAL>c ≤ x ⊓ y ↔ c ≤ x ∧ c ≤ y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>a₁ b₁ : M<VAR>a₂ b₂ : ↥S<GOAL>f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>x g : G<VAR>hx : x ∈ centralizer ↑P<VAR>hy : g⁻¹ * x * g ∈ centralizer ↑P<GOAL>∃ n ∈ (↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>x g : G<VAR>hx : x ∈ centralizer ↑P<VAR>hy : g⁻¹ * x * g ∈ centralizer ↑P<VAR>h1 : ↑P ≤ centralizer ↑(zpowers x)<GOAL>∃ n ∈ (↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>x g : G<VAR>hx : x ∈ centralizer ↑P<VAR>hy : g⁻¹ * x * g ∈ centralizer ↑P<VAR>h1 : ↑P ≤ centralizer ↑(zpowers x)<VAR>h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)<GOAL>∃ n ∈ (↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>x g : G<VAR>hx : x ∈ centralizer ↑P<VAR>hy : g⁻¹ * x * g ∈ centralizer ↑P<VAR>h1 : ↑P ≤ centralizer ↑(zpowers x)<VAR>h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)<VAR>h : ↥(centralizer ↑(zpowers x))<VAR>hh : h • (g • P).subtype h2 = P.subtype h1<GOAL>∃ n ∈ (↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>x g : G<VAR>hx : x ∈ centralizer ↑P<VAR>hy : g⁻¹ * x * g ∈ centralizer ↑P<VAR>h1 : ↑P ≤ centralizer ↑(zpowers x)<VAR>h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)<VAR>h : ↥(centralizer ↑(zpowers x))<VAR>hh : ((↑h * g) • P).subtype ⋯ = P.subtype h1<GOAL>∃ n ∈ (↑P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>x g : G<VAR>hx : x ∈ centralizer ↑P<VAR>hy : g⁻¹ * x * g ∈ centralizer ↑P<VAR>h1 : ↑P ≤ centralizer ↑(zpowers x)<VAR>h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)<VAR>h : ↥(centralizer ↑(zpowers x))<VAR>hh : ((↑h * g) • P).subtype ⋯ = P.subtype h1<GOAL>g⁻¹ * x * g = (↑h * g)⁻¹ * x * (↑h * g)
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b c : α<VAR>inst✝ : Invertible c<GOAL>a * ⅟c = b ↔ a = b * c
<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>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>0 ≤ deriv f 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>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>0 ≤ f' x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>inst✝ : MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ ι)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>c₂ : Cofan fun k => X ↑k<VAR>hc₂ : IsColimit c₂<GOAL>Mono (Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>p : α → β → Bool<VAR>hp : Primrec₂ p<VAR>a : β<VAR>l : List β<VAR>n : α<GOAL>(bif p (id n) a then 0 else (List.findIdx (p n) l).succ) = List.findIdx (p n) (a :: l)
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ed : EDist α<VAR>edist_self✝¹ : ∀ (x : α), edist x x = 0<VAR>edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x<VAR>edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z<VAR>U : UniformSpace α<VAR>hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}<VAR>ed' : EDist α<VAR>edist_self✝ : ∀ (x : α), edist x x = 0<VAR>edist_comm✝ : ∀ (x y : α), edist x y = edist y x<VAR>edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z<VAR>U' : UniformSpace α<VAR>hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}<VAR>h : toEDist = toEDist<GOAL>U = U'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Group α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : MulAction β α<VAR>H : Subgroup α<VAR>inst✝ : QuotientAction β H<VAR>b : β<VAR>q : α ⧸ H<GOAL>↑(b • Quotient.out' q) = b • q
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>p : A.obj (op X)<VAR>p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))<VAR>q : A.obj (op X)<VAR>q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm q)))<VAR>h : fst ⟨p, p'⟩ = fst ⟨q, q'⟩<VAR>h' : F.map (eqToHom ⋯) (snd ⟨q, q'⟩) = snd ⟨p, p'⟩<GOAL>⟨p, p'⟩ = ⟨q, q'⟩
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>p : A.obj (op X)<VAR>p' q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))<VAR>h : fst ⟨p, p'⟩ = fst ⟨p, q'⟩<VAR>h' : F.map (eqToHom ⋯) (snd ⟨p, q'⟩) = snd ⟨p, p'⟩<GOAL>⟨p, p'⟩ = ⟨p, q'⟩
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>1 < a⁻¹ ↔ a < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁴ : PseudoEMetricSpace α<VAR>inst✝³ : PseudoEMetricSpace β<VAR>inst✝² : FunLike F α β<VAR>inst✝¹ : Subsingleton α<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<GOAL>edist x y = 0 ∨ edist x y = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<GOAL>κ.compProdFun η a ∅ = 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p : P1<VAR>c : k<GOAL>(lineMap p p) c = p
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.33491, u_1} C<VAR>Φ : C ⥤ C<VAR>ε : 𝟭 C ⟶ Φ<VAR>J : Type u<VAR>inst✝² : LinearOrder J<VAR>inst✝¹ : IsWellOrder J fun x x_1 => x < x_1<VAR>inst✝ : OrderBot J<VAR>j : J<VAR>iter₁ iter₂ iter₃✝ iter₃ : Iteration ε j<VAR>f : iter₁.Hom iter₂<VAR>g : iter₂.Hom iter₃<VAR>i : J<VAR>hi : i < j<GOAL>(f.natTrans ≫ g.natTrans).app ⟨wellOrderSucc i, ⋯⟩ = (iter₁.isoSucc i hi).hom ≫ whiskerRight ((f.natTrans ≫ g.natTrans).app ⟨i, ⋯⟩) Φ ≫ (iter₃.isoSucc i hi).inv
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : AddCommGroup P<VAR>inst✝⁷ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R N<VAR>inst✝³ : Module.Finite R N<VAR>inst✝² : Module.Free R P<VAR>inst✝¹ : Module.Finite R P<VAR>inst✝ : IsReduced R<VAR>f g : Module.End R M<VAR>μ : R<VAR>h_comm : Commute f g<VAR>n : Module.End R M := g - (algebraMap R (Module.End R M)) μ<VAR>hg : IsNilpotent n<GOAL>(trace R M) (f ∘ₗ g) = μ * (trace R M) f
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : AddCommGroup P<VAR>inst✝⁷ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R N<VAR>inst✝³ : Module.Finite R N<VAR>inst✝² : Module.Free R P<VAR>inst✝¹ : Module.Finite R P<VAR>inst✝ : IsReduced R<VAR>f g : Module.End R M<VAR>μ : R<VAR>h_comm : Commute f g<VAR>n : Module.End R M := g - (algebraMap R (Module.End R M)) μ<VAR>hg : (trace R M) (f ∘ₗ n) = 0<GOAL>(trace R M) (f ∘ₗ g) = μ * (trace R M) f
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : AddCommGroup P<VAR>inst✝⁷ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R N<VAR>inst✝³ : Module.Finite R N<VAR>inst✝² : Module.Free R P<VAR>inst✝¹ : Module.Finite R P<VAR>inst✝ : IsReduced R<VAR>f g : Module.End R M<VAR>μ : R<VAR>h_comm : Commute f g<VAR>n : Module.End R M := g - (algebraMap R (Module.End R M)) μ<VAR>hg : (trace R M) (f ∘ₗ n) = 0<VAR>hμ : g = (algebraMap R (Module.End R M)) μ + n<GOAL>(trace R M) (f ∘ₗ g) = μ * (trace R M) f
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : AddCommGroup P<VAR>inst✝⁷ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R N<VAR>inst✝³ : Module.Finite R N<VAR>inst✝² : Module.Free R P<VAR>inst✝¹ : Module.Finite R P<VAR>inst✝ : IsReduced R<VAR>f g : Module.End R M<VAR>μ : R<VAR>h_comm : Commute f g<VAR>n : Module.End R M := g - (algebraMap R (Module.End R M)) μ<VAR>hg : (trace R M) (f ∘ₗ n) = 0<VAR>hμ : g = (algebraMap R (Module.End R M)) μ + n<VAR>this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f<GOAL>(trace R M) (f ∘ₗ g) = μ * (trace R M) f
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsRefl α r<VAR>c : Cardinal.{u_1}<GOAL>c ≤ cof r ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsRefl α r<VAR>c : Cardinal.{u_1}<GOAL>(∀ b ∈ {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}, c ≤ b) ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsRefl α r<VAR>c : Cardinal.{u_1}<GOAL>(∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b) → c ≤ #↑S) → ∀ b ∈ {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}, c ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>e.target = e'.target
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>s : Set G<GOAL>(∀ x ∈ s, DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x) ↔ ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>a : R<GOAL>(X - C a).degree = 1
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>inst✝ : Nonempty J<VAR>s : Trident f<VAR>W : C<VAR>k l : W ⟶ s.pt<VAR>h : k ≫ s.ι = l ≫ s.ι<GOAL>k ≫ s.π.app one = l ≫ s.π.app one
<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>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : IsOpen s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), f x ⤳ g x<GOAL>Continuous (s.piecewise f g)
<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>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : IsOpen s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), f x ⤳ g x<VAR>this : ∀ (U : Set Y), IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U<GOAL>Continuous (s.piecewise f g)
<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>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : IsOpen s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), f x ⤳ g x<VAR>this : ∀ (U : Set Y), IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U<GOAL>∀ (s_1 : Set Y), IsOpen s_1 → IsOpen (s.piecewise f g ⁻¹' s_1)
<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>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : IsOpen s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), f x ⤳ g x<VAR>this : ∀ (U : Set Y), IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U<VAR>U : Set Y<VAR>hU : IsOpen U<GOAL>IsOpen (s.piecewise f g ⁻¹' U)