ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<VAR>I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<VAR>I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ<VAR>J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<VAR>I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ<VAR>J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n<VAR>P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<VAR>I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ<VAR>J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n<VAR>P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ<VAR>hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<VAR>I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ<VAR>J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n<VAR>P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ<VAR>hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1<VAR>A : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<VAR>I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ<VAR>J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n<VAR>P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ<VAR>hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1<VAR>A : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)<VAR>this : Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : MetrizableSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>φ : ℕ → α → ℝ := fun n x => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n<VAR>hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x<VAR>I : ∀ (n : ℕ), IntegrableOn (fun x => c x ^ n) s μ<VAR>J : ∀ (n : ℕ), 0 ≤ᶠ[ae (μ.restrict s)] fun x => c x ^ n<VAR>P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ<VAR>hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1<VAR>A : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)<VAR>this : Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))<VAR>x✝ : ℕ<GOAL>(∫ (x : α) in s, c x ^ x✝ ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ x✝ • g x ∂μ = ∫ (x : α) in s, φ x✝ x • g x ∂μ
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>p : Submodule R P<VAR>q : Submodule R Q<GOAL>range (mapIncl p q) = Submodule.span R (Set.image2 (fun x x_1 => x ⊗ₜ[R] x_1) ↑p ↑q)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>p : Submodule R P<VAR>q : Submodule R Q<GOAL>Submodule.span R {t | ∃ m n, p.subtype m ⊗ₜ[R] q.subtype n = t} = Submodule.span R (Set.image2 (fun x x_1 => x ⊗ₜ[R] x_1) ↑p ↑q)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hs : NullMeasurableSet s μ<GOAL>(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hs : NullMeasurableSet s μ<GOAL>μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hs : NullMeasurableSet s μ<GOAL>(μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>hs : NullMeasurableSet s μ<VAR>x : α<GOAL>x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ
<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✝ : α<VAR>inst✝¹ : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont✝ : Continuous g<VAR>inst✝ : TopologicalSpace β<VAR>U : Set α'<VAR>hU : IsOpen U<VAR>f : ↑U → β<VAR>cont : Continuous f<VAR>supp : HasCompactMulSupport f<VAR>x : α'<VAR>h : x ∈ mulTSupport (extend Subtype.val f 1)<GOAL>ContinuousAt (extend Subtype.val f 1) x
<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✝ : α<VAR>inst✝¹ : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont✝ : Continuous g<VAR>inst✝ : TopologicalSpace β<VAR>U : Set α'<VAR>hU : IsOpen U<VAR>f : ↑U → β<VAR>cont : Continuous f<VAR>supp : HasCompactMulSupport f<VAR>x : α'<VAR>h : x ∈ mulTSupport (extend Subtype.val f 1)<GOAL>ContinuousAt f ⟨x, ⋯⟩
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H✝ H : Subgroup G<VAR>h : H.Normal<VAR>f : G →* N<VAR>hf : Surjective ⇑f<GOAL>(Subgroup.map f H).Normal
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H✝ H : Subgroup G<VAR>h : H.Normal<VAR>f : G →* N<VAR>hf : Surjective ⇑f<GOAL>Subgroup.map f H.normalizer ≤ (Subgroup.map f H).normalizer
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<GOAL>(f z).re = z.re
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<GOAL>∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z✝ z : ℂ<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>x₁ x₂ : M<VAR>y₁ y₂ : ↥S<GOAL>f x₁ * ↑((IsUnit.liftRight (f.restrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.restrict S) h) y₂)⁻¹ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<GOAL>m ≤ n → s ^ m ⊆ s ^ n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<GOAL>s ^ m ⊆ s ^ m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<GOAL>∀ (n : ℕ), m ≤ n → s ^ m ⊆ s ^ n → s ^ m ⊆ s ^ (n + 1)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>hp : ¬1 < p<GOAL>pNilradical R p ≤ nilradical R
<VAR>a b c : ℤ<VAR>h : a.gcd b = 1<VAR>heq : a * b = c ^ 2<GOAL>∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
<VAR>a b c : ℤ<VAR>h : a.gcd b = 1<VAR>heq : a * b = c ^ 2<VAR>h' : IsUnit (GCDMonoid.gcd a b)<GOAL>∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
<VAR>a b c : ℤ<VAR>h : a.gcd b = 1<VAR>heq : a * b = c ^ 2<VAR>h' : IsUnit (GCDMonoid.gcd a b)<VAR>d : ℤ<VAR>u : ℤˣ<VAR>hu : d ^ 2 * ↑u = a<GOAL>∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
<VAR>a b c : ℤ<VAR>h : a.gcd b = 1<VAR>heq : a * b = c ^ 2<VAR>h' : IsUnit (GCDMonoid.gcd a b)<VAR>d : ℤ<VAR>u : ℤˣ<VAR>hu : d ^ 2 * ↑u = a<GOAL>a = d ^ 2 ∨ a = -d ^ 2
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>I J : Ideal S<GOAL>spanNorm R I * spanNorm R J ≤ spanNorm R (I * J)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>I J : Ideal S<GOAL>span (⇑(Algebra.norm R) '' (↑I * ↑J)) ≤ span (⇑(Algebra.norm R) '' ↑(I * J))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>I J : Ideal S<GOAL>↑I * ↑J ≤ ↑(I * J)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>I J : Ideal S<VAR>x : S<VAR>hxI : x ∈ ↑I<VAR>y : S<VAR>hyJ : y ∈ ↑J<GOAL>(fun x x_1 => x * x_1) x y ∈ ↑(I * J)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁷ : CommRing R₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>N : Type u_9<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>b✝ : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝² : Fintype ι'<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R (ι → R)<VAR>A : Matrix ι ι R<GOAL>b.toMatrix ⇑(Pi.basisFun R ι) * A = of fun i j => (b.repr (Aᵀ j)) i
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a b : α<VAR>S : α → α → Prop<VAR>H : ∀ (a b : α), R a b → S a b<VAR>l : List α<VAR>p : Chain' R l<GOAL>Chain' S l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>IsChain (fun x x_1 => x ≤ x_1) (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>IsChain (fun x x_1 => x ≤ x_1) (f '' univ)
<VAR>α : Type u<VAR>inst✝ : CanonicallyLinearOrderedCommMonoid α<VAR>a b c : α<GOAL>min a (b * c) = min a (min a b * min a c)
<VAR>α : Type u<VAR>inst✝ : CanonicallyLinearOrderedCommMonoid α<VAR>a b c : α<VAR>hb : a ≤ b<GOAL>min a (b * c) = min a (min a b * min a c)
<VAR>α : Type u<VAR>inst✝ : CanonicallyLinearOrderedCommMonoid α<VAR>a b c : α<VAR>hb : b ≤ a<GOAL>min a (b * c) = min a (min a b * min a c)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝² : Group N<VAR>inst✝¹ : Group P<VAR>K : Subgroup G<VAR>M : Type u_7<VAR>inst✝ : MulOneClass M<VAR>f : G →* G'<VAR>g : G' →* G''<VAR>h : g.comp f = 1<VAR>y : G<GOAL>f y ∈ g.ker
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x y z : α<VAR>s✝ s : Set α<GOAL>EMetric.diam (⇑f '' s) = ↑(ratio f) * EMetric.diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x y z : α<VAR>s✝ s : Set α<GOAL>↑(ratio f) * EMetric.diam s ≤ EMetric.diam (⇑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x y z : α<VAR>s✝ s : Set α<GOAL>EMetric.diam s ≤ EMetric.diam (⇑f '' s) / ↑(ratio f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x y z : α<VAR>s✝ s : Set α<GOAL>EMetric.diam s ≤ ↑(ratio f)⁻¹ * EMetric.diam (⇑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x y z : α<VAR>s✝ s : Set α<GOAL>ratio f ≠ 0
<VAR>n : ℕ<VAR>hn : Even n<GOAL>closure (range fun x => x ^ n) = nonneg ℤ
<VAR>n : ℕ<VAR>hn : Even n<VAR>x : ℤ<VAR>hx : x ∈ nonneg ℤ<GOAL>x ∈ closure (range fun x => x ^ n)
<VAR>n : ℕ<VAR>hn : Even n<VAR>x : ℤ<VAR>hx : x ∈ nonneg ℤ<VAR>this : x = x.natAbs • 1 ^ n<GOAL>x ∈ closure (range fun x => x ^ n)
<VAR>n : ℕ<VAR>hn : Even n<VAR>x : ℤ<VAR>hx : x ∈ nonneg ℤ<VAR>this : x = x.natAbs • 1 ^ n<GOAL>x.natAbs • 1 ^ n ∈ closure (range fun x => x ^ n)
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>hix : (of G (fun i j h => ⇑(f' i j h)) i) x = 0<VAR>this : Nonempty ι<GOAL>∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>hix : (of G (fun i j h => ⇑(f' i j h)) i) x = 0<VAR>this : Nonempty ι<VAR>j : ι<VAR>s : Set ((i : ι) × G i)<VAR>H : ∀ k ∈ s, k.fst ≤ j<VAR>hxs : (FreeCommRing.of ⟨i, x⟩).IsSupported s<VAR>hx : ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (FreeCommRing.of ⟨i, x⟩)) = 0<GOAL>∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>hix : (of G (fun i j h => ⇑(f' i j h)) i) x = 0<VAR>this : Nonempty ι<VAR>j : ι<VAR>s : Set ((i : ι) × G i)<VAR>H : ∀ k ∈ s, k.fst ≤ j<VAR>hxs : (FreeCommRing.of ⟨i, x⟩).IsSupported s<VAR>hx : ∀ [inst : DecidablePred fun x => x ∈ s], (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (FreeCommRing.of ⟨i, x⟩)) = 0<VAR>hixs : ⟨i, x⟩ ∈ s<GOAL>∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → CommRing (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f' i j h)<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>hix : (of G (fun i j h => ⇑(f' i j h)) i) x = 0<VAR>this : Nonempty ι<VAR>j : ι<VAR>s : Set ((i : ι) × G i)<VAR>H : ∀ k ∈ s, k.fst ≤ j<VAR>hxs : (FreeCommRing.of ⟨i, x⟩).IsSupported s<VAR>hixs : ⟨i, x⟩ ∈ s<VAR>hx : (lift fun ix => (f' (↑ix).fst j ⋯) (↑ix).snd) ((restriction s) (FreeCommRing.of ⟨i, x⟩)) = 0<GOAL>∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>a✝ : Nontrivial α<GOAL>Finite α
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>a✝ : Nontrivial α<VAR>x y : α<VAR>hne : x ≠ y<GOAL>Finite α
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>a✝ : Nontrivial α<VAR>x y : α<VAR>hne : x ≠ y<VAR>z : α<GOAL>z ∈ {x, y}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : b ≤ a<GOAL>[[a, b]] = Icc b a
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume ↔ -1 < s.re
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<VAR>h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume<GOAL>-1 < s.re
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<VAR>h : IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) volume<VAR>B : IntegrableOn (fun a => a ^ s.re) (Set.Ioo 0 t) volume<GOAL>-1 < s.re