ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>n : ℕ<GOAL>n ∈ Finset.filter IsPrimePow (a * b).divisors ↔ n ∈ Finset.filter IsPrimePow (a.divisors ∪ b.divisors)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>n : ℕ<GOAL>IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>M : Type w₁<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L₁<VAR>inst✝⁶ : LieAlgebra R L₁<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : LieRingModule L₂ M<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : LieModule R L₂ M<VAR>t : R<VAR>x : L₁<VAR>m : M<GOAL>⁅t • x, m⁆ = t • ⁅x, m⁆
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>M : Type w₁<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L₁<VAR>inst✝⁶ : LieAlgebra R L₁<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : LieRingModule L₂ M<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : LieModule R L₂ M<VAR>t : R<VAR>x : L₁<VAR>m : M<GOAL>⁅x, t • m⁆ = t • ⁅x, m⁆
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>i : Arrow T<VAR>X Y : T<VAR>p : X ≅ Y<VAR>sq : i ⟶ mk p.hom<GOAL>i.hom ≫ sq.right ≫ p.inv = sq.left
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>m : M<VAR>i : ℕ<VAR>a : R<VAR>a_in : a ∈ ↑(I ^ i • ⊤)<GOAL>a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>m : M<VAR>i : ℕ<VAR>a : R<VAR>a_in : a ∈ I ^ i<GOAL>a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>h : (x, y) ∈ f.graph<GOAL>x ∈ f.domain
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>h : (x, y) ∈ f.graph<GOAL>∃ y, (x, y) ∈ f.graph
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖2 • z + y‖ * ‖2 • z + y‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>a✝ : StrongEpi f<GOAL>StrongEpi g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>a✝ : StrongEpi g<GOAL>StrongEpi f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup Fₗ<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>inst✝¹ : NormedSpace 𝕜₃ G<VAR>inst✝ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c<GOAL>∃ C, ∀ (z : E), ‖f z‖ ≤ C * ‖z‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup Fₗ<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>inst✝¹ : NormedSpace 𝕜₃ G<VAR>inst✝ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c<VAR>k : 𝕜<VAR>hk : 1 < ‖k‖<GOAL>∃ C, ∀ (z : E), ‖f z‖ ≤ C * ‖z‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup Fₗ<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>inst✝¹ : NormedSpace 𝕜₃ G<VAR>inst✝ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c<VAR>k : 𝕜<VAR>hk : 1 < ‖k‖<GOAL>∀ (z : E), ‖f z‖ ≤ c * (‖k‖ / r) * ‖z‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup Fₗ<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>inst✝¹ : NormedSpace 𝕜₃ G<VAR>inst✝ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x y z✝ : E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c<VAR>k : 𝕜<VAR>hk : 1 < ‖k‖<VAR>z : E<GOAL>‖f z‖ ≤ c * (‖k‖ / r) * ‖z‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup Fₗ<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>inst✝¹ : NormedSpace 𝕜₃ G<VAR>inst✝ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z✝ : E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c<VAR>k : 𝕜<VAR>hk : 1 < ‖k‖<VAR>z x : E<VAR>hko : r / ‖k‖ ≤ ‖x‖<VAR>hxo : ‖x‖ < r<GOAL>‖f x‖ ≤ c * (‖k‖ / r) * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup Fₗ<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>inst✝¹ : NormedSpace 𝕜₃ G<VAR>inst✝ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z✝ : E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c<VAR>k : 𝕜<VAR>hk : 1 < ‖k‖<VAR>z x : E<VAR>hko : r / ‖k‖ ≤ ‖x‖<VAR>hxo : ‖x‖ < r<GOAL>0 ≤ c
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup Fₗ<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>inst✝¹ : NormedSpace 𝕜₃ G<VAR>inst✝ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z✝ : E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c<VAR>k : 𝕜<VAR>hk : 1 < ‖k‖<VAR>z x : E<VAR>hko : r / ‖k‖ ≤ ‖x‖<VAR>hxo : ‖x‖ < r<GOAL>1 ≤ ‖x‖ * ‖k‖ / r
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Monoid M<VAR>x : Mˣ<VAR>u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)<GOAL>↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Monoid M<VAR>x : Mˣ<VAR>u : ↥(MulAction.stabilizer (ConjAct Mˣ) x)<VAR>this : ↑u • x = x<GOAL>↑x * ↑(ConjAct.ofConjAct ↑u) = ↑(ConjAct.ofConjAct ↑u) * ↑x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Monoid M<VAR>x : Mˣ<VAR>u : (↥(Submonoid.centralizer {↑x}))ˣ<GOAL>ConjAct.toConjAct ((Units.map (Submonoid.centralizer {↑x}).subtype) u) • x = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Monoid M<VAR>x : Mˣ<VAR>u : (↥(Submonoid.centralizer {↑x}))ˣ<GOAL>(Units.map (Submonoid.centralizer {↑x}).subtype) u * x = x * (Units.map (Submonoid.centralizer {↑x}).subtype) u
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(x - y) * ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) = x ^ n - x ^ m * y ^ (n - m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))<GOAL>(x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) = x ^ n - x ^ m * y ^ (n - m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))<GOAL>(x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) = x ^ n - x ^ m * y ^ (n - m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))<GOAL>(x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) = x ^ n - x ^ m * y ^ (n - m)
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))<GOAL>(x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v✝ : V<VAR>f : V → W<VAR>inst✝ : Subsingleton V<VAR>v w : V<GOAL>G.Adj v w → (SimpleGraph.comap f G').Adj v w
<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : Set ↑Γ(X, U)<VAR>hs : Ideal.span s = ⊤<GOAL>⨆ i ∈ s, X.basicOpen i = U
<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : Set ↑Γ(X, U)<VAR>hs : Ideal.span s = ⊤<GOAL>⨆ i ∈ s, X.basicOpen i ≤ U
<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : Set ↑Γ(X, U)<VAR>hs : Ideal.span s = ⊤<GOAL>U ≤ ⨆ i ∈ s, X.basicOpen i
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a * (b * a⁻¹) = b
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Ioi a ↔ x ∈ Ioi (r • a)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y, a < y ∧ r * y = x) ↔ r * a < x
<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 : γ<GOAL>⋃ x ∈ ↑t, (fun a => f a x) '' ↑s = image2 f ↑s ↑t
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Ring R<VAR>n : ℤ<GOAL>derivative ↑n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Ring R<VAR>n : ℤ<GOAL>derivative (C ↑n) = 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<GOAL>e ∈ ⋃ φ, ⋃ U, ⋃ (hU : IsOpen U), ⋃ (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) U), ⋃ (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) U), {e | e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU ⋯ ⋯)} ↔ ∃ φ U, ∃ (hU : IsOpen U) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) U) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) U), e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU ⋯ ⋯)
<VAR>C : Type u_5<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_5} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_3<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>X : C<GOAL>(zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)
<VAR>C : Type u_5<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_5} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_3<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>X : C<VAR>h : whiskerLeft F (zero F s i).hom = (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom<GOAL>(zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<GOAL>∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<VAR>h₁ : x⁻¹ ≠ 1<GOAL>∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<VAR>h₁ : x⁻¹ ≠ 1<VAR>h₂ : x⁻¹ - 1 ≠ 0<GOAL>∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<VAR>h₁ : x⁻¹ ≠ 1<VAR>h₂ : x⁻¹ - 1 ≠ 0<VAR>h₃ : x - 1 ≠ 0<GOAL>∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<VAR>h₁ : x⁻¹ ≠ 1<VAR>h₂ : x⁻¹ - 1 ≠ 0<VAR>h₃ : x - 1 ≠ 0<VAR>h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x<GOAL>∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<VAR>h₁ : x⁻¹ ≠ 1<VAR>h₂ : x⁻¹ - 1 ≠ 0<VAR>h₃ : x - 1 ≠ 0<VAR>h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x<GOAL>1 * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = (x - 1) * (x⁻¹ ^ n - 1)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<VAR>h₁ : x⁻¹ ≠ 1<VAR>h₂ : x⁻¹ - 1 ≠ 0<VAR>h₃ : x - 1 ≠ 0<VAR>h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x<GOAL>(x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>Q : Fin 3 → R<VAR>u : Rˣ<GOAL>W.Nonsingular ((fun m => m • Q) u) ↔ W.Nonsingular Q
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : ℕ → α<VAR>l : Filter α<VAR>k : ℕ<GOAL>Tendsto (f ∘ fun n => n + k) atTop l ↔ Tendsto f atTop l
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<GOAL>(∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<VAR>this : (∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i)) * (x - 1) = x ^ n - 1 ^ n<GOAL>(∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<VAR>this : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1<GOAL>(∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
<VAR>s : ℕ<VAR>h : s ≠ 0<GOAL>(s.xgcdAux 1 0 0 0 1).2.1 = 1
<VAR>s : ℕ<VAR>h : s.succ ≠ 0<GOAL>(s.succ.xgcdAux 1 0 0 0 1).2.1 = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T1Space Y<VAR>f : X → Y<VAR>x : X<VAR>y : Y<VAR>h : Tendsto f (𝓝 x) (𝓝 y)<GOAL>ContinuousAt f x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), r i n < n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : R.n₀ ≤ n<GOAL>∀ (i : α), r i n < n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<VAR>P : Set X → Prop<VAR>hP : ∀ (s t : Set X), s ⊆ t → P s → P t<GOAL>(∀ (i : Set X), x ∈ i ∧ IsOpen i → P i) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → P s
<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<GOAL>∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>u v : Fin n<GOAL>u ⋖ v ∨ v ⋖ u ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
<VAR>n : ℕ<GOAL>0 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 0
<VAR>n : ℕ<GOAL>1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1
<VAR>n✝ n : ℕ<VAR>a : ℕ := n + 2<GOAL>n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
<VAR>n✝ n : ℕ<VAR>a : ℕ := n + 2<VAR>ha : a ≠ 1 := succ_succ_ne_one n<GOAL>n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
<VAR>n✝ n : ℕ<VAR>a : ℕ := n + 2<VAR>ha : a ≠ 1 := succ_succ_ne_one n<GOAL>∃ p, Prime p ∧ p ∣ n + 2
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>(v.onQuot ⋯).supp = 0
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>Ideal.map (Ideal.Quotient.mk v.supp) v.supp = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>i j : ℕ<GOAL>∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>r : R<VAR>n : ℕ<GOAL>∃ j, r • I ^ j ≤ I ^ n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>r : R<VAR>n : ℕ<GOAL>r • I ^ n ≤ I ^ n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>r : R<VAR>n : ℕ<VAR>x : R<VAR>hx : x ∈ ↑(I ^ n)<GOAL>(DistribMulAction.toLinearMap R R r) x ∈ I ^ n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>n : ℕ<GOAL>∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ n)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>n : ℕ<GOAL>↑(I ^ n) * ↑(I ^ n) ⊆ ↑(I ^ n)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>n : ℕ<VAR>x : R<VAR>_hx : x ∈ ↑(I ^ n)<VAR>b : R<VAR>hb : b ∈ ↑(I ^ n)<GOAL>(fun x x_1 => x * x_1) x b ∈ ↑(I ^ n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.217769, u_2} D<VAR>inst✝¹ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>J : C<VAR>f : S.X₂ ⟶ J<VAR>inst✝ : Injective J<VAR>hf : S.f ≫ f = 0<GOAL>S.g ≫ hS.descToInjective f hf = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.217769, u_2} D<VAR>inst✝¹ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>J : C<VAR>f : S.X₂ ⟶ J<VAR>inst✝ : Injective J<VAR>hf : S.f ≫ f = 0<VAR>this : Mono S.fromOpcycles<GOAL>S.g ≫ hS.descToInjective f hf = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.217769, u_2} D<VAR>inst✝¹ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>J : C<VAR>f : S.X₂ ⟶ J<VAR>inst✝ : Injective J<VAR>hf : S.f ≫ f = 0<VAR>this : Mono S.fromOpcycles<GOAL>S.g ≫ Injective.factorThru (S.descOpcycles f hf) S.fromOpcycles = f
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>S ∈ rightTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>(∀ (g : G), ∃! s, Quotient.mk'' ↑s = Quotient.mk'' g) ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>α : Type u<VAR>β : Type v<VAR>f fa g : α → α<VAR>x y : α<VAR>fb : β → β<VAR>m n k : ℕ<VAR>e : Perm α<VAR>h : Function.Commute f g<GOAL>Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<VAR>r : ℝ<VAR>w : α<VAR>hw : 1 < ‖w‖<VAR>n : ℕ<VAR>hn : r < ‖w‖ ^ n<GOAL>r < ‖w ^ n‖