ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>H : (Ideal.Quotient.mk (Ideal.span {a | (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, (fun i j h => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})) x = 0<VAR>this : (α : Sort ?u.611507) → DecidableEq α<GOAL>∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), x.IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) x) = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>H : (Ideal.Quotient.mk (Ideal.span {a | (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, (fun i j h => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})) x = 0<VAR>this : (α : Sort ?u.611507) → DecidableEq α<GOAL>∀ x ∈ {a | (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, (fun i j h => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}, ∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), x.IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) x) = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>H : (Ideal.Quotient.mk (Ideal.span {a | (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, (fun i j h => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})) x = 0<VAR>this : (α : Sort ?u.611507) → DecidableEq α<GOAL>∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), IsSupported 0 s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) 0) = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>H : (Ideal.Quotient.mk (Ideal.span {a | (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, (fun i j h => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})) x = 0<VAR>this : (α : Sort ?u.611507) → DecidableEq α<GOAL>∀ (x y : FreeCommRing ((i : ι) × G i)), (∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), x.IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) x) = 0) → (∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), y.IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) y) = 0) → ∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), (x + y).IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (x + y)) = 0
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : FreeCommRing ((i : ι) × G i)<VAR>H : (Ideal.Quotient.mk (Ideal.span {a | (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, (fun i j h => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})) x = 0<VAR>this : (α : Sort ?u.611507) → DecidableEq α<GOAL>∀ (a x : FreeCommRing ((i : ι) × G i)), (∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), x.IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) x) = 0) → ∃ j s, ∃ (H : ∀ k ∈ s, k.fst ≤ j), (a • x).IsSupported s ∧ ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (a • x)) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b c : α<VAR>hc : p * b = a * c<GOAL>p ∣ a ∨ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b c : α<VAR>hc : p * b = a * c<VAR>h : p ∣ a<GOAL>p ∣ a ∨ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b x : α<VAR>hc : p * b = a * (p * x)<GOAL>p ∣ a ∨ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<VAR>f : α → β<VAR>H : r ≤ ker f<VAR>g : Quotient r → β<VAR>Hg : f = g ∘ Quotient.mk''<VAR>x✝ : Quotient r<VAR>x : α<GOAL>Quotient.lift f H (Quot.mk Setoid.r x) = g (Quot.mk Setoid.r x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : Setoid α<VAR>f : α → β<VAR>H : r ≤ ker f<VAR>g : Quotient r → β<VAR>Hg : f = g ∘ Quotient.mk''<VAR>x✝ : Quotient r<VAR>x : α<GOAL>(g ∘ Quotient.mk'') x = g (Quot.mk Setoid.r x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>s : Set β<VAR>hf : Measurable f<VAR>hs : MeasurableSet s<VAR>c : ℝ≥0∞<GOAL>∫⁻ (a : α), s.indicator (fun x => c) (f a) ∂μ = c * μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>S : Type u_4<VAR>inst✝³ : Monoid S<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DistribMulAction S M<VAR>sR : Set R<VAR>s : Set S<VAR>N : Submodule R M<VAR>r : S<VAR>m : M<VAR>mem1 : r ∈ s<VAR>mem2 : m ∈ N<GOAL>r • m ∈ s • N
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>S : Type u_4<VAR>inst✝³ : Monoid S<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DistribMulAction S M<VAR>sR : Set R<VAR>s : Set S<VAR>N : Submodule R M<VAR>r : S<VAR>m : M<VAR>mem1 : r ∈ s<VAR>mem2 : m ∈ N<GOAL>∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}, r • m ∈ p
<VAR>k n✝ : ℕ<GOAL>(n✝ + 1).ascFactorial k = k ! * (n✝ + 1 + k - 1).choose k
<VAR>k n✝ : ℕ<GOAL>k ! * (n✝ + k).choose k = k ! * (n✝ + 1 + k - 1).choose k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>γ : Type u_4<VAR>f : α → β<VAR>x : Part α<VAR>g : β → Part γ<GOAL>(map f x).bind g = x.bind fun y => g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>γ : Type u_4<VAR>f : α → β<VAR>x : Part α<VAR>g : β → Part γ<GOAL>(x.bind fun x => ((some ∘ f) x).bind g) = x.bind fun y => g (f y)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝³ : CompleteSpace F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : BorelSpace G<VAR>g : G → E'' →L[𝕜] E'<VAR>hf : LocallyIntegrable f μ<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x₀ : G<VAR>x : E''<GOAL>((f ⋆[precompR E'' L, μ] g) x₀) x = (f ⋆[L, μ] fun a => (g a) x) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝³ : CompleteSpace F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : BorelSpace G<VAR>g : G → E'' →L[𝕜] E'<VAR>hf : LocallyIntegrable f μ<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x₀ : G<VAR>x : E''<VAR>this : ConvolutionExistsAt f g x₀ (precompR E'' L) μ<GOAL>((f ⋆[precompR E'' L, μ] g) x₀) x = (f ⋆[L, μ] fun a => (g a) x) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝³ : CompleteSpace F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : BorelSpace G<VAR>g : G → E'' →L[𝕜] E'<VAR>hf : LocallyIntegrable f μ<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x₀ : G<VAR>x : E''<VAR>this : ConvolutionExistsAt f g x₀ (precompR E'' L) μ<GOAL>∫ (x_1 : G), (((precompR E'' L) (f x_1)) (g (x₀ - x_1))) x ∂μ = ∫ (t : G), (L (f t)) ((g (x₀ - t)) x) ∂μ
<VAR>α : Type u<VAR>c✝ d c : Cardinal.{u}<VAR>h : c < ℵ₀<GOAL>↑(toNat c) = ↑(Classical.choose ⋯)
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ + (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) + (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ + ⁅L c, 2 • L (b * c)⁆) = ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) + (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆)
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ + (⁅L b, L (a * a)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) + (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ + ⁅L c, 2 • L (b * c)⁆) = ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) + (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆)
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L a, L (c * a)⁆ + 2 • ⁅L a, L (b * c)⁆ + (⁅L b, L (a * a)⁆ + ⁅L b, L (c * c)⁆ + 2 • ⁅L b, L (a * b)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L b, L (b * c)⁆) + (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + 2 • ⁅L c, L (a * b)⁆ + 2 • ⁅L c, L (c * a)⁆ + 2 • ⁅L c, L (b * c)⁆) = ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) + (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>k : ℕ<VAR>x : R<GOAL>matPolyEquiv (stdBasisMatrix i j ((monomial k) x)) = (monomial k) (stdBasisMatrix i j x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>k : ℕ<VAR>x : R<GOAL>(polyEquivTensor R (Matrix n n R)).symm ((Algebra.TensorProduct.comm R R[X] (Matrix n n R)) ((monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1)) = (monomial k) (stdBasisMatrix i j x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>k : ℕ<VAR>x : R<GOAL>(polyEquivTensor R (Matrix n n R)) ((polyEquivTensor R (Matrix n n R)).symm ((Algebra.TensorProduct.comm R R[X] (Matrix n n R)) ((monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1))) = (polyEquivTensor R (Matrix n n R)) ((monomial k) (stdBasisMatrix i j x))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>k : ℕ<VAR>x : R<GOAL>stdBasisMatrix i j 1 ⊗ₜ[R] (monomial k) x = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] X ^ k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>k : ℕ<VAR>x : R<GOAL>stdBasisMatrix i j 1 ⊗ₜ[R] (monomial k) x = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>k : ℕ<VAR>x : R<GOAL>(x • stdBasisMatrix i j 1) ⊗ₜ[R] (X ^ k) = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>inst✝ : SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : Memℒp f p μ<GOAL>Tendsto (fun n => Memℒp.toLp ↑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯) atTop (𝓝 (Memℒp.toLp f hf))
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>a : α<GOAL>{a}.prod = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>q : β → Prop<VAR>inst✝ : DecidablePred q<GOAL>filter (fun x => q x.2) (s ×ˢ t) = s ×ˢ filter q t
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(toPadicInt p).comp (fromPadicInt p) = RingHom.id ℤ_[p]
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>∀ (n : ℕ), (PadicInt.toZModPow n).comp ((toPadicInt p).comp (fromPadicInt p)) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(PadicInt.toZModPow n).comp ((toPadicInt p).comp (fromPadicInt p)) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(toZModPow p n).comp (fromPadicInt p) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)).comp (lift (fun k => (zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) ⋯) = PadicInt.toZModPow n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>((zmodEquivTrunc p n).symm.toRingHom.comp (zmodEquivTrunc p n).toRingHom).comp (PadicInt.toZModPow n) = PadicInt.toZModPow n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>K : CochainComplex C ℤ<GOAL>(subcategoryAcyclic C).P ((quotient C (ComplexShape.up ℤ)).obj K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>K : CochainComplex C ℤ<GOAL>(∀ (n : ℤ), IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K))) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<GOAL>IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K)) ↔ HomologicalComplex.ExactAt K n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<GOAL>IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K)) ↔ IsZero (HomologicalComplex.homology K n)
<VAR>𝕜 : Type v<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<GOAL>‖↑‖x‖ • coord 𝕜 x h‖ = 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>h : 1 ≤ a<VAR>n : ℕ<GOAL>a ^ n ≤ a ^ (n + 1)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>h : 1 ≤ a<VAR>n : ℕ<GOAL>a ^ n ≤ a * a ^ n
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>k : ℕ<GOAL>C r ^ k = 0 ↔ r ^ k = 0
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ : Measure Ω<GOAL>levyProkhorovEDist μ μ = 0
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ : Measure Ω<GOAL>levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ⊤)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ : Measure Ω<VAR>ε : ℝ≥0∞<VAR>x✝¹ : ε ∈ Ioo 0 ⊤<VAR>B : Set Ω<VAR>x✝ : MeasurableSet B<VAR>hε₀ : 0 < ε<VAR>hε_top : ε < ⊤<GOAL>μ B ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ : Measure Ω<VAR>ε : ℝ≥0∞<VAR>x✝¹ : ε ∈ Ioo 0 ⊤<VAR>B : Set Ω<VAR>x✝ : MeasurableSet B<VAR>hε₀ : 0 < ε<VAR>hε_top : ε < ⊤<GOAL>0 < ε.toReal
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>hP : P.IsEquipartition<VAR>hu : u ∈ P.parts<VAR>hucard : ¬u.card = m * 4 ^ P.parts.card + a<GOAL>(4 ^ P.parts.card - (a + 1)) * m + (a + 1) * (m + 1) = u.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>hP : P.IsEquipartition<VAR>hu : u ∈ P.parts<VAR>hucard : ¬u.card = m * 4 ^ P.parts.card + a<VAR>this : m * 4 ^ P.parts.card ≤ Fintype.card α / P.parts.card<GOAL>(4 ^ P.parts.card - (a + 1)) * m + (a + 1) * (m + 1) = u.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>hP : P.IsEquipartition<VAR>hu : u ∈ P.parts<VAR>hucard : ¬u.card = Fintype.card α / P.parts.card<VAR>this : m * 4 ^ P.parts.card ≤ Fintype.card α / P.parts.card<GOAL>(4 ^ P.parts.card - (a + 1)) * m + (a + 1) * (m + 1) = u.card
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonAssocSemiring R<VAR>x y : R<GOAL>{ toFun := ⇑(single 0), map_one' := ⋯ }.toFun (x * y) = { toFun := ⇑(single 0), map_one' := ⋯ }.toFun x * { toFun := ⇑(single 0), map_one' := ⋯ }.toFun y
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>this : TopologicalSpace A := hB.topology<VAR>U : Set A<VAR>hU : U ∈ 𝓝 0<GOAL>∃ V, ↑V ⊆ U
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>this : TopologicalSpace A := hB.topology<VAR>U : Set A<VAR>hU : U ∈ 𝓝 0<VAR>i : ι<VAR>hi : ↑(B i) ⊆ U<GOAL>∃ V, ↑V ⊆ U
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>i : ℕ<VAR>h : i.succ < m.succ<VAR>x : α<VAR>u : Fin m → α<GOAL>vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<GOAL>content 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>s : Finset M<VAR>x : M<VAR>hx : x ∈ span R ↑s<GOAL>x ∈ span R (_root_.id '' ↑s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>comap norm atTop = cobounded E
<VAR>α : Type u<GOAL>(ofFn fun i => [][↑i]) = []
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(ofFn fun i => (a :: l)[↑i]) = a :: l
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>((a :: l)[↑0] :: ofFn fun i => (a :: l)[↑i.succ]) = a :: l
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(ofFn fun i => (a :: l)[↑i.succ]) = l