ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>CondIndepFun m' hm' f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.440575, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 ⋯ ⋯<GOAL>g.map' 0 1 ⋯ ⋯ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.440575, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 ⋯ ⋯<GOAL>g.map' 1 2 ⋯ ⋯ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.440575, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 ⋯ ⋯<GOAL>g.map' 2 3 ⋯ ⋯ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.440575, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 ⋯ ⋯<GOAL>g.map' 3 4 ⋯ ⋯ ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.440575, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 ⋯ ⋯<GOAL>g.map' 4 5 ⋯ ⋯ ≫ app₅.inv = app₄.inv ≫ f.map' 4 5 ⋯ ⋯
<VAR>c₁ c₂ : Code<VAR>n₁ n₂ : ℕ<VAR>h₁ : c₁ = c₂<VAR>h₃ : Code.const n₁ = Code.const n₂<VAR>h₄ : Code.id = Code.id<GOAL>n₁ = n₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : Measure α<VAR>a b : α<VAR>inst✝ : NoAtoms μ<GOAL>μ {a} ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : Measure α<VAR>a b : α<VAR>inst✝ : NoAtoms μ<GOAL>0 ≠ ⊤
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x y z : M<VAR>h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source<GOAL>↑(extChartAt I x) z ∈ ((extChartAt I x).symm ≫ extChartAt I y).source
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x y z : M<VAR>h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source<GOAL>↑(extChartAt I x) z ∈ ↑(extChartAt I x) '' ((extChartAt I x).source ∩ (extChartAt I y).source)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>hc : AddLECancellable c<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ b<GOAL>a ≤ b - c ↔ c ≤ b - a
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<VAR>v : ι → Set α<VAR>hsv : s ⊆ iUnion v<VAR>hvc : ∀ (i : ι), IsClosed (v i)<VAR>hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<VAR>v : ι → Set α<VAR>hsv : s ⊆ iUnion v<VAR>hvc : ∀ (i : ι), IsClosed (v i)<VAR>hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)<VAR>this : ∀ (i : ι), ∃ r' < r i, v i ⊆ ball (c i) r'<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<VAR>v : ι → Set α<VAR>hsv : s ⊆ iUnion v<VAR>hvc : ∀ (i : ι), IsClosed (v i)<VAR>hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)<VAR>r' : ι → ℝ<VAR>hlt : ∀ (i : ι), r' i < r i<VAR>hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g : α → M<VAR>a : α<VAR>h1 : s.mulIndicator f = f<VAR>h2 : s ⊆ t<GOAL>t.mulIndicator f = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g : α → M<VAR>a : α<VAR>h1 : mulSupport f ⊆ s<VAR>h2 : s ⊆ t<GOAL>mulSupport f ⊆ t
<VAR>x y : ℝ<VAR>hy : 0 < y<GOAL>√x < √y ↔ x < y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : SemilatticeSup α<VAR>b c : α<VAR>inst✝ : OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>ha : SupPrime ⊥<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a✝ b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u : Set α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<VAR>x✝ : α<GOAL>x✝ ∈ insert a s \ s ↔ x✝ ∈ {a}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a✝ b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u : Set α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<VAR>x✝ : α<GOAL>x✝ = a → x✝ ∉ s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>h : DifferentiableAt 𝕜 (fun y => c + f y) x<GOAL>DifferentiableAt 𝕜 f x
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : Nontrivial R<GOAL>(nodal s v).natDegree = s.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>2 ≤ (f.cycleOf x).support.card ↔ f x ≠ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>h : 2 ≤ (f.cycleOf x).support.card<GOAL>f x ≠ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>h : f x = x<GOAL>(f.cycleOf x).support.card < 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>h : f.cycleOf x = 1<GOAL>(f.cycleOf x).support.card < 2
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>f : α →ᵇ β<GOAL>‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : { p // p ∣ I }<GOAL>comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)) ∣ J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : { p // p ∣ I }<VAR>this : RingHom.ker (Ideal.Quotient.mk J) ≤ comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X))<GOAL>comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)) ∣ J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : { p // p ∣ I }<VAR>this : J ≤ comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X))<GOAL>comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)) ∣ J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : Ideal R<VAR>hX : X ∣ I<VAR>Y : Ideal R<VAR>hY : Y ∣ I<VAR>h : ⟨X, hX⟩ ≤ ⟨Y, hY⟩<GOAL>(fun X => ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩) ⟨X, hX⟩ ≤ (fun X => ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩) ⟨Y, hY⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : Ideal R<VAR>hX : X ∣ I<VAR>Y : Ideal R<VAR>hY : Y ∣ I<VAR>h : X ≤ Y<GOAL>comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) X)) ≤ ↑((fun X => ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) ↑X)), ⋯⟩) ⟨Y, hY⟩)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : Ideal R<VAR>hX : X ∣ I<VAR>Y : Ideal R<VAR>hY : Y ∣ I<VAR>h : X ≤ Y<GOAL>map (Ideal.Quotient.mk I) X ≤ map (Ideal.Quotient.mk I) Y ⊔ comap f ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : Ideal R<VAR>hX : X ∣ I<VAR>Y : Ideal R<VAR>hY : Y ∣ I<VAR>h : X ≤ Y<GOAL>map (Ideal.Quotient.mk I) X ≤ map (Ideal.Quotient.mk I) Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν ν' : Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>((κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x)).toReal ≤ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν ν' : Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<GOAL>((κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x)).toReal ≤ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν ν' : Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>((κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x)).toReal ≤ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν ν' : Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h0' : (ν' a) (countablePartitionSet n x) ≠ 0<GOAL>((κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x)).toReal ≤ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν ν' : Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h0' : (ν' a) (countablePartitionSet n x) ≠ 0<GOAL>(κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x) ≤ (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν ν' : Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h0' : (ν' a) (countablePartitionSet n x) ≠ 0<GOAL>(κ a) (countablePartitionSet n x ×ˢ s) / (ν' a) (countablePartitionSet n x) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν ν' : Kernel α γ<VAR>hνν' : ν ≤ ν'<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h0' : (ν' a) (countablePartitionSet n x) ≠ 0<GOAL>(κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ≠ ⊤
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : Mul M<VAR>inst✝⁵ : ContinuousMul M<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : MulOneClass β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousMul β<VAR>f : F<VAR>tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>ContinuousMul α
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : Mul M<VAR>inst✝⁵ : ContinuousMul M<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : MulOneClass β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousMul β<VAR>f : F<VAR>tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>Continuous (⇑f ∘ fun p => p.1 * p.2)
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : Mul M<VAR>inst✝⁵ : ContinuousMul M<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : MulOneClass β<VAR>inst✝¹ : MonoidHomClass F α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousMul β<VAR>f : F<VAR>tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>Continuous fun x => f x.1 * f x.2
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>hx : x ∈ thickening δ E<GOAL>x ∈ cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>hx : infEdist x E < ENNReal.ofReal δ<GOAL>x ∈ cthickening δ E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<GOAL>ContinuousAt (dslope f a) b ↔ ContinuousAt f b
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : Module.Free R M₁<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Finite R M'<GOAL>finrank R (M × M') = finrank R M + finrank R M'
<VAR>b : ℕ<VAR>h : 1 ≤ b<GOAL>∃ᶠ (n : ℕ) in Filter.atTop, n.FermatPsp b
<VAR>b : ℕ<VAR>h : 1 ≤ b<VAR>n : ℕ<GOAL>∃ b_1 ≥ n, b_1.FermatPsp b
<VAR>b : ℕ<VAR>h : 1 ≤ b<VAR>n p : ℕ<VAR>hp : p.FermatPsp b ∧ n ≤ p<GOAL>∃ b_1 ≥ n, b_1.FermatPsp b
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s t : Set ι<VAR>hs : Disjoint s t<GOAL>Disjoint (span R (v '' s)) (span R (v '' t))
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s t : Set ι<VAR>hs : Disjoint s t<GOAL>∀ (x : M), (∃ l ∈ Finsupp.supported R R s, (Finsupp.total ι M R v) l = x) → (∃ l ∈ Finsupp.supported R R t, (Finsupp.total ι M R v) l = x) → x = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s t : Set ι<VAR>hs : Disjoint s t<VAR>l₁ : ι →₀ R<VAR>hl₁ : l₁ ∈ Finsupp.supported R R s<VAR>l₂ : ι →₀ R<VAR>hl₂ : l₂ ∈ Finsupp.supported R R t<VAR>H : (Finsupp.total ι M R v) l₂ = (Finsupp.total ι M R v) l₁<GOAL>(Finsupp.total ι M R v) l₁ = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>s t : Set ι<VAR>hs : Disjoint s t<VAR>l₁ : ι →₀ R<VAR>hl₁ : l₁ ∈ Finsupp.supported R R s<VAR>l₂ : ι →₀ R<VAR>hl₂ : l₂ ∈ Finsupp.supported R R t<VAR>H : l₂ = l₁<GOAL>(Finsupp.total ι M R v) l₁ = 0