ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<VAR>n₁ : ℕ<VAR>hn₁ : (f r) (↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x ∈ Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r))<GOAL>↑r ^ (n₂ + n₁) • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<VAR>n₁ : ℕ<VAR>hn₁ : (f r) (↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x ∈ Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r))<GOAL>↑r ^ (n₂ + n₁) • x ∈ Submodule.span R ↑(sf r)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<VAR>n₁ : ℕ<VAR>hn₁ : (f r) (↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x ∈ Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r))<GOAL>↑r ^ n₂ • ↑r ^ n₁ • x ∈ Submodule.span R ↑(sf r)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i✝ j : ι<VAR>a : α i✝<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<GOAL>Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i✝ j : ι<VAR>a : α i✝<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<GOAL>Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) ⊆ Sigma.mk i '' (g i ⁻¹' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i✝ j✝ : ι<VAR>a : α i✝<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<VAR>j : ι<VAR>x : α j<VAR>y : β (f i)<VAR>hys : y ∈ s<VAR>hxy : ⟨f i, y⟩ = Sigma.map f g ⟨j, x⟩<GOAL>⟨j, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i✝ j✝ : ι<VAR>a : α i✝<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<VAR>j : ι<VAR>x : α j<VAR>y : β (f i)<VAR>hys : y ∈ s<VAR>hxy : i = j ∧ HEq y (g j x)<GOAL>⟨j, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i✝ j : ι<VAR>a : α i✝<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<VAR>y : β (f i)<VAR>hys : y ∈ s<VAR>x : α i<VAR>hxy : HEq y (g i x)<GOAL>⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i✝ j : ι<VAR>a : α i✝<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<VAR>y : β (f i)<VAR>hys : y ∈ s<VAR>x : α i<VAR>hxy : y = g i x<GOAL>⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b : α<VAR>s t : Finset α<VAR>a : α<GOAL>(s \ t).erase a = s.erase a \ t.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>b : WithBot α<VAR>h : ∀ (a : α), a ∈ l → ↑a ≤ b<GOAL>l.maximum ≤ b
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>f : σ → τ<VAR>h : Injective f<VAR>i : σ<GOAL>degreeOf (f i) ((rename f) p) = degreeOf i p
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a / b = 0 ↔ a = 0 ∨ b = ⊤
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : FirstCountableTopology X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>s : Set X<VAR>inj : InjOn f s<VAR>sc : IsCompact s<VAR>fc : ∀ x ∈ s, ContinuousAt f x<VAR>loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u<VAR>this : ∀ x ∈ s ×ˢ s, ∀ᶠ (y : X × X) in 𝓝 x, f y.1 = f y.2 → y.1 = y.2<GOAL>∃ t ∈ 𝓝ˢ s, InjOn f t
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : FirstCountableTopology X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>s : Set X<VAR>inj : InjOn f s<VAR>sc : IsCompact s<VAR>fc : ∀ x ∈ s, ContinuousAt f x<VAR>loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u<VAR>this : ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2<GOAL>∃ t ∈ 𝓝ˢ s, InjOn f t
<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 : α), 0 < log (b i * ↑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<GOAL>∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑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<VAR>i : α<GOAL>∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑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<VAR>i : α<VAR>h : Tendsto (fun n => log (b i * ↑n)) atTop atTop<GOAL>∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑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✝³² : SeminormedAddCommGroup E<VAR>inst✝³¹ : SeminormedAddCommGroup Eₗ<VAR>inst✝³⁰ : SeminormedAddCommGroup F<VAR>inst✝²⁹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁸ : SeminormedAddCommGroup G<VAR>inst✝²⁷ : SeminormedAddCommGroup Gₗ<VAR>inst✝²⁶ : NontriviallyNormedField 𝕜<VAR>inst✝²⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝²³ : NormedSpace 𝕜 E<VAR>inst✝²² : NormedSpace 𝕜 Eₗ<VAR>inst✝²¹ : NormedSpace 𝕜₂ F<VAR>inst✝²⁰ : NormedSpace 𝕜 Fₗ<VAR>inst✝¹⁹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁸ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹⁶ : FunLike 𝓕 E F<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝¹⁵ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝¹⁴ : RingHomInvPair σ₂₁ σ₁₂<VAR>E' : Type u_11<VAR>F' : Type u_12<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>𝕜₁' : Type u_13<VAR>𝕜₂' : Type u_14<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₁'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>inst✝⁹ : NormedSpace 𝕜₁' E'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₁' : 𝕜₁' →+* 𝕜<VAR>σ₁₃' : 𝕜₁' →+* 𝕜₃<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'<VAR>inst✝⁶ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁵ : RingHomIsometric σ₂₃<VAR>inst✝⁴ : RingHomIsometric σ₁₃'<VAR>inst✝³ : RingHomIsometric σ₂₃'<VAR>inst✝² : RingHomIsometric σ₁₃<VAR>inst✝¹ : RingHomIsometric σ₁'<VAR>inst✝ : RingHomIsometric σ₂'<VAR>f : E →L[𝕜] Fₗ →L[𝕜] Gₗ<VAR>x x' : E<VAR>y y' : Fₗ<GOAL>(f (x + x')) (y + y') = (f x) y + (f.deriv₂ (x, y)) (x', y') + (f 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✝³² : SeminormedAddCommGroup E<VAR>inst✝³¹ : SeminormedAddCommGroup Eₗ<VAR>inst✝³⁰ : SeminormedAddCommGroup F<VAR>inst✝²⁹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁸ : SeminormedAddCommGroup G<VAR>inst✝²⁷ : SeminormedAddCommGroup Gₗ<VAR>inst✝²⁶ : NontriviallyNormedField 𝕜<VAR>inst✝²⁵ : NontriviallyNormedField 𝕜₂<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜₃<VAR>inst✝²³ : NormedSpace 𝕜 E<VAR>inst✝²² : NormedSpace 𝕜 Eₗ<VAR>inst✝²¹ : NormedSpace 𝕜₂ F<VAR>inst✝²⁰ : NormedSpace 𝕜 Fₗ<VAR>inst✝¹⁹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁸ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹⁶ : FunLike 𝓕 E F<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝¹⁵ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝¹⁴ : RingHomInvPair σ₂₁ σ₁₂<VAR>E' : Type u_11<VAR>F' : Type u_12<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>𝕜₁' : Type u_13<VAR>𝕜₂' : Type u_14<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₁'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂'<VAR>inst✝⁹ : NormedSpace 𝕜₁' E'<VAR>inst✝⁸ : NormedSpace 𝕜₂' F'<VAR>σ₁' : 𝕜₁' →+* 𝕜<VAR>σ₁₃' : 𝕜₁' →+* 𝕜₃<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>inst✝⁷ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'<VAR>inst✝⁶ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>inst✝⁵ : RingHomIsometric σ₂₃<VAR>inst✝⁴ : RingHomIsometric σ₁₃'<VAR>inst✝³ : RingHomIsometric σ₂₃'<VAR>inst✝² : RingHomIsometric σ₁₃<VAR>inst✝¹ : RingHomIsometric σ₁'<VAR>inst✝ : RingHomIsometric σ₂'<VAR>f : E →L[𝕜] Fₗ →L[𝕜] Gₗ<VAR>x x' : E<VAR>y y' : Fₗ<GOAL>(f x) y + ((f x') y + ((f x) y' + (f x') y')) = (f x) y + ((f x) y' + ((f x') y + (f x') y'))
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>M : Matrix n n R<GOAL>(toMatrixAlgEquiv v₁) ((toLinAlgEquiv v₁) M) = M
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>h0 : τ ≠ 0<GOAL>∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>h0 : τ ≠ 0<VAR>h2 : 0 < (-I * τ).re<GOAL>∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))
<VAR>a b c x : ℕ<GOAL>x ∈ Icc a.succ b ↔ x ∈ Ioc a b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atBot<GOAL>Tendsto (fun x => f x • r) l atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Tendsto (fun x => -f x) l atTop<GOAL>Tendsto (fun x => -f x • r) l atTop
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : DecidableEq J<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>j j' : J<GOAL>ι f j ≫ π f j' = if h : j = j' then eqToHom ⋯ else 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<GOAL>(A.submatrix ⇑e ⇑e).det = A.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<GOAL>∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ∑ σ : Perm m, ↑↑(sign σ) * ∏ i : m, A (σ i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<GOAL>∀ (x : Perm n), ↑↑(sign x) * ∏ i : n, A.submatrix (⇑e) (⇑e) (x i) i = ↑↑(sign (e.permCongr x)) * ∏ i : m, A ((e.permCongr x) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<VAR>σ : Perm n<GOAL>↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ↑↑(sign (e.permCongr σ)) * ∏ i : m, A ((e.permCongr σ) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<VAR>σ : Perm n<GOAL>↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ↑↑(sign σ) * ∏ i : m, A ((e.permCongr σ) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<VAR>σ : Perm n<GOAL>∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ∏ i : m, A ((e.permCongr σ) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<VAR>σ : Perm n<GOAL>∀ (x : n), A.submatrix (⇑e) (⇑e) (σ x) x = A ((e.permCongr σ) (e x)) (e x)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>e : n ≃ m<VAR>A : Matrix m m R<VAR>σ : Perm n<VAR>i : n<GOAL>A.submatrix (⇑e) (⇑e) (σ i) i = A ((e.permCongr σ) (e i)) (e i)
<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<GOAL>IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → s ∈ l
<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>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)<GOAL>Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f 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>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)<GOAL>Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
<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>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)<GOAL>Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>(∀ i ∈ s, Prime (f i)) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>(∀ i ∈ ∅, Prime (f i)) → (∀ i ∈ ∅, ∀ j ∈ ∅, i ≠ j → f i ≠ f j) → (∅.inf fun i => f i ^ e i) = ∏ i ∈ ∅, f i ^ e i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → ((∀ i ∈ s, Prime (f i)) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i) → (∀ i ∈ insert a s, Prime (f i)) → (∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j) → ((insert a s).inf fun i => f i ^ e i) = ∏ i ∈ insert a s, f i ^ e i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>ih : (∀ i ∈ s, Prime (f i)) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<GOAL>((insert a s).inf fun i => f i ^ e i) = ∏ i ∈ insert a s, f i ^ e i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<GOAL>((insert a s).inf fun i => f i ^ e i) = ∏ i ∈ insert a s, f i ^ e i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<GOAL>f a ^ e a ⊓ ∏ i ∈ s, f i ^ e i = f a ^ e a * ∏ x ∈ s, f x ^ e x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<GOAL>∀ (P : Ideal R), f a ^ e a ≤ P → ∏ x ∈ s, f x ^ e x ≤ P → ¬P.IsPrime