ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : ∀ J ≤ I, (↑J).FG<VAR>hx : ¬x = 0<VAR>h_gx : (algebraMap R₁ K) x ≠ 0<VAR>h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0<GOAL>∀ J ≤ spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I, (↑J).FG
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : ∀ J ≤ I, (↑J).FG<VAR>hx : ¬x = 0<VAR>h_gx : (algebraMap R₁ K) x ≠ 0<VAR>h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0<VAR>J : FractionalIdeal R₁⁰ K<VAR>hJ : J ≤ spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I<GOAL>(↑J).FG
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : ∀ J ≤ I, (↑J).FG<VAR>hx : ¬x = 0<VAR>h_gx : (algebraMap R₁ K) x ≠ 0<VAR>h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0<VAR>J : FractionalIdeal R₁⁰ K<VAR>hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I<GOAL>(↑J).FG
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : ∀ J ≤ I, (↑J).FG<VAR>hx : ¬x = 0<VAR>h_gx : (algebraMap R₁ K) x ≠ 0<VAR>h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0<VAR>J : FractionalIdeal R₁⁰ K<VAR>hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I<VAR>s : Finset K<VAR>hs : span R₁ ↑s = ↑(J * spanSingleton R₁⁰ ((algebraMap R₁ K) x))<GOAL>(↑J).FG
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : ∀ J ≤ I, (↑J).FG<VAR>hx : ¬x = 0<VAR>h_gx : (algebraMap R₁ K) x ≠ 0<VAR>h_spanx : spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≠ 0<VAR>J : FractionalIdeal R₁⁰ K<VAR>hJ : J * spanSingleton R₁⁰ ((algebraMap R₁ K) x) ≤ I<VAR>s : Finset K<VAR>hs : span R₁ ↑s = ↑(J * spanSingleton R₁⁰ ((algebraMap R₁ K) x))<GOAL>span R₁ ↑(s * {((algebraMap R₁ K) x)⁻¹}) = ↑J
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>ContDiff ℝ 1 fun x => ‖x‖ ^ p
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>(Differentiable ℝ fun x => ‖x‖ ^ p) ∧ Continuous (fderiv ℝ fun x => ‖x‖ ^ p)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>Continuous (fderiv ℝ fun x => ‖x‖ ^ p)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>∀ (x : E), ContinuousAt (fderiv ℝ fun x => ‖x‖ ^ p) x
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StrictOrderedSemiring Γ<VAR>x : PowerSeries R<VAR>n : ℕ<GOAL>((ofPowerSeries Γ R) x).coeff ↑n = (PowerSeries.coeff R n) x
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>h : t.Sized<GOAL>t.toList.length = t.size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<GOAL>(map (⇑f) μ).InnerRegular ↔ μ.InnerRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>h : (map (⇑f) μ).InnerRegular<GOAL>μ.InnerRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>h : (map (⇑f) μ).InnerRegular<GOAL>μ = map (⇑f.symm) (map (⇑f) μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>U : Set α<VAR>ε : ℝ≥0∞<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>h : (map (⇑f) μ).InnerRegular<GOAL>μ = map (⇑f.symm ∘ ⇑f) μ
<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>d : ℕ<GOAL>mk 1 * (1 - X) = 1
<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>d : ℕ<GOAL>∀ (n : ℕ), (coeff S n) ((1 - X) * mk 1) = (coeff S n) 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f✝ g : β → α<VAR>a✝ : α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β → γ → α<VAR>a : α<GOAL>(s.sup fun b => t.sup (f b)) ≤ a ↔ (t.sup fun c => s.sup fun b => f b c) ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s₁ s₂ : Stream' α<VAR>h : ∀ (n : ℕ), take n s₁ = take n s₂<GOAL>s₁ = s₂
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s₁ s₂ : Stream' α<VAR>h : ∀ (n : ℕ), take n s₁ = take n s₂<GOAL>∀ (n : ℕ), s₁.get n = s₂.get n
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2) (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)<GOAL>HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2) (sinZeta (↑a) s)<GOAL>HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2) (sinZeta (↑a) s)<GOAL>HasSum (fun n => (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s) (sinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2) (sinZeta (↑a) s)<VAR>n : ℕ<GOAL>(cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s = -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2) (sinZeta (↑a) s)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s = -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun n => -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2) (sinZeta (↑a) s)<GOAL>(cexp (-(2 * ↑π * ↑a * ↑0) * I) - cexp (2 * ↑π * ↑a * ↑0 * I)) * I / 2 / ↑0 ^ s = -I * ↑(↑0).sign * cexp (2 * ↑π * I * ↑a * ↑0) / ↑0 ^ s / 2 + -(-I * ↑(↑0).sign) * cexp (-(2 * ↑π * I * ↑a * ↑0)) / ↑0 ^ s / 2
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : StrictMono u<GOAL>∑' (k : ℕ), f k ≤ ∑ k ∈ range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : StrictMono u<GOAL>⨆ i, ∑ a ∈ range (u i), f a ≤ ∑ k ∈ range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : StrictMono u<VAR>n : ℕ<GOAL>∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : StrictMono u<VAR>n : ℕ<VAR>this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)<GOAL>∑ k ∈ range n, (u (k + 1) - u k) • f (u k) ≤ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : StrictMono u<VAR>n : ℕ<VAR>this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)<GOAL>∑ x ∈ range n, ↑(u (x + 1) - u x) * f (u x) ≤ ∑' (k : ℕ), ↑(u (k + 1) - u k) * f (u k)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x✝ x : P<GOAL>intrinsicFrontier 𝕜 {x} = ∅
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>inst✝ : HasOuterApproxClosed Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ι → ProbabilityMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>E : Set Ω<VAR>E_nullbdry : μ (frontier E) = 0<GOAL>Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>inst✝ : HasOuterApproxClosed Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ι → ProbabilityMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>E : Set Ω<VAR>E_nullbdry : μ (frontier E) = 0<VAR>E_nullbdry' : ↑μ (frontier E) = 0<GOAL>Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>inst✝ : HasOuterApproxClosed Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ι → ProbabilityMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>E : Set Ω<VAR>E_nullbdry : μ (frontier E) = 0<VAR>E_nullbdry' : ↑μ (frontier E) = 0<VAR>key : Tendsto (fun i => ↑(μs i) E) L (𝓝 (↑μ E))<GOAL>Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
<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>c c₁ c₂ p₁ p₂ : P<GOAL>c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ = ⟪c -ᵥ p₂, 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>c c₁ c₂ p₁ p₂ : P<GOAL>⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫_ℝ = 0 ↔ 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫_ℝ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>s : Set α<GOAL>IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_3, u_1} C<VAR>inst✝¹⁴ : Category.{u_4, u_2} D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : HasShift D ℤ<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : HasZeroObject D<VAR>inst✝⁹ : Preadditive C<VAR>inst✝⁸ : Preadditive D<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated C<VAR>inst✝⁴ : Pretriangulated D<VAR>F : C ⥤ D<VAR>inst✝³ : F.CommShift ℤ<VAR>inst✝² : F.IsTriangulated<VAR>inst✝¹ : (F.mapComposableArrows 2).EssSurj<VAR>inst✝ : IsTriangulated C<VAR>Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D<VAR>u₁₂ : Y₁ ⟶ Y₂<VAR>u₂₃ : Y₂ ⟶ Y₃<VAR>u₁₃ : Y₁ ⟶ Y₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : Y₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : Y₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : Y₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>α : ComposableArrows C 2<VAR>e : (F.mapComposableArrows 2).obj α ≅ ComposableArrows.mk₂ u₁₂ u₂₃<GOAL>Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_3, u_1} C<VAR>inst✝¹⁴ : Category.{u_4, u_2} D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : HasShift D ℤ<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : HasZeroObject D<VAR>inst✝⁹ : Preadditive C<VAR>inst✝⁸ : Preadditive D<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated C<VAR>inst✝⁴ : Pretriangulated D<VAR>F : C ⥤ D<VAR>inst✝³ : F.CommShift ℤ<VAR>inst✝² : F.IsTriangulated<VAR>inst✝¹ : (F.mapComposableArrows 2).EssSurj<VAR>inst✝ : IsTriangulated C<VAR>Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D<VAR>u₁₂ : Y₁ ⟶ Y₂<VAR>u₂₃ : Y₂ ⟶ Y₃<VAR>u₁₃ : Y₁ ⟶ Y₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : Y₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : Y₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : Y₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>X₁ X₂ X₃ : C<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>e : (F.mapComposableArrows 2).obj (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃<GOAL>Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_3, u_1} C<VAR>inst✝¹⁴ : Category.{u_4, u_2} D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : HasShift D ℤ<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : HasZeroObject D<VAR>inst✝⁹ : Preadditive C<VAR>inst✝⁸ : Preadditive D<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated C<VAR>inst✝⁴ : Pretriangulated D<VAR>F : C ⥤ D<VAR>inst✝³ : F.CommShift ℤ<VAR>inst✝² : F.IsTriangulated<VAR>inst✝¹ : (F.mapComposableArrows 2).EssSurj<VAR>inst✝ : IsTriangulated C<VAR>Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D<VAR>u₁₂ : Y₁ ⟶ Y₂<VAR>u₂₃ : Y₂ ⟶ Y₃<VAR>u₁₃ : Y₁ ⟶ Y₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : Y₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : Y₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : Y₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>X₁ X₂ X₃ : C<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>e : (F.mapComposableArrows 2).obj (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃<VAR>w✝² : C<VAR>w✝¹ : X₂ ⟶ w✝²<VAR>w✝ : w✝² ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂' : Triangle.mk f w✝¹ w✝ ∈ distinguishedTriangles<GOAL>Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_3, u_1} C<VAR>inst✝¹⁴ : Category.{u_4, u_2} D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : HasShift D ℤ<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : HasZeroObject D<VAR>inst✝⁹ : Preadditive C<VAR>inst✝⁸ : Preadditive D<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated C<VAR>inst✝⁴ : Pretriangulated D<VAR>F : C ⥤ D<VAR>inst✝³ : F.CommShift ℤ<VAR>inst✝² : F.IsTriangulated<VAR>inst✝¹ : (F.mapComposableArrows 2).EssSurj<VAR>inst✝ : IsTriangulated C<VAR>Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D<VAR>u₁₂ : Y₁ ⟶ Y₂<VAR>u₂₃ : Y₂ ⟶ Y₃<VAR>u₁₃ : Y₁ ⟶ Y₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : Y₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : Y₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : Y₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>X₁ X₂ X₃ : C<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>e : (F.mapComposableArrows 2).obj (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃<VAR>w✝⁵ : C<VAR>w✝⁴ : X₂ ⟶ w✝⁵<VAR>w✝³ : w✝⁵ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂' : Triangle.mk f w✝⁴ w✝³ ∈ distinguishedTriangles<VAR>w✝² : C<VAR>w✝¹ : X₃ ⟶ w✝²<VAR>w✝ : w✝² ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃' : Triangle.mk g w✝¹ w✝ ∈ distinguishedTriangles<GOAL>Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_3, u_1} C<VAR>inst✝¹⁴ : Category.{u_4, u_2} D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : HasShift D ℤ<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : HasZeroObject D<VAR>inst✝⁹ : Preadditive C<VAR>inst✝⁸ : Preadditive D<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated C<VAR>inst✝⁴ : Pretriangulated D<VAR>F : C ⥤ D<VAR>inst✝³ : F.CommShift ℤ<VAR>inst✝² : F.IsTriangulated<VAR>inst✝¹ : (F.mapComposableArrows 2).EssSurj<VAR>inst✝ : IsTriangulated C<VAR>Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D<VAR>u₁₂ : Y₁ ⟶ Y₂<VAR>u₂₃ : Y₂ ⟶ Y₃<VAR>u₁₃ : Y₁ ⟶ Y₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : Y₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : Y₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : Y₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>X₁ X₂ X₃ : C<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>e : (F.mapComposableArrows 2).obj (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃<VAR>w✝⁸ : C<VAR>w✝⁷ : X₂ ⟶ w✝⁸<VAR>w✝⁶ : w✝⁸ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂' : Triangle.mk f w✝⁷ w✝⁶ ∈ distinguishedTriangles<VAR>w✝⁵ : C<VAR>w✝⁴ : X₃ ⟶ w✝⁵<VAR>w✝³ : w✝⁵ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃' : Triangle.mk g w✝⁴ w✝³ ∈ distinguishedTriangles<VAR>w✝² : C<VAR>w✝¹ : X₃ ⟶ w✝²<VAR>w✝ : w✝² ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃' : Triangle.mk (f ≫ g) w✝¹ w✝ ∈ distinguishedTriangles<GOAL>Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} D<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasFiniteBiproducts D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M N : Mat_ C<VAR>f : M ⟶ N<VAR>i : N.ι<GOAL>(F.map f ≫ (additiveObjIsoBiproduct F N).hom) ≫ biproduct.π (fun i => F.obj ((embedding C).obj (N.X i))) i = ((additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j => F.map ((embedding C).map (f i j))) ≫ biproduct.π (fun i => F.obj ((embedding C).obj (N.X i))) i
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} D<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasFiniteBiproducts D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M N : Mat_ C<VAR>f : M ⟶ N<VAR>i : N.ι<GOAL>((additiveObjIsoBiproduct F M).inv ≫ F.map f ≫ F.map fun j k => if h : j = i then eqToHom ⋯ else 0) = biproduct.desc fun j => F.map ((embedding C).map (f j i))
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} D<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasFiniteBiproducts D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M N : Mat_ C<VAR>f : M ⟶ N<VAR>i : N.ι<VAR>j : M.ι<GOAL>(biproduct.ι (fun i => F.obj ((embedding C).obj (M.X i))) j ≫ (additiveObjIsoBiproduct F M).inv ≫ F.map f ≫ F.map fun j k => if h : j = i then eqToHom ⋯ else 0) = biproduct.ι (fun i => F.obj ((embedding C).obj (M.X i))) j ≫ biproduct.desc fun j => F.map ((embedding C).map (f j i))
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} D<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasFiniteBiproducts D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M N : Mat_ C<VAR>f : M ⟶ N<VAR>i : N.ι<VAR>j : M.ι<GOAL>F.map ((fun j_1 k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j k => if h : j = i then eqToHom ⋯ else 0) = F.map ((embedding C).map (f j i))
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} D<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasFiniteBiproducts D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M N : Mat_ C<VAR>f : M ⟶ N<VAR>i : N.ι<VAR>j : M.ι<GOAL>((fun j_1 k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j k => if h : j = i then eqToHom ⋯ else 0) = (embedding C).map (f j i)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} D<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasFiniteBiproducts D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M N : Mat_ C<VAR>f : M ⟶ N<VAR>i : N.ι<VAR>j : M.ι<GOAL>((fun j_1 k => if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j k => if h : j = i then eqToHom ⋯ else 0) PUnit.unit PUnit.unit = (embedding C).map (f j i) PUnit.unit PUnit.unit
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>xs : List α<VAR>h : xs.Nodup<VAR>i : Fin xs.length<GOAL>xs.formPerm (xs.get i) = xs.get ⟨(↑i + 1) % xs.length, ⋯⟩
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>L : C ⥤ D<VAR>hL : W.IsInvertedBy L<GOAL>φ.map L hL ≫ L.map φ.s = L.map φ.f