ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t✝ : Set α<VAR>f : α → β → M<VAR>s : Finset α<VAR>t : Finset β<GOAL>∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ ↑t), f i j = ∏ᶠ (j : β) (_ : j ∈ ↑t) (i : α) (_ : i ∈ ↑s), f i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t✝ : Set α<VAR>f : α → β → M<VAR>s : Finset α<VAR>t : Finset β<GOAL>∏ i ∈ s, ∏ i_1 ∈ t, f i i_1 = ∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z w : ℂ<VAR>h : z.im = w.im<GOAL>edist z w = edist z.re w.re
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) (cocompact V) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (x : V) in cocompact V, dist (∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v) 0 < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>g : V → E<VAR>hg_supp : HasCompactSupport g<VAR>hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2<VAR>hg_cont : Continuous g<GOAL>∀ᶠ (x : V) in cocompact V, dist (∫ (v : V), 𝐞 (-⟪v, x⟫_ℝ) • f v) 0 < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>g : V → E<VAR>hg_supp : HasCompactSupport g<VAR>hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2<VAR>hg_cont : Continuous g<VAR>w : V<VAR>hI : dist (∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) 0 < ε / 2<GOAL>dist (∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) 0 < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>g : V → E<VAR>hg_supp : HasCompactSupport g<VAR>hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2<VAR>hg_cont : Continuous g<VAR>w : V<VAR>hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε / 2<GOAL>‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - 0‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>g : V → E<VAR>hg_supp : HasCompactSupport g<VAR>hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2<VAR>hg_cont : Continuous g<VAR>w : V<VAR>hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε / 2<VAR>this : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v‖ ≤ ε / 2<GOAL>‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - 0‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>g : V → E<VAR>hg_supp : HasCompactSupport g<VAR>hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2<VAR>hg_cont : Continuous g<VAR>w : V<VAR>hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε / 2<VAR>this : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v‖ + ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε / 2 + ε / 2<GOAL>‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - 0‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>g : V → E<VAR>hg_supp : HasCompactSupport g<VAR>hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2<VAR>hg_cont : Continuous g<VAR>w : V<VAR>hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε / 2<VAR>this : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v‖ + ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε<GOAL>‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - 0‖ < ε
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>hfi : Integrable f volume<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>g : V → E<VAR>hg_supp : HasCompactSupport g<VAR>hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2<VAR>hg_cont : Continuous g<VAR>w : V<VAR>hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε / 2<VAR>this : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v‖ + ‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0‖ < ε<GOAL>‖(∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - 0‖ = ‖((∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) + ((∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • g v) - 0)‖
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>g : CliffordAlgebra Q →ₐ[R] A<VAR>m : M<GOAL>g ((ι Q) m) * g ((ι Q) m) = (algebraMap R A) (Q m)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<GOAL>dickson 1 1 (m * n) = (dickson 1 1 m).comp (dickson 1 1 n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>dickson 1 1 (m * n) = (dickson 1 1 m).comp (dickson 1 1 n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>dickson 1 ((Int.castRingHom R) 1) (m * n) = (dickson 1 ((Int.castRingHom R) 1) m).comp (dickson 1 ((Int.castRingHom R) 1) n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>map (Int.castRingHom R) (dickson 1 1 (m * n)) = map (Int.castRingHom R) ((dickson 1 1 m).comp (dickson 1 1 n))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) ((dickson 1 1 m).comp (dickson 1 1 n))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>((Chebyshev.T ℚ ↑m + Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n)).comp (C ⅟2 * X) = ((Chebyshev.T ℚ ↑m + Chebyshev.T ℚ ↑m).comp (C ⅟2 * X)).comp ((Chebyshev.T ℚ ↑n + Chebyshev.T ℚ ↑n).comp (C ⅟2 * X))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>((2 * Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n)).comp (C ⅟2 * X) = (((2 * Chebyshev.T ℚ ↑m).comp (C ⅟2 * X)).comp (2 * Chebyshev.T ℚ ↑n)).comp (C ⅟2 * X)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>(2 * Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n) = ((2 * Chebyshev.T ℚ ↑m).comp (C ⅟2 * X)).comp (2 * Chebyshev.T ℚ ↑n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>(2 * Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n) = (2 * Chebyshev.T ℚ ↑m).comp ((C ⅟2 * X).comp (2 * Chebyshev.T ℚ ↑n))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>m n : ℕ<VAR>h : 1 = (Int.castRingHom R) 1<GOAL>Chebyshev.T ℚ ↑n = (C ⅟2 * X).comp (2 * Chebyshev.T ℚ ↑n)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => ν (Prod.mk x ⁻¹' s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => (sum (sFiniteSeq ν)) (Prod.mk x ⁻¹' s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => ∑' (i : ℕ), (sFiniteSeq ν i) (Prod.mk x ⁻¹' s)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ a : α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ
<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>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : ∀ (x : ℝ), f' x < 0<VAR>x : ℝ<GOAL>deriv f x < 0
<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>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : ∀ (x : ℝ), f' x < 0<VAR>x : ℝ<GOAL>f' x < 0
<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>h : s₁ ⊆ s₂<VAR>hg : ∀ x ∈ s₂ \ s₁, g x = 1<VAR>hfg : ∀ x ∈ s₁, f x = g x<GOAL>∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i
<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>h : s₁ ⊆ s₂<VAR>hg : ∀ x ∈ s₂ \ s₁, g x = 1<VAR>hfg : ∀ x ∈ s₁, f x = g x<GOAL>∏ i ∈ s₁, f i = ∏ x ∈ s₁, g x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>a : α<GOAL>count a (map Prod.fst m.toEnumFinset.val) = count a m
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ≥0∞<VAR>f' : α → ℝ≥0∞ := AEMeasurable.mk f hf<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>n : ℕ<GOAL>⌊a + ↑n⌋ = ⌊a⌋ + ↑n
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>h : Subsingleton G<VAR>x y : Subgroup G<VAR>i : G<GOAL>1 ∈ x ↔ 1 ∈ y
<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 z : E<GOAL>⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜
<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 z : E<GOAL>(starRingEnd 𝕜) ⟪y, x⟫_𝕜 + (starRingEnd 𝕜) ⟪z, x⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>closedBall x r = ⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : OuterMeasure α<VAR>a : ℝ≥0∞<VAR>b : α<VAR>s : Set α<GOAL>(a • dirac b) s = s.indicator (fun x => a) b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : Semiring R<VAR>x y : R<GOAL>evalEval x y Y = y
<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 : α<GOAL>sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : Monoid γ<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>ha : a ∉ s<VAR>comm : (↑(cons a s ha)).Pairwise fun a b => Commute (f a) (f b)<GOAL>(cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>h : Submodule.span ℝ {x} = Submodule.span ℝ {y}<GOAL>2 • o.oangle x z = 2 • o.oangle y z
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>h : ∃ z, z • x = y<GOAL>2 • o.oangle x z = 2 • o.oangle y z
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x z : V<VAR>r : ℝˣ<GOAL>2 • o.oangle x z = 2 • o.oangle (r • x) z
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b✝ b' : β<VAR>c : γ<VAR>t : Finset β<VAR>hf : ∀ (b : β), Injective fun a => f a b<VAR>b : β<VAR>hb : b ∈ t<GOAL>s.card ≤ (image₂ f s t).card
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b✝ b' : β<VAR>c : γ<VAR>t : Finset β<VAR>hf : ∀ (b : β), Injective fun a => f a b<VAR>b : β<VAR>hb : b ∈ t<GOAL>(image₂ f s {b}).card ≤ (image₂ f s t).card
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.63975, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryExtensive C<VAR>inst✝¹ : ∀ (X : C), Projective X<VAR>inst✝ : ReflectsFiniteProducts s<VAR>hF : IsSheaf (coherentTopology C) (F ⋙ s)<GOAL>IsSheaf (coherentTopology C) F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.63975, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryExtensive C<VAR>inst✝¹ : ∀ (X : C), Projective X<VAR>inst✝ : ReflectsFiniteProducts s<VAR>hF : Nonempty (PreservesFiniteProducts (F ⋙ s))<GOAL>Nonempty (PreservesFiniteProducts F)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasRightHomology<VAR>A : C<VAR>f₁ f₂ : S.opcycles ⟶ A<GOAL>f₁ = f₂ ↔ S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<GOAL>vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>Y Z : C<VAR>P Q : Subobject Y<VAR>f : Z ⟶ Y<VAR>h : P ≤ Q<GOAL>P.Factors f → Q.Factors f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>Y Z : C<VAR>P Q : Subobject Y<VAR>f : Z ⟶ Y<VAR>h : P ≤ Q<GOAL>(representative.obj P).Factors f → (representative.obj Q).Factors f
<VAR>X Y : Skeleton<VAR>x✝ : IsIsomorphic X Y<VAR>h : X ≅ Y<VAR>a : Fin X.len<GOAL>(h.inv { down := (fun x => (h.hom { down := x }).down) a }).down = a
<VAR>X Y : Skeleton<VAR>x✝ : IsIsomorphic X Y<VAR>h : X ≅ Y<VAR>a : Fin X.len<GOAL>(h.inv (h.hom { down := a })).down = a
<VAR>X Y : Skeleton<VAR>x✝ : IsIsomorphic X Y<VAR>h : X ≅ Y<VAR>a : Fin Y.len<GOAL>(h.hom { down := (fun x => (h.inv { down := x }).down) a }).down = a
<VAR>X Y : Skeleton<VAR>x✝ : IsIsomorphic X Y<VAR>h : X ≅ Y<VAR>a : Fin Y.len<GOAL>(h.hom (h.inv { down := a })).down = a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M<VAR>a b : ℕ<VAR>hab : a < b<VAR>f : ℕ → M<VAR>ha : a ∉ Ico (a + 1) b<GOAL>∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖) ↔ angle x y = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖)<GOAL>angle x y = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖)<VAR>h₁ : ‖x‖ * ‖y‖ ≠ 0<GOAL>angle x y = π
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₂ : W<VAR>ω₁ : List B<VAR>hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)<GOAL>cs.length (cs.wordProd ω₁ * w₂) ≤ cs.length (cs.wordProd ω₁) + cs.length w₂
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω₁ : List B<VAR>hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)<VAR>ω₂ : List B<VAR>hω₂ : ω₂.length = cs.length (cs.wordProd ω₂)<GOAL>cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω₁ : List B<VAR>hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)<VAR>ω₂ : List B<VAR>hω₂ : ω₂.length = cs.length (cs.wordProd ω₂)<VAR>this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length<GOAL>cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)
<VAR>M' : Type u_1<VAR>inst✝³ : Monoid M'<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>φ : M →* N<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>h : φ.CompTriple ψ χ<VAR>x : M<GOAL>ψ (φ x) = χ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<VAR>c : R<GOAL>(A.updateRow i (A i + c • A j)).det = A.det
<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>α : ι → Type u_2<VAR>l : List ι<VAR>fs : (i : ι) → List (α i)<VAR>f : (i : ι) → i ∈ l → α i<GOAL>f ∈ l.pi fs ↔ f ∈ (↑l).pi fun x => ↑(fs x)
<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>α : ι → Type u_2<VAR>l : List ι<VAR>fs : (i : ι) → List (α i)<VAR>f : (i : ι) → i ∈ l → α i<GOAL>f ∈ l.pi fs ↔ f ∈ ↑(l.pi fs)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ range (n + 1 + 1), ↑((n + 1 + 1).choose k) * bernoulli k = if n + 1 + 1 = 1 then 1 else 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>f : ∑ k ∈ range n.succ.succ, ↑(n.succ.succ.choose k) * bernoulli' k = ↑n.succ.succ<GOAL>∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>f : ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) = ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)<GOAL>∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>f : ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) = ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)<GOAL>∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>f : ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) = ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)<GOAL>↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1) = ↑n / 2