ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁵ : Module R M₂<VAR>inst✝⁴ : Module R M₃<VAR>inst✝³ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝² : DecidableEq ι<VAR>P : ι → Prop<VAR>inst✝¹ : DecidablePred P<VAR>inst✝ : DecidableEq { a // ¬P a }<VAR>x : (i : { a // P a }) → M₁ ↑i<VAR>z : (i : { a // ¬P a }) → M₁ ↑i<VAR>i : { a // ¬P a }<VAR>c : M₁ ↑i<GOAL>(fun j => if h : P j then x ⟨j, h⟩ else update z i c ⟨j, h⟩) = update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>(sphere x r).Nonempty ↔ 0 ≤ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>y : E<VAR>hy : y ≠ x<GOAL>(sphere x r).Nonempty ↔ 0 ≤ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>y : E<VAR>hy : y ≠ x<VAR>hr : 0 ≤ r<GOAL>r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>y : E<VAR>hy : y ≠ x<VAR>hr : 0 ≤ r<VAR>this : ‖y - x‖ ≠ 0<GOAL>r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>y : E<VAR>hy : y ≠ x<VAR>hr : 0 ≤ r<VAR>this : ‖y - x‖ ≠ 0<GOAL>|r| * (|‖y - x‖|⁻¹ * ‖y - x‖) = r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>y : E<VAR>hy : y ≠ x<VAR>hr : 0 ≤ r<VAR>this : ‖y - x‖ ≠ 0<GOAL>|r| * (‖y - x‖⁻¹ * ‖y - x‖) = r
<VAR>z : 𝔻<GOAL>abs ↑z ≠ abs (-1)
<VAR>z : 𝔻<GOAL>abs ↑z ≠ 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>s : Set β<VAR>hs : IsOpen s<VAR>f : β → α<VAR>f_cont : Continuous f<GOAL>AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>s : Set β<VAR>hs : IsOpen s<VAR>f : β → α<VAR>f_cont : Continuous f<GOAL>AnalyticSet (range fun x => f ↑x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>s : Set β<VAR>hs : IsOpen s<VAR>f : β → α<VAR>f_cont : Continuous f<VAR>this : PolishSpace ↑s<GOAL>AnalyticSet (range fun x => f ↑x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar 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 g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>inst✝ : Nontrivial A<GOAL>spectrum R 1 = {1}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar 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 g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>inst✝ : Nontrivial A<VAR>this : 1 = (algebraMap R A) 1<GOAL>spectrum R 1 = {1}
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : NormedRing A<VAR>inst✝¹¹ : NormedAlgebra ℂ A<VAR>inst✝¹⁰ : CompleteSpace A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : CstarRing A<VAR>inst✝⁷ : NormedRing B<VAR>inst✝⁶ : NormedAlgebra ℂ B<VAR>inst✝⁵ : CompleteSpace B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : CstarRing B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : AlgHomClass F ℂ A B<VAR>inst✝ : StarAlgHomClass F ℂ A B<VAR>φ : F<VAR>a : A<GOAL>‖φ a‖₊ ≤ ‖a‖₊
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : NormedRing A<VAR>inst✝¹¹ : NormedAlgebra ℂ A<VAR>inst✝¹⁰ : CompleteSpace A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : CstarRing A<VAR>inst✝⁷ : NormedRing B<VAR>inst✝⁶ : NormedAlgebra ℂ B<VAR>inst✝⁵ : CompleteSpace B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : CstarRing B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : AlgHomClass F ℂ A B<VAR>inst✝ : StarAlgHomClass F ℂ A B<VAR>φ : F<VAR>a : A<GOAL>∀ (s : A), IsSelfAdjoint s → ‖φ s‖₊ ≤ ‖s‖₊
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : NormedRing A<VAR>inst✝¹¹ : NormedAlgebra ℂ A<VAR>inst✝¹⁰ : CompleteSpace A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : CstarRing A<VAR>inst✝⁷ : NormedRing B<VAR>inst✝⁶ : NormedAlgebra ℂ B<VAR>inst✝⁵ : CompleteSpace B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : CstarRing B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : AlgHomClass F ℂ A B<VAR>inst✝ : StarAlgHomClass F ℂ A B<VAR>φ : F<VAR>a s : A<VAR>hs : IsSelfAdjoint s<GOAL>‖φ s‖₊ ≤ ‖s‖₊
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LeftCancelMonoid G<VAR>inst✝ : Finite G<VAR>x✝ y : G<VAR>n : ℕ<VAR>x : G<GOAL>IsOfFinOrder x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LeftCancelMonoid G<VAR>inst✝ : Finite G<VAR>x✝ y : G<VAR>n : ℕ<VAR>x : G<VAR>h : ¬IsOfFinOrder x<GOAL>False
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<GOAL>map Prod.swap (μ.prod ν) = ν.prod μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>this : (sum fun i => map Prod.swap ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2))) = sum fun i => map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))<GOAL>map Prod.swap (μ.prod ν) = ν.prod μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>this : (sum fun i => map Prod.swap ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2))) = sum fun i => map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))<GOAL>(sum fun i => map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))) = sum fun p => (sFiniteSeq ν p.1).prod (sFiniteSeq μ p.2)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>this : (sum fun i => map Prod.swap ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2))) = sum fun i => map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))<VAR>i : ℕ × ℕ<GOAL>map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1)) = (sFiniteSeq ν i.1).prod (sFiniteSeq μ i.2)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>this : (sum fun i => map Prod.swap ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2))) = sum fun i => map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))<VAR>i : ℕ × ℕ<GOAL>∀ (s : Set β) (t : Set α), MeasurableSet s → MeasurableSet t → (map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))) (s ×ˢ t) = (sFiniteSeq ν i.1) s * (sFiniteSeq μ i.2) t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>this : (sum fun i => map Prod.swap ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2))) = sum fun i => map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))<VAR>i : ℕ × ℕ<VAR>s : Set β<VAR>t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))) (s ×ˢ t) = (sFiniteSeq ν i.1) s * (sFiniteSeq μ i.2) t
<VAR>q a b c : ℚ<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : d ≠ 0<VAR>hn : n /. ↑d ≠ 0<GOAL>n /. ↑d * (n /. ↑d)⁻¹ = 1
<VAR>q a b c : ℚ<VAR>n : ℤ<VAR>d : ℕ<VAR>hd : d ≠ 0<VAR>hn : ¬n = 0<GOAL>n /. ↑d * (n /. ↑d)⁻¹ = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>k : ℕ<VAR>hk : 0 < k<VAR>a b : ℕ<VAR>x✝ : b ≥ 1<GOAL>a / k ≤ b ↔ a ≤ (fun b => b * k + (k - 1)) b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>k : ℕ<VAR>hk : 0 < k<VAR>b : ℕ<VAR>x✝ : b ≥ 1<GOAL>b = b * k / k
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : Integrable f μ<GOAL>∃ x, ∫ (a : α), f a ∂μ ≤ f x
<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>s : Finset I<VAR>f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ<VAR>a✝ : f ∈ ⊤<GOAL>f ∈ Submodule.span ℤ (Set.range (spanFinBasis C s))
<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>s : Finset I<VAR>f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ<VAR>a✝ : f ∈ ⊤<GOAL>∃ c, (c.sum fun i a => a • spanFinBasis C s i) = f
<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>s : Finset I<VAR>f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ<VAR>a✝ : f ∈ ⊤<GOAL>((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) = f
<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>s : Finset I<VAR>f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ<VAR>a✝ : f ∈ ⊤<VAR>x : ↑(π C fun x => x ∈ s)<GOAL>(LocallyConstant.evalₗ ℤ x) ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) = f x
<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>s : Finset I<VAR>f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ<VAR>a✝ : f ∈ ⊤<VAR>x : ↑(π C fun x => x ∈ s)<GOAL>(if (Finsupp.onFinset Finset.univ f.toFun ⋯) x = 0 then 0 else ↑((Finsupp.onFinset Finset.univ f.toFun ⋯) x) x) = f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : HasMFDerivAt I I' f x f'<GOAL>MDifferentiableAt I I' f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : HasMFDerivAt I I' f x f'<GOAL>ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>x : X<VAR>l : Filter X<GOAL>(𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : IsDomain R<VAR>hf : f.degree ≠ 0<GOAL>Function.Injective ⇑(of f)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : IsDomain R<VAR>hf : f.degree ≠ 0<GOAL>∀ (a : R), (of f) a = 0 → a = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : IsDomain R<VAR>hf : f.degree ≠ 0<VAR>p : R<VAR>hp : (of f) p = 0<GOAL>p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : IsDomain R<VAR>hf : f.degree ≠ 0<VAR>p : R<VAR>hp : f ∣ C p<GOAL>p = 0
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝ : L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h2 : lift.{w, w'} #M ≤ lift.{w', w} κ<GOAL>∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝ : L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h2 : lift.{w, w'} #M ≤ lift.{w', w} κ<VAR>N0 : (L.elementaryDiagram M).ModelType<VAR>hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0<GOAL>∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝ : L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ<VAR>N0 : (L.elementaryDiagram M).ModelType<VAR>hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0<GOAL>∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝ : L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ<VAR>N0 : (L.elementaryDiagram M).ModelType<VAR>hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0<VAR>N : Bundled L[[M]].Structure<VAR>hN : #↑N = κ<VAR>NN0 : ↑N ↪ₑ[L[[M]]] ↑N0<GOAL>∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝ : L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ<VAR>N0 : (L.elementaryDiagram M).ModelType<VAR>hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0<VAR>N : Bundled L[[M]].Structure<VAR>hN : #↑N = κ<VAR>NN0 : ↑N ↪ₑ[L[[M]]] ↑N0<VAR>this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N<GOAL>∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝ : L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ<VAR>N0 : (L.elementaryDiagram M).ModelType<VAR>hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0<VAR>N : Bundled L[[M]].Structure<VAR>hN : #↑N = κ<VAR>NN0 : ↑N ↪ₑ[L[[M]]] ↑N0<VAR>this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N<VAR>h : ↑N ⊨ L.elementaryDiagram M<GOAL>∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<GOAL>M.det = ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<GOAL>s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<GOAL>s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → ℕ<GOAL>∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<VAR>x : α<VAR>hx : x ∈ s<VAR>hs : s.EquitableOn f<VAR>w : α<VAR>hw : w ∈ s<VAR>hwx : f w < f x<GOAL>∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<VAR>x : α<VAR>hx : x ∈ s<VAR>hs : s.EquitableOn f<VAR>w : α<VAR>hw : w ∈ s<VAR>hwx : f w < f x<VAR>y : α<VAR>hy : y ∈ s<GOAL>(f w).succ ≤ (f y).succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<VAR>x : α<VAR>hx : x ∈ s<VAR>hs : s.EquitableOn f<VAR>w : α<VAR>hw : w ∈ s<VAR>hwx : f w < f x<VAR>y : α<VAR>hy : y ∈ s<GOAL>f x ≤ (f y).succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ (a : α), e a ∈ t ↔ a ∈ s<VAR>b : β<VAR>hb : b ∈ t<GOAL>e (e.symm b) ∈ t
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁷ : TopologicalSpace β✝<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : TopologicalSpace δ<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Lattice β<VAR>inst✝² : TopologicalLattice β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>f : α →ₘ[μ] β<GOAL>↑(f ⊔ -f) =ᶠ[ae μ] fun x => ↑f x ⊔ -↑f x
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁷ : TopologicalSpace β✝<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : TopologicalSpace δ<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Lattice β<VAR>inst✝² : TopologicalLattice β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>f : α →ₘ[μ] β<VAR>x : α<VAR>hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x<VAR>hx_neg : ↑(-f) x = (-↑f) x<GOAL>↑(f ⊔ -f) x = ↑f x ⊔ -↑f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<GOAL>integralCLM 0 = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ : F ⟶ G<VAR>p' p q : ℤ<VAR>hpq : p + 0 = q<GOAL>F.d p' p ≫ (ofHom φ).v p q hpq = F.d p' q ≫ φ.f q
<VAR>α : Type u_1<VAR>r c : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<VAR>hfg : f =O[l] g<VAR>hg : 0 ≤ᶠ[l] g<GOAL>(fun x => √(f x)) =O[l] fun x => √(g x)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<GOAL>AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>AddMonoidAlgebra.supDegree id (toFinsupp 0) = natDegree 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>h : p ≠ 0<GOAL>AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>h : p ≠ 0<GOAL>↑(AddMonoidAlgebra.supDegree id p.toFinsupp) = ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>h : p ≠ 0<GOAL>p.toFinsupp.support.Nonempty
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>All P (l.node4L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b : α<VAR>inst✝ : LT α<VAR>x : α<GOAL>⊥ < ↑x ↔ ↑x ≠ ⊥
<VAR>α : Type u_1<VAR>f : Perm α<VAR>s : Set α<GOAL>SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n)) s s
<VAR>α : Type u_1<VAR>f : Perm α<VAR>s : Set α<GOAL>SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑f)^[n] s s
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound ε ≤ Fintype.card G<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<GOAL>False