ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁷ : OrderedRing 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : Nontrivial 𝕜<VAR>inst✝ : DenselyOrdered 𝕜<VAR>x z : E<VAR>h : z = x<VAR>a : 𝕜<VAR>ha₀ : 0 < a<VAR>ha₁ : a < 1<GOAL>z ∈ openSegment 𝕜 x x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁷ : OrderedRing 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : Nontrivial 𝕜<VAR>inst✝ : DenselyOrdered 𝕜<VAR>x z : E<VAR>h : z = x<VAR>a : 𝕜<VAR>ha₀ : 0 < a<VAR>ha₁ : a < 1<GOAL>a • x + (1 - a) • x = z
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>S : Type u_2<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>p : R[X]<GOAL>(aeval x) p = p.smeval x
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>S : Type u_2<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>p : R[X]<GOAL>(p.sum fun e a => (fun r => r • 1) a * x ^ e) = p.sum (smul_pow x)
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>S : Type u_2<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>p : R[X]<GOAL>(p.sum fun e a => a • x ^ e) = p.sum (smul_pow x)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>m₂ : M₂<GOAL>(toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (ι Q₂) m₂) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<GOAL>(∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y) ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>n : ℕ<GOAL>(r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r).coeff n = (p.scaleRoots r * q.scaleRoots r).coeff n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>n : ℕ<GOAL>r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) = (p.scaleRoots r * q.scaleRoots r).coeff n
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<VAR>this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹<GOAL>cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → M₁ i<VAR>i : ι<VAR>v : M₁ i<GOAL>f (update x i v) = f x - f (update x i (x i - v))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝² : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>inst✝¹ : DecidableEq (Ideal R)<VAR>inst✝ : DecidableEq (Ideal A)<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ normalizedFactors I<GOAL>↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ normalizedFactors J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝² : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>inst✝¹ : DecidableEq (Ideal R)<VAR>inst✝ : DecidableEq (Ideal A)<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ normalizedFactors I<VAR>hI : I ≠ ⊥<GOAL>↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ normalizedFactors J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝² : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>inst✝¹ : DecidableEq (Ideal R)<VAR>inst✝ : DecidableEq (Ideal A)<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ normalizedFactors I<VAR>hI : I ≠ ⊥<GOAL>∀ (l l' : { l // l ∣ I }), ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝² : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>inst✝¹ : DecidableEq (Ideal R)<VAR>inst✝ : DecidableEq (Ideal A)<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ normalizedFactors I<VAR>hI : I ≠ ⊥<VAR>l : Ideal R<VAR>hl : l ∣ I<VAR>l' : Ideal R<VAR>hl' : l' ∣ I<GOAL>↑((idealFactorsEquivOfQuotEquiv f).toEquiv ⟨l, hl⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv ⟨l', hl'⟩) ↔ ↑⟨l, hl⟩ ∣ ↑⟨l', hl'⟩
<GOAL>ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)
<GOAL>ConvexOn ℝ (Ioi 0) fun s => log (Gamma (s / 2))
<GOAL>ConvexOn ℝ (Ioi 0) fun s => log (Gamma (s / 2 + 1 / 2))
<GOAL>ConvexOn ℝ (Ioi 0) fun s => s * log 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>f : Filter α<VAR>g : Filter β<VAR>inst✝ : g.NeBot<VAR>s : Set α<GOAL>s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν k : ℕ<VAR>w : k < n - ν<GOAL>eval 1 ((⇑derivative)^[k] (bernsteinPolynomial R n ν)) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν k : ℕ<VAR>w : k < n - ν<GOAL>eval 1 ((⇑derivative)^[k] ((bernsteinPolynomial R n (n - ν)).comp (1 - X))) = 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>j : J<GOAL>biproduct.ι (fun j => X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j
<VAR>n i : ℕ<GOAL>2 ^ i &&& n = 2 ^ i * (n.testBit i).toNat
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝² : Countable G<VAR>inst✝¹ : MeasurableSMul G α<VAR>inst✝ : SMulInvariantMeasure G α ν<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<GOAL>(if funDom : HasFundamentalDomain G α ν then ν ⋯.choose else 0) = ν s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝² : Countable G<VAR>inst✝¹ : MeasurableSMul G α<VAR>inst✝ : SMulInvariantMeasure G α ν<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<GOAL>ν ⋯.choose = ν s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝² : Countable G<VAR>inst✝¹ : MeasurableSMul G α<VAR>inst✝ : SMulInvariantMeasure G α ν<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<GOAL>IsFundamentalDomain G ⋯.choose ν
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>n : ℕ := addOrderOf u<VAR>B : Set (AddCircle T) := ball x (T / (2 * ↑n))<VAR>hI : I =ᶠ[ae volume] B<GOAL>IsAddFundamentalDomain (↥G) I volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>n : ℕ := addOrderOf u<VAR>B : Set (AddCircle T) := ball x (T / (2 * ↑n))<VAR>hI : I =ᶠ[ae volume] B<VAR>hn : 1 ≤ ↑n<GOAL>IsAddFundamentalDomain (↥G) I volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>n : ℕ := addOrderOf u<VAR>B : Set (AddCircle T) := ball x (T / (2 * ↑n))<VAR>hI : I =ᶠ[ae volume] B<VAR>hn : 1 ≤ ↑n<GOAL>NullMeasurableSet I volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>n : ℕ := addOrderOf u<VAR>B : Set (AddCircle T) := ball x (T / (2 * ↑n))<VAR>hI : I =ᶠ[ae volume] B<VAR>hn : 1 ≤ ↑n<GOAL>∀ (g : ↥G), g ≠ 0 → AEDisjoint volume (g +ᵥ I) I
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>n : ℕ := addOrderOf u<VAR>B : Set (AddCircle T) := ball x (T / (2 * ↑n))<VAR>hI : I =ᶠ[ae volume] B<VAR>hn : 1 ≤ ↑n<GOAL>∀ (g : ↥G), QuasiMeasurePreserving (fun x => g +ᵥ x) volume volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>n : ℕ := addOrderOf u<VAR>B : Set (AddCircle T) := ball x (T / (2 * ↑n))<VAR>hI : I =ᶠ[ae volume] B<VAR>hn : 1 ≤ ↑n<GOAL>volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>cyclesMap φ ≫ h₂.cyclesIso.hom = h₁.cyclesIso.hom ≫ γ.φK
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => f x / r) l atTop
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ = (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖) / 2 - ‖I • x - z‖ * ‖I • x - z‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ = 2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<VAR>h₀ : ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ + ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ = 2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)<GOAL>‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ = 2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁷ : Category.{?u.127948, u_1} C₁<VAR>inst✝⁶ : Category.{?u.127952, u_2} C₂<VAR>inst✝⁵ : Category.{?u.127956, u_3} C₃<VAR>inst✝⁴ : Category.{?u.127960, u_4} C₄<VAR>inst✝³ : Category.{?u.127964, u_5} C₁₂<VAR>inst✝² : Category.{?u.127968, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>i₁₂ : ρ₁₂.I₁₂<VAR>h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂<GOAL>ρ₁₂.q (i₁₂, i₃) = j
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint b c<VAR>hsup : Disjoint a (b ⊔ c)<GOAL>Disjoint (a ⊔ b) c
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint b c<VAR>hsup : Disjoint a (b ⊔ c)<GOAL>Disjoint c (b ⊔ a)
<VAR>α : Type u_1<VAR>a b c : α<VAR>inst✝² : Lattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : IsModularLattice α<VAR>h : Disjoint b c<VAR>hsup : Disjoint a (b ⊔ c)<GOAL>Disjoint (c ⊔ b) a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y x' y' : ℝ<VAR>hx : x ∈ Icc x' y'<VAR>hy : y ∈ Icc x' y'<GOAL>dist x y ≤ y' - x'
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : Gᶜ.Adj v w<GOAL>Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : Gᶜ.Adj v w<GOAL>((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})).card = n - (2 * k - μ) - 2
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : Gᶜ.Adj v w<GOAL>(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})).card = n - (2 * k - μ) - 2
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : Gᶜ.Adj v w<VAR>hne : v ≠ w<GOAL>(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})).card = n - (2 * k - μ) - 2
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : v ≠ w ∧ ¬G.Adj v w<VAR>hne : v ≠ w<GOAL>(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})).card = n - (2 * k - μ) - 2
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : v ≠ w ∧ ¬G.Adj v w<VAR>hne : v ≠ w<GOAL>(G.neighborFinset v ∪ G.neighborFinset w)ᶜ.card - (1 + 1) = n - (2 * k - μ) - 2
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : v ≠ w ∧ ¬G.Adj v w<VAR>hne : v ≠ w<GOAL>w ∉ {v}
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<VAR>v w : V<VAR>ha : v ≠ w ∧ ¬G.Adj v w<VAR>hne : v ≠ w<GOAL>{w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ a b c : α<VAR>l : List α<VAR>ih : (permutations'Aux a l).bind (permutations'Aux b) ~ (permutations'Aux b l).bind (permutations'Aux a)<GOAL>(permutations'Aux a (c :: l)).bind (permutations'Aux b) ~ (permutations'Aux b (c :: l)).bind (permutations'Aux a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ a b c : α<VAR>l : List α<VAR>ih : (permutations'Aux a l).bind (permutations'Aux b) ~ (permutations'Aux b l).bind (permutations'Aux a)<GOAL>(b :: a :: c :: l) :: (a :: b :: c :: l) :: (map (cons a ∘ cons c) (permutations'Aux b l) ++ (map (cons c) (permutations'Aux a l)).bind (permutations'Aux b)) ~ (a :: b :: c :: l) :: (b :: a :: c :: l) :: (map (cons b ∘ cons c) (permutations'Aux a l) ++ (map (cons c) (permutations'Aux b l)).bind (permutations'Aux a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ a b c : α<VAR>l : List α<VAR>ih : (permutations'Aux a l).bind (permutations'Aux b) ~ (permutations'Aux b l).bind (permutations'Aux a)<GOAL>map (cons a ∘ cons c) (permutations'Aux b l) ++ (map (cons c) (permutations'Aux a l)).bind (permutations'Aux b) ~ map (cons b ∘ cons c) (permutations'Aux a l) ++ (map (cons c) (permutations'Aux b l)).bind (permutations'Aux a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ a b c : α<VAR>l : List α<VAR>ih : (permutations'Aux a l).bind (permutations'Aux b) ~ (permutations'Aux b l).bind (permutations'Aux a)<VAR>this : ∀ (a b : α), (map (cons c) (permutations'Aux a l)).bind (permutations'Aux b) ~ map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) ((permutations'Aux a l).bind (permutations'Aux b))<GOAL>map (cons a ∘ cons c) (permutations'Aux b l) ++ (map (cons c) (permutations'Aux a l)).bind (permutations'Aux b) ~ map (cons b ∘ cons c) (permutations'Aux a l) ++ (map (cons c) (permutations'Aux b l)).bind (permutations'Aux a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ a b c : α<VAR>l : List α<VAR>ih : (permutations'Aux a l).bind (permutations'Aux b) ~ (permutations'Aux b l).bind (permutations'Aux a)<VAR>this : ∀ (a b : α), (map (cons c) (permutations'Aux a l)).bind (permutations'Aux b) ~ map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) ((permutations'Aux a l).bind (permutations'Aux b))<GOAL>map (cons a ∘ cons c) (permutations'Aux b l) ++ (map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) ((permutations'Aux a l).bind (permutations'Aux b))) ~ map (cons b ∘ cons c) (permutations'Aux a l) ++ (map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons c) ((permutations'Aux b l).bind (permutations'Aux a)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ a b c : α<VAR>l : List α<VAR>ih : (permutations'Aux a l).bind (permutations'Aux b) ~ (permutations'Aux b l).bind (permutations'Aux a)<VAR>this : ∀ (a b : α), (map (cons c) (permutations'Aux a l)).bind (permutations'Aux b) ~ map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) ((permutations'Aux a l).bind (permutations'Aux b))<GOAL>map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) ((permutations'Aux a l).bind (permutations'Aux b)) ~ map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons c) ((permutations'Aux b l).bind (permutations'Aux a))
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<GOAL>#(Perm α) = 2 ^ #α
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F = 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>quadraticCharFun F a = 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F = 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>¬IsSquare a → False
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s✝ : Set M<VAR>x✝ : M<VAR>s : Set (M × M')<VAR>x : M × M'<VAR>hxs : UniqueMDiffWithinAt (I.prod I') s x<GOAL>mfderivWithin (I.prod I') I Prod.fst s x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s✝ : Set M<VAR>x✝ : M<VAR>s : Set (M × M')<VAR>x : M × M'<VAR>hxs : UniqueMDiffWithinAt (I.prod I') s x<GOAL>mfderiv (I.prod I') I Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>i = typein (fun x x_1 => x < x_1) (enum (fun x x_1 => x < x_1) i ⋯)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Group M<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>c : Con M<VAR>n : ℕ<VAR>w x : M<VAR>h : c w x<GOAL>c (w ^ Int.ofNat n) (x ^ Int.ofNat n)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Group M<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>c : Con M<VAR>n : ℕ<VAR>w x : M<VAR>h : c w x<GOAL>c (w ^ Int.negSucc n) (x ^ Int.negSucc n)
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f✝ : ι → α<VAR>R : Type u_1<VAR>inst✝ : CompleteLinearOrder R<VAR>f : ι → R<VAR>has_least_elem : ⨅ i, f i ∈ range f<GOAL>⋃ i, Ici (f i) = Ici (⨅ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>(∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<VAR>x✝ : Set α<GOAL>(∃ t₂ ∈ g, ∀ x ∈ x✝, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x | (fun y => ∀ x ∈ x✝, (x, y) ∈ s) x}