ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>z : 𝕝<VAR>hz : z ≠ 0<VAR>f1 : 𝕝 → 𝕝 := fun a => 1 / z * a<VAR>f2 : 𝕝 → 𝕝 := fun b => (1 - b)⁻¹<VAR>f3 : 𝕝 → 𝕝 := fun c => 1 - c / z<VAR>feq : f1 ∘ f2 ∘ f3 = Inv.inv<GOAL>AnalyticAt 𝕜 Inv.inv z
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>z : 𝕝<VAR>hz : z ≠ 0<VAR>f1 : 𝕝 → 𝕝 := fun a => 1 / z * a<VAR>f2 : 𝕝 → 𝕝 := fun b => (1 - b)⁻¹<VAR>f3 : 𝕝 → 𝕝 := fun c => 1 - c / z<VAR>feq : f1 ∘ f2 ∘ f3 = Inv.inv<VAR>f3val : f3 z = 0<GOAL>AnalyticAt 𝕜 Inv.inv z
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>z : 𝕝<VAR>hz : z ≠ 0<VAR>f1 : 𝕝 → 𝕝 := fun a => 1 / z * a<VAR>f2 : 𝕝 → 𝕝 := fun b => (1 - b)⁻¹<VAR>f3 : 𝕝 → 𝕝 := fun c => 1 - c / z<VAR>feq : f1 ∘ f2 ∘ f3 = Inv.inv<VAR>f3val : f3 z = 0<VAR>f3an : AnalyticAt 𝕜 f3 z<GOAL>AnalyticAt 𝕜 Inv.inv z
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯<VAR>hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ↑(f_seq n)<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯<VAR>hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ↑(f_seq n)<VAR>hf_seq_int : ∀ (n : ℕ), Integrable (↑(f_seq n)) μ<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯<VAR>hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ↑(f_seq n)<VAR>hf_seq_int : ∀ (n : ℕ), Integrable (↑(f_seq n)) μ<VAR>hf_seq_int_m : ∀ (n : ℕ), Integrable (↑(f_seq n)) (μ.trim hm)<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯<VAR>hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ↑(f_seq n)<VAR>hf_seq_int : ∀ (n : ℕ), Integrable (↑(f_seq n)) μ<VAR>hf_seq_int_m : ∀ (n : ℕ), Integrable (↑(f_seq n)) (μ.trim hm)<VAR>hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), ↑(f_seq n) x ∂μ = ∫ (x : β), ↑(f_seq n) x ∂μ.trim hm<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯<VAR>hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ↑(f_seq n)<VAR>hf_seq_int : ∀ (n : ℕ), Integrable (↑(f_seq n)) μ<VAR>hf_seq_int_m : ∀ (n : ℕ), Integrable (↑(f_seq n)) (μ.trim hm)<VAR>hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), ↑(f_seq n) x ∂μ = ∫ (x : β), ↑(f_seq n) x ∂μ.trim hm<VAR>h_lim_1 : Tendsto (fun n => ∫ (x : β), ↑(f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<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>H : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>inst✝ : NormedAddCommGroup H<VAR>m m0 : MeasurableSpace β<VAR>μ : Measure β<VAR>hm : m ≤ m0<VAR>f : β → G<VAR>hf : StronglyMeasurable f<VAR>hG : CompleteSpace G<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hf_int : Integrable f μ<VAR>this : SeparableSpace ↑(range f ∪ {0})<VAR>f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯<VAR>hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ↑(f_seq n)<VAR>hf_seq_int : ∀ (n : ℕ), Integrable (↑(f_seq n)) μ<VAR>hf_seq_int_m : ∀ (n : ℕ), Integrable (↑(f_seq n)) (μ.trim hm)<VAR>hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), ↑(f_seq n) x ∂μ = ∫ (x : β), ↑(f_seq n) x ∂μ.trim hm<VAR>h_lim_1 : Tendsto (fun n => ∫ (x : β), ↑(f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))<VAR>h_lim_2 : Tendsto (fun n => ∫ (x : β), ↑(f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ.trim hm))<GOAL>∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : J.plusObj P ⟶ Q<VAR>hγ : J.toPlus P ≫ γ = η<GOAL>γ = J.plusMap η ≫ (J.isoToPlus Q hQ).inv
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>γ : J.plusObj P ⟶ Q<VAR>hγ : J.toPlus P ≫ γ = η<GOAL>γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap (J.toPlus P) ≫ J.plusMap γ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>x✝ : E<VAR>a✝⁵ : x✝ ∈ ↑K<VAR>y✝ : E<VAR>a✝⁴ : y✝ ∈ ↑K<VAR>a✝³ b✝ : 𝕜<VAR>a✝² : 0 ≤ a✝³<VAR>a✝¹ : 0 ≤ b✝<VAR>a✝ : a✝³ + b✝ = 1<GOAL>a✝³ • x✝ + b✝ • y✝ ∈ ↑K
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x : R<VAR>y : P<GOAL>y ∈ ↑(Ideal.span {x}) ↔ y ∈ spanSingleton S ((algebraMap R P) x)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x : R<VAR>y : P<GOAL>(∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) ↔ ∃ z, z • (algebraMap R P) x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<GOAL>(μ.singularPart ν).singularPart ν = μ.singularPart ν
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<GOAL>(((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩) = fromCoset ⟨(x * b) • ↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<GOAL>(Equiv.swap (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) ∞) ((g x) ((Equiv.symm (Equiv.swap (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) ∞)) (fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩))) = fromCoset ⟨(x * b) • ↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<GOAL>(Equiv.swap (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) ∞) ((g x) (fromCoset ⟨b • ↑(MonoidHom.range f), ⋯⟩)) = fromCoset ⟨(x * b) • ↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<GOAL>(Equiv.swap (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) ∞) (fromCoset ⟨(x * b) • ↑(MonoidHom.range f), ⋯⟩) = fromCoset ⟨(x * b) • ↑(MonoidHom.range f), ⋯⟩
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<VAR>r : x * b ∈ MonoidHom.range f<GOAL>b ∈ MonoidHom.range f
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<VAR>hx : x ∈ MonoidHom.range f<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<VAR>r : x * b ∈ MonoidHom.range f<GOAL>b = x⁻¹ * (x * b)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B C : Matrix n n α<VAR>h : A * B = 1<VAR>g : C * A = 1<GOAL>B = C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>fst✝ : α<VAR>snd✝ : M<GOAL>(fst✝, snd✝) ∈ f.graph ↔ f (fst✝, snd✝).1 = (fst✝, snd✝).2 ∧ (fst✝, snd✝).2 ≠ 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : SeminormedRing 𝕜<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>S : Set (Set E)<VAR>hS : S.Finite<GOAL>IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝ : RingHomInvPair τ₁₂ τ₂₁<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₁] M<VAR>h : g.comp f = id<VAR>m : M<VAR>hm : f m = 0<GOAL>m = 0
<VAR>x y z : PartENat<VAR>h : x < y<VAR>hz : z ≠ ⊤<GOAL>x + z < y + z
<VAR>y z : PartENat<VAR>hz : z ≠ ⊤<VAR>m : ℕ<VAR>h : ↑m < y<GOAL>↑m + z < y + z
<VAR>y : PartENat<VAR>m : ℕ<VAR>h : ↑m < y<VAR>k : ℕ<VAR>hz : ↑k ≠ ⊤<GOAL>↑m + ↑k < y + ↑k
<VAR>m k : ℕ<VAR>hz : ↑k ≠ ⊤<VAR>h : ↑m < ⊤<GOAL>↑m + ↑k < ⊤ + ↑k
<VAR>m k : ℕ<VAR>hz : ↑k ≠ ⊤<VAR>n : ℕ<VAR>h : ↑m < ↑n<GOAL>↑m + ↑k < ↑n + ↑k
<VAR>m k : ℕ<VAR>hz : ↑k ≠ ⊤<VAR>n : ℕ<VAR>h : m < n<GOAL>m + k < n + k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LT α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a * b < a<GOAL>a * b < a * 1
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<GOAL>Primrec' fun v => (unpair (f v)).2
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>s : Primrec' fun v => (f v).sqrt<GOAL>Primrec' fun v => (unpair (f v)).2
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>s : Primrec' fun v => (f v).sqrt<VAR>fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt<GOAL>Primrec' fun v => (unpair (f v)).2
<VAR>n : ℕ<VAR>f : Vector ℕ n → ℕ<VAR>hf : Primrec' f<VAR>s : Primrec' fun v => (f v).sqrt<VAR>fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt<VAR>v : Vector ℕ n<GOAL>(if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v).sqrt else f v - (f v).sqrt * (f v).sqrt - (f v).sqrt) = (unpair (f v)).2
<VAR>S : Type u<VAR>inst✝ : State S<VAR>s t : S<VAR>m : t ∈ r s<VAR>h : turnBound s = 0<GOAL>False
<VAR>S : Type u<VAR>inst✝ : State S<VAR>s t✝ : S<VAR>m : t✝ ∈ r s<VAR>h : turnBound s = 0<VAR>t : turnBound t✝ < turnBound s<GOAL>False
<VAR>S : Type u<VAR>inst✝ : State S<VAR>s t✝ : S<VAR>m : t✝ ∈ r s<VAR>h : turnBound s = 0<VAR>t : turnBound t✝ < 0<GOAL>False
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.prev { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs.dropLast }
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>(support fun x => ↑f x / ∫ (x : E), ↑f x ∂μ) = ball c f.rOut
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.think.Results a (n + 1)<GOAL>s.Results a n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.think.Results a (n + 1)<VAR>n' : ℕ<VAR>r : s.Results a n'<VAR>e : n + 1 = n' + 1<GOAL>s.Results a n
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<GOAL>(rightShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.rightUnshift n hn
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : AddMonoid A<VAR>s✝ t u : Set M<VAR>N : Type u_6<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : MulAction M N<VAR>inst✝ : IsScalarTower M N N<VAR>r : M<VAR>s : Set N<VAR>x : N<VAR>hx : x ∈ closure s<GOAL>∃ n, r ^ n • x ∈ closure (r • s)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : AddMonoid A<VAR>s✝ t u : Set M<VAR>N : Type u_6<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : MulAction M N<VAR>inst✝ : IsScalarTower M N N<VAR>r : M<VAR>s : Set N<VAR>x : N<VAR>hx : x ∈ closure s<GOAL>∀ x ∈ s, (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : AddMonoid A<VAR>s✝ t u : Set M<VAR>N : Type u_6<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : MulAction M N<VAR>inst✝ : IsScalarTower M N N<VAR>r : M<VAR>s : Set N<VAR>x : N<VAR>hx : x ∈ closure s<GOAL>(fun x => ∃ n, r ^ n • x ∈ closure (r • s)) 1
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : AddMonoid A<VAR>s✝ t u : Set M<VAR>N : Type u_6<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : MulAction M N<VAR>inst✝ : IsScalarTower M N N<VAR>r : M<VAR>s : Set N<VAR>x : N<VAR>hx : x ∈ closure s<GOAL>∀ (x y : N), (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) y → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) (x * y)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁴ : NormedAddCommGroup D<VAR>inst✝¹³ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<VAR>inst✝ : DecidableEq ι<VAR>k : ℕ∞<VAR>x : (i : ι) → F' i<VAR>i : ι<GOAL>ContDiff 𝕜 k (update x i)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁴ : NormedAddCommGroup D<VAR>inst✝¹³ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<VAR>inst✝ : DecidableEq ι<VAR>k : ℕ∞<VAR>x : (i : ι) → F' i<VAR>i : ι<GOAL>∀ (i_1 : ι), ContDiff 𝕜 k fun x_1 => update x i x_1 i_1
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>r : R<VAR>p q : R[X]<GOAL>(taylor r) (p * q) = (taylor r) p * (taylor r) q
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : Filter (α × β)<GOAL>Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)