ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<VAR>ht : ∀ i ∈ s, MeasurableSet (t i)<GOAL>MeasurableSet (⋂ a ∈ s, eval a ⁻¹' t a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedCommRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>σ : Type u_5<VAR>f : E → σ → B<VAR>hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x => f x i) z<VAR>p : MvPolynomial σ A<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) p) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedCommRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>σ : Type u_5<VAR>f : E → σ → B<VAR>hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x => f x i) z<VAR>p : MvPolynomial σ A<VAR>k : A<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) (C k)) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedCommRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>σ : Type u_5<VAR>f : E → σ → B<VAR>hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x => f x i) z<VAR>p✝ p q : MvPolynomial σ A<VAR>hp : AnalyticAt 𝕜 (fun x => (aeval (f x)) p) z<VAR>hq : AnalyticAt 𝕜 (fun x => (aeval (f x)) q) z<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) (p + q)) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedCommRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>σ : Type u_5<VAR>f : E → σ → B<VAR>hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x => f x i) z<VAR>p✝ p : MvPolynomial σ A<VAR>i : σ<VAR>hp : AnalyticAt 𝕜 (fun x => (aeval (f x)) p) z<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) (p * X i)) z
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>x₁ x₂ y₁ : E<VAR>hy₁ : y₁ ∈ p.ball x₁ r₁<VAR>y₂ : E<VAR>hy₂ : y₂ ∈ p.ball x₂ r₂<GOAL>(fun x x_1 => x + x_1) y₁ y₂ ∈ p.ball (x₁ + x₂) (r₁ + r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>x₁ x₂ y₁ : E<VAR>hy₁ : y₁ ∈ p.ball x₁ r₁<VAR>y₂ : E<VAR>hy₂ : y₂ ∈ p.ball x₂ r₂<GOAL>p (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂
<VAR>p n : ℕ<VAR>hp : Prime p<VAR>h : p ∣ n<GOAL>φ (p * n) = p * φ n
<VAR>p n : ℕ<VAR>hp : Prime p<VAR>h : p ∣ n<VAR>h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n<GOAL>φ (p * n) = p * φ n
<VAR>p n : ℕ<VAR>hp : Prime p<VAR>h : p ∣ n<VAR>h1 : φ p * φ (p * n) = φ p * (φ n * p)<GOAL>φ (p * n) = p * φ n
<VAR>X✝ Y Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f) g<VAR>X : Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>r : ↑⋯.choose<GOAL>Set.range ⇑(X.affineBasisCover.map ⟨x, r⟩).val.base = ⇑(X.affineCover.map x).val.base '' (PrimeSpectrum.basicOpen r).carrier
<VAR>X✝ Y Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f) g<VAR>X : Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>r : ↑⋯.choose<GOAL>⇑(X.affineCover.map ⟨x, r⟩.fst).val.base '' Set.range ⇑(((fun x => affineBasisCoverOfAffine ⋯.choose) ⟨x, r⟩.fst).map ⟨x, r⟩.snd).val.base = ⇑(X.affineCover.map x).val.base '' (PrimeSpectrum.basicOpen r).carrier
<VAR>X✝ Y Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f) g<VAR>X : Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>r : ↑⋯.choose<GOAL>Set.range ⇑(((fun x => affineBasisCoverOfAffine ⋯.choose) ⟨x, r⟩.fst).map ⟨x, r⟩.snd).val.base = (PrimeSpectrum.basicOpen r).carrier
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>H : P f<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<GOAL>Q (Scheme.Hom.app f ⊤)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝² : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>H : P f<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<GOAL>Q (Scheme.Hom.appLE f ⊤ (f ⁻¹ᵁ ⊤) ⋯)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>c c' : Chain α<VAR>f : α →o β<VAR>g : β →o γ<VAR>w : α<VAR>h : w ∈ c<GOAL>f w ∈ c.map f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x y z : G<VAR>H : ∀ (a : G), x * a = y ↔ a = z<GOAL>(single x r * f) y = r * f z
<VAR>α : Type u_1<VAR>f g h : Perm α<GOAL>f.Disjoint f ↔ f = 1
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f.Disjoint f<GOAL>f = 1
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>s : ℝ<GOAL>(fun x => cexp (-a * ↑x ^ 2)) =o[cocompact ℝ] fun x => |x| ^ s
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>s : ℝ<GOAL>(fun x => cexp (-a * ↑x ^ 2)) = fun x => cexp (-a * ↑x ^ 2 + 0 * ↑x)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>s : ℝ<GOAL>(-a).re < 0
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>Tendsto (fun δ => (cthickening δ E).mulIndicator f) (𝓝 0) (𝓝 ((closure E).mulIndicator f))
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>∀ (x : α), Tendsto (fun i => (cthickening i E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>Tendsto (fun i => (cthickening i E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))
<VAR>α : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>inst✝¹ : One β<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>Tendsto (fun x_1 => (closure E).mulIndicator f x) (𝓝 0) (𝓝 ((closure E).mulIndicator f x))
<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>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>image compl (s ⊻ t) = image compl s ⊼ image compl t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝⁵ : GroupWithZero G₀<VAR>inst✝⁴ : TopologicalSpace G₀<VAR>inst✝³ : HasContinuousInv₀ G₀<VAR>inst✝² : ContinuousMul G₀<VAR>f g : α → G₀<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>a : α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h₀ : ∀ (x : α), g x ≠ 0<GOAL>Continuous (f / g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : G<GOAL>↑↑((condexpInd G hm μ s) c) =ᶠ[ae μ] ↑↑(indicatorConstLp 1 ⋯ hμs c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : G<GOAL>↑↑((condexpInd G hm μ s) c) =ᶠ[ae μ] s.indicator fun x => c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : G<GOAL>↑↑(condexpIndSMul hm ⋯ hμs c) =ᶠ[ae μ] s.indicator fun x => c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : G<GOAL>(fun a => ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ hμs 1)) a • c) =ᶠ[ae μ] s.indicator fun x => c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : G<GOAL>(fun a => ↑↑(indicatorConstLp 2 ⋯ hμs 1) a • c) =ᶠ[ae μ] s.indicator fun x => c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : G<VAR>x : α<VAR>hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x => 1) x<GOAL>(fun a => ↑↑(indicatorConstLp 2 ⋯ hμs 1) a • c) x = s.indicator (fun x => c) x
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<VAR>h : IsPell { re := ↑x, im := ↑y }<GOAL>↑(x * x - Pell.d a1 * y * y) = ↑1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<VAR>h : IsPell { re := ↑x, im := ↑y }<GOAL>↑(x * x) - ↑(Pell.d a1 * y * y) = ↑1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<VAR>h : x * x - Pell.d a1 * y * y = 1<GOAL>↑(x * x) - ↑(Pell.d a1 * y * y) = 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>x y : ℕ<VAR>h : x * x - Pell.d a1 * y * y = 1<GOAL>↑1 = 1
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>inst✝ : DecidableEq α<VAR>k : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>(∃ v ∈ 𝒜, s ⊆ v ∧ s.card = k) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>(∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal * p.toReal) = ∑' (i : α), ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>0 ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>i : α<GOAL>0 ≤ ‖↑f i‖ ^ p.toReal
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β i ≃+ β₁ i<VAR>f₂ : (i : ι) → β₁ i ≃+ β₂ i<GOAL>(addEquiv fun i => (f i).trans (f₂ i)) = (addEquiv f).trans (addEquiv f₂)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β i ≃+ β₁ i<VAR>f₂ : (i : ι) → β₁ i ≃+ β₂ i<GOAL>∀ (i : ι), (fun i x => (f₂ i) x) i 0 = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β i ≃+ β₁ i<VAR>f₂ : (i : ι) → β₁ i ≃+ β₂ i<GOAL>∀ (i : ι), (fun i x => (f i) x) i 0 = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β i ≃+ β₁ i<VAR>f₂ : (i : ι) → β₁ i ≃+ β₂ i<GOAL>∀ (i : ι), ((fun i x => (f₂ i) x) i ∘ (fun i x => (f i) x) i) 0 = 0
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>x y : ↥(RingHom.ker (algebraMap A B))<GOAL>(fun x => 1 ⊗ₜ[A] (D R A) ↑x) (x + y) = (fun x => 1 ⊗ₜ[A] (D R A) ↑x) x + (fun x => 1 ⊗ₜ[A] (D R A) ↑x) y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>r : A<VAR>x : ↥(RingHom.ker (algebraMap A B))<GOAL>{ toFun := fun x => 1 ⊗ₜ[A] (D R A) ↑x, map_add' := ⋯ }.toFun (r • x) = (RingHom.id A) r • { toFun := fun x => 1 ⊗ₜ[A] (D R A) ↑x, map_add' := ⋯ }.toFun x
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<GOAL>sign l.prod = (-1) ^ l.length
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<VAR>h₁ : List.map (⇑sign) l = List.replicate l.length (-1)<GOAL>sign l.prod = (-1) ^ l.length
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>H : Subgroup Gˣ<VAR>x : Gˣ<GOAL>↑x ∈ H.ofUnits ↔ x ∈ H
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a : R<VAR>this : (p : Prop) → Decidable p<VAR>h : ¬a = 0<GOAL>¬a ≺ 1
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<GOAL>C * (y - x) ≤ f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<VAR>hxy' : x = y<GOAL>C * (y - x) ≤ f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<VAR>hxy' : x < y<GOAL>C * (y - x) ≤ f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<VAR>hxy' : x < y<VAR>hxyD : Icc x y ⊆ D<GOAL>C * (y - x) ≤ f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<VAR>hxy' : x < y<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<GOAL>C * (y - x) ≤ f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<VAR>hxy' : x < y<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>a : ℝ<VAR>a_mem : a ∈ Ioo x y<VAR>ha : deriv f a = (f y - f x) / (y - x)<GOAL>C * (y - x) ≤ f y - f x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<VAR>hxy' : x < y<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>a : ℝ<VAR>a_mem : a ∈ Ioo x y<VAR>ha : deriv f a = (f y - f x) / (y - x)<VAR>this : C ≤ (f y - f x) / (y - x)<GOAL>C * (y - x) ≤ f y - f x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.29264, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>p q : ℤ<VAR>hpq : p + -1 = q<GOAL>((inl φ).comp (snd φ) ⋯).v p q hpq = Cochain.v 0 p q hpq
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>m : τ → τ<VAR>f₁ f₂ : Filter τ<VAR>hf : Tendsto m f₁ f₂<GOAL>ω f₁ (fun t x => ϕ (m t) x) s ⊆ ω f₂ ϕ s
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>m : τ → τ<VAR>f₁ f₂ : Filter τ<VAR>hf : Tendsto m f₁ f₂<VAR>u : Set τ<VAR>hu : u ∈ f₂<GOAL>closure (image2 (fun t x => ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure (image2 ϕ u s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>m : τ → τ<VAR>f₁ f₂ : Filter τ<VAR>hf : Tendsto m f₁ f₂<VAR>u : Set τ<VAR>hu : u ∈ f₂<GOAL>closure (image2 ϕ (m '' (m ⁻¹' u)) s) ⊆ closure (image2 ϕ u s)
<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>hn : v ≠ w<VAR>hna : ¬Gᶜ.Adj v w<GOAL>Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ)
<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>hn : v ≠ w<VAR>hna : ¬Gᶜ.Adj v w<GOAL>((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})).card = n - (2 * k - ℓ)
<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>hn : v ≠ w<VAR>hna : v ≠ w → G.Adj v w<GOAL>((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})).card = n - (2 * k - ℓ)
<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>hn : v ≠ w<VAR>hna : v ≠ w → G.Adj v w<VAR>h2' : G.Adj v w<GOAL>((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})).card = n - (2 * k - ℓ)