ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x✝ y z x : α<GOAL>toDual x ∈ (⇑ofDual ⁻¹' s).ordConnectedComponent (toDual x✝) ↔ toDual x ∈ ⇑ofDual ⁻¹' s.ordConnectedComponent x✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x✝ y z x : α<GOAL>⇑ofDual ⁻¹' [[x✝, x]] ⊆ ⇑ofDual ⁻¹' s ↔ toDual x ∈ ⇑ofDual ⁻¹' s.ordConnectedComponent x✝
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝² : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>ust : G.IsUniform ε s t<VAR>hst : Disjoint s t<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>htu : Disjoint t u<GOAL>(1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝² : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>ust : G.IsUniform ε s t<VAR>hst : Disjoint s t<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>htu : Disjoint t u<GOAL>↑(filter (fun x => match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) (s ×ˢ t ×ˢ u)).card ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝² : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>ust : G.IsUniform ε s t<VAR>hst : Disjoint s t<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>htu : Disjoint t u<GOAL>(filter (fun x => match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) (s ×ˢ t ×ˢ u)).card ≤ (G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝² : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>ust : G.IsUniform ε s t<VAR>hst : Disjoint s t<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>htu : Disjoint t u<GOAL>∀ a ∈ filter (fun x => match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) (s ×ˢ t ×ˢ u), (fun x => match x with | (x, y, z) => {x, y, z}) a ∈ G.cliqueFinset 3
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝² : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t)<VAR>ust : G.IsUniform ε s t<VAR>hst : Disjoint s t<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t u)<VAR>utu : G.IsUniform ε t u<VAR>htu : Disjoint t u<GOAL>Set.InjOn (fun x => match x with | (x, y, z) => {x, y, z}) ↑(filter (fun x => match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) (s ×ˢ t ×ˢ u))
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝² : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t✝ u : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)<VAR>ust : G.IsUniform ε s t✝<VAR>hst : Disjoint s t✝<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)<VAR>utu : G.IsUniform ε t✝ u<VAR>htu : Disjoint t✝ u<VAR>x₁ y₁ z₁ : α<VAR>h₁ : (x₁, y₁, z₁) ∈ ↑(filter (fun x => match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) (s ×ˢ t✝ ×ˢ u))<VAR>x₂ y₂ z₂ : α<VAR>h₂ : (x₂, y₂, z₂) ∈ ↑(filter (fun x => match x with | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c) (s ×ˢ t✝ ×ˢ u))<VAR>t : (fun x => match x with | (x, y, z) => {x, y, z}) (x₁, y₁, z₁) = (fun x => match x with | (x, y, z) => {x, y, z}) (x₂, y₂, z₂)<GOAL>(x₁, y₁, z₁) = (x₂, y₂, z₂)
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝² : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t✝ u : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)<VAR>ust : G.IsUniform ε s t✝<VAR>hst : Disjoint s t✝<VAR>dsu : 2 * ε ≤ ↑(G.edgeDensity s u)<VAR>usu : G.IsUniform ε s u<VAR>hsu : Disjoint s u<VAR>dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)<VAR>utu : G.IsUniform ε t✝ u<VAR>htu : Disjoint t✝ u<VAR>x₁ y₁ z₁ x₂ y₂ z₂ : α<VAR>t : (fun x => match x with | (x, y, z) => {x, y, z}) (x₁, y₁, z₁) = (fun x => match x with | (x, y, z) => {x, y, z}) (x₂, y₂, z₂)<VAR>h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁<VAR>h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂<GOAL>(x₁, y₁, z₁) = (x₂, y₂, z₂)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommRing R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalRing R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type ?u.1282777) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ f a ≤ cfcₙ g a ↔ ∀ x ∈ σₙ R a, f x ≤ g x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommRing R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalRing R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>(∀ (x : ↑(σₙ R a)), { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x ≤ { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔ ∀ x ∈ σₙ R a, f x ≤ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>s t : Set ι<VAR>f : ι → Set α<VAR>h : (s ∪ t).PairwiseDisjoint f<GOAL>(⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>s t : Set ι<VAR>f : ι → Set α<VAR>h : (s ∪ t).PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ s \ t<VAR>a : α<VAR>ha : a ∈ f i<GOAL>a ∉ ⋃ x ∈ t, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>s t : Set ι<VAR>f : ι → Set α<VAR>h : (s ∪ t).PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ s \ t<VAR>a : α<VAR>ha : a ∈ f i<GOAL>¬∃ i, ∃ (_ : i ∈ t), a ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>s t : Set ι<VAR>f : ι → Set α<VAR>h : (s ∪ t).PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ s \ t<VAR>a : α<VAR>ha : a ∈ f i<VAR>j : ι<VAR>hj : j ∈ t<VAR>haj : a ∈ f j<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<GOAL>StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>h : ∀ (a b : α), a ⋖ b → f a < f b<VAR>a b : α<VAR>hab : a < b<GOAL>f a < f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>h : ∀ (a b : α), a ⋖ b → f a < f b<VAR>a b : α<VAR>hab : a < b<VAR>this : TransGen CovBy a b → TransGen LT.lt (f a) (f b)<GOAL>f a < f b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>h : ∀ (a b : α), a ⋖ b → f a < f b<VAR>a b : α<VAR>hab : a < b<VAR>this : a < b → f a < f b<GOAL>f a < f b
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>A : Continuous fun t => x₀ + t • v<VAR>this : ∀ᶠ (x : E) in 𝓝 (x₀ + 0 • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖x - 0‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f' : F<VAR>s t✝ : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>A : Continuous fun t => x₀ + t • v<VAR>this : ∀ᶠ (x : E) in 𝓝 (x₀ + 0 • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>t : 𝕜<VAR>ht : t ∈ (fun t => x₀ + t • v) ⁻¹' {x | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}<GOAL>‖f (x₀ + t • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖t - 0‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ : E → F<VAR>f' : F<VAR>s t✝ : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>A : Continuous fun t => x₀ + t • v<VAR>this : ∀ᶠ (x : E) in 𝓝 (x₀ + 0 • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<VAR>t : 𝕜<VAR>ht : ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)<GOAL>‖f (x₀ + t • v) - f (x₀ + 0 • v)‖ ≤ C * ‖v‖ * ‖t - 0‖
<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>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>ht : t₀ ∈ Ioo a b<VAR>hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<VAR>t' : ℝ<VAR>ht' : t' ∈ Ioo a b<GOAL>f t' = g t'
<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>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>ht : t₀ ∈ Ioo a b<VAR>hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<VAR>t' : ℝ<VAR>ht' : t' ∈ Ioo a b<VAR>h : t' < t₀<GOAL>f t' = g t'
<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>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>ht : t₀ ∈ Ioo a b<VAR>hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<VAR>t' : ℝ<VAR>ht' : t' ∈ Ioo a b<VAR>h : t₀ ≤ t'<GOAL>f t' = g t'
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<GOAL>(Z₁ ⊗ Z₂) ◁ (f₁ ⊗ f₂) ≫ tensor_μ C (Z₁, Z₂) (Y₁, Y₂) = tensor_μ C (Z₁, Z₂) (X₁, X₂) ≫ (Z₁ ◁ f₁ ⊗ Z₂ ◁ f₂)
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : Field 𝕜<VAR>inst✝⁵ : IsAlgClosed 𝕜<VAR>inst✝⁴ : Linear 𝕜 C<VAR>inst✝³ : HasKernels C<VAR>X Y : C<VAR>inst✝² : FiniteDimensional 𝕜 (X ⟶ X)<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<GOAL>finrank 𝕜 (X ⟶ Y) ≤ 1
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : Field 𝕜<VAR>inst✝⁵ : IsAlgClosed 𝕜<VAR>inst✝⁴ : Linear 𝕜 C<VAR>inst✝³ : HasKernels C<VAR>X Y : C<VAR>inst✝² : FiniteDimensional 𝕜 (X ⟶ X)<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>h : Subsingleton (X ⟶ Y)<GOAL>finrank 𝕜 (X ⟶ Y) ≤ 1
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>𝕜 : Type u_2<VAR>inst✝⁶ : Field 𝕜<VAR>inst✝⁵ : IsAlgClosed 𝕜<VAR>inst✝⁴ : Linear 𝕜 C<VAR>inst✝³ : HasKernels C<VAR>X Y : C<VAR>inst✝² : FiniteDimensional 𝕜 (X ⟶ X)<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>h : Nontrivial (X ⟶ Y)<GOAL>finrank 𝕜 (X ⟶ Y) ≤ 1
<VAR>n : ℕ<VAR>t : ℝ<VAR>ht' : t ≤ ↑n<GOAL>(1 - t / ↑n) ^ n ≤ rexp (-t)
<VAR>t : ℝ<VAR>ht' : t ≤ ↑0<GOAL>(1 - t / ↑0) ^ 0 ≤ rexp (-t)
<VAR>n : ℕ<VAR>t : ℝ<VAR>ht' : t ≤ ↑n<VAR>hn : n ≠ 0<GOAL>(1 - t / ↑n) ^ n ≤ rexp (-t)
<VAR>n : ℕ<VAR>t : ℝ<VAR>ht' : t ≤ ↑n<VAR>hn : n ≠ 0<GOAL>rexp (-t) = rexp (-(t / ↑n)) ^ n
<VAR>n : ℕ<VAR>t : ℝ<VAR>ht' : t ≤ ↑n<VAR>hn : n ≠ 0<GOAL>0 ≤ 1 - t / ↑n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<GOAL>↑((toEven Q) (reverse (involute x))) = reverse ↑((toEven Q) x)
<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 : Set α<VAR>f✝ g✝ f g : α → ℝ≥0∞<VAR>h : f =ᶠ[ae μ] g<GOAL>⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), g x ∂μ
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>(S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom = h.cyclesIso.hom ≫ h.π
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : Nonempty (α ≃ β)<GOAL>∃ g, ∀ (x : ↑s), g ↑x = f x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : Nonempty (α ≃ β)<GOAL>Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : Nonempty (α ≃ β)<VAR>g : α ≃ β<GOAL>Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : lift.{max u v, u} #α = lift.{max u v, v} #β<VAR>g : α ≃ β<GOAL>Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : lift.{max u v, u} #α = lift.{max u v, v} #β<VAR>g : α ≃ β<GOAL>lift.{max u v, u} #↑s = lift.{max u v, v} #↑(range ⇑f)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : lift.{max u v, u} #α = lift.{max u v, v} #β<VAR>g : α ≃ β<GOAL>Injective ⇑f
<VAR>α : Type u_3<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>f : α → Option β → γ<VAR>as : List α<VAR>bs : List β<GOAL>zipWithLeft' f as bs = zipWithLeft'TR f as bs
<VAR>α : Type u_3<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>f : α → Option β → γ<VAR>as : List α<VAR>bs : List β<VAR>acc : Array γ<VAR>head✝ : α<VAR>tail✝ : List α<GOAL>zipWithLeft'TR.go f (head✝ :: tail✝) [] acc = match zipWithLeft' f (head✝ :: tail✝) [] with | (l, r) => (acc.toList ++ l, r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c d a b : G<GOAL>a * (b / a) = b
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<GOAL>μH[1] = volume
<VAR>α : Type u_1<VAR>f g h : Perm α<VAR>x : α<VAR>hfx : f x = x<VAR>n : ℕ<GOAL>(f ^ Int.negSucc n) x = x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>hmn : m + 1 ≤ n<GOAL>ContDiff 𝕜 m fun p => (fderiv 𝕜 f p.1) p.2
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>hf : ContDiffOn 𝕜 n f univ<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffOn 𝕜 m (fun p => (fderiv 𝕜 f p.1) p.2) univ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>hf : ContDiffOn 𝕜 n f univ<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffOn 𝕜 m (fun p => (fderivWithin 𝕜 f univ p.1) p.2) (univ ×ˢ univ)
<VAR>n : ℕ<VAR>c : Char<VAR>l : List Char<GOAL>{ data := l }.IsSuffix (leftpad n c { data := l })
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>e : X ≃ᵢ Y<GOAL>ratio e.toDilationEquiv = 1
<VAR>n : ℕ<GOAL>χ₈ ↑n = χ₈ ↑(n % 8)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>P : ι → α → Prop<VAR>x✝ : α<GOAL>x✝ ∈ ⋂ i, {x | P i x} ↔ x✝ ∈ {x | ∀ (i : ι), P i x}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ X Y Z : C<VAR>sXY : BinaryFan X Y<VAR>P : IsLimit sXY<VAR>sYZ : BinaryFan Y Z<VAR>Q : IsLimit sYZ<VAR>s : BinaryFan sXY.pt Z<VAR>R : IsLimit s<VAR>t : Cone (pair X sYZ.pt)<GOAL>R.lift (BinaryFan.assocInv P t) ≫ Q.lift (BinaryFan.mk (s.fst ≫ sXY.snd) s.snd) = BinaryFan.snd t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ X Y Z : C<VAR>sXY : BinaryFan X Y<VAR>P : IsLimit sXY<VAR>sYZ : BinaryFan Y Z<VAR>Q : IsLimit sYZ<VAR>s : BinaryFan sXY.pt Z<VAR>R : IsLimit s<VAR>t : Cone (pair X sYZ.pt)<GOAL>∀ (j : Discrete WalkingPair), (R.lift (BinaryFan.assocInv P t) ≫ Q.lift (BinaryFan.mk (s.fst ≫ sXY.snd) s.snd)) ≫ sYZ.π.app j = BinaryFan.snd t ≫ sYZ.π.app j
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ X Y Z : C<VAR>sXY : BinaryFan X Y<VAR>P : IsLimit sXY<VAR>sYZ : BinaryFan Y Z<VAR>Q : IsLimit sYZ<VAR>s : BinaryFan sXY.pt Z<VAR>R : IsLimit s<VAR>t : Cone (pair X sYZ.pt)<VAR>m : t.pt ⟶ (BinaryFan.assoc Q s).pt<VAR>w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j<GOAL>m = (fun t => R.lift (BinaryFan.assocInv P t)) t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ X Y Z : C<VAR>sXY : BinaryFan X Y<VAR>P : IsLimit sXY<VAR>sYZ : BinaryFan Y Z<VAR>Q : IsLimit sYZ<VAR>s : BinaryFan sXY.pt Z<VAR>R : IsLimit s<VAR>t : Cone (pair X sYZ.pt)<VAR>m : t.pt ⟶ (BinaryFan.assoc Q s).pt<VAR>w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j<VAR>h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)<GOAL>m = (fun t => R.lift (BinaryFan.assocInv P t)) t
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>G✝ : Type u_2<VAR>inst✝² : Group G✝<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ∣ Nat.card G<VAR>this : Fintype G<GOAL>∃ x, orderOf x = p
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>G✝ : Type u_2<VAR>inst✝² : Group G✝<VAR>n : ℕ<VAR>G : Type u_3<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>this : Fintype G<VAR>hdvd : p ∣ Fintype.card G<GOAL>∃ x, orderOf x = p
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B✝ B : ℝ<VAR>hB : B ≤ 0<GOAL>volume (convexBodySum K B) = 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B✝ B : ℝ<VAR>hB✝ : B ≤ 0<VAR>hB : B < 0<GOAL>volume (convexBodySum K B) = 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B✝ B : ℝ<VAR>hB✝ : B ≤ 0<VAR>hB : B = 0<GOAL>volume (convexBodySum K B) = 0