ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>evalEval x y (C (C 2) * Y + C (C W.a₁ * X + C W.a₃)) = 2 * y + W.a₁ * x + W.a₃
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>2 * y + (W.a₁ * x + W.a₃) = 2 * y + W.a₁ * x + W.a₃
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>j : C ⥤ D<VAR>inst✝ : Coreflective j<VAR>X : D<GOAL>(coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) = j.map ((coreflector j).map ((coreflectorAdjunction j).counit.app X))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>j : C ⥤ D<VAR>inst✝ : Coreflective j<VAR>X : D<GOAL>j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X)) ≫ (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) = j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X) ≫ (coreflector j).map ((coreflectorAdjunction j).counit.app X))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : n + 1 = m<VAR>z : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + m = q<VAR>q₁ q₂ : ℤ<VAR>hq₁ : q₁ = q - 1<VAR>hq₂ : p + 1 = q₂<GOAL>p + n = q₁
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : n + 1 = m<VAR>z : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + m = q<VAR>q₁ q₂ : ℤ<VAR>hq₁ : q₁ = q - 1<VAR>hq₂ : p + 1 = q₂<GOAL>q₂ + n = q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Module.Flat R M₂<VAR>rs : List R<VAR>h : IsWeaklyRegular M rs<GOAL>IsWeaklyRegular (M₂ ⊗[R] M) rs
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hr : r' < r<GOAL>∃ C, ∀ y ∈ EMetric.ball x r', ∀ z ∈ EMetric.ball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hnqp : padicNorm p q ≥ 0<VAR>hnrp : padicNorm p r ≥ 0<VAR>hq : q = 0<GOAL>padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hnqp : padicNorm p q ≥ 0<VAR>hnrp : padicNorm p r ≥ 0<VAR>hq : ¬q = 0<VAR>hr : r = 0<GOAL>padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hnqp : padicNorm p q ≥ 0<VAR>hnrp : padicNorm p r ≥ 0<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqr : ¬q + r = 0<GOAL>↑p ^ (-padicValRat p (q + r)) ≤ max (↑p ^ (-padicValRat p q)) (↑p ^ (-padicValRat p r))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hnqp : padicNorm p q ≥ 0<VAR>hnrp : padicNorm p r ≥ 0<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqr : ¬q + r = 0<GOAL>↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q) ∨ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hnqp : padicNorm p q ≥ 0<VAR>hnrp : padicNorm p r ≥ 0<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqr : ¬q + r = 0<GOAL>↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hnqp : padicNorm p q ≥ 0<VAR>hnrp : padicNorm p r ≥ 0<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqr : ¬q + r = 0<GOAL>1 ≤ ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hnqp : padicNorm p q ≥ 0<VAR>hnrp : padicNorm p r ≥ 0<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqr : ¬q + r = 0<GOAL>-padicValRat p (q + r) ≤ -padicValRat p q
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n✝ m n : ℕ<GOAL>IsOfFinOrder a → IsOfFinOrder (a ^ n)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n✝ m n : ℕ<GOAL>(∃ n, 0 < n ∧ a ^ n = 1) → ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n✝ m✝ n m : ℕ<VAR>hm : 0 < m<VAR>ha : a ^ m = 1<GOAL>∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
<VAR>S : Type u<VAR>inst✝³ : Semiring S<VAR>T : Type v<VAR>inst✝² : Semiring T<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>n : ℕ<VAR>p : R[X]<VAR>inst✝ : Algebra R S<VAR>x : S<GOAL>eval x ((ascPochhammer S n).comp (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<GOAL>↑n < find P
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<GOAL>∀ (h : (find P).Dom), n < (find P).get h
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<VAR>h₁ : (find P).Dom<GOAL>n < (find P).get h₁
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<VAR>h₁ : (find P).Dom<GOAL>n < Nat.find h₁
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<VAR>h₁ : (find P).Dom<VAR>h₂ : P (Nat.find h₁)<GOAL>n < Nat.find h₁
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<VAR>h₁ : (find P).Dom<GOAL>P (Nat.find h₁) → n < Nat.find h₁
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<VAR>h₁ : (find P).Dom<GOAL>Nat.find h₁ ≤ n → ¬P (Nat.find h₁)
<VAR>R : Type u<VAR>M : Type v<VAR>S : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Ring S<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<VAR>I : Ideal S<VAR>hI : IsPrincipal (comap f I)<GOAL>I = Submodule.span S {f (IsPrincipal.generator (comap f I))}
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x y : M₀<VAR>h : IsUnit x<GOAL>y * x * inverse x = y
<VAR>a b m✝ n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>pr : n < m<GOAL>∏ p ∈ Finset.filter Prime (Finset.range m), p ^ padicValNat p n = n
<VAR>a b m✝ n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>pr : n < m<GOAL>∏ p ∈ Finset.filter Prime (Finset.range m), p ^ padicValNat p n = n.factorization.prod fun x x_1 => x ^ x_1
<VAR>a b m✝ n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>pr : n < m<GOAL>(n.factorization.prod fun x x_1 => x ^ x_1) = ∏ p ∈ Finset.filter Prime (Finset.range m), p ^ padicValNat p n
<VAR>a b m✝ n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>pr : n < m<GOAL>n.factorization.support ⊆ Finset.filter Prime (Finset.range m)
<VAR>a b m✝ n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>pr : n < m<GOAL>∀ x ∈ Finset.filter Prime (Finset.range m) \ n.factorization.support, x ^ padicValNat x n = 1
<VAR>a b m✝ n✝ p n : ℕ<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>pr : n < m<GOAL>∀ x ∈ n.factorization.support, (fun x x_1 => x ^ x_1) x (n.factorization x) = x ^ padicValNat x n
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t α<GOAL>traverse pure x = pure x
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t α<VAR>this : traverse pure x = pure (traverse pure x)<GOAL>traverse pure x = pure x
<VAR>x✝ y x : ℝ<GOAL>arccos (-x) = π - arccos x
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>angle x (x + y) < π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>0 < ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (aleph 1).ord).α<GOAL>∅ ∈ let i := i; let S := ⋃ j, generateMeasurableRec s ↑j; s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝ : MetricSpace P<VAR>p₁ p₂ : P<VAR>s : Sphere P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>dist p₁ s.center = dist p₂ s.center
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l₁ l₂ : Filter α<GOAL>l₁ ⤳ l₂ ↔ l₁ ≤ l₂
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →L[𝕜] 𝕜<VAR>h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c<GOAL>‖f‖ ≤ c / r
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →L[𝕜] 𝕜<VAR>h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c<GOAL>0 ≤ c / r
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →L[𝕜] 𝕜<VAR>h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c<GOAL>∀ (x : E), ‖f x‖ ≤ c / r * ‖x‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →L[𝕜] 𝕜<VAR>h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c<GOAL>∀ z ∈ closedBall 0 r, ‖↑f z‖ ≤ c
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>w * cs.simple i * cs.simple i = w
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x✝ y z : R<VAR>a✝ b c a : ℍ[R,c₁,c₂]<VAR>x : R<VAR>h : a = ↑x<GOAL>a = ↑a.re
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>v x : ℤ<GOAL>x ∈ filter (fun x => x ≡ v [ZMOD r]) (Ioc a b) ↔ x ∈ map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ioc (a - v) (b - v)))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>x : ↑(C' C ho)<GOAL>((Linear_CC' C hsC ho) ((πs C o) y)) x = 0 x
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>x : ↑(C' C ho)<GOAL>y (ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) - y (ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x)) = 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>x : ↑(C' C ho)<GOAL>y (ProjRestrict C (fun x => ord I x < o) (CC'₁ C hsC ho x)) = y (ProjRestrict C (fun x => ord I x < o) (CC'₀ C ho x))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>x : ↑(C' C ho)<VAR>i : I<GOAL>(if ord I i < o then SwapTrue o (↑x) i else false) = if ord I i < o then ↑x i else false
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>x : ↑(C' C ho)<VAR>i : I<GOAL>ord I i < o → SwapTrue o (↑x) i = ↑x i
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>x : ↑(C' C ho)<VAR>i : I<GOAL>ord I i < o → ord I i = o → true = ↑x i
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>f : α → α<VAR>n✝ : ℕ<VAR>hf : Involutive f<VAR>n : ℕ<GOAL>f^[2 * n] = id
<VAR>x y✝ z : ZFSet<VAR>h : x.IsTransitive<VAR>y : ZFSet<VAR>hy : y ∈ ⋃₀ x<GOAL>y ∈ x
<VAR>x y✝ z✝ : ZFSet<VAR>h : x.IsTransitive<VAR>y : ZFSet<VAR>hy : y ∈ ⋃₀ x<VAR>z : ZFSet<VAR>hz : z ∈ x<VAR>hz' : y ∈ z<GOAL>y ∈ x
<VAR>f : ℕ → ℂ<VAR>m : ℝ<VAR>h : ∀ (n : ℕ), n ≠ 0 → Complex.abs (f n) ≤ m<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>1 < (↑s).re
<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✝⁶ : OrderedRing 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>x y z p : P<GOAL>Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>h0✝ : 0 ≤ R<VAR>f : ℂ → E<VAR>c : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z<VAR>h0 : 0 < R<GOAL>(∮ (z : ℂ) in C(c, R), f z) = 0
<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) x).cos = ‖x‖ / ‖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 x (x - y)).cos = ‖x‖ / ‖x - y‖
<VAR>α β : Type u<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{max u_1 u_2}<VAR>i : ι<GOAL>f i ≤ sum f
<VAR>α β : Type u<VAR>ι : Type u_1<VAR>f : ι → Cardinal.{max u_1 u_2}<VAR>i : ι<GOAL>⟦Quotient.out (f i)⟧ ≤ sum f
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Iic a)<VAR>f : ι → ↑(Iic a)<VAR>p : ι → Prop<GOAL>↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Iic a)<VAR>f : ι → ↑(Iic a)<VAR>p : ι → Prop<VAR>h✝ : IsEmpty ι<GOAL>↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Iic a)<VAR>f : ι → ↑(Iic a)<VAR>p : ι → Prop<VAR>h✝ : Nonempty ι<GOAL>↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : γ), ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : γ) in univ, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α →ₘ[μ] β<GOAL>f.Integrable ↔ f ∈ Lp β 1 μ
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (x - r • y) y).sign = (o.oangle x y).sign
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<VAR>k : 𝕜<GOAL>σ (↑ₐ k) = {k}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>x : X<VAR>s : Set X<VAR>hsx : s ∈ 𝓝 x<VAR>hsf : {i | (f i ∩ s).Nonempty}.Finite<GOAL>∃ t ∈ 𝓝 x, {i | ((fun i => closure (f i)) i ∩ t).Nonempty}.Finite
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>x : X<VAR>s : Set X<VAR>hsx : s ∈ 𝓝 x<VAR>hsf : {i | (f i ∩ s).Nonempty}.Finite<VAR>i : ι<VAR>hi : i ∈ {i | ((fun i => closure (f i)) i ∩ interior s).Nonempty}<GOAL>i ∈ {i | (f i ∩ s).Nonempty}
<VAR>r : ℝ<GOAL>r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
<VAR>r : ℝ<VAR>hn : r < 0<GOAL>r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
<GOAL>sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1
<VAR>r : ℝ<VAR>hp : 0 < r<GOAL>r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>f : M ≃ₗ[A] M<GOAL>LinearMap.det ↑f * LinearMap.det ↑f.symm = 1
<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>s t : Finset α<VAR>h : G.IsUniform ε s t<VAR>t' : Finset α<VAR>ht' : t' ⊆ t<VAR>s' : Finset α<VAR>hs' : s' ⊆ s<VAR>ht : ↑t.card * ε ≤ ↑t'.card<VAR>hs : ↑s.card * ε ≤ ↑s'.card<GOAL>|↑(G.edgeDensity t' s') - ↑(G.edgeDensity t 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>s t : Finset α<VAR>h : G.IsUniform ε s t<VAR>t' : Finset α<VAR>ht' : t' ⊆ t<VAR>s' : Finset α<VAR>hs' : s' ⊆ s<VAR>ht : ↑t.card * ε ≤ ↑t'.card<VAR>hs : ↑s.card * ε ≤ ↑s'.card<GOAL>|↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝¹ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>i✝ : ι'<VAR>i : ι<GOAL>(b.repr ((b.prod b') (Sum.inr i✝)).1) i = (b.repr 0) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝¹ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>i✝ : ι'<VAR>i : ι<GOAL>(Finsupp.single (Sum.inr i✝) 1) (Sum.inl i) = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hba : b ≤ a<VAR>hdc : d ≤ c<GOAL>a * d + b * c ≤ a * c + b * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hba : b ≤ a<VAR>hdc : d ≤ c<GOAL>b * c + a * d ≤ b * d + a * c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : MulZeroClass α<VAR>s t : Finset α<VAR>hs : s.Nonempty<GOAL>0 ⊆ s * 0
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝ : (v : V) → Fintype ↑(M.neighborSet v)<GOAL>M.IsMatching ↔ ∀ v ∈ M.verts, M.degree v = 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.67791, u_1} C<VAR>inst✝¹ : Category.{?u.67795, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>(Q W).map s ≫ Qinv s hs = 𝟙 ((Q W).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.67791, u_1} C<VAR>inst✝¹ : Category.{?u.67795, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>homMk (mk s s hs) = 𝟙 ((Q W).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.67791, u_1} C<VAR>inst✝¹ : Category.{?u.67795, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>LeftFractionRel (mk s s hs) (ofHom W (𝟙 ((Q W).obj X)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.67791, u_1} C<VAR>inst✝¹ : Category.{?u.67795, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>Qinv s hs ≫ (Q W).map s = 𝟙 ((Q W).obj Y)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.67791, u_1} C<VAR>inst✝¹ : Category.{?u.67795, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>homMk (ofInv s hs) ≫ homMk (ofHom W s) = 𝟙 ((Q W).obj Y)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.67791, u_1} C<VAR>inst✝¹ : Category.{?u.67795, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>homMk ((ofInv s hs).comp₀ (ofHom W s) (ofHom W (𝟙 Y))) = 𝟙 ((Q W).obj Y)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.67791, u_1} C<VAR>inst✝¹ : Category.{?u.67795, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>s : X ⟶ Y<VAR>hs : W s<GOAL>LeftFractionRel ((ofInv s hs).comp₀ (ofHom W s) (ofHom W (𝟙 Y))) (ofHom W (𝟙 ((Q W).obj Y)))
<VAR>α : Type u_1<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<GOAL>card αˣ = card α - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ t : Set α<VAR>s : Finset α<VAR>inst✝ : Fintype ↑t<GOAL>s ⊂ t.toFinset ↔ ↑s ⊂ t