ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>hd : α<VAR>tl l' : List α<VAR>f : ℕ ↪o ℕ<VAR>w : f 0 < l'.length<VAR>h : l'[f 0] = hd<VAR>f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) ⋯<VAR>hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'<VAR>this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?<GOAL>hd :: tl <+ l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl l' : List α<VAR>f : ℕ ↪o ℕ<VAR>w : f 0 < l'.length<VAR>h : l'[f 0] = hd<VAR>f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) ⋯<VAR>hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'<VAR>this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?<GOAL>[hd] ++ tl <+ take (f 0 + 1) l' ++ drop (f 0 + 1) l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl l' : List α<VAR>f : ℕ ↪o ℕ<VAR>w : f 0 < l'.length<VAR>h : l'[f 0] = hd<VAR>f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) ⋯<VAR>hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'<VAR>this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?<GOAL>[hd] <+ take (f 0 + 1) l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl l' : List α<VAR>f : ℕ ↪o ℕ<VAR>w : f 0 < l'.length<VAR>h : l'[f 0] = hd<VAR>f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) ⋯<VAR>hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'<VAR>this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?<GOAL>(take (f 0).succ l')[f 0] ∈ take (f 0 + 1) l'
<VAR>α : Type u<VAR>β✝ : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>β : α → Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Finset ((a : α) × β a)<VAR>t : Finset α<VAR>ht : image Sigma.fst s ⊆ t<GOAL>(t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝³ : CommRing T<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>p : T[X]<VAR>n : ℕ<GOAL>(p ^ n).aroots S = n • p.aroots S
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>a : α<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<VAR>h : a ∉ s<GOAL>Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>f (fract x) - fract x = f x - x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<GOAL>(fun x => (map f μ).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<GOAL>(fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this : SigmaFinite (map f ν)<GOAL>(fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this✝ : SigmaFinite (map f ν)<VAR>this : SigmaFinite (map f (μ.singularPart ν))<GOAL>(fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this✝¹ : SigmaFinite (map f ν)<VAR>this✝ : SigmaFinite (map f (μ.singularPart ν))<VAR>this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))<GOAL>(fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this✝¹ : SigmaFinite (map f ν)<VAR>this✝ : SigmaFinite (map f (μ.singularPart ν))<VAR>this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))<VAR>h_add : (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) =ᶠ[ae (map f ν)] (map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)<GOAL>(fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this✝¹ : SigmaFinite (map f ν)<VAR>this✝ : SigmaFinite (map f (μ.singularPart ν))<VAR>this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))<VAR>h_add : (fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] fun x => ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)<GOAL>(fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this✝¹ : SigmaFinite (map f ν)<VAR>this✝ : SigmaFinite (map f (μ.singularPart ν))<VAR>this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))<VAR>h_add : (fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] fun x => ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)<GOAL>(μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun x => ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this✝¹ : SigmaFinite (map f ν)<VAR>this✝ : SigmaFinite (map f (μ.singularPart ν))<VAR>this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))<VAR>h_add : (fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] fun x => ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)<GOAL>(μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] fun x => (map f (μ.singularPart ν)).rnDeriv (map f ν) (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>this✝¹ : SigmaFinite (map f ν)<VAR>this✝ : SigmaFinite (map f (μ.singularPart ν))<VAR>this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))<VAR>h_add : (fun x => (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᶠ[ae ν] fun x => ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)<GOAL>(ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν] fun x => (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x y : ℕ<VAR>H : ↑x = ↑y<GOAL>↑x = ↑y
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>M : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>a : A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>m : M<GOAL>X • (of R M a) m = (of R M a) (a • m)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f✝ f g : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<GOAL>(((compHom (D k)).comp Φ) f) g = ∑ ij ∈ antidiagonal k, (((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2)) f) g
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f✝ f g : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<GOAL>(((compHom (D k)).comp Φ) f) g = ((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)) f) g
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<VAR>m : ℕ<VAR>r : R<VAR>n : ℕ<VAR>s : R<GOAL>(((((compHom (D k)).comp Φ).comp (monomial m).toAddMonoidHom) r).comp (monomial n).toAddMonoidHom) s = ((((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)).comp (monomial m).toAddMonoidHom) r).comp (monomial n).toAddMonoidHom) s
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<VAR>m : ℕ<VAR>r : R<VAR>n : ℕ<VAR>s : R<GOAL>(monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) = ∑ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<VAR>m : ℕ<VAR>r : R<VAR>n : ℕ<VAR>s : R<VAR>aux : ∀ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) = (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))<GOAL>(monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) = ∑ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<VAR>m : ℕ<VAR>r : R<VAR>n : ℕ<VAR>s : R<VAR>aux : ∀ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) = (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))<GOAL>(monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) = ∑ x ∈ antidiagonal k, (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<VAR>m : ℕ<VAR>r : R<VAR>n : ℕ<VAR>s : R<VAR>aux : ∀ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) = (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))<GOAL>(monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) = (monomial (m + n - k)) ((∑ i ∈ antidiagonal k, ↑(m.choose i.1) * ↑(n.choose i.2)) * (r * s))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom<VAR>Φ : R[X] →+ R[X] →+ R[X] := mul<VAR>m : ℕ<VAR>r : R<VAR>n : ℕ<VAR>s : R<VAR>aux : ∀ x ∈ antidiagonal k, (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) = (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))<GOAL>↑((m + n).choose k) = ∑ i ∈ antidiagonal k, ↑(m.choose i.1) * ↑(n.choose i.2)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>n : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<GOAL>t ≤ s → s ∈ ↑𝒜.shatterer → t ∈ ↑𝒜.shatterer
<VAR>m n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>h : n = 0 → b = true<VAR>a✝ : n.div2.bits = n.bits.tail<GOAL>(bit b n).div2.bits = (bit b n).bits.tail
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>f : α →₀ M<VAR>inst✝ : CommMonoid N<VAR>g : α → M → N<GOAL>(filter p f).prod g = ∏ x ∈ (filter p f).support, g x (f x)
<VAR>n b m : ℕ<GOAL>m < (b + 2) ^ ((b + 2).digits m).length
<VAR>n b m : ℕ<GOAL>m = ofDigits (b + 2) ((b + 2).digits m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>s : Set α<VAR>t : Set β<VAR>S : (i : ι) → Set (π i)<GOAL>IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>t : Set β<VAR>S : (i : ι) → Set (π i)<GOAL>IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>s : Set α<VAR>t : Set β<VAR>S : (i : ι) → Set (π i)<VAR>hs : s.Nonempty<GOAL>IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>s : Set α<VAR>S : (i : ι) → Set (π i)<VAR>hs : s.Nonempty<GOAL>IsBounded (s ×ˢ ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsBounded s ∧ IsBounded ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Bornology α<VAR>inst✝¹ : Bornology β<VAR>inst✝ : (i : ι) → Bornology (π i)<VAR>s : Set α<VAR>t : Set β<VAR>S : (i : ι) → Set (π i)<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L✝ : Type u_3<VAR>M : Type u_4<VAR>ι : Type u_5<VAR>ιₘ : Type u_6<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : Nontrivial R<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Algebra R A<VAR>inst✝¹⁷ : LieRing L✝<VAR>inst✝¹⁶ : LieAlgebra R L✝<VAR>inst✝¹⁵ : Module.Finite R L✝<VAR>inst✝¹⁴ : Module.Free R L✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>inst✝¹¹ : LieRingModule L✝ M<VAR>inst✝¹⁰ : LieModule R L✝ M<VAR>inst✝⁹ : Module.Finite R M<VAR>inst✝⁸ : Module.Free R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ιₘ<VAR>inst✝⁴ : DecidableEq ιₘ<VAR>b : Basis ι R L✝<VAR>bₘ : Basis ιₘ R M<VAR>x✝ : L✝<VAR>K : Type u_7<VAR>L : Type u_8<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>x : L<GOAL>IsRegular K x ↔ finrank K ↥(engel K x) = rank K L
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B C : Matrix n n α<VAR>h : A⁻¹ = B⁻¹<VAR>h' : IsUnit A.det<GOAL>A = B
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B C : Matrix n n α<VAR>h : A⁻¹ = B⁻¹<VAR>h' : IsUnit A.det<GOAL>B * A⁻¹ = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B C : Matrix n n α<VAR>h : A⁻¹ = B⁻¹<VAR>h' : IsUnit A.det<GOAL>B * B⁻¹ = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B C : Matrix n n α<VAR>h : A⁻¹ = B⁻¹<VAR>h' : IsUnit A.det<GOAL>IsUnit B.det
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∉ s<VAR>f : α → β<VAR>b : β<GOAL>∏ x ∈ s, update f i b x = ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∉ s<VAR>f : α → β<VAR>b : β<GOAL>∀ x ∈ s, update f i b x = f x
<VAR>α : Type u_1<VAR>a : α<VAR>m n : Nat<VAR>l : List α<GOAL>(l.set m a).get? n = if m = n then (fun x => a) <$> l.get? n else l.get? n
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w x : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>r : G.Walk u x<GOAL>(p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>p : T[X]<VAR>a : S<GOAL>a ∈ p.aroots S ↔ p ≠ 0 ∧ (aeval a) p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>p : T[X]<VAR>a : S<GOAL>Function.Injective ⇑(algebraMap T S)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>f g : ↥(lp G 2)<GOAL>Summable fun i => ⟪↑f i, ↑g i⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>f g : ↥(lp G 2)<GOAL>(ENNReal.toReal 2).IsConjExponent (ENNReal.toReal 2)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>f g : ↥(lp G 2)<GOAL>∀ (i : ι), ‖⟪↑f i, ↑g i⟫_𝕜‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>f g : ↥(lp G 2)<VAR>i : ι<GOAL>‖⟪↑f i, ↑g i⟫_𝕜‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>huX : IsUniform X s ℙ volume<GOAL>∫ (x : Ω), X x ∂ℙ = (volume s)⁻¹.toReal * ∫ (x : ℝ) in s, x
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → ℝ<VAR>s : Set ℝ<VAR>huX : IsUniform X s ℙ volume<GOAL>∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂(volume s)⁻¹ • volume.restrict s
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v2 v3 : ℕ<GOAL>padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max (stationaryPoint hf) (max v2 v3)))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v2 v3 : ℕ<GOAL>stationaryPoint hf ≤ max (stationaryPoint hf) (max v2 v3)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v2 v3 : ℕ<GOAL>stationaryPoint hf ≤ stationaryPoint hf
<VAR>x✝ y x : ℝ<VAR>hx : x ≤ -1<GOAL>arcsin x = -(π / 2)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>p : MvPolynomial σ R<GOAL>(rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>p : MvPolynomial σ R<GOAL>(sum p fun s a => (monomial (s.sum fun a => Finsupp.single (f a))) a) = sum p fun a => Finsupp.single (a.sum fun a => Finsupp.single (f a))
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>log x ≤ y ↔ x ≤ rexp y
<VAR>b : EReal<VAR>h : b < 0<VAR>h' : b ≠ ⊥<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<GOAL>a' / b < a / b
<VAR>b : EReal<VAR>h : b < 0<VAR>h' : b ≠ ⊥<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<GOAL>a' / b ≠ a / b
<VAR>b : EReal<VAR>h : b < 0<VAR>h' : b ≠ ⊥<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<VAR>hyp : a' / b = a / b<GOAL>False
<VAR>b : EReal<VAR>h : b < 0<VAR>h' : b ≠ ⊥<VAR>a a' : EReal<VAR>a_lt_a' : a < a'<VAR>hyp : a' / b = a / b<GOAL>a = a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a b ∪ Ioc b a = Ioc (min a b) (max b a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p✝ : Filter ι✝<VAR>g : ι✝ → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>V : ι → Set (β × β)<VAR>h : (𝓤 β).HasBasis p V<GOAL>𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 1<GOAL>finrank k ↥(vectorSpan k (Set.range p)) ≤ n
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : F), IsSolvable (minpoly F ((algebraMap F ↥(solvableByRad F E)) α)).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α β : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F β).Gal → IsSolvable (minpoly F (α + β)).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F (-α)).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α β : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F β).Gal → IsSolvable (minpoly F (α * β)).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)), IsSolvable (minpoly F α).Gal → IsSolvable (minpoly F α⁻¹).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → IsSolvable (minpoly F (α ^ n)).Gal → IsSolvable (minpoly F α).Gal