ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<GOAL>↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<VAR>xle : xn a1 (2 * n - k) ≤ xn a1 n<GOAL>↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<VAR>xle : xn a1 (2 * n - k) ≤ xn a1 n<GOAL>xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<VAR>xle : xn a1 (2 * n - k) ≤ xn a1 n<GOAL>xn a1 k % xn a1 n = (xn a1 n - xn a1 (2 * n - k)) % xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<VAR>xle : xn a1 (2 * n - k) ≤ xn a1 n<GOAL>xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n - xn a1 (2 * n - k) + xn a1 (2 * n - k) [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<VAR>xle : xn a1 (2 * n - k) ≤ xn a1 n<GOAL>xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<VAR>xle : xn a1 (2 * n - k) ≤ xn a1 n<VAR>t : xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]<GOAL>xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>k : ℕ<VAR>kn : k > n<VAR>k2n : k ≤ 2 * n<VAR>k2nl : 2 * n - k < n := lt_of_add_lt_add_right (let_fun this := Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n))) (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n)); this)<VAR>xle : xn a1 (2 * n - k) ≤ xn a1 n<VAR>t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]<GOAL>xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>ij : i < n + 1<VAR>j2n : n + 1 ≤ 2 * n<VAR>jnn : n + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)<VAR>o : n = n ∨ n < n<GOAL>↑(xn a1 i % xn a1 n) < ↑(xn a1 (n + 1) % xn a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>ij : i < n + 1<VAR>j2n : n + 1 ≤ 2 * n<VAR>jnn : n + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)<VAR>o : n = n ∨ n < n<GOAL>↑(xn a1 i % xn a1 n) < ↑(xn a1 n) - ↑(xn a1 (n - 1))
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>ij : i < n + 1<VAR>j2n : n + 1 ≤ 2 * n<VAR>jnn : n + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)<VAR>o : n = n ∨ n < n<GOAL>xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>ij : i < n + 1<VAR>j2n : n + 1 ≤ 2 * n<VAR>jnn : n + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)<VAR>o : n = n ∨ n < n<VAR>lin : i < n<GOAL>xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>ij : i < n + 1<VAR>j2n : n + 1 ≤ 2 * n<VAR>jnn : n + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)<VAR>o : n = n ∨ n < n<VAR>ein : i = n<GOAL>xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>o : j = n ∨ n < j<VAR>jn : j > n<VAR>lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n<GOAL>↑(xn a1 j % xn a1 n) < ↑(xn a1 (j + 1) % xn a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>o : j = n ∨ n < j<VAR>jn : j > n<VAR>lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n<GOAL>↑(xn a1 n) - ↑(xn a1 (2 * n - j)) < ↑(xn a1 n) - ↑(xn a1 (2 * n - (j + 1)))
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>o : j = n ∨ n < j<VAR>jn : j > n<VAR>lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n<GOAL>2 * n - (j + 1) < 2 * n - j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i n : ℕ<VAR>npos : 0 < n<VAR>j : ℕ<VAR>ij : i < j + 1<VAR>j2n : j + 1 ≤ 2 * n<VAR>jnn : j + 1 ≠ n<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)<VAR>lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))<VAR>o : j = n ∨ n < j<VAR>jn : j > n<VAR>lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n<GOAL>(2 * n - j).pred < 2 * n - j
<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>θ : Real.Angle<VAR>x : V<VAR>hx : x ≠ 0<GOAL>↑(o.rotation θ).toLinearEquiv = (Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]
<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>θ : Real.Angle<VAR>x : V<VAR>hx : x ≠ 0<GOAL>∀ (i : Fin 2), ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) i) = ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]) ((o.basisRightAngleRotation x hx) i)
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<VAR>hyp1 : v (x - y) < ↑γ * (v y * v y)<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<VAR>hyp1 : v (x - y) < ↑γ * (v y * v y)<VAR>hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<VAR>hyp1 : v (x - y) < ↑γ * (v y * v y)<VAR>hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ<VAR>hyp2 : v (x - y) < v y<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<VAR>hyp1 : v (x - y) < ↑γ * (v y * v y)<VAR>hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ<VAR>hyp2 : v (x - y) < v y<VAR>key : v x = v y<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<VAR>hyp1 : v (x - y) < ↑γ * (v y * v y)<VAR>hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ<VAR>hyp2 : v (x - y) < v y<VAR>key : v x = v y<VAR>x_ne : x ≠ 0<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x y : K<VAR>γ : Γ₀ˣ<VAR>y_ne : y ≠ 0<VAR>h : v (x - y) < min (↑γ * (v y * v y)) (v y)<VAR>hyp1 : v (x - y) < ↑γ * (v y * v y)<VAR>hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ<VAR>hyp2 : v (x - y) < v y<VAR>key : v x = v y<VAR>x_ne : x ≠ 0<VAR>decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹<GOAL>v (x⁻¹ - y⁻¹) < ↑γ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝² : DecidableEq α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : (x : α) → Decidable ¬p x<GOAL>(filter p s).dens + (filter (fun a => ¬p a) s).dens = s.dens
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<VAR>n : ℕ<GOAL>countP p (n • s) = n * countP p s
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁷ : CommRing P<VAR>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<GOAL>IsDomain S
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁷ : CommRing P<VAR>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<GOAL>Nontrivial S
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁷ : CommRing P<VAR>K : Type u_4<VAR>inst✝⁶ : IsLocalization M✝ S<VAR>Q : Type u_5<VAR>inst✝⁵ : CommRing Q<VAR>g : R →+* P<VAR>inst✝⁴ : Algebra P Q<VAR>A : Type u_6<VAR>inst✝³ : CommRing A<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A S<VAR>M : Submonoid A<VAR>inst✝ : IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<GOAL>NoZeroDivisors S
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<GOAL>1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<VAR>H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs<GOAL>1 ≤ (↑(x 0) / ‖x‖) ^ 2
<VAR>z : ℍ<VAR>x : Fin 2 → ℤ<VAR>hx : x ≠ 0<VAR>H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs<GOAL>1 ≤ (↑(x 1) / ‖x‖) ^ 2
<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>α : Type u_17<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Nonempty α<VAR>f : α → E<VAR>g : α → F<GOAL>f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'<VAR>H : optParam (∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q') ⋯<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).liftOn f H = f p q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>a : α<VAR>f✝ f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>ha : a ∉ s<VAR>𝒜 : Finset (Finset α)<VAR>f : Finset α → β<GOAL>collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>a : α<VAR>f✝ f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t u : Finset α<VAR>ha : a ∉ s<VAR>𝒜 : Finset (Finset α)<VAR>f : Finset α → β<GOAL>∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅, f t = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : Monoid β<VAR>inst✝³ : AddGroup β<VAR>inst✝² : DistribMulAction α β<VAR>inst✝¹ : IsScalarTower α β β<VAR>inst✝ : SMulCommClass α β β<VAR>r : α<VAR>a : β<GOAL>IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>v : M<VAR>x : CliffordAlgebra Q<VAR>fx : N<GOAL>((foldr'Aux Q f) v) (((foldr'Aux Q f) v) (x, fx)) = Q v • (x, fx)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>v : M<VAR>x : CliffordAlgebra Q<VAR>fx : N<GOAL>((ι Q) v * ((ι Q) v * x), (f v) ((ι Q) v * x, (f v) (x, fx))) = Q v • (x, fx)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<GOAL>condexpIndL1 hm μ (s ∪ t) x = condexpIndL1 hm μ s x + condexpIndL1 hm μ t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<GOAL>condexpIndL1 hm μ (s ∪ t) x = condexpIndL1 hm μ s x + condexpIndL1 hm μ t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<VAR>hμst : μ (s ∪ t) ≠ ⊤<GOAL>condexpIndL1Fin hm ⋯ hμst x = condexpIndL1Fin hm hs hμs x + condexpIndL1Fin hm ht hμt x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<GOAL>∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ ↔ f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>h_le : ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ<GOAL>g =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f g : α → ℝ<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>h_le : ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ<GOAL>∫ (x : α), (g - f) x ∂μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>dist (f n) a ≤ C / 2 ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n = C / 2 ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>↑(Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = ↑(Fin.last p.length)