ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace ℝ E<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace ℝ F<VAR>inst✝¹¹ : NormedAddCommGroup F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(Lp G' 1 μ)<VAR>hf : 0 ≤ f<VAR>g : { g // 0 ≤ g }<GOAL>∀ (a : { g // 0 ≤ g }), (fun g => 0 ≤ (setToL1 hT) ↑g) (coeSimpleFuncNonnegToLpNonneg 1 μ G' a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K F<VAR>ι : Type w<VAR>h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)<VAR>x : S<GOAL>(norm R) x = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K F<VAR>ι : Type w<VAR>h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)<VAR>x : S<GOAL>(if H : ∃ s, Nonempty (Basis { x // x ∈ s } R S) then detAux (Trunc.mk ⋯.some) else 1) ((lmul R S) x) = 1
<VAR>x y : ℝ<VAR>hy : 0 ≤ y<GOAL>√x ≤ √y ↔ x ≤ y
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>(inlX φ j i hij ≫ d φ i j) ≫ fstX φ j k hjk = (-F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>(inlX φ j i hij ≫ d φ i j) ≫ sndX φ j = (-F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j) ≫ sndX φ j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<GOAL>(⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i.down).sets
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f f' g g' : ℕ → R<VAR>hf : ∀ {n : ℕ}, n ≠ 0 → f n = f' n<VAR>hg : ∀ {n : ℕ}, n ≠ 0 → g n = g' n<GOAL>f ⍟ g = f' ⍟ g'
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<GOAL>IsMaxChain (fun x x_1 => x ≤ x_1) (range f)
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<VAR>hmono : Monotone f<GOAL>IsMaxChain (fun x x_1 => x ≤ x_1) (range f)
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<VAR>hmono : Monotone f<VAR>t : Set α<VAR>htc : IsChain (fun x x_1 => x ≤ x_1) t<VAR>hbt : range f ⊆ t<VAR>x : α<VAR>hx : x ∈ t<GOAL>x ∈ range f
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<VAR>hmono : Monotone f<VAR>t : Set α<VAR>htc : IsChain (fun x x_1 => x ≤ x_1) t<VAR>hbt : range f ⊆ t<VAR>x : α<VAR>hx : x ∈ t<GOAL>∃ y, f y = x
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<VAR>hmono : Monotone f<VAR>t : Set α<VAR>htc : IsChain (fun x x_1 => x ≤ x_1) t<VAR>hbt : range f ⊆ t<VAR>x : α<VAR>hx : x ∈ t<VAR>h : ∀ (y : Fin (n + 1)), f y ≠ x<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : BoundedOrder α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>h0 : f 0 = ⊥<VAR>hlast : f (Fin.last n) = ⊤<VAR>hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ<VAR>hmono : Monotone f<VAR>t : Set α<VAR>htc : IsChain (fun x x_1 => x ≤ x_1) t<VAR>hbt : range f ⊆ t<VAR>x : α<VAR>hx : x ∈ t<VAR>h : ∀ (y : Fin (n + 1)), f y ≠ x<VAR>k : Fin (n + 1)<GOAL>f k < x
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A : Type u_2<VAR>inst✝² : AddGroup A<VAR>N : Type u_3<VAR>inst✝¹ : Group N<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>r : R<VAR>k : ℤ<GOAL>↑k * r ∈ zmultiples r
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMul G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s μ<VAR>c : G<GOAL>μ ((fun x => c • x) ⁻¹' s) = μ s
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMul G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s μ<VAR>c : G<GOAL>μ ((fun x => c • x) ⁻¹' s) = μ ((fun x => c • x) ⁻¹' toMeasurable μ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → β<VAR>s : Set α<GOAL>Prod.fst '' graphOn f s = s
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h₁ : s ≠ t<VAR>h₂ : ¬G.IsUniform ε s t<GOAL>ε ≤ ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) - G.edgeDensity s t|
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h₁ : s ≠ t<VAR>h₂ : ¬G.IsUniform ε s t<VAR>lt : WellOrderingRel s t<GOAL>ε ≤ ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) - G.edgeDensity s t|
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s : Finset α<VAR>a b : α<VAR>h₁ : s ≠ s<VAR>h₂ : ¬G.IsUniform ε s s<GOAL>ε ≤ ↑|G.edgeDensity (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) - G.edgeDensity s s|
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h₁ : s ≠ t<VAR>h₂ : ¬G.IsUniform ε s t<VAR>gt : WellOrderingRel t s<GOAL>ε ≤ ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) - G.edgeDensity s t|
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : y ≠ 0<GOAL>(x ^ y) ^ y⁻¹ = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>h₁ : ↑⌈x⌉₊ < x + 1<GOAL>rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>h₁ : ↑⌈x⌉₊ < x + 1<VAR>h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊<GOAL>rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>h₁ : ↑⌈x⌉₊ < x + 1<VAR>h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊<GOAL>x + 1 ≤ rexp (x + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>f : γ → α<VAR>g : α → β<VAR>s : Finset γ<GOAL>⨅ x ∈ image f s, g x = ⨅ y ∈ s, g (f y)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>σ τ : ↥(alternatingGroup α)<VAR>hσ : (↑σ).IsThreeCycle<VAR>hτ : (↑τ).IsThreeCycle<GOAL>(↑σ).support.card + 2 ≤ card α
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f✝ : (i : ι) → s i →ₗ[R] t i<VAR>f : (i : ι) → s i ≃ₗ[R] t i<VAR>m : (i : ι) → s i<GOAL>(congr f) ((tprod R) m) = ⨂ₜ[R] (i : ι), (f i) (m i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<VAR>b : HilbertBasis ι 𝕜 ↥U<VAR>x : E<GOAL>HasSum (fun i => ⟪↑((fun i => b.repr.symm (lp.single 2 i 1)) i), x⟫_𝕜 • (fun i => b.repr.symm (lp.single 2 i 1)) i) ((orthogonalProjection U) x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>|x - ↑(round x)| = min (fract x) (1 - fract x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>|x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>hx : fract x < 1 - fract x<GOAL>|x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>hx : fract x ≥ 1 - fract x<GOAL>|x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd' C 0 a a ⋯).hom.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.Cb X Y<VAR>h : f ∈ GromovHausdorff.candidatesB X Y<GOAL>hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD f
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.Cb X Y<VAR>h : f ∈ GromovHausdorff.candidatesB X Y<VAR>r : ℝ<VAR>hr : HD (GromovHausdorff.optimalGHDist X Y) < r<GOAL>hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ r
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.Cb X Y<VAR>h : f ∈ GromovHausdorff.candidatesB X Y<VAR>r : ℝ<VAR>hr : HD (GromovHausdorff.optimalGHDist X Y) < r<VAR>A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r<GOAL>hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ r
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.Cb X Y<VAR>h : f ∈ GromovHausdorff.candidatesB X Y<VAR>r : ℝ<VAR>hr : HD (GromovHausdorff.optimalGHDist X Y) < r<VAR>A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r<GOAL>0 ≤ r
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.Cb X Y<VAR>h : f ∈ GromovHausdorff.candidatesB X Y<VAR>r : ℝ<VAR>hr : HD (GromovHausdorff.optimalGHDist X Y) < r<VAR>A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r<GOAL>∀ x ∈ range (optimalGHInjr X Y), ∃ y ∈ range (optimalGHInjl X Y), dist x y ≤ r
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>m : ι → OuterMeasure β<GOAL>(comap f) (⨅ i, m i) = ⨅ i, (comap f) (m i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>((comap f) (⨅ i, m i)) s = (⨅ i, (comap f) (m i)) s
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>(⨅ i, (comap f) (m i)) s ≤ ((comap f) (⨅ i, m i)) s
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>∀ (i : ℕ → Set β), s ⊆ ⋃ i_1, f ⁻¹' i i_1 → ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (f '' t n) ≤ ∑' (n : ℕ), ⨅ i_2, (m i_2) (i n)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>t : ℕ → Set β<VAR>ht : s ⊆ ⋃ i, f ⁻¹' t i<VAR>k : ℕ<GOAL>⨅ i, (m i) (f '' (f ⁻¹' t k)) ≤ ⨅ i, (m i) (t k)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : C<VAR>inst✝ : HasPullbacks C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : Over X<VAR>y : Over Y<VAR>v : x ⟶ (pullback f).obj y<GOAL>(v.left ≫ pullback.fst y.hom f) ≫ y.hom = ((map f).obj x).hom
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>i : ι<VAR>s : Set α<GOAL>s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>i : ι<VAR>s : Set α<GOAL>s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} ↔ s ∈ π i ∨ s ∈ {univ}
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>θ : Angle<GOAL>(n • θ).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>θ : Angle<GOAL>(n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>θ : Angle<VAR>h' : 0 < ↑n<GOAL>(n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>(structureSheaf R).presheaf.stalkSpecializes h ≫ (stalkIso R x).hom = (stalkIso R y).hom ≫ let_fun this := PrimeSpectrum.localizationMapOfSpecializes h; this
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>(stalkIso R y).inv ≫ (structureSheaf R).presheaf.stalkSpecializes h = (let_fun this := PrimeSpectrum.localizationMapOfSpecializes h; this) ≫ (stalkIso R x).inv
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Monoid α<VAR>inst✝ : HasDistribNeg α<VAR>a✝ : α<VAR>c : ℕ<VAR>a : α<GOAL>(-a) ^ (c + c) = a ^ (c + c)
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoid α<VAR>x y z : α<VAR>inst✝ : DecompositionMonoid α<VAR>H1 : IsRelPrime x y<VAR>H2 : IsRelPrime x z<GOAL>IsRelPrime x (y * z)
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoid α<VAR>x y z : α<VAR>inst✝ : DecompositionMonoid α<VAR>H1 : IsRelPrime y x<VAR>H2 : IsRelPrime z x<GOAL>IsRelPrime (y * z) x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>preNormEDS b c d 1 = 1
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀<GOAL>Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>hδ : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ ∧ x ∈ ball x₀ ε<GOAL>Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ<VAR>hδε : ∀ x ∈ ball x₀ δ, x ∈ ball x₀ ε<GOAL>Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ<VAR>hδε : ∀ x ∈ ball x₀ δ, x ∈ ball x₀ ε<VAR>h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖<GOAL>Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ<VAR>hδε : ∀ x ∈ ball x₀ δ, x ∈ ball x₀ ε<VAR>h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖<VAR>bound_integrable : Integrable (fun a => ‖bound a‖) μ<GOAL>Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f : α → β<VAR>h : a < b<GOAL>Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f (𝓝[>] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f : α → β<VAR>h : a < b<GOAL>Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c : α<VAR>u : αˣ<GOAL>↑u⁻¹ = 1 /ₚ u
<VAR>n : ℕ<GOAL>Coprime 2 n ↔ Odd n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsArtinian R M<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in atTop, IsCompl (ker (f ^ n)) (range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsArtinian R M<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : Disjoint (ker (f ^ n)) (range (f ^ n)) ∧ Codisjoint (ker (f ^ n)) (range (f ^ n))<GOAL>IsCompl (ker (f ^ n)) (range (f ^ n))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((structureSheaf R).presheaf.obj (op U))<GOAL>((structureSheaf R).presheaf.germ ⟨x, hxU⟩ ≫ stalkToFiberRingHom R x ≫ localizationToStalk R x) s = ((structureSheaf R).presheaf.germ ⟨x, hxU⟩ ≫ 𝟙 ((structureSheaf R).presheaf.stalk x)) s