ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : Y<VAR>y : X<VAR>z : Y<GOAL>∀ (p q : Z), |dist (Ψ p) (Ψ q) - dist (Φ p) (Φ q)| ≤ 2 * ε
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>k : Nat<VAR>t : List α<GOAL>l.eraseIdx k <+: (l ++ t).eraseIdx k
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>w x : M<VAR>x✝ : c w x<GOAL>c (w ^ 0) (x ^ 0)
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>n : ℕ<VAR>w x : M<VAR>h : c w x<GOAL>c (w ^ n.succ) (x ^ n.succ)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>{x | s ∈ 𝓝 x} = {x | 𝓝 x ≤ 𝓟 s}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>x y : R<GOAL>CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>x y : R<GOAL>(∀ (i : Fin (Nat.succ 0).succ), IsIdempotentElem (![x, y] i)) ∧ (∀ (i j : Fin (Nat.succ 0).succ), i ≠ j → ![x, y] i * ![x, y] j = 0) ∧ ∑ i : Fin (Nat.succ 0).succ, ![x, y] i = 1 ↔ IsIdempotentElem x ∧ y = 1 - x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>x y : R<GOAL>(IsIdempotentElem x ∧ IsIdempotentElem y) ∧ (x * y = 0 ∧ y * x = 0) ∧ x + y = 1 ↔ IsIdempotentElem x ∧ x + y = 1
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex x < toLex (update x i a) ↔ x i < a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex x < toLex (update x i a) → x i < a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<VAR>j : ι<VAR>hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → toLex x j_1 = toLex (update x i a) j_1<VAR>h : x j < update x i a j<GOAL>x i < a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>j : ι<VAR>a : β j<VAR>hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → toLex x j_1 = toLex (update x j a) j_1<VAR>h : x j < update x j a j<GOAL>x j < a
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>bernoulli' 1 = 1 / 2
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>1 - ∑ k ∈ range 1, ↑(Nat.choose 1 k) / (↑1 - ↑k + 1) * bernoulli' k = 1 / 2
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasProduct f<VAR>inst✝ : HasProduct (f ∘ ⇑ε)<VAR>b : β<GOAL>(reindex ε f).inv ≫ π (f ∘ ⇑ε) b = π f (ε b)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n✝ m✝ : ℕ<VAR>F G : ComposableArrows C n✝<VAR>n m : ℕ<VAR>h : n + 1 ≤ m<VAR>f g : ComposableArrows C m<VAR>app : f.obj' n ⋯ ≅ g.obj' n ⋯<VAR>app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h<VAR>w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h<GOAL>g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 = ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>↑‖(X ω - ∫ (x : Ω), X x ∂μ) ^ 2‖₊ = ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>‖(X ω - ∫ (x : Ω), X x ∂μ) ^ 2‖₊ = ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2).toNNReal
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>(σ 0) n = n.divisors.card
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<VAR>f : α → β<VAR>h : ∀ a ∈ b, IsOpen (f ⁻¹' a)<GOAL>t ≤ induced f (generateFrom b)
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<VAR>f : α → β<VAR>h : ∀ a ∈ b, IsOpen (f ⁻¹' a)<GOAL>t ≤ generateFrom (preimage f '' b)
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<VAR>f : α → β<VAR>h : ∀ a ∈ b, IsOpen (f ⁻¹' a)<GOAL>∀ s ∈ preimage f '' b, IsOpen s
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<VAR>f : α → β<VAR>h : ∀ a ∈ b, IsOpen (f ⁻¹' a)<GOAL>∀ a ∈ b, IsOpen (f ⁻¹' a)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>x : FamilyOfElements P ⊤<VAR>t₁ t₂ : P.obj (op X)<VAR>h₁ : x.IsAmalgamation t₁<VAR>h₂ : x.IsAmalgamation t₂<GOAL>t₁ = t₂
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>x : FamilyOfElements P ⊤<VAR>t₁ t₂ : P.obj (op X)<VAR>h₁ : x.IsAmalgamation t₁<VAR>h₂ : x.IsAmalgamation t₂<VAR>q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) trivial<GOAL>t₁ = t₂
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>x : FamilyOfElements P ⊤<VAR>t₁ t₂ : P.obj (op X)<VAR>h₁ : x.IsAmalgamation t₁<VAR>h₂ : x.IsAmalgamation t₂<VAR>q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) trivial<VAR>q₂ : P.map (𝟙 X).op t₂ = x (𝟙 X) trivial<GOAL>t₁ = t₂
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>x : FamilyOfElements P ⊤<VAR>t₁ t₂ : P.obj (op X)<VAR>h₁ : x.IsAmalgamation t₁<VAR>h₂ : x.IsAmalgamation t₂<VAR>q₁ : t₁ = x (𝟙 X) trivial<VAR>q₂ : t₂ = x (𝟙 X) trivial<GOAL>t₁ = t₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>Function.Injective ⇑f ↔ ker f = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>Function.Injective ⇑f ↔ ∀ (x : R), x ∈ ⇑f ⁻¹' {0} ↔ x ∈ ↑⊥
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x ^ 2 = (sin a * cos a - sin b * cos b + b - a) / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a✝ b : α<VAR>inst✝ : LE α<VAR>a : α<GOAL>⊤ ≤ ↑a ↔ ↑a = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<GOAL>{ ofColex := s } < { ofColex := t } ↔ ∃ w ∈ t \ s, filter (fun x => w < x) s = filter (fun x => w < x) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<GOAL>(∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a) ↔ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ p : ℕ<VAR>f : R →+* S<VAR>q : R[X]<VAR>hp : ¬p = 0<VAR>n✝ : ℕ<GOAL>(map f ((expand R p) q)).coeff n✝ = ((expand S p) (map f q)).coeff n✝
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ p : ℕ<VAR>f : R →+* S<VAR>q : R[X]<VAR>hp : ¬p = 0<VAR>n✝ : ℕ<GOAL>f (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = if p ∣ n✝ then (map f q).coeff (n✝ / p) else 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>hab : a ≠ b<VAR>h : ¬G.Adj a b<GOAL>incMatrix R G a e * incMatrix R G b e = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>hab : a ≠ b<VAR>h : ¬G.Adj a b<GOAL>e ∉ G.incidenceSet a ∩ G.incidenceSet b
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝ : MulZeroOneClass R<VAR>a b : α<VAR>e : Sym2 α<VAR>hab : a ≠ b<VAR>h : ¬G.Adj a b<GOAL>e ∉ ∅
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>σ.support.card = 3 ↔ σ.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.support.card = 3<GOAL>σ.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.support.card = 3<VAR>h0 : ¬σ.cycleType = 0<GOAL>σ.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.support.card = 3<VAR>h0 : ¬σ.cycleType = 0<VAR>n : ℕ<VAR>hn : n ∈ σ.cycleType<GOAL>σ.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.support.card = 3<VAR>h0 : ¬σ.cycleType = 0<VAR>n : ℕ<VAR>hn : n ∈ σ.cycleType<VAR>h1 : ¬σ.cycleType.erase n = 0<GOAL>σ.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.support.card = 3<VAR>h0 : ¬σ.cycleType = 0<VAR>n : ℕ<VAR>hn : n ∈ σ.cycleType<VAR>h1 : ¬σ.cycleType.erase n = 0<VAR>m : ℕ<VAR>hm : m ∈ σ.cycleType.erase n<GOAL>σ.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h0 : ¬σ.cycleType = 0<VAR>n : ℕ<VAR>hn : n ∈ σ.cycleType<VAR>h1 : ¬σ.cycleType.erase n = 0<VAR>m : ℕ<VAR>h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3<VAR>hm : m ∈ σ.cycleType.erase n<GOAL>σ.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h0 : ¬σ.cycleType = 0<VAR>n : ℕ<VAR>hn : n ∈ σ.cycleType<VAR>h1 : ¬σ.cycleType.erase n = 0<VAR>m : ℕ<VAR>h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3<VAR>hm : m ∈ σ.cycleType.erase n<VAR>this : ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False<GOAL>σ.IsThreeCycle
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I : Box ι<VAR>s : Finset (ι × ℝ)<GOAL>(splitMany I ∅).IsPartition
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I : Box ι<VAR>s✝ : Finset (ι × ℝ)<VAR>a : ι × ℝ<VAR>s : Finset (ι × ℝ)<VAR>x✝ : a ∉ s<VAR>hs : (splitMany I s).IsPartition<GOAL>(splitMany I (insert a s)).IsPartition
<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>x y z : P<VAR>h : Wbtw R x y z<GOAL>Collinear R {x, y, z}
<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>x y z : P<VAR>h : Wbtw R x y z<GOAL>∃ p₀ v, ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ 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>x y z : P<VAR>h : Wbtw R x y z<VAR>p : P<VAR>hp : p ∈ {x, y, z}<GOAL>∃ r, p = r • (z -ᵥ x) +ᵥ x
<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>x y z : P<VAR>h : Wbtw R x y z<VAR>p : P<VAR>hp : p = x ∨ p = y ∨ p = z<GOAL>∃ r, p = r • (z -ᵥ x) +ᵥ x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>Nontrivial ↥H ↔ H ≠ ⊥
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>(∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedRing 𝕝<VAR>inst✝⁶ : NormedSpace 𝕜 𝕝<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SMulWithZero 𝕝 E<VAR>inst✝² : IsScalarTower 𝕜 𝕝 E<VAR>s t u v A B : Set E<VAR>x✝ : E<VAR>a b : 𝕜<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>hA : A ∈ 𝓝 0<VAR>x : E<GOAL>A ∈ 𝓝 (0 • x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>f : ⊤ ↪g G<GOAL>¬G.CliqueFree (Fintype.card α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>f : ⊤ ↪g G<GOAL>Nonempty (⊤ ↪g G)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<GOAL>Valued.v ↑r = v.valuation ↑r
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Type u_2<VAR>inst✝² : AddCommGroup S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : Module R S<VAR>p q : R[X]<VAR>x : S<GOAL>(p - q).smeval x = p.smeval x - q.smeval x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesColimit (span f g) F<VAR>s : IsPushout f g h i<GOAL>IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesColimit (span f g) F<VAR>s : IsPushout f g h i<GOAL>((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅ ⋯.cocone.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesColimit (span f g) F<VAR>s : IsPushout f g h i<GOAL>((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫ ?refine_1.hom = ⋯.cocone.ι.app WalkingCospan.left
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : PreservesColimit (span f g) F<VAR>s : IsPushout f g h i<GOAL>((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫ ?refine_1.hom = ⋯.cocone.ι.app WalkingCospan.right
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝³ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Finite (Sylow p G)<VAR>inst✝ : (↑P).FiniteIndex<GOAL>(transferSylow P hP).ker.IsComplement' ↑P
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝³ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Finite (Sylow p G)<VAR>inst✝ : (↑P).FiniteIndex<VAR>hf : Function.Bijective ⇑((transferSylow P hP).restrict ↑P)<GOAL>(transferSylow P hP).ker.IsComplement' ↑P
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝³ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Finite (Sylow p G)<VAR>inst✝ : (↑P).FiniteIndex<VAR>hf : Function.Injective ⇑((transferSylow P hP).restrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤<GOAL>(transferSylow P hP).ker.IsComplement' ↑P
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝³ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Finite (Sylow p G)<VAR>inst✝ : (↑P).FiniteIndex<VAR>hf : Function.Injective ⇑((transferSylow P hP).restrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤<VAR>this : Function.Surjective ⇑(transferSylow P hP)<GOAL>(transferSylow P hP).ker.IsComplement' ↑P
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝³ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ centralizer ↑P<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Finite (Sylow p G)<VAR>inst✝ : (↑P).FiniteIndex<VAR>hf : (transferSylow P hP).ker ⊓ ↑P = ⊥ ∧ ↑(transferSylow P hP).ker * ↑↑P = Set.univ<VAR>this : Function.Surjective ⇑(transferSylow P hP)<GOAL>(transferSylow P hP).ker.IsComplement' ↑P
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>f : M ↪ₑ[L] N<VAR>T : L.Theory<GOAL>M ⊨ T ↔ N ⊨ T
<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 : α → E<VAR>h : f =ᶠ[ae μ] g<GOAL>⨍ (x : α), f x ∂μ = ⨍ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ<GOAL>Tendsto (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ<VAR>h_ae_forall_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), f n x = AEStronglyMeasurable.mk (f n) ⋯ x<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ<VAR>h_ae_forall_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), f n x = AEStronglyMeasurable.mk (f n) ⋯ x<VAR>x : α<VAR>hx_tendsto : Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hxf_eq : ∀ (n : ℕ), f n x = AEStronglyMeasurable.mk (f n) ⋯ x<VAR>hxg_eq : g x = AEStronglyMeasurable.mk g ⋯ x<GOAL>Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>this : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g ⋯) p μ<VAR>h_ae_forall_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), f n x = AEStronglyMeasurable.mk (f n) ⋯ x<VAR>x : α<VAR>hx_tendsto : Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hxf_eq : ∀ (n : ℕ), f n x = AEStronglyMeasurable.mk (f n) ⋯ x<VAR>hxg_eq : g x = AEStronglyMeasurable.mk g ⋯ x<VAR>n : ℕ<GOAL>AEStronglyMeasurable.mk (f n) ⋯ x = f n x
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V'<VAR>inst✝ : Module K V'<VAR>n : ℕ<VAR>f : V →ₗ[K] V'<GOAL>↑n ≤ f.rank ↔ ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x