ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>x y : G<GOAL>↑↑(condexpIndSMul hm hs hμs x + condexpIndSMul hm hs hμs y) =ᶠ[ae μ] fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm hs hμs y) x_1
<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>x y : G<VAR>a : α<GOAL>(↑↑(condexpIndSMul hm hs hμs x) + ↑↑(condexpIndSMul hm hs hμs y)) a = (fun x_1 => ↑↑(condexpIndSMul hm hs hμs x) x_1 + ↑↑(condexpIndSMul hm hs hμs y) x_1) a
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 0
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.d₂ c₁₂ i₁ i₂ i₁₂' = 0
<VAR>m n : ℤ<GOAL>Odd n ↔ ¬Even n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c<VAR>h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b<GOAL>b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p]
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c<VAR>h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b<VAR>h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c<VAR>h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b<VAR>h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c<VAR>h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b<VAR>h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>h₁₂₃ : toIcoMod hp a b ≤ toIcoMod hp a c<VAR>h₁₃₂ : toIcoMod hp a c ≤ toIcoMod hp a b<VAR>h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>r : 𝕜<GOAL>⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜
<VAR>m n a b c d : ℕ<GOAL>a + n ≡ a [MOD n]
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>(a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
<VAR>b : ℕ<VAR>hab : Coprime 0 b<GOAL>(0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>ha : a > 0<GOAL>(a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
<VAR>a : ℕ<VAR>ha : a > 0<VAR>hab : a.Coprime 0<GOAL>(a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>ha : a > 0<VAR>hb : b > 0<GOAL>(a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>hθ : ¬Function.Injective ⇑(Hom.toOrderHom θ)<GOAL>∃ i θ', θ = σ i ≫ θ'
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1<GOAL>∃ i θ', θ = σ i ≫ θ'
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1<VAR>x y : Fin (n + 2)<VAR>h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y<VAR>h₂ : x < y<GOAL>∃ i θ', θ = σ i ≫ θ'
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1<VAR>x y : Fin (n + 2)<VAR>h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y<VAR>h₂ : x < y<GOAL>∃ θ', θ = σ (x.castPred ⋯) ≫ θ'
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1<VAR>x y : Fin (n + 2)<VAR>h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y<VAR>h₂ : x < y<GOAL>(Hom.toOrderHom θ) (x.castPred ⋯).castSucc = (Hom.toOrderHom θ) (x.castPred ⋯).succ
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1<VAR>x y : Fin (n + 2)<VAR>h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y<VAR>h₂ : x < y<GOAL>(Hom.toOrderHom θ) (x.castPred ⋯).castSucc ≤ (Hom.toOrderHom θ) (x.castPred ⋯).succ
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n + 1] ⟶ Δ'<VAR>hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1<VAR>x y : Fin (n + 2)<VAR>h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y<VAR>h₂ : x < y<GOAL>(Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝⁴ : Fintype ι✝<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>ι : Type u_5<VAR>inst✝ : Fintype ι<GOAL>dimH univ = ↑(Fintype.card ι)
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : Set ι<VAR>inst✝ : Finite ↑s<VAR>t : ι → Set α<VAR>H : ∀ i ∈ s, Finite ↑(t i)<GOAL>Finite ↑(⋃ x ∈ s, t x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : Set ι<VAR>inst✝ : Finite ↑s<VAR>t : ι → Set α<VAR>H : ∀ i ∈ s, Finite ↑(t i)<GOAL>Finite ↑(⋃ x, t ↑x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : Set ι<VAR>inst✝ : Finite ↑s<VAR>t : ι → Set α<VAR>H : ∀ i ∈ s, Finite ↑(t i)<VAR>this : ∀ (i : ↑s), Finite ↑(t ↑i)<GOAL>Finite ↑(⋃ x, t ↑x)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>m n : ℤ<VAR>x : ℝ≥0<VAR>hx : ↑x ≠ 0<GOAL>↑x ^ (m + n) = ↑x ^ m * ↑x ^ n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>m n : ℤ<VAR>x : ℝ≥0<VAR>hx : x ≠ 0<GOAL>↑x ^ (m + n) = ↑x ^ m * ↑x ^ n
<VAR>L : Type u_1<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : TopologicalSpace L<VAR>inst✝ : ContinuousSup L<VAR>α : Type u_2<VAR>l : Filter α<VAR>f : ℕ → α → L<VAR>g : ℕ → L<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))<GOAL>Tendsto (fun a => (partialSups fun x => f x a) n) l (𝓝 ((partialSups g) n))
<VAR>k : ℕ<VAR>m : ℕ := 2 ^ k.primesBelow.card<VAR>N₀ : ℕ := 2 * m ^ 2<VAR>hN₀ : N₀ = 2 * m ^ 2<VAR>S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p<GOAL>1 / 2 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p
<VAR>k : ℕ<VAR>m : ℕ := 2 ^ k.primesBelow.card<VAR>N₀ : ℕ := 2 * m ^ 2<VAR>hN₀ : N₀ = 2 * m ^ 2<VAR>S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p<GOAL>1 / 2 ≤ S
<VAR>k : ℕ<VAR>m : ℕ := 2 ^ k.primesBelow.card<VAR>N₀ : ℕ := 2 * m ^ 2<VAR>hN₀ : N₀ = 2 * m ^ 2<VAR>S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p<GOAL>2 * ↑N₀ ≤ ↑m * ↑(2 * N₀).sqrt + 2 * ↑N₀ * S
<VAR>k : ℕ<VAR>m : ℕ := 2 ^ k.primesBelow.card<VAR>N₀ : ℕ := 2 * m ^ 2<VAR>hN₀ : N₀ = 2 * m ^ 2<VAR>S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p<GOAL>↑((2 * N₀).roughNumbersUpTo k).card ≤ 2 * ↑N₀ * S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : List α<VAR>a b : α<VAR>h : s(a, b) ∈ xs.sym2<GOAL>b ∈ xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : List α<VAR>a b : α<VAR>h : s(b, a) ∈ xs.sym2<GOAL>b ∈ xs
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → MetricSpace (E i)<VAR>i : ι<VAR>x : E i<VAR>j : ι<VAR>y : E j<VAR>k : ι<VAR>z : E k<GOAL>dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → MetricSpace (E i)<VAR>i : ι<VAR>x : E i<VAR>j : ι<VAR>y : E j<VAR>z : E i<GOAL>dist ⟨i, x⟩ ⟨i, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨i, z⟩
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → MetricSpace (E i)<VAR>i : ι<VAR>x : E i<VAR>j : ι<VAR>y : E j<VAR>k : ι<VAR>z : E k<VAR>hik : i ≠ k<GOAL>dist ⟨i, x⟩ ⟨k, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨k, z⟩
<VAR>m n : ℕ<GOAL>Even (m * n) ↔ Even m ∨ Even n
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<GOAL>p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<VAR>hz : p.count a.factors = 0<GOAL>p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<VAR>hb0 : p.count b.factors = 0<GOAL>p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<VAR>hb0 : p.count b.factors = 0<GOAL>p.count a.factors = p.count (a * b).factors
<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>p : T[X]<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Algebra T S<VAR>inst✝² : CommRing S'<VAR>inst✝¹ : IsDomain S'<VAR>inst✝ : Algebra T S'<VAR>hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0<VAR>f : S →ₐ[T] S'<VAR>x : S<VAR>hx : x ∈ p.rootSet S<GOAL>f x ∈ p.rootSet 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>p : T[X]<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Algebra T S<VAR>inst✝² : CommRing S'<VAR>inst✝¹ : IsDomain S'<VAR>inst✝ : Algebra T S'<VAR>hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0<VAR>f : S →ₐ[T] S'<VAR>x : S<VAR>hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0<GOAL>map (algebraMap T S') p ≠ 0 ∧ (aeval (f x)) 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>p : T[X]<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Algebra T S<VAR>inst✝² : CommRing S'<VAR>inst✝¹ : IsDomain S'<VAR>inst✝ : Algebra T S'<VAR>hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0<VAR>f : S →ₐ[T] S'<VAR>x : S<VAR>hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0<GOAL>map (algebraMap T S') p ≠ 0 ∧ 0 = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<GOAL>(laurent 0) f = f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<VAR>p✝ q✝ : R[X]<VAR>hq✝ : q✝ ≠ 0<GOAL>(laurent 0) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝) = (algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<GOAL>angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
<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>u : ι → UniformSpace γ<GOAL>uniformSpace α γ 𝔖 = ⨅ i, uniformSpace α γ 𝔖
<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>u : ι → UniformSpace γ<GOAL>⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) = ⨅ i, ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ)
<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>u : ι → UniformSpace γ<GOAL>⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) = ⨅ j, ⨅ i, ⨅ (_ : j ∈ 𝔖), UniformSpace.comap (⇑UniformFun.ofFun ∘ j.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑j) γ)
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>b : ℝ<VAR>hb : 0 ≤ b<VAR>a : ℝ≥0<GOAL>↑a ≤ ENNReal.ofReal b ↔ (↑a).toReal ≤ b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>a b x y : α<GOAL>sign (x * y) = sign x * sign y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>f' ≤ slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>S ∈ 𝓝[<] y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>∃ l ∈ Iio y, Ico l y ⊆ S
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>a b c d : α<GOAL>Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f f' : ↥(Lp E p μ)<GOAL>‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ ↑c * ‖f - f'‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f f' : ↥(Lp E p μ)<GOAL>∀ᵐ (x : α) ∂μ, ‖↑↑(hg.compLp g0 f - hg.compLp g0 f') x‖ ≤ ↑c * ‖↑↑(f - f') x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f f' : ↥(Lp E p μ)<VAR>a : α<VAR>ha1 : ↑↑(hg.compLp g0 f) a = (g ∘ ↑↑f) a<VAR>ha2 : ↑↑(hg.compLp g0 f') a = (g ∘ ↑↑f') a<VAR>ha3 : ↑↑(hg.compLp g0 f - hg.compLp g0 f') a = (↑↑(hg.compLp g0 f) - ↑↑(hg.compLp g0 f')) a<VAR>ha4 : ↑↑(f - f') a = (↑↑f - ↑↑f') a<GOAL>‖↑↑(hg.compLp g0 f - hg.compLp g0 f') a‖ ≤ ↑c * ‖↑↑(f - f') a‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f f' : ↥(Lp E p μ)<VAR>a : α<VAR>ha1 : ↑↑(hg.compLp g0 f) a = (g ∘ ↑↑f) a<VAR>ha2 : ↑↑(hg.compLp g0 f') a = (g ∘ ↑↑f') a<VAR>ha3 : ↑↑(hg.compLp g0 f - hg.compLp g0 f') a = (↑↑(hg.compLp g0 f) - ↑↑(hg.compLp g0 f')) a<VAR>ha4 : ↑↑(f - f') a = (↑↑f - ↑↑f') a<GOAL>dist (g (↑↑f a)) (g (↑↑f' a)) ≤ ↑c * dist (↑↑f a) (↑↑f' a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>a₁ a₂ b₁ b₂ : β<VAR>h₁ : abv (a₁ - b₁) < ε / 2<VAR>h₂ : abv (a₂ - b₂) < ε / 2<GOAL>abv (a₁ + a₂ - (b₁ + b₂)) < ε
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<GOAL>HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<GOAL>HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x<GOAL>HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x<VAR>c : HasDerivAt (fun x => -(Complex.cos (↑x * (2 * z)) / (2 * z))) (-(-Complex.sin (↑x * (2 * z)) * (2 * z) / (2 * z))) x<GOAL>HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x<VAR>c : HasDerivAt (fun x => -Complex.cos (↑x * (2 * z)) / (2 * z)) (Complex.sin (↑x * (2 * z))) x<GOAL>HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x<VAR>c : HasDerivAt (fun x => -Complex.cos (2 * z * ↑x) / (2 * z)) (Complex.sin (2 * z * ↑x)) x<GOAL>HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>(l.erase a).length = l.length.pred
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>(eraseP (fun x => a == x) l).length = l.length.pred
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<GOAL>Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<GOAL>Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<GOAL>Measure.map (⇑e.symm) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>(Measure.map (⇑e.symm) (gaussianReal μ v)) s' = (gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)) s'
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * gaussianPDFReal μ v (e x)) = ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>⟨c ^ 2, ⋯⟩ * v ≠ 0
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)) = ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<VAR>x : ℝ<GOAL>|c⁻¹| * (|c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x) = gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<VAR>x : ℝ<GOAL>|c⁻¹| * |c| = 1