ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Function.Injective (sum_to C ho)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))<VAR>x✝ : ↑(MaxProducts C ho)<VAR>a : Products I<VAR>ha : a ∈ GoodProducts (π C fun x => ord I x < o)<VAR>b : Products I<VAR>hb : b ∈ MaxProducts C ho<VAR>hab : a = b<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))<VAR>x✝ : ↑(MaxProducts C ho)<VAR>a : Products I<VAR>ha : a ∈ GoodProducts (π C fun x => ord I x < o)<VAR>b : Products I<VAR>hb : a ∈ MaxProducts C ho<VAR>hab : a = b<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))<VAR>x✝ : ↑(MaxProducts C ho)<VAR>a : Products I<VAR>ha : a ∈ GoodProducts (π C fun x => ord I x < o)<VAR>b : Products I<VAR>hb : a ∈ MaxProducts C ho<VAR>hab : a = b<VAR>ha' : ord I (term I ho) < o<GOAL>False
<VAR>α : Type u_1<VAR>s✝ t✝ u s t : Set α<VAR>h : s ⊆ t<VAR>h_surj : Surjective (inclusion h)<GOAL>s = t
<VAR>α : Type u_1<VAR>s✝ t✝ u s t : Set α<VAR>h : s ⊆ t<VAR>h_surj : Surjective (inclusion h)<VAR>x : α<VAR>hx : x ∈ t<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>s✝ t✝ u s t : Set α<VAR>h : s ⊆ t<VAR>h_surj : Surjective (inclusion h)<VAR>x : α<VAR>hx : x ∈ t<VAR>y : ↑s<VAR>hy : inclusion h y = ⟨x, hx⟩<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>(x ◃ x) ◃ y = x ◃ y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>(∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ c, 0 < c ∧ c • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<GOAL>(∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>r : ℝ<VAR>h : HasSum (fun a => ↑(f a)) ↑r<GOAL>HasSum f r
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>r : ℝ<VAR>h : HasSum f r<GOAL>HasSum (fun a => ↑(f a)) ↑r
<VAR>R : Type u₁<VAR>inst✝¹ : CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>f : Ring.Perfection R p<VAR>n m✝ m : ℕ<VAR>ih : (coeff R p (n + m)) ((⇑(frobenius (Ring.Perfection R p) p))^[m] f) = (coeff R p n) f<GOAL>(coeff R p (n + m.succ)) ((⇑(frobenius (Ring.Perfection R p) p))^[m.succ] f) = (coeff R p n) f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>h_obj : ∀ (X : C), F.obj X = G.obj X<VAR>h_map : autoParam (∀ (X Y : C) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) _auto✝<GOAL>F = G
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>f : F →ₗ[𝕜] 𝕜<VAR>g : E →ₗ[𝕜] F<VAR>x✝ : E<GOAL>(f.toSeminorm.comp g) x✝ = (f ∘ₗ g).toSeminorm x✝
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>↑↑↑((condexpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) =ᶠ[ae μ] fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<GOAL>↑↑↑((condexpL2 E' 𝕜 hm) ((toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>h_comp : ↑↑↑((condexpL2 E' 𝕜 hm) ((toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))<GOAL>↑↑↑((condexpL2 E' 𝕜 hm) ((toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁸ : RCLike 𝕜<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁵ : CompleteSpace E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : InnerProductSpace 𝕜 E'<VAR>inst✝¹² : CompleteSpace E'<VAR>inst✝¹¹ : NormedSpace ℝ E'<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁴ : RCLike 𝕜'<VAR>inst✝³ : NormedAddCommGroup E''<VAR>inst✝² : InnerProductSpace 𝕜' E''<VAR>inst✝¹ : CompleteSpace E''<VAR>inst✝ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>h_comp : ↑↑↑((condexpL2 E' 𝕜 hm) ((toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] ↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))<GOAL>↑↑((toSpanSingleton ℝ x).compLp ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t✝ : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : LinearOrder γ<VAR>a b : γ<VAR>s t : Set γ<VAR>ha : IsGreatest s a<VAR>hb : IsGreatest t b<GOAL>max a b ∈ s ∪ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Ord α<VAR>inst✝² : Ord β<VAR>inst✝¹ : TransOrd α<VAR>inst✝ : TransOrd β<GOAL>TransOrd (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Ord α<VAR>inst✝² : Ord β<VAR>inst✝¹ : TransOrd α<VAR>inst✝ : TransOrd β<GOAL>TransCmp (compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd))
<VAR>θ : Angle<GOAL>↑θ.expMapCircle = ↑θ.cos + ↑θ.sin * I
<VAR>x✝ : ℝ<GOAL>↑(↑x✝).expMapCircle = ↑(↑x✝).cos + ↑(↑x✝).sin * I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>inst✝ : Fintype ι<VAR>μ : ι → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum μ) s = (∑ i : ι, μ i) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>c : E<VAR>c' : F''<VAR>hc' : c' ≠ 0<VAR>l : Filter α<GOAL>IsBigOWith (‖c‖ / ‖c'‖) l (fun _x => c) fun _x => c'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>c : E<VAR>c' : F''<VAR>hc' : c' ≠ 0<VAR>l : Filter α<GOAL>∀ᶠ (x : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>c : E<VAR>c' : F''<VAR>hc' : c' ≠ 0<VAR>l : Filter α<GOAL>∀ (a : α), a ∈ {x | (fun x => ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>c : E<VAR>c' : F''<VAR>hc' : c' ≠ 0<VAR>l : Filter α<VAR>x : α<GOAL>x ∈ {x | (fun x => ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>nonzero : μ ≠ 0<VAR>f : Ω → E<GOAL>average (↑μ) f = ∫ (ω : Ω), f ω ∂↑μ.normalize
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>nonzero : μ ≠ 0<VAR>f : Ω → E<GOAL>∫ (x : Ω), f x ∂(↑μ univ)⁻¹ • ↑μ = ∫ (ω : Ω), f ω ∂μ.mass⁻¹ • ↑μ
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>nonzero : μ ≠ 0<VAR>f : Ω → E<GOAL>(↑μ univ)⁻¹ = ↑ENNReal.ofNNRealHom.toMonoidWithZeroHom μ.mass⁻¹
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Fintype ι₁<VAR>inst✝¹ : Finite ι₂<VAR>inst✝ : DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<GOAL>(fun i => ((toMatrix b₁ b₂) 0).toMvPolynomial i) = 0
<GOAL>((1 - √5) / 2) ^ 2 - ((1 - √5) / 2 + 1) = 0
<GOAL>-5 / 4 + √5 ^ 2 * (1 / 4) = 0
<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>hg : Differentiable 𝕜 g<GOAL>(Differentiable 𝕜 fun y => f y + g y) ↔ Differentiable 𝕜 f
<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>hg : Differentiable 𝕜 g<VAR>h : Differentiable 𝕜 fun y => f y + g y<GOAL>Differentiable 𝕜 f
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype o<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Field R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>A : Matrix m n R<GOAL>finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype o<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Field R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>A : Matrix m n R<GOAL>(fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᴴ * A).mulVecLin)) = (fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>hno : s.Nodup<GOAL>s ≤ t.dedup ↔ s ≤ t
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>h : C r = 0<GOAL>r = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>h : C r = 0<GOAL>0 = C 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>h : IsUnit (C r)<GOAL>IsUnit r
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>h : IsUnit (C r)<GOAL>IsUnit (constantCoeff (C r))
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>h : IsUnit (C r)<GOAL>Type ?u.214285
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>a b : MvPolynomial σ R<VAR>hd : C r ∣ a * b<GOAL>C r ∣ a ∨ C r ∣ b
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>s : Finset σ<VAR>a' b' : MvPolynomial { x // x ∈ s } R<VAR>hd : C r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'<GOAL>C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>s : Finset σ<VAR>a' b' : MvPolynomial { x // x ∈ s } R<VAR>hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'<GOAL>C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>s : Finset σ<VAR>a' b' : MvPolynomial { x // x ∈ s } R<VAR>hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'<VAR>this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'<GOAL>C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>s : Finset σ<VAR>a' b' : MvPolynomial { x // x ∈ s } R<VAR>hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'<VAR>this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'<GOAL>(rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r : R<VAR>hr : Prime r<VAR>s : Finset σ<VAR>a' b' : MvPolynomial { x // x ∈ s } R<VAR>hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'<VAR>this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'<VAR>f : MvPolynomial { x // x ∈ s } R →+* MvPolynomial σ R := (rename Subtype.val).toRingHom<GOAL>(rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : delta * r.size < l.size<VAR>H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Valid' o₁ (l.rotateR x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : delta * r.size < l.size<VAR>H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Valid' o₂ (l.rotateR x r).dual o₁
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : delta * r.size < l.size<VAR>H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>Valid' o₂ (r.dual.rotateL x l.dual) o₁
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : delta * r.size < l.size<VAR>H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>¬r.dual.size + l.dual.size ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : delta * r.size < l.size<VAR>H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>delta * r.dual.size < l.dual.size
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H1 : ¬l.size + r.size ≤ 1<VAR>H2 : delta * r.size < l.size<VAR>H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3<GOAL>2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → γ<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>(image2 f s t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → γ<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>this : Finite ↑s<GOAL>(image2 f s t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → γ<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>this✝ : Finite ↑s<VAR>this : Finite ↑t<GOAL>(image2 f s t).Finite
<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>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => κ.compProdFun η a s