ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝¹ : SeparableSpace ↑s<VAR>this✝ : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ + δ + δ < ε<VAR>k : ℕ<VAR>hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ < δ<VAR>this : ‖(∫ (a : Ω), Y k 0 a) - ∫ (a : Ω), X 0 a‖ < δ<VAR>I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ<VAR>J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (a : Ω), Y k 0 a‖ < δ<GOAL>∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (a : Ω), X 0 a‖ < ε
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasureSpace Ω<VAR>inst✝⁵ : IsProbabilityMeasure ℙ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>X : ℕ → Ω → E<VAR>hint : Integrable (X 0) ℙ<VAR>h' : StronglyMeasurable (X 0)<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>s : Set E := Set.range (X 0) ∪ {0}<VAR>zero_s : 0 ∈ s<VAR>this✝¹ : SeparableSpace ↑s<VAR>this✝ : Nonempty ↑s<VAR>φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)<VAR>Y : ℕ → ℕ → Ω → E := fun k i => ↑(φ k) ∘ X i<VAR>A : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>B : ∀ᵐ (ω : Ω), ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) a))<VAR>ω : Ω<VAR>hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (a : Ω), Y k 0 a))<VAR>h'ω : ∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (a : Ω), ‖(X 0 - Y k 0) a‖))<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ + δ + δ < ε<VAR>k : ℕ<VAR>hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ < δ<VAR>this : ‖(∫ (a : Ω), Y k 0 a) - ∫ (a : Ω), X 0 a‖ < δ<VAR>I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ<VAR>J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (a : Ω), Y k 0 a‖ < δ<VAR>n : ℕ<VAR>hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ<VAR>h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (a : Ω), Y k 0 a‖ < δ<GOAL>‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - ∫ (a : Ω), X 0 a‖ < ε
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>a.natAbs = b.natAbs ↔ a = b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>S : Type u_3<VAR>M₀ : Type u_4<VAR>M₁ : Type u_5<VAR>R : Type u_6<VAR>G : Type u_7<VAR>G₀ : Type u_8<VAR>inst✝⁷ : Mul M<VAR>inst✝⁶ : Monoid N<VAR>inst✝⁵ : Semigroup S<VAR>inst✝⁴ : MulZeroClass M₀<VAR>inst✝³ : MulOneClass M₁<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Group G<VAR>inst✝ : CancelMonoidWithZero G₀<VAR>p : N<VAR>n✝ : ℕ<VAR>h : IsIdempotentElem p<VAR>n : ℕ<VAR>ih : p ^ (n + 1) = p<GOAL>p ^ (n.succ + 1) = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>(if 1 = ⊤ then eLpNormEssSup (↑↑f - ↑↑g) μ else ∫⁻ (a : α), ↑‖↑↑f a - ↑↑g a‖₊ ∂μ).toReal = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal
<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>p1 p2 p3 : P<VAR>h2 : p2 ≠ p1<VAR>h3 : p3 ≠ p1<GOAL>∠ p1 p2 p3 + ∠ p2 p3 p1 + ∠ p3 p1 p2 = π
<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>p1 p2 p3 : P<VAR>h2 : p2 ≠ p1<VAR>h3 : p3 ≠ p1<GOAL>∠ p3 p1 p2 + ∠ p1 p3 p2 + ∠ p1 p2 p3 = π
<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>p1 p2 p3 : P<VAR>h2 : p2 ≠ p1<VAR>h3 : p3 ≠ p1<GOAL>InnerProductGeometry.angle (p3 -ᵥ p1) (p2 -ᵥ p1) + InnerProductGeometry.angle (p1 -ᵥ p3) (p2 -ᵥ p3) + InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = π
<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>p1 p2 p3 : P<VAR>h2 : p2 ≠ p1<VAR>h3 : p3 ≠ p1<GOAL>InnerProductGeometry.angle (p3 -ᵥ p1) (p2 -ᵥ p1) + InnerProductGeometry.angle (p3 -ᵥ p1) (p3 -ᵥ p1 - (p2 -ᵥ p1)) + InnerProductGeometry.angle (p2 -ᵥ p1) (p2 -ᵥ p1 - (p3 -ᵥ p1)) = π
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>h₁ : ℵ₀ ≤ #β<VAR>h₂ : #α < (#β).ord.cof<GOAL>∃ a, #↑(f ⁻¹' {a}) = #β
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>h₁ : ℵ₀ ≤ #β<VAR>h₂ : #α < (#β).ord.cof<VAR>this : ∃ a, #β ≤ #↑(f ⁻¹' {a})<GOAL>∃ a, #↑(f ⁻¹' {a}) = #β
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>h₁ : ℵ₀ ≤ #β<VAR>h₂ : #α < (#β).ord.cof<VAR>x : α<VAR>h : #β ≤ #↑(f ⁻¹' {x})<GOAL>#↑(f ⁻¹' {x}) ≤ #β
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>h₁ : ℵ₀ ≤ #β<VAR>h₂ : #α < (#β).ord.cof<VAR>x : α<VAR>h : #β ≤ #↑(f ⁻¹' {x})<GOAL>∃ p, #↑p = #↑(f ⁻¹' {x})
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal B<GOAL>Submodule.restrictScalars R (map includeRight I) = LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal B<GOAL>(Submodule.restrictScalars R (map includeRight I)).carrier = (LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)).carrier
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal B<GOAL>(Submodule.restrictScalars R (map includeRight I)).carrier ≤ (LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)).carrier
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>I : Ideal B<GOAL>(LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)).carrier ≤ (Submodule.restrictScalars R (map includeRight I)).carrier
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>(b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>m : ℕ∞<VAR>n : ℕ<GOAL>↑m < ↑n ↔ m < ↑n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>i : ℕ<GOAL>f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)) ≫ Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1) = f (i + 1) i ≫ Q.d i (i + 1)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>i : ℕ<VAR>this : (ComplexShape.up ℕ).prev (i + 1) = i<GOAL>f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)) ≫ Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1) = f (i + 1) i ≫ Q.d i (i + 1)
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)<GOAL>↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)<GOAL>((X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)).coeff k = (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)<GOAL>(∑ i ∈ range (n % p + 1), ∑ j ∈ range (n / p + 1), X ^ i * ↑((n % p).choose i) * (X ^ (p * j) * ↑((n / p).choose j))).coeff k = (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)<GOAL>(∑ k ∈ range (n % p + 1), ∑ k' ∈ range (n / p + 1), X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')).coeff k = (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)<VAR>h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x<GOAL>(∑ k ∈ range (n % p + 1), ∑ k' ∈ range (n / p + 1), X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')).coeff k = (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)<VAR>h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x<GOAL>(∑ x ∈ range (n % p + 1), ∑ x_1 ∈ range (n / p + 1), if k = x + p * x_1 then 1 * ↑((n % p).choose x * (n / p).choose x_1) else 0) = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)<VAR>h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x<GOAL>(if (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1) then 1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) else 0) = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
<VAR>q : ℚ≥0<VAR>hq : q ≠ 0<GOAL>q⁻¹.den = q.num
<VAR>q : ℚ≥0<VAR>hq : q ≠ 0<GOAL>(↑q.den).natAbs.Coprime q.num
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμν : μ univ = ν univ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<GOAL>μ = ν
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμν : μ univ = ν univ<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<GOAL>∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>rootSpace H (2⁻¹ • ⇑α) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥<VAR>W : Weight K (↥H) L := { toFun := 2⁻¹ • ⇑α, weightSpace_ne_bot' := h }<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥<VAR>W : Weight K (↥H) L := { toFun := 2⁻¹ • ⇑α, weightSpace_ne_bot' := h }<VAR>hW : 2 • ⇑W = ⇑α<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>h : ¬rootSpace H (2⁻¹ • ⇑α) = ⊥<VAR>W : Weight K (↥H) L := { toFun := 2⁻¹ • ⇑α, weightSpace_ne_bot' := h }<VAR>hW : 2 • ⇑W = ⇑α<GOAL>weightSpace L ⇑α = ⊥
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.edist u v ≠ ⊤ ↔ G.Reachable u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Reachable u v<GOAL>G.edist u v ≠ ⊤
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Reachable u v<VAR>hx : G.edist u v = ⊤<GOAL>False
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : G.Reachable u v<VAR>hx : G.Walk u v → False<GOAL>False
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<VAR>A : C<VAR>f g : X φ j ⟶ A<VAR>h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g<VAR>h₂ : inrX φ j ≫ f = inrX φ j ≫ g<GOAL>f = g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<VAR>A : C<VAR>f g : X φ j ⟶ A<VAR>h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g<VAR>h₂ : inrX φ j ≫ f = inrX φ j ≫ g<VAR>this : HasBinaryBiproduct (F.X i) (G.X j)<GOAL>f = g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<VAR>A : C<VAR>f g : X φ j ⟶ A<VAR>h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g<VAR>h₂ : inrX φ j ≫ f = inrX φ j ≫ g<VAR>this : HasBinaryBiproduct (F.X i) (G.X j)<GOAL>(XIsoBiprod φ j i hij).inv ≫ f = (XIsoBiprod φ j i hij).inv ≫ g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<VAR>A : C<VAR>f g : X φ j ⟶ A<VAR>h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g<VAR>h₂ : inrX φ j ≫ f = inrX φ j ≫ g<VAR>this : HasBinaryBiproduct (F.X i) (G.X j)<GOAL>biprod.inl ≫ (XIsoBiprod φ j i hij).inv ≫ f = biprod.inl ≫ (XIsoBiprod φ j i hij).inv ≫ g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<VAR>A : C<VAR>f g : X φ j ⟶ A<VAR>h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g<VAR>h₂ : inrX φ j ≫ f = inrX φ j ≫ g<VAR>this : HasBinaryBiproduct (F.X i) (G.X j)<GOAL>biprod.inr ≫ (XIsoBiprod φ j i hij).inv ≫ f = biprod.inr ≫ (XIsoBiprod φ j i hij).inv ≫ g
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<GOAL>𝟭 (W.Localization ⥤ D) = functor W D ⋙ inverse W D
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G✝ : C ⥤ D<VAR>hG : W.IsInvertedBy G✝<VAR>G : W.Localization ⥤ D<GOAL>(𝟭 (W.Localization ⥤ D)).obj G = (functor W D ⋙ inverse W D).obj G
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>G₁ G₂ : W.Localization ⥤ D<VAR>τ : G₁ ⟶ G₂<GOAL>(𝟭 (W.Localization ⥤ D)).map τ = eqToHom ⋯ ≫ (functor W D ⋙ inverse W D).map τ ≫ eqToHom ⋯
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).neighborSet w = {v}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj ⋯).neighborSet w = {v}
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a : α<GOAL>Sigma.ι (fun a => pullback g₁ (Sigma.ι X a)) a ≫ (fun x => (Sigma.desc fun a => pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₁ ≫ Sigma.desc e) = Sigma.ι (fun a => pullback g₁ (Sigma.ι X a)) a ≫ (fun x => (Sigma.desc fun a => pullback.fst g₁ (Sigma.ι X a)) ≫ x) (g₂ ≫ Sigma.desc e)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a : α<GOAL>pullback.fst g₁ (Sigma.ι X a) ≫ g₁ ≫ Sigma.desc e = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a : α<GOAL>(pullback.snd g₁ (Sigma.ι X a) ≫ Sigma.ι X a) ≫ Sigma.desc e = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a : α<GOAL>pullback.snd g₁ (Sigma.ι X a) ≫ e a = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a b : α<GOAL>Sigma.ι (fun a_1 => pullback (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) b ≫ (fun x => (Sigma.desc fun a_1 => pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) ≫ x) (pullback.snd g₁ (Sigma.ι X a) ≫ e a) = Sigma.ι (fun a_1 => pullback (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) b ≫ (fun x => (Sigma.desc fun a_1 => pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) ≫ x) (pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e)