ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<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>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>fs gs : ℕ → α → F'<VAR>f g : α → F'<VAR>hfs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>hgs_int : ∀ (n : ℕ), Integrable (gs n) μ<VAR>hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))<VAR>hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))<VAR>bound_fs : α → ℝ<VAR>h_int_bound_fs : Integrable bound_fs μ<VAR>bound_gs : α → ℝ<VAR>h_int_bound_gs : Integrable bound_gs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x<VAR>hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>condexpL1 hm μ g = condexpL1 hm μ f
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<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>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>fs gs : ℕ → α → F'<VAR>f g : α → F'<VAR>hfs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>hgs_int : ∀ (n : ℕ), Integrable (gs n) μ<VAR>hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))<VAR>hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))<VAR>bound_fs : α → ℝ<VAR>h_int_bound_fs : Integrable bound_fs μ<VAR>bound_gs : α → ℝ<VAR>h_int_bound_gs : Integrable bound_gs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x<VAR>hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>hn_eq : ∀ (n : ℕ), condexpL1 hm μ (gs n) = condexpL1 hm μ (fs n)<GOAL>condexpL1 hm μ g = condexpL1 hm μ f
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<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>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>fs gs : ℕ → α → F'<VAR>f g : α → F'<VAR>hfs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>hgs_int : ∀ (n : ℕ), Integrable (gs n) μ<VAR>hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))<VAR>hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))<VAR>bound_fs : α → ℝ<VAR>h_int_bound_fs : Integrable bound_fs μ<VAR>bound_gs : α → ℝ<VAR>h_int_bound_gs : Integrable bound_gs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x<VAR>hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>hn_eq : ∀ (n : ℕ), condexpL1 hm μ (gs n) = condexpL1 hm μ (fs n)<VAR>hcond_fs : Tendsto (fun n => condexpL1 hm μ (fs n)) atTop (𝓝 (condexpL1 hm μ f))<GOAL>condexpL1 hm μ g = condexpL1 hm μ f
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<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>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>fs gs : ℕ → α → F'<VAR>f g : α → F'<VAR>hfs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>hgs_int : ∀ (n : ℕ), Integrable (gs n) μ<VAR>hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))<VAR>hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))<VAR>bound_fs : α → ℝ<VAR>h_int_bound_fs : Integrable bound_fs μ<VAR>bound_gs : α → ℝ<VAR>h_int_bound_gs : Integrable bound_gs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x<VAR>hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>hn_eq : ∀ (n : ℕ), condexpL1 hm μ (gs n) = condexpL1 hm μ (fs n)<VAR>hcond_fs : Tendsto (fun n => condexpL1 hm μ (fs n)) atTop (𝓝 (condexpL1 hm μ f))<VAR>hcond_gs : Tendsto (fun n => condexpL1 hm μ (gs n)) atTop (𝓝 (condexpL1 hm μ g))<GOAL>condexpL1 hm μ g = condexpL1 hm μ f
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : MulZeroOneClass M₀<VAR>s t : Set ι<VAR>i : ι<VAR>inst✝ : Nontrivial M₀<GOAL>s.indicator 1 i = 0 ↔ i ∉ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>(↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>h₁ : derivative (T R (n + 2)) = derivative (X * T R (n + 1) - (1 - X ^ 2) * U R n)<GOAL>(↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>h₁ : ↑(n + 2) * U R (n + 2 - 1) = 1 * T R (n + 1) + X * (↑(n + 1) * U R (n + 1 - 1)) - ((0 - ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * derivative (U R n))<GOAL>(↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>h₁ : ↑(n + 2) * U R (n + 2 - 1) = 1 * T R (n + 1) + X * (↑(n + 1) * U R (n + 1 - 1)) - ((0 - ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * derivative (U R n))<VAR>h₂ : T R (n + 1) = U R (n + 1) - X * U R (n + 1 - 1)<GOAL>(↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * derivative (U R n)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>χ : DirichletCharacter R 1<VAR>x✝ : ℕ<GOAL>χ ↑x✝ = 1 x✝
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : x ≤ 1<VAR>n : ℕ<GOAL>x ^ (n + 1) ≤ 1
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : x ≤ 1<VAR>n : ℕ<GOAL>x ^ n * x ≤ 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → Prop<VAR>u : ℕ → ℕ<VAR>hu : ∀ (N : ℕ), u N > N<VAR>hu' : ∀ (N : ℕ), P (u N)<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → Prop<VAR>u : ℕ → ℕ<VAR>hu : ∀ (N : ℕ), u N > N<VAR>hu' : ∀ (N : ℕ), P (u N)<VAR>n : ℕ<GOAL>u^[n + 1] 0 < u^[n + 1 + 1] 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>P : ℕ → Prop<VAR>u : ℕ → ℕ<VAR>hu : ∀ (N : ℕ), u N > N<VAR>hu' : ∀ (N : ℕ), P (u N)<VAR>n : ℕ<GOAL>P ((fun n => u^[n + 1] 0) n)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s✝ t : Set G<VAR>ht : IsOpen t<VAR>s : Set G<GOAL>closure s / t = s / t
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace α'<VAR>inst✝² : One β<VAR>inst✝¹ : One γ<VAR>inst✝ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<GOAL>HasCompactMulSupport f ↔ IsCompact (closure (mulSupport f))
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r : X<VAR>s : ↥S<GOAL>1 • (r /ₒ s) = r /ₒ s
<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>term n 1 = log (↑n + 1) - log ↑n - 1 / (↑n + 1)
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x<GOAL>term n 1 = log (↑n + 1) - log ↑n - 1 / (↑n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<GOAL>a ∈ sᶜ ↔ a ∉ s
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>p ^ m ∣ x.appr n - x.appr m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m k : ℕ<VAR>h : m ≤ m + k<GOAL>p ^ m ∣ x.appr (m + k) - x.appr m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m k : ℕ<VAR>ih : p ^ m ∣ x.appr (m + k) - x.appr m<GOAL>p ^ m ∣ x.appr (m + (k + 1)) - x.appr m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m k : ℕ<VAR>ih : p ^ m ∣ x.appr (m + k) - x.appr m<GOAL>p ^ m ∣ x.appr (m + k + 1) - x.appr m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m k : ℕ<VAR>ih : p ^ m ∣ x.appr (m + k) - x.appr m<VAR>h : ¬x - ↑(x.appr (m + k)) = 0<GOAL>p ^ m ∣ x.appr (m + k) + p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ ((x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val - x.appr m
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m k : ℕ<VAR>ih : p ^ m ∣ x.appr (m + k) - x.appr m<VAR>h : ¬x - ↑(x.appr (m + k)) = 0<GOAL>p ^ m ∣ p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ ((x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val + (x.appr (m + k) - x.appr m)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m k : ℕ<VAR>ih : p ^ m ∣ x.appr (m + k) - x.appr m<VAR>h : ¬x - ↑(x.appr (m + k)) = 0<GOAL>p ^ m ∣ p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ ((x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>m k : ℕ<VAR>ih : p ^ m ∣ x.appr (m + k) - x.appr m<VAR>h : ¬x - ↑(x.appr (m + k)) = 0<GOAL>p ^ m ∣ p ^ (m + k)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s✝ s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (f i)<VAR>hfin : ∃ i, μ (f i) ≠ ⊤<VAR>s : ι → Set α := fun i => ⋂ j, ⋂ (_ : j ≤ i), f j<VAR>iInter_eq : ⋂ i, f i = ⋂ i, s i<GOAL>μ (⋂ i, f i) = ⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s✝ s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (f i)<VAR>hfin : ∃ i, μ (f i) ≠ ⊤<VAR>s : ι → Set α := fun i => ⋂ j, ⋂ (_ : j ≤ i), f j<VAR>iInter_eq : ⋂ i, f i = ⋂ i, s i<VAR>ms : ∀ (i : ι), MeasurableSet (s i)<GOAL>μ (⋂ i, f i) = ⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s✝ s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (f i)<VAR>hfin : ∃ i, μ (f i) ≠ ⊤<VAR>s : ι → Set α := fun i => ⋂ j, ⋂ (_ : j ≤ i), f j<VAR>iInter_eq : ⋂ i, f i = ⋂ i, s i<VAR>ms : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Directed (fun x x_1 => x ⊇ x_1) s<VAR>hfin' : ∃ i, μ (s i) ≠ ⊤<GOAL>μ (⋂ i, f i) = ⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b : α<VAR>inst✝ : IsDirected α fun x x_1 => x ≥ x_1<VAR>s : Set α<VAR>a : α<GOAL>BddBelow (insert a s) ↔ BddBelow s
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace B<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>inst✝ : Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : E b<GOAL>(Pretrivialization.symmₗ R e b) ((Pretrivialization.linearMapAt R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace B<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>inst✝ : Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : E b<GOAL>(Pretrivialization.symmₗ R e b) (↑(linearEquivAt R e b hb) y) = y
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctor C (a + 0)).obj X = (shiftFunctor C a).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd C a 0).hom.app X = eqToHom ⋯ ≫ (shiftFunctorZero C A).inv.app ((shiftFunctor C a).obj X)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>B : Matrix m n α<GOAL>‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : NonUnitalSeminormedRing α<VAR>A : Matrix l m α<VAR>B : Matrix m n α<GOAL>(Finset.univ.sup fun i => ∑ x : n, ‖∑ j : m, A i j * B j x‖₊) ≤ (Finset.univ.sup fun i => ∑ j : m, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j : n, ‖B i j‖₊
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Monoid M<VAR>S : Finset (MonoidAlgebra R M)<VAR>hS : adjoin R ↑S = ⊤<VAR>this : DecidableEq M := Classical.decEq M<GOAL>∃ G, adjoin R (⇑(of R M) '' ↑G) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Monoid M<VAR>S : Finset (MonoidAlgebra R M)<VAR>hS : adjoin R ↑S = ⊤<VAR>this : DecidableEq M := Classical.decEq M<GOAL>adjoin R (⇑(of R M) '' ↑(S.biUnion fun f => f.support)) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Monoid M<VAR>S : Finset (MonoidAlgebra R M)<VAR>hS : adjoin R ↑S = ⊤<VAR>this✝ : DecidableEq M := Classical.decEq M<VAR>this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support<GOAL>adjoin R (⇑(of R M) '' ↑(S.biUnion fun f => f.support)) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Monoid M<VAR>S : Finset (MonoidAlgebra R M)<VAR>hS : adjoin R ↑S = ⊤<VAR>this✝ : DecidableEq M := Classical.decEq M<VAR>this : ↑(S.biUnion fun f => f.support) = ⋃ f ∈ S, ↑f.support<GOAL>adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.support) = ⊤
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ : α → G<VAR>s✝ : Set α<VAR>x : α<VAR>inst✝² : Group H<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : TopologicalGroup H<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>hf' : DenseRange ⇑f<VAR>s : Subgroup G<VAR>hs : s.topologicalClosure = ⊤<GOAL>(Subgroup.map f s).topologicalClosure = ⊤
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ : α → G<VAR>s✝ : Set α<VAR>x : α<VAR>inst✝² : Group H<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : TopologicalGroup H<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>hf' : DenseRange ⇑f<VAR>s : Subgroup G<VAR>hs : ↑s.topologicalClosure = ↑⊤<GOAL>↑(Subgroup.map f s).topologicalClosure = ↑⊤
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ : α → G<VAR>s✝ : Set α<VAR>x : α<VAR>inst✝² : Group H<VAR>inst✝¹ : TopologicalSpace H<VAR>inst✝ : TopologicalGroup H<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>hf' : DenseRange ⇑f<VAR>s : Subgroup G<VAR>hs : Dense ↑s<GOAL>Dense ↑(Subgroup.map f s)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)<VAR>p : ℕ<VAR>p_pos : p > 0<VAR>hp_mixedChar : MixedCharZero R p<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)<VAR>p : ℕ<VAR>p_pos : p > 0<VAR>hp_mixedChar : MixedCharZero R p<VAR>I : Ideal R<VAR>hI_ne_top : I ≠ ⊤<VAR>hI_p : CharP (R ⧸ I) p<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)<VAR>p : ℕ<VAR>p_pos : p > 0<VAR>hp_mixedChar : MixedCharZero R p<VAR>I : Ideal R<VAR>hI_ne_top : I ≠ ⊤<VAR>hI_p : CharP (R ⧸ I) p<VAR>hI_zero : CharP (R ⧸ I) 0<GOAL>False
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : DecidableEq σ<VAR>n : σ →₀ ℕ<VAR>a : R<VAR>φ : MvPowerSeries σ R<GOAL>inv.aux a φ n = if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>n : σ →₀ ℕ<VAR>a : R<VAR>φ : MvPowerSeries σ R<GOAL>inv.aux a φ n = if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{?u.29669, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.29676, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.29683, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>a : M<VAR>ha : a = 0<VAR>d : M<VAR>h : ShiftedHom Z T d<GOAL>d + a = d
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.29676, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.29683, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>d : M<VAR>h : ShiftedHom Z T d<GOAL>(mk₀ 0 ⋯ f).comp ((mk₀ 0 ⋯ g).comp h ⋯) ⋯ = (mk₀ 0 ⋯ (f ≫ g)).comp h ⋯
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.29676, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.29683, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>d : M<VAR>h : ShiftedHom Z T d<GOAL>0 + 0 = 0
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.29676, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.29683, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>d : M<VAR>h : ShiftedHom Z T d<GOAL>d + 0 + 0 = d
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>HasFTaylorSeriesUpTo (↑(n + 1)) f p ↔ (∀ (x : E), (p x 0).uncurry0 = f x) ∧ (∀ (x : E), HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧ HasFTaylorSeriesUpTo (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) fun x => (p x).shift
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hs_mem : t ∈ hC.diffFinset hs ht<GOAL>False
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hs_mem : t ∈ hC.diffFinset hs ht<GOAL>t ⊆ s \ t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hs_mem : t ∈ hC.diffFinset hs ht<GOAL>t ⊆ ⋃₀ ↑(hC.diffFinset hs ht)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>ι : Sort u_1<VAR>S : ι → Subalgebra R A<VAR>x : A<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<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 : Finset α<VAR>a b : α<GOAL>↑s = {a, b} ↔ s = {a, b}
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<GOAL>QuotientMeasureEqMeasurePreimage ν (c • haarMeasure K)
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<VAR>c_ne_top : c ≠ ⊤<GOAL>QuotientMeasureEqMeasurePreimage ν (c • haarMeasure K)
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ✝ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<VAR>c_ne_top : c ≠ ⊤<VAR>μ : Measure (G ⧸ Γ) := c • haarMeasure K<GOAL>QuotientMeasureEqMeasurePreimage ν μ