ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : ↑r < p.radius<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>H : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<GOAL>∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>a b : E<GOAL>⟪a, b⟫_ℝ ^ 2 + (o.areaForm a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>s : Set α<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>s : Set α<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<VAR>this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>s : Set α<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<VAR>this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x<VAR>t : Set ↑s<VAR>htc : t.Countable<VAR>htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>s : Set α<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<VAR>this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x<VAR>t : Set ↑s<VAR>htc : t.Countable<VAR>htU : ⋃ x ∈ t, Subtype.val ⁻¹' f ↑x = univ<VAR>x : α<VAR>hx : x ∈ s<GOAL>x ∈ ⋃ x ∈ Subtype.val '' t, f x
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>s : Set α<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<VAR>this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x<VAR>t : Set ↑s<VAR>htc : t.Countable<VAR>x : α<VAR>hx : x ∈ s<VAR>htU : ∀ (x : ↑s), ↑x ∈ ⋃ i ∈ t, f ↑i<GOAL>x ∈ ⋃ y ∈ t, f ↑y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<GOAL>∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<GOAL>∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<GOAL>∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<GOAL>StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<GOAL>StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<VAR>hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k<GOAL>StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<VAR>hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k<VAR>s : Set α := limsup S atTop<VAR>hs : s = limsup S atTop<GOAL>StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<VAR>hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k<VAR>s : Set α := limsup S atTop<VAR>hs : s = limsup S atTop<VAR>hμs : μ s = 0<GOAL>StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<VAR>hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k<VAR>s : Set α := limsup S atTop<VAR>hs : s = limsup S atTop<VAR>hμs : μ s = 0<VAR>h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))<GOAL>StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<VAR>hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k<VAR>s : Set α := limsup S atTop<VAR>hs : s = limsup S atTop<VAR>hμs : μ s = 0<VAR>h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))<GOAL>StrictMono ns ∧ μ {a | ¬Tendsto (fun i => f (ns i) a) atTop (𝓝 (g a))} = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<VAR>hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k<VAR>s : Set α := limsup S atTop<VAR>hs : s = limsup S atTop<VAR>hμs : μ s = 0<VAR>h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))<VAR>x : α<GOAL>x ∈ {a | ¬Tendsto (fun i => f (ns i) a) atTop (𝓝 (g a))} → x ∈ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>h_lt_ε_real : ∀ (ε : ℝ), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε<VAR>ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg<VAR>S : ℕ → Set α := fun k => {x | 2⁻¹ ^ k ≤ dist (f (ns k) x) (g x)}<VAR>hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k<VAR>s : Set α := limsup S atTop<VAR>hs : s = limsup S atTop<VAR>hμs : μ s = 0<VAR>h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))<VAR>x : α<GOAL>x ∉ s → Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = arctan b - arctan a
<VAR>a b c d d' : List Γ'<GOAL>update (elim a b c d) stack d' = elim a b c d'
<VAR>a b c d d' : List Γ'<VAR>x : K'<GOAL>update (elim a b c d) stack d' x = elim a b c d' x
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>f : α → P.M<VAR>hyp : ∀ (x : α), (f x).dest = P.map f (g x)<VAR>x : α<GOAL>f x = M.corec g x
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>f : α → P.M<VAR>hyp : ∀ (x : α), (f x).dest = P.map f (g x)<VAR>x : α<GOAL>∀ (x : α), (fun x => True) x → ∃ a f_1 f', (f x).dest = ⟨a, f_1⟩ ∧ (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>f : α → P.M<VAR>hyp : ∀ (x : α), (f x).dest = P.map f (g x)<VAR>x : α<VAR>a✝ : True<VAR>a : P.A<VAR>f' : P.B a → α<VAR>gxeq : g x = ⟨a, f'⟩<GOAL>∃ a f_1 f', (f x).dest = ⟨a, f_1⟩ ∧ (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>f : α → P.M<VAR>hyp : ∀ (x : α), (f x).dest = P.map f (g x)<VAR>x : α<VAR>a✝ : True<VAR>a : P.A<VAR>f' : P.B a → α<VAR>gxeq : g x = ⟨a, f'⟩<VAR>h₀ : (f x).dest = ⟨a, f ∘ f'⟩<GOAL>∃ a f_1 f', (f x).dest = ⟨a, f_1⟩ ∧ (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>f : α → P.M<VAR>hyp : ∀ (x : α), (f x).dest = P.map f (g x)<VAR>x : α<VAR>a✝ : True<VAR>a : P.A<VAR>f' : P.B a → α<VAR>gxeq : g x = ⟨a, f'⟩<VAR>h₀ : (f x).dest = ⟨a, f ∘ f'⟩<VAR>h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩<GOAL>∃ a f_1 f', (f x).dest = ⟨a, f_1⟩ ∧ (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>f : α → P.M<VAR>hyp : ∀ (x : α), (f x).dest = P.map f (g x)<VAR>x : α<VAR>a✝ : True<VAR>a : P.A<VAR>f' : P.B a → α<VAR>gxeq : g x = ⟨a, f'⟩<VAR>h₀ : (f x).dest = ⟨a, f ∘ f'⟩<VAR>h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩<VAR>i : P.B a<GOAL>∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>add' W (neg' W f) f = L.map 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>α : W.LeftFraction X Y<GOAL>add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>α : W.LeftFraction X Y<VAR>this : IsIso (L.map α.s)<GOAL>add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>α : W.LeftFraction X Y<VAR>this : IsIso (L.map α.s)<GOAL>(LeftFraction₂.mk (-α.f) α.f α.s ⋯).add.map L ⋯ = L.map 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>Polynomial.derivative (bernsteinPolynomial R n 0) = -↑n * bernsteinPolynomial R (n - 1) 0
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Monoid G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulAction G M<VAR>f : G × G → M<VAR>hf : IsMulTwoCocycle f<VAR>g : G<GOAL>f (1, g) = f (1, 1)
<VAR>R✝ : Type u_1<VAR>inst✝⁹ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>x : M<VAR>h : (of I M) x = (ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)<GOAL>(ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ[R] x
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : G →* H<VAR>j : X →ₑ[⇑φ] Y<VAR>hφ : Function.Surjective ⇑φ<VAR>hj : Function.Injective ⇑j<VAR>B : Set X<VAR>hB : IsBlock G B<GOAL>IsBlock H (⇑j '' B)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : G →* H<VAR>j : X →ₑ[⇑φ] Y<VAR>hφ : Function.Surjective ⇑φ<VAR>hj : Function.Injective ⇑j<VAR>B : Set X<VAR>hB : IsBlock G B<GOAL>∀ (g g' : H), g • ⇑j '' B = g' • ⇑j '' B ∨ Disjoint (g • ⇑j '' B) (g' • ⇑j '' B)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : G →* H<VAR>j : X →ₑ[⇑φ] Y<VAR>hφ : Function.Surjective ⇑φ<VAR>hj : Function.Injective ⇑j<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g g' : G<GOAL>φ g • ⇑j '' B = φ g' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (φ g' • ⇑j '' B)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : G →* H<VAR>j : X →ₑ[⇑φ] Y<VAR>hφ : Function.Surjective ⇑φ<VAR>hj : Function.Injective ⇑j<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g g' : G<GOAL>⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : G →* H<VAR>j : X →ₑ[⇑φ] Y<VAR>hφ : Function.Surjective ⇑φ<VAR>hj : Function.Injective ⇑j<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g g' : G<VAR>h : g • B = g' • B<GOAL>⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>X : Type u_2<VAR>inst✝² : MulAction G X<VAR>H : Type u_3<VAR>Y : Type u_4<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction H Y<VAR>φ : G →* H<VAR>j : X →ₑ[⇑φ] Y<VAR>hφ : Function.Surjective ⇑φ<VAR>hj : Function.Injective ⇑j<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g g' : G<VAR>h : Disjoint (g • B) (g' • B)<GOAL>⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a✝ b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>a : α<VAR>ha : a ∈ minimals r x<VAR>a' : α<VAR>h' : a' ∈ x<GOAL>s (f a') (f a) → s (f a) (f a')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a✝ b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>a : α<VAR>ha : a ∈ minimals r x<VAR>a' : α<VAR>h' : a' ∈ x<GOAL>r a' a → r a a'
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<VAR>this : Fact (finrank ℝ F = finrank ℝ F)<VAR>o : Orientation ℝ F (Fin (finrank ℝ F)) := (stdOrthonormalBasis ℝ F).toBasis.orientation<GOAL>volume (parallelepiped ⇑b) = 1
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<VAR>this : Fact (finrank ℝ F = finrank ℝ F)<VAR>o : Orientation ℝ F (Fin (finrank ℝ F)) := (stdOrthonormalBasis ℝ F).toBasis.orientation<GOAL>o.volumeForm.measure (parallelepiped ⇑b) = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>inversion c R '' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}
<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>m0 : MeasurableSpace α<VAR>m : Set (Measure α)<VAR>hm : m.Nonempty<VAR>ht : MeasurableSet t<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((sInf m).restrict t) s = (sInf ((fun μ => μ.restrict t) '' m)) s
<VAR>ι : Type u_1<VAR>inst✝² : Fintype ι<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>I : Box ι<VAR>x : E<GOAL>(BoxAdditiveMap.volume I) x = (∏ j : ι, (I.upper j - I.lower j)) • x
<VAR>ι : Type u_1<VAR>inst✝² : Fintype ι<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>I : Box ι<VAR>x : E<GOAL>volume.toBoxAdditive I • x = (∏ j : ι, (I.upper j - I.lower j)) • x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ y = y ↔ x = ⊥ ∧ y = ⊥
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A✝ : Type z<VAR>A' : Type u_1<VAR>B✝ : Type u_2<VAR>a✝ b : R✝<VAR>n : ℕ<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : Semiring A✝<VAR>inst✝⁷ : Semiring B✝<VAR>inst✝⁶ : Algebra R✝ A✝<VAR>inst✝⁵ : Algebra R✝ B✝<VAR>p✝ q r : R✝[X]<VAR>R : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>p : R[X]<VAR>f : A →ₐ[R] B<VAR>a : A<GOAL>f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A✝ : Type z<VAR>A' : Type u_1<VAR>B✝ : Type u_2<VAR>a✝ b : R✝<VAR>n : ℕ<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : Semiring A✝<VAR>inst✝⁷ : Semiring B✝<VAR>inst✝⁶ : Algebra R✝ A✝<VAR>inst✝⁵ : Algebra R✝ B✝<VAR>p✝ q r : R✝[X]<VAR>R : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>p : R[X]<VAR>f : A →ₐ[R] B<VAR>a : A<GOAL>f (∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * a ^ n) = ∑ n ∈ p.support, (algebraMap R B) (p.coeff n) * f a ^ n
<VAR>k G : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : Monoid G<VAR>V W : FDRep k G<VAR>i : V ≅ W<VAR>g : G<GOAL>W.ρ g = (isoToLinearEquiv i).conj (V.ρ g)
<VAR>k G : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : Monoid G<VAR>V W : FDRep k G<VAR>i : V ≅ W<VAR>g : G<GOAL>W.ρ g = ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).inv ≫ V.ρ g ≫ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom
<VAR>k G : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : Monoid G<VAR>V W : FDRep k G<VAR>i : V ≅ W<VAR>g : G<GOAL>((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom ≫ W.ρ g = V.ρ g ≫ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom
<GOAL>StrictConvexOn ℝ (Set.Ici 0) fun x => x * log x
<GOAL>∀ x ∈ interior (Set.Ici 0), 0 < deriv^[2] (fun x => x * log x) x
<VAR>x : ℝ<VAR>hx : x ∈ interior (Set.Ici 0)<GOAL>0 < deriv^[2] (fun x => x * log x) x
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < deriv^[2] (fun x => x * log x) x
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < x⁻¹
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g✝ : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>a : 𝕜<VAR>s t : Set 𝕜<VAR>ha : a ∈ s<VAR>hsu : UniqueDiffWithinAt 𝕜 s a<VAR>hf : HasDerivWithinAt f 0 t (g a)<VAR>hst : MapsTo g s t<VAR>hfg : f ∘ g =ᶠ[𝓝[s] a] id<VAR>hg : DifferentiableWithinAt 𝕜 g s a<GOAL>False
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g✝ : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f g : 𝕜 → 𝕜<VAR>a : 𝕜<VAR>s t : Set 𝕜<VAR>ha : a ∈ s<VAR>hsu : UniqueDiffWithinAt 𝕜 s a<VAR>hf : HasDerivWithinAt f 0 t (g a)<VAR>hst : MapsTo g s t<VAR>hfg : f ∘ g =ᶠ[𝓝[s] a] id<VAR>hg : DifferentiableWithinAt 𝕜 g s a<VAR>this : HasDerivWithinAt id (0 * derivWithin g s a) s a<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : LinearOrderedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : SMul 𝕜 β<VAR>f : F → β<VAR>g : E →ᵃ[𝕜] F<VAR>s : Set F<VAR>hf : ConvexOn 𝕜 s f<VAR>x : E<VAR>hx : x ∈ ⇑g ⁻¹' s<VAR>y : E<VAR>hy : y ∈ ⇑g ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (g (a • x + b • y)) = f (a • g x + b • g y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x✝ : Z<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Z<VAR>x : X<VAR>e : Trivialization F proj<VAR>hf_proj : ContinuousAt (proj ∘ f) x<VAR>he : proj (f x) ∈ e.baseSet<VAR>hf : ContinuousAt (↑e ∘ f) x<GOAL>ContinuousAt f x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x✝ : Z<VAR>X : Type u_6<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Z<VAR>x : X<VAR>e : Trivialization F proj<VAR>hf_proj : ContinuousAt (proj ∘ f) x<VAR>he : proj (f x) ∈ e.baseSet<VAR>hf : ContinuousAt (↑e ∘ f) x<GOAL>ContinuousAt (↑e.toPartialHomeomorph ∘ f) x