ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω✝ : Type u_1<VAR>inst✝⁷ : PseudoEMetricSpace Ω✝<VAR>inst✝⁶ : MeasurableSpace Ω✝<VAR>inst✝⁵ : OpensMeasurableSpace Ω✝<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>inst✝⁴ : L.NeBot<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>μs : ι → Measure Ω<VAR>h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>rs : ℕ → ℝ := Classical.choose ex<VAR>rs_pos : ∀ (n : ℕ), 0 < rs n<VAR>rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0<VAR>Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)<VAR>key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>μF_finite : μ F < ⊤<VAR>keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))<VAR>nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)<VAR>m : ℕ<VAR>hm : ∀ b ≥ m, μ (Metric.cthickening (rs b) F) < μ F + ↑ε<VAR>aux' : ∀ (i : ι), (μs i) F ≤ (μs i) (Metric.thickening (rs m) F)<VAR>aux : (fun i => (μs i) F) ≤ᶠ[L] fun i => (μs i) (Metric.thickening (rs m) F)<GOAL>μ (Metric.thickening (rs m) F) ≤ μ F + ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<GOAL>{ ofColex := s \ t } < { ofColex := t \ s } ↔ { ofColex := s } < { ofColex := t }
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>this : Unique ι<GOAL>(⇑b = fun x => 1) ∨ ⇑b = fun x => -1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>this✝ : Unique ι<VAR>this : b default = 1 ∨ b default = -1<GOAL>(⇑b = fun x => 1) ∨ ⇑b = fun x => -1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>this✝ : Unique ι<VAR>this : b default = 1 ∨ b default = -1<GOAL>(const ι (b default) = fun x => 1) ∨ const ι (b default) = fun x => -1
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulZeroClass R M<VAR>f : α → R<VAR>f' : α → M<VAR>x : α<VAR>hf : HasCompactSupport f'<GOAL>HasCompactSupport (f • f')
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulZeroClass R M<VAR>f : α → R<VAR>f' : α → M<VAR>x : α<VAR>hf : f' =ᶠ[coclosedCompact α] 0<GOAL>f • f' =ᶠ[coclosedCompact α] 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>a : α<VAR>l : List α<VAR>a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l<VAR>hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b<VAR>Ha : a ∈ ↑(a :: l)<VAR>Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)<GOAL>Chain r ↑(a :: l)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>a : α<VAR>l : List α<VAR>a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l<VAR>hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b<VAR>Ha : a ∈ ↑(a :: l)<VAR>Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)<GOAL>List.Chain r a (l ++ [a])
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>a : α<VAR>l : List α<VAR>a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l<VAR>hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b<VAR>Ha : a ∈ ↑(a :: l)<VAR>Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)<GOAL>List.Pairwise r (a :: (l ++ [a]))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>a : α<VAR>l : List α<VAR>a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l<VAR>hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b<VAR>Ha : a ∈ ↑(a :: l)<VAR>Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)<GOAL>(∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>a : α<VAR>l : List α<VAR>a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l<VAR>hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b<VAR>Ha : a ∈ ↑(a :: l)<VAR>Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)<VAR>b : α<VAR>hb : b ∈ l ++ [a]<GOAL>r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>a : α<VAR>l : List α<VAR>a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l<VAR>hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b<VAR>Ha : a ∈ ↑(a :: l)<VAR>Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)<VAR>b : α<VAR>hb : b ∈ l<VAR>c : α<VAR>hc : c ∈ [a]<GOAL>r b c
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>p : P<VAR>h : Submodule.span k (range Subtype.val) = ⊤<GOAL>affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s) = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>p : P<VAR>h : Submodule.span k (range Subtype.val) = ⊤<GOAL>(affineSpan k ({p} ∪ (fun v => v +ᵥ p) '' s)).direction = ⊤.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>p : P<VAR>h : Submodule.span k (range Subtype.val) = ⊤<GOAL>Submodule.span k (range Subtype.val) ≤ Submodule.span k ((fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>p : P<VAR>h : Submodule.span k (range Subtype.val) = ⊤<GOAL>range Subtype.val ⊆ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>p : P<VAR>h : Submodule.span k (range Subtype.val) = ⊤<VAR>v' : { x // x ∈ s }<GOAL>↑v' ∈ (fun x => x -ᵥ p) '' ({p} ∪ (fun v => v +ᵥ p) '' s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set V<VAR>p : P<VAR>h : Submodule.span k (range Subtype.val) = ⊤<VAR>v' : { x // x ∈ s }<GOAL>↑v' +ᵥ p ∈ {p} ∪ (fun v => v +ᵥ p) '' s ∧ (fun x => x -ᵥ p) (↑v' +ᵥ p) = ↑v'
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → Preorder (α i)<VAR>x y✝ y : (i : ι) → α i<GOAL>(y ∈ univ.pi fun i => Icc (x i) (y✝ i)) ↔ y ∈ Icc x y✝
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<VAR>c : KernelFork f<VAR>i : IsLimit c<GOAL>(Fork.ι c ≫ let c' := KernelFork.ofι (Fork.ι c) ⋯; let i' := isKernelCompMono i (section_ f) ⋯; let i'' := isLimitForkOfKernelFork i'; (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction) = 𝟙 c.pt
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<VAR>c : KernelFork f<VAR>i : IsLimit c<GOAL>section_ f ≫ (splitMonoOfIdempotentOfIsLimitFork C ⋯ (isLimitForkOfKernelFork (isKernelCompMono i (section_ f) ⋯))).retraction = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<VAR>c : KernelFork f<VAR>i : IsLimit c<GOAL>section_ f ≫ i.lift (Fork.ofι (Fork.ι (kernelForkOfFork (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯))) ⋯) = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<VAR>c : KernelFork f<VAR>i : IsLimit c<GOAL>section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯) = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<VAR>c : KernelFork f<VAR>i : IsLimit c<VAR>this : Mono (Fork.ι c) := mono_of_isLimit_fork i<GOAL>section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯) = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<VAR>c : KernelFork f<VAR>i : IsLimit c<VAR>this : Mono (Fork.ι c) := mono_of_isLimit_fork i<GOAL>(section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯)) ≫ Fork.ι c = 0
<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>s : yoneda.obj X ⟶ A<VAR>p : OverArrows (yonedaCollectionPresheafToA F) s<GOAL>YonedaCollection.fst p.val = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g g₁ g₂ : Filter β<GOAL>f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : Type w<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ C<VAR>c₁ : Fan F.obj<VAR>c₂ : Fan fun f => F.obj f.fst.2<VAR>s t : c₁.pt ⟶ c₂.pt<VAR>hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd<VAR>ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }<VAR>i : Fork s t<VAR>j₁ j₂ : J<VAR>f : j₁ ⟶ j₂<GOAL>𝟙 i.pt ≫ i.ι ≫ c₁.π.app { as := j₂ } = (i.ι ≫ c₁.π.app { as := j₁ }) ≫ F.map f
<VAR>a✝ b✝ m n p✝ p a b : ℕ<VAR>hab : a.Coprime b<VAR>hpa : p ∈ a.primeFactorsList<GOAL>(a * b).factorization p = a.factorization p
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<GOAL>s.WOppSide x y ↔ ∃ p ∈ s, Wbtw R x p y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.WOppSide x y<GOAL>∃ p ∈ s, Wbtw R x p y
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb₀ : 0 < b<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (c₁ * log x) (c₂ * log x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb₀ : 0 < b<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (1 * log x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb₀ : 0 < b<VAR>h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (1 * log x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb₀ : 0 < b<VAR>h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop<VAR>x : ℝ<VAR>hx_pos : 1 < x<VAR>hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y<GOAL>∀ u ∈ Set.Icc (b * x) x, log u ∈ Set.Icc (1 / 2 * log x) (1 * log x)
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb₀ : 0 < b<VAR>h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop<VAR>x : ℝ<VAR>hx_pos : 1 < x<VAR>hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>1 / 2 * log x ≤ log u
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb₀ : 0 < b<VAR>h_tendsto : Tendsto (fun x => 1 / 2 * log x) atTop atTop<VAR>x : ℝ<VAR>hx_pos : 1 < x<VAR>hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>log u ≤ 1 * log x
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹¹ : CommSemiring R₂<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁸ : CommRing R₃<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M : Matrix n n R₂<VAR>x y : M₂<GOAL>∑ i : n, ∑ j : n, (b.repr x) i • (b.repr y) j • M i j = ∑ i : n, ∑ j : n, (b.repr x) i * M i j * (b.repr y) j
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>Pb : P ≠ ⊥<VAR>hP : ∀ (x : R), C x ∈ P → x = 0<GOAL>∃ p ∈ P, Polynomial.map (Quotient.mk (comap C P)) p ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>Pb : P ≠ ⊥<VAR>hP : ∀ (x : R), C x ∈ P → x = 0<VAR>m : ↥P<VAR>hm : m ≠ 0<GOAL>∃ p ∈ P, Polynomial.map (Quotient.mk (comap C P)) p ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>Pb : P ≠ ⊥<VAR>hP : ∀ (x : R), C x ∈ P → x = 0<VAR>m : ↥P<VAR>hm : m ≠ 0<VAR>pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0<GOAL>↑m = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>Pb : P ≠ ⊥<VAR>hP : ∀ (x : R), C x ∈ P → x = 0<VAR>m : ↥P<VAR>hm : m ≠ 0<VAR>pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0<GOAL>Function.Injective ⇑(mapRingHom (Quotient.mk (comap C P)))
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>Pb : P ≠ ⊥<VAR>hP : ∀ (x : R), C x ∈ P → x = 0<VAR>m : ↥P<VAR>hm : m ≠ 0<VAR>pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0<GOAL>RingHom.ker (Quotient.mk (comap C P)) = ⊥
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>P : Ideal R[X]<VAR>Pb : P ≠ ⊥<VAR>hP : ∀ (x : R), C x ∈ P → x = 0<VAR>m : ↥P<VAR>hm : m ≠ 0<VAR>pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0<GOAL>comap C P = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝¹ : BooleanAlgebra α<VAR>inst✝ : BooleanAlgebra β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>a : β<VAR>b : α<GOAL>(u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>n i : ℕ<VAR>h : i < (enumFrom n l).length<GOAL>i < l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>n i : ℕ<VAR>h : i < (enumFrom n l).length<GOAL>(enumFrom n l)[i] = (n + i, l[i])
<VAR>m : ℕ<GOAL>1 + ↑m = ↑(succ m)
<VAR>m : ℕ<GOAL>↑(m + 1) = ↑(succ m)
<VAR>f✝ f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
<VAR>f✝ f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
<VAR>f✝ f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>(-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
<VAR>f✝ f : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>x : ℝ<VAR>hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>sq : Square C<VAR>F : C ⥤ D<GOAL>F.map sq.f₁₂ ≫ F.map sq.f₂₄ = F.map sq.f₁₃ ≫ F.map sq.f₃₄
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : MapsTo h s s'<VAR>hy : y = h x<GOAL>HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>n : ℕ<VAR>f : α ≃ Fin n<GOAL>Nat.card α = n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 1 ≤ a<GOAL>a⁻¹ ≤ 1
<VAR>n : ℕ<GOAL>φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
<VAR>n : ℕ<VAR>this : 3 ≤ n + 3<GOAL>φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2
<VAR>n : ℕ<VAR>this : 3 ≤ n + 3<GOAL>φ (n + 3) = 1 ↔ n + 3 = 2
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<GOAL>∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<VAR>g : E →ₗ[ℝ] ℝ<VAR>g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x<VAR>g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖<GOAL>∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<VAR>g : E →ₗ[ℝ] ℝ<VAR>g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x<VAR>g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖<VAR>g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯<GOAL>∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<VAR>g : E →ₗ[ℝ] ℝ<VAR>g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x<VAR>g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖<VAR>g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯<GOAL>‖g'‖ = ‖f‖
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<VAR>g : E →ₗ[ℝ] ℝ<VAR>g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x<VAR>g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖<VAR>g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯<GOAL>‖f‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<VAR>g : E →ₗ[ℝ] ℝ<VAR>g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x<VAR>g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖<VAR>g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯<VAR>x : ↥p<GOAL>‖f x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<VAR>g : E →ₗ[ℝ] ℝ<VAR>g_eq : ∀ (x : ↥p), g ↑x = f x<VAR>g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖<VAR>g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯<VAR>x : ↥p<GOAL>‖g ↑x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖
<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>hf : HasStrictFDerivAt f f' x<VAR>c : F<GOAL>HasStrictFDerivAt (fun x => c - f x) (-f') x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.62056, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : IsColimit (CokernelCofork.ofπ S.g ⋯)<VAR>inst✝ : S.HasHomology<GOAL>S.Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.62056, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : IsColimit (CokernelCofork.ofπ S.g ⋯)<VAR>inst✝ : S.HasHomology<GOAL>Mono S.fromOpcycles
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.62056, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : IsColimit (CokernelCofork.ofπ S.g ⋯)<VAR>inst✝ : S.HasHomology<VAR>this : IsSplitMono S.fromOpcycles<GOAL>Mono S.fromOpcycles
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>p : (Matrix n n R)[X]<VAR>i j : n<VAR>k : ℕ<VAR>t : p = matPolyEquiv (matPolyEquiv.symm p)<GOAL>(matPolyEquiv.symm p i j).coeff k = (matPolyEquiv (matPolyEquiv.symm p)).coeff k i j
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Field k<VAR>inst✝³ : CharZero k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AddTorsor V P<VAR>a b : P<GOAL>(homothety a (1 / 2)) b = midpoint k a b