ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<VAR>this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }<VAR>this : IsDomain A := NoZeroDivisors.to_isDomain A<GOAL>Function.Injective ⇑((mul R A) x)
<VAR>α : Type u_1<VAR>inst✝¹ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<VAR>inst✝ : NoZeroSMulDivisors ℕ α<VAR>hn : n ≠ 0<VAR>m : ℤ<GOAL>n • b - n • a = m • n • p ↔ b - a = m • p
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>x : CliffordAlgebra Q<GOAL>(changeForm h') ((changeForm h) x) = (changeForm ⋯) x
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>r : R<GOAL>(changeForm h') ((changeForm h) ((algebraMap R (CliffordAlgebra Q)) r)) = (changeForm ⋯) ((algebraMap R (CliffordAlgebra Q)) r)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>x y : CliffordAlgebra Q<VAR>hx : (changeForm h') ((changeForm h) x) = (changeForm ⋯) x<VAR>hy : (changeForm h') ((changeForm h) y) = (changeForm ⋯) y<GOAL>(changeForm h') ((changeForm h) (x + y)) = (changeForm ⋯) (x + y)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>m : CliffordAlgebra Q<VAR>x : M<VAR>hx : (changeForm h') ((changeForm h) m) = (changeForm ⋯) m<GOAL>(changeForm h') ((changeForm h) ((ι Q) x * m)) = (changeForm ⋯) ((ι Q) x * m)
<VAR>p : Γ' → Bool<VAR>k₁ k₂ : K'<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L₁ : List Γ'<VAR>o : Option Γ'<VAR>L₂ : List Γ'<VAR>S : K' → List Γ'<VAR>h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂<VAR>h₂ : S rev = []<VAR>e : splitAtPred p (S k₁) = (L₁, o, L₂)<GOAL>Reaches₁ (TM2.step tr) { l := some (move₂ p k₁ k₂ q), var := s, stk := S } { l := some q, var := none, stk := update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂) }
<VAR>p : Γ' → Bool<VAR>k₁ k₂ : K'<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L₁ : List Γ'<VAR>o : Option Γ'<VAR>L₂ : List Γ'<VAR>S : K' → List Γ'<VAR>h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂<VAR>h₂ : S rev = []<VAR>e : splitAtPred p (S k₁) = (L₁, o, L₂)<GOAL>TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x => false) rev k₂ q))) o (update (update S k₁ L₂) rev (L₁.reverseAux (S rev)))) { l := some q, var := none, stk := update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂) }
<VAR>p : Γ' → Bool<VAR>k₁ k₂ : K'<VAR>q : Λ'<VAR>s : Option Γ'<VAR>L₁ : List Γ'<VAR>o : Option Γ'<VAR>L₂ : List Γ'<VAR>S : K' → List Γ'<VAR>h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂<VAR>h₂ : S rev = []<VAR>e : splitAtPred p (S k₁) = (L₁, o, L₂)<GOAL>TransGen (fun a b => (match a with | { l := none, var := var, stk := stk } => none | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) = some b) (bif o.isSome then { l := some (Λ'.move (fun x => false) rev k₂ q), var := o, stk := update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁ (o.iget :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁) } else { l := some (Λ'.move (fun x => false) rev k₂ q), var := o, stk := update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) }) { l := some q, var := none, stk := update (update S k₁ ((match (motive := Option Γ' → (List Γ' → List Γ') → (Γ' → List Γ' → List Γ') → List Γ' → List Γ') o, id, List.cons with | some x, x_1, f => f x | none, y, x => y) L₂)) k₂ (L₁ ++ S k₂) }
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>a : A<VAR>M : Matrix n n A<GOAL>invFun R A n (a • M) = a ⊗ₜ[R] 1 * invFun R A n M
<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>hg : DifferentiableOn 𝕜 g s<GOAL>DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 f s
<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>hg : DifferentiableOn 𝕜 g s<VAR>h : DifferentiableOn 𝕜 (fun y => f y + g y) s<GOAL>DifferentiableOn 𝕜 f s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>toIocMod hp a a = a + p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>a < a + p ∧ ∃ z, a = a + p + z • p
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b c d : α<VAR>hf : MonotoneOn f s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f (max a b) = max (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>sz : Nat<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>buckets : Buckets α β<VAR>H : buckets.WF<VAR>x✝³ : AssocList α β<VAR>x✝² : x✝³ ∈ (Buckets.mk (buckets.val.size * 2) ⋯).val.data<VAR>x✝¹ : α × β<VAR>x✝ : x✝¹ ∈ x✝³.toList<GOAL>(fun k x => ((hash k).toUSize % buckets.val.size).toNat < 0) x✝¹.fst x✝¹.snd
<VAR>p : ℝ × ℝ<VAR>hp_fst : 0 < p.1<GOAL>(fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)
<VAR>p : ℝ × ℝ<VAR>hp_fst : 0 < p.1<GOAL>∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>map reverse l.inits = l.reverse.tails.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>l : List α<GOAL>map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse
<VAR>n k : ℕ<GOAL>n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
<VAR>n k : ℕ<VAR>e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)<GOAL>n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>x : α<VAR>h : ∀ y ∈ s, [[x, y]] ⊆ s<VAR>y : α<VAR>hy : y ∈ s<VAR>z : α<VAR>hz : z ∈ s<GOAL>[[y, x]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]
<VAR>o : Ordinal.{u_1}<GOAL>-nim o = nim o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, -nim k = nim k<GOAL>-nim o = nim o
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, -nim k = nim k<GOAL>(-mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) = mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, -nim k = nim k<GOAL>(mk (Quotient.out o).α (Quotient.out o).α (fun j => -nim (typein (fun x x_1 => x < x_1) j)) fun i => -nim (typein (fun x x_1 => x < x_1) i)) = mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>J l R * J l R = -1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>fromBlocks (0 * 0 + -1 * 1) (0 * -1 + -1 * 0) (1 * 0 + 0 * 1) (1 * -1 + 0 * 0) = -1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>fromBlocks (-1) 0 0 (-1) = -1
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Group α<VAR>inst✝² : CommSemigroup β<VAR>inst✝¹ : LE β<VAR>inst✝ : SubmultiplicativeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a ≤ f b * f (a / b)
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>x : K<VAR>h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B<VAR>i : ℕ<GOAL>‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>x : K<VAR>h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B<VAR>i : ℕ<VAR>hx : IsIntegral ℚ x<GOAL>‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>x : K<VAR>h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B<VAR>i : ℕ<VAR>hx : IsIntegral ℚ x<GOAL>‖(map (algebraMap ℚ A) (minpoly ℚ x)).coeff i‖ ≤ max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>x : K<VAR>h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B<VAR>i : ℕ<VAR>hx : IsIntegral ℚ x<VAR>z : A<VAR>hz : z ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots<GOAL>‖z‖ ≤ B
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).cos = ‖y‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (x + y)).cos = ‖y‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (y + x)).cos = ‖y‖ / ‖y + x‖
<VAR>d : ℤ<VAR>a b : Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>hbx : 0 < b.x<VAR>hby : 0 < b.y<GOAL>0 < (a * b).y
<VAR>d : ℤ<VAR>a b : Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>hbx : 0 < b.x<VAR>hby : 0 < b.y<GOAL>0 < a.x * b.y + a.y * b.x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>x✝ : E<GOAL>x✝ ∈ extremePoints 𝕜 B → x✝ ∈ extremePoints 𝕜 A
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<GOAL>Nontrivial (OreLocalization S R) ↔ 0 ∉ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<VAR>hr : Symmetric r<GOAL>{a, b}.Pairwise r ↔ a ≠ b → r a b
<VAR>m n : Nat<GOAL>m ∈ iota n ↔ 1 ≤ m ∧ m ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.Finite<VAR>this : Fintype ↑s<GOAL>s.encard = ↑h.toFinset.card
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f g : A<GOAL>↑(basicOpen 𝒜 (f * g)) = ↑(basicOpen 𝒜 f ⊓ basicOpen 𝒜 g)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Zero α<VAR>d₁ d₂ : n → α<VAR>h : ∀ (i : n), d₁ i = d₂ i<GOAL>diagonal d₁ = diagonal d₂
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hq0 : 0 ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>h : eLpNorm' f q μ = 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hq0 : 0 ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>h : ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ = 0 ∧ 0 < 1 / q ∨ ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ = ⊤ ∧ 1 / q < 0<GOAL>f =ᶠ[ae μ] 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>h : IsKernelPair f a b<VAR>inst✝ : IsIso a<GOAL>Mono f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>h : IsKernelPair f a b<VAR>inst✝ : IsIso a<VAR>l : X ⟶ (IsPullback.cone h).pt<VAR>h₁ : l ≫ (IsPullback.cone h).fst = 𝟙 X<VAR>h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X<GOAL>Mono f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>h : IsKernelPair f a b<VAR>inst✝ : IsIso a<VAR>l : X ⟶ (IsPullback.cone h).pt<VAR>h₁ : l = inv a<VAR>h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X<GOAL>Mono f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>h : IsKernelPair f a b<VAR>inst✝ : IsIso a<VAR>l : X ⟶ (IsPullback.cone h).pt<VAR>h₁ : l = inv a<VAR>h₂ : (IsPullback.cone h).snd = a<GOAL>Mono f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>R X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>h : IsKernelPair f a b<VAR>inst✝ : IsIso a<VAR>l : X ⟶ (IsPullback.cone h).pt<VAR>h₁ : l = inv a<VAR>h₂ : (IsPullback.cone h).snd = a<VAR>Z : C<VAR>l' : Z ⟶ (IsPullback.cone h).pt<VAR>e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f<GOAL>l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<GOAL>(∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p<GOAL>a ∣ b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p<GOAL>a.factorization ≤ b.factorization
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p<VAR>q : ℕ<GOAL>a.factorization q ≤ b.factorization q
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p<VAR>q : ℕ<VAR>hq_le : q ≤ 1<GOAL>a.factorization q ≤ b.factorization q
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p<VAR>q : ℕ<VAR>hq1 : 1 < q<GOAL>a.factorization q ≤ b.factorization q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : DivisionSemiring α<VAR>h : Periodic f c<VAR>a : α<GOAL>Periodic (fun x => f (x / a)) (c * a)
<VAR>R : Type u_1<VAR>n k : ℕ<GOAL>(pow (k + 1)) n = if k + 1 = 0 ∧ n = 0 then 0 else n ^ (k + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Finset β<VAR>f : α → β<VAR>hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})<GOAL>∑ b ∈ s, μ (f ⁻¹' {b}) = μ (f ⁻¹' ↑s)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hn : 2 ≤ l.length<VAR>x : { x // x ∈ l }<GOAL>2 ≤ l.attach.length
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hn✝ : 2 ≤ l.length<VAR>x : { x // x ∈ l }<VAR>hn : 2 ≤ l.attach.length<GOAL>l.attach.Nodup
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>I : Type u<VAR>f✝ : I → Type v<VAR>x y : (i : I) → f✝ i<VAR>i j : I<VAR>η : Type v<VAR>R : Type w<VAR>s : ι → η<VAR>inst✝ : MulOneClass R<VAR>f g : ι → R<GOAL>{ toFun := fun f => extend s f 1, map_one' := ⋯ }.toFun (f * g) = { toFun := fun f => extend s f 1, map_one' := ⋯ }.toFun f * { toFun := fun f => extend s f 1, map_one' := ⋯ }.toFun g
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>Y - (C (C 2) * Y + C (C W.a₁ * X + C W.a₃)) = -Y - C (C W.a₁ * X + C W.a₃)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>Y - (2 * Y + (C (C W.a₁) * C X + C (C W.a₃))) = -Y - (C (C W.a₁) * C X + C (C W.a₃))
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f a p : K[X]<VAR>ha0 : a ≠ 0<VAR>hp : Prime p<VAR>ih : Splits (RingHom.id K) a → Splits i a<VAR>hfi : Splits (RingHom.id K) (p * a)<GOAL>p ∣ map (RingHom.id K) p
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : E → F<VAR>x : E<VAR>y : F<GOAL>Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : BooleanAlgebra α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>s t : Finset α<GOAL>s \\ tᶜˢ = s ⊼ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>s ∈ 𝓝ˢ t ↔ ∀ x ∈ t, s ∈ 𝓝 x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Monoid G<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : Module k V<VAR>ρ : Representation k G V<VAR>g : G<GOAL>ρ.asAlgebraHom ((of k G) g) = ρ g
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f : V → E<VAR>N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>𝓕 (iteratedFDeriv ℝ n f) = fun w => fourierPowSMulRight (-innerSL ℝ) (𝓕 f) w n
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f : V → E<VAR>N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>𝓕 (iteratedFDeriv ℝ n f) = fun w => fourierPowSMulRight (-(innerSL ℝ).flip) (𝓕 f) w n
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>s t : Set V<VAR>sconn : (induce s G).Connected<VAR>tconn : (induce t G).Connected<VAR>sintert : (s ∩ t).Nonempty<GOAL>(induce (s ∪ t) G).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>s t : Set V<VAR>sconn : (⊤.induce s).Connected<VAR>tconn : (⊤.induce t).Connected<VAR>sintert : (s ∩ t).Nonempty<GOAL>(⊤.induce (s ∪ t)).Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (c : ℝ) in atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : CancelCommMonoid α<VAR>s : Set α<VAR>a✝ : α<VAR>hs : ThreeGPFree s<VAR>a : α<VAR>ha : a ∈ s<VAR>c : α<VAR>hc : c ∈ s<VAR>hb : a ∈ s<VAR>habc : a * c = a * a<GOAL>a = c
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Finset M<VAR>s : span R ↑w = ⊤<GOAL>#ι ≤ ↑w.card
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>h₁ : Integrable f μ<VAR>h₂ : Integrable f ν<GOAL>↑(nndist (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂(μ + ν))) ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>f : α → G<VAR>h₁ : Integrable f μ<VAR>h₂ : Integrable f ν<GOAL>↑‖∫ (x : α), f x ∂ν‖₊ ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>x : E<VAR>S : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection S<GOAL>‖x‖ ^ 2 = ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ ^ 2