ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>L0 : ℕ → E →L[𝕜] F := fun e => L e (n e) (n e)<VAR>this : CauchySeq L0<VAR>f' : E →L[𝕜] F<VAR>f'K : f' ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<VAR>Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>L0 : ℕ → E →L[𝕜] F := fun e => L e (n e) (n e)<VAR>this✝ : CauchySeq L0<VAR>f' : E →L[𝕜] F<VAR>f'K : f' ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<VAR>Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>this : HasFDerivAt f f' x<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>L0 : ℕ → E →L[𝕜] F := fun e => L e (n e) (n e)<VAR>this✝ : CauchySeq L0<VAR>f' : E →L[𝕜] F<VAR>f'K : fderiv 𝕜 f x ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<VAR>Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>this : HasFDerivAt f f' x<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>inst✝ : EssFiniteType R S<VAR>f g : S →ₐ[R] T<VAR>H : ∀ s ∈ finset R S, f s = g s<GOAL>f = g
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>inst✝ : EssFiniteType R S<VAR>f g : S →ₐ[R] T<VAR>H : ∀ s ∈ finset R S, f s = g s<GOAL>f.toRingHom = g.toRingHom
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>inst✝ : EssFiniteType R S<VAR>f g : S →ₐ[R] T<VAR>H : ∀ s ∈ finset R S, f s = g s<GOAL>f.comp (algebraMap (↥(subalgebra R S)) S) = g.comp (algebraMap (↥(subalgebra R S)) S)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>inst✝ : EssFiniteType R S<VAR>f g : S →ₐ[R] T<VAR>H : ∀ s ∈ finset R S, f s = g s<GOAL>f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S) = g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>inst✝ : EssFiniteType R S<VAR>f g : S →ₐ[R] T<VAR>H : ∀ s ∈ finset R S, f s = g s<GOAL>adjoin R {x | ↑x ∈ finset R S} = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R T<VAR>inst✝² : Algebra S T<VAR>inst✝¹ : IsScalarTower R S T<VAR>inst✝ : EssFiniteType R S<VAR>f g : S →ₐ[R] T<VAR>H : ∀ s ∈ finset R S, f s = g s<GOAL>Set.EqOn ⇑(f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) ⇑(g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) {x | ↑x ∈ finset R S}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : Computation α<VAR>a : α<VAR>h1 : a ∈ s<VAR>h2 : a ∈ t<VAR>a' : α<VAR>ma : a' ∈ s<GOAL>a' ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : Computation α<VAR>a : α<VAR>h1 : a ∈ s<VAR>h2 : a ∈ t<VAR>a' : α<VAR>ma : a' ∈ s<GOAL>a ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : Computation α<VAR>a : α<VAR>h1 : a ∈ s<VAR>h2 : a ∈ t<VAR>a' : α<VAR>ma : a' ∈ t<GOAL>a' ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : Computation α<VAR>a : α<VAR>h1 : a ∈ s<VAR>h2 : a ∈ t<VAR>a' : α<VAR>ma : a' ∈ t<GOAL>a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ s t : Set α<GOAL>𝓟 s = 𝓟 t ↔ s = t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ s t : Set α<GOAL>s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>inst✝ : (j : Fin (n + 1)) → Group (α j)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<GOAL>i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)
<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>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>f : F →SL[σ₂₃] G<VAR>g : F' ≃ₛₗᵢ[σ₂'] F<GOAL>‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖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>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>f : F →SL[σ₂₃] G<VAR>g : F' ≃ₛₗᵢ[σ₂'] F<VAR>h✝ : Subsingleton F'<GOAL>‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖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>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>f : F →SL[σ₂₃] G<VAR>g : F' ≃ₛₗᵢ[σ₂'] F<VAR>h✝ : Nontrivial F'<GOAL>‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖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>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>f : F →SL[σ₂₃] G<VAR>g : F' ≃ₛₗᵢ[σ₂'] F<VAR>h✝ : Nontrivial F'<GOAL>‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ ≤ ‖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>𝕜₂' : Type u_11<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomInvPair σ₂' σ₂''<VAR>inst✝⁶ : RingHomInvPair σ₂'' σ₂'<VAR>inst✝⁵ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁴ : RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>inst✝³ : RingHomIsometric σ₂₃<VAR>inst✝² : RingHomIsometric σ₂'<VAR>inst✝¹ : RingHomIsometric σ₂''<VAR>inst✝ : RingHomIsometric σ₂₃'<VAR>f : F →SL[σ₂₃] G<VAR>g : F' ≃ₛₗᵢ[σ₂'] F<VAR>h✝ : Nontrivial F'<GOAL>‖f‖ ≤ ‖f.comp g.toLinearIsometry.toContinuousLinearMap‖
<VAR>Ω : Type u_1<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>μ : FiniteMeasure Ω<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c<VAR>f : Ω →ᵇ ℝ≥0<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))<GOAL>Tendsto (fun i => μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>μ : FiniteMeasure Ω<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c<VAR>f : Ω →ᵇ ℝ≥0<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))<GOAL>Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂↑μ) L (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity (f * g)) s = ((μ.withDensity f).withDensity g) s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<GOAL>T R 2 = 2 * X ^ 2 - 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>xs ys : List α<VAR>ls : List (List α)<VAR>f : List α → List α<VAR>h : ∀ (x : α), x ∈ xs → ¬p x = true<GOAL>splitOnP p xs = [xs]
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>y p d z w : R<VAR>h0 : z * z * w ≠ 0<VAR>h : IsRadical (z * z * w)<GOAL>IsUnit z
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>y p d z w : R<VAR>h0 : z * z * w ≠ 0<VAR>h : z * z * w ∣ z * w<GOAL>IsUnit z
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>y p d z w : R<VAR>h0 : z * z * w ≠ 0<VAR>h : z * (z * w) ∣ 1 * (z * w)<GOAL>z * w ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>y p d z w : R<VAR>h0 : z ≠ 0 ∧ z * w ≠ 0<VAR>h : z * (z * w) ∣ 1 * (z * w)<GOAL>z * w ≠ 0
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>n.natSize = (↑n).size
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>φ : V ⥤q C<GOAL>of ⋙q (lift φ).toPrefunctor = φ
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>φ : V ⥤q C<GOAL>∀ (X : V), (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
<VAR>V : Type u₁<VAR>inst✝¹ : Quiver V<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>φ : V ⥤q C<GOAL>∀ (X Y : V) (f : X ⟶ Y), (of ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>hs : s.Nodup<GOAL>s.permutations.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>s : List α<VAR>hs : s.Nodup<GOAL>s.permutations'.Nodup
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>x : E<GOAL>x ∈ parallelepiped v ↔ ∃ t ∈ Icc 0 1, x = ∑ i : ι, t i • v i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys ≤ levenshtein C xs (y :: ys)
<VAR>n : ℕ<VAR>M : Type u_1<VAR>M₁ : Type u_2<VAR>F : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : FunLike F M M₁<VAR>inst✝⁴ : AddMonoidHomClass F M M₁<VAR>inst✝³ : Module (ZMod n) M<VAR>inst✝² : Module (ZMod n) M₁<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubgroupClass S M<VAR>x✝ : M<VAR>K : S<VAR>f : F<VAR>c : ZMod n<VAR>x : M<GOAL>f (c • x) = c • f x
<VAR>n : ℕ<VAR>M : Type u_1<VAR>M₁ : Type u_2<VAR>F : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : FunLike F M M₁<VAR>inst✝⁴ : AddMonoidHomClass F M M₁<VAR>inst✝³ : Module (ZMod n) M<VAR>inst✝² : Module (ZMod n) M₁<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubgroupClass S M<VAR>x✝ : M<VAR>K : S<VAR>f : F<VAR>c : ZMod n<VAR>x : M<GOAL>f (↑c.cast • x) = ↑c.cast • f x
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<GOAL>{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty<GOAL>Function.Injective p.index
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<GOAL>x = y
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty<VAR>x : Ordinal.{u}<VAR>hxy : p.index x = p.index x<VAR>x_le_y : x ≤ x<GOAL>x = x
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<VAR>H : x < y<GOAL>x = y
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<VAR>H : x < y<VAR>h : ∀ (x : Ordinal.{u}), ∃ x_1, p.c x_1 ∉ p.iUnionUpTo x ∧ p.R x ≤ p.τ * p.r x_1<GOAL>x = y
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<VAR>H : x < y<VAR>h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x<GOAL>x = y
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<VAR>H : x < y<VAR>h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x<VAR>A : p.c (p.index y) ∉ p.iUnionUpTo y<GOAL>x = y
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<VAR>H : x < y<VAR>h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x<VAR>A : ∀ x < y, p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))<GOAL>x = y
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<VAR>H : x < y<VAR>h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x<VAR>A : p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))<GOAL>x = y
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝ : Nonempty β<VAR>p : TauPackage β α<VAR>x y : Ordinal.{u}<VAR>hxy : p.index x = p.index y<VAR>x_le_y : x ≤ y<VAR>H : x < y<VAR>h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x<VAR>A : p.r (p.index y) ≤ 0<GOAL>x = y
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<GOAL>cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - M.M i i'))<GOAL>cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i'))<GOAL>cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i' i))<GOAL>cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonAssocRing R<VAR>a : R<GOAL>a * a - 1 = (a + 1) * (a - 1)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : (x : M) → x ∈ ⨆ i, N i → Prop<VAR>hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯<VAR>h0 : C 0 ⋯<VAR>hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, N i<GOAL>C x hx
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : (x : M) → x ∈ ⨆ i, N i → Prop<VAR>hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯<VAR>h0 : C 0 ⋯<VAR>hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, N i<GOAL>∃ (x_1 : x ∈ ⨆ i, N i), C x x_1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : (x : M) → x ∈ ⨆ i, N i → Prop<VAR>hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯<VAR>h0 : C 0 ⋯<VAR>hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ ⨆ i, N i<VAR>i : ι<VAR>x : M<VAR>hx : x ∈ N i<GOAL>(fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : (x : M) → x ∈ ⨆ i, N i → Prop<VAR>hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯<VAR>h0 : C 0 ⋯<VAR>hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, N i<GOAL>(fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) 0