ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : Semigroup α<VAR>inst✝² : IsCancelMul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : Semigroup α<VAR>inst✝² : IsCancelMul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>∀ x ∈ s * {t.min' ht} ∩ ({s.max' hs} * t), x = s.max' hs * t.min' ht
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : Semigroup α<VAR>inst✝² : IsCancelMul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>∀ a ∈ s, ∀ x ∈ t, s.max' hs * x = a * t.min' ht → a = s.max' hs
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : Cochain F G (-1)<VAR>i j : ℤ<VAR>hij : j + 1 = i<GOAL>i + -1 = j
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : Cochain F G (-1)<VAR>p : ℤ<GOAL>(δ (-1) 0 z).v p p ⋯ = (Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij => z.v i j ⋯)).v p p ⋯
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : Cochain F G (-1)<VAR>p : ℤ<GOAL>z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + Int.negOnePow 0 • F.d p (p + 1) ≫ z.v (p + 1) p ⋯ = (Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij => z.v i j ⋯)).v p p ⋯
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : Cochain F G (-1)<VAR>p : ℤ<GOAL>z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p ⋯ = (Homotopy.nullHomotopicMap' fun i j hij => z.v i j ⋯).f p
<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>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : Cochain F G (-1)<VAR>p : ℤ<GOAL>z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p ⋯ = F.d p (p + 1) ≫ z.v (p + 1) p ⋯ + z.v p (p - 1) ⋯ ≫ G.d (p - 1) p
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : V<GOAL>↑e (x - y) = ↑e (y - x)
<VAR>n m k : ℕ<VAR>i j : Fin k<GOAL>HEq i j ↔ ↑i = ↑j
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFPowerSeriesAt f p x<GOAL>HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFPowerSeriesAt f p x<GOAL>(fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖) =o[nhds (x, x)] fun x => ‖x.1 - x.2‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFPowerSeriesAt f p x<GOAL>Tendsto (fun y => ‖y - (x, x)‖) (nhds (x, x)) (nhds 0)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFPowerSeriesAt f p x<GOAL>‖id (x, x) - (x, x)‖ = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - X)
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>h✝ : (type r).IsLimit<VAR>S : Set α<VAR>H : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>a : α<VAR>a' : α := enum r (succ (typein r a)) ⋯<VAR>b : α<VAR>h : b ∈ S<VAR>ab : ¬r b a'<GOAL>typein r a < typein r a'
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>h✝ : (type r).IsLimit<VAR>S : Set α<VAR>H : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>a : α<VAR>a' : α := enum r (succ (typein r a)) ⋯<VAR>b : α<VAR>h : b ∈ S<VAR>ab : ¬r b a'<GOAL>typein r a < succ (typein r a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>s t : α → Set β<VAR>ht : Tendsto t la lb.smallSets<VAR>hst : ∀ᶠ (x : α) in la, s x ⊆ t x<GOAL>Tendsto s la lb.smallSets
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>s t : α → Set β<VAR>ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1<VAR>hst : ∀ᶠ (x : α) in la, s x ⊆ t x<GOAL>∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m✝ : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSimpleModule R M<VAR>m : M<VAR>hm : m ≠ 0<GOAL>Ideal.IsMaximal (ker (toSpanSingleton R M m))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m✝ : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSimpleModule R M<VAR>m : M<VAR>hm : m ≠ 0<GOAL>IsSimpleModule R (R ⧸ ker (toSpanSingleton R M m))
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>f : M → M'<VAR>f' : E →L[𝕜] E'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hd : DenseRange ⇑f'<GOAL>UniqueMDiffWithinAt I' (f '' s) (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>f : M → M'<VAR>f' : E →L[𝕜] E'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hd : DenseRange ⇑f'<VAR>this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x<GOAL>UniqueMDiffWithinAt I' (f '' s) (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>f : M → M'<VAR>f' : E →L[𝕜] E'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hd : DenseRange ⇑f'<VAR>this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x<GOAL>↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I ⊆ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>f : M → M'<VAR>f' : E →L[𝕜] E'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hd : DenseRange ⇑f'<VAR>this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x<GOAL>writtenInExtChartAt I I' x f '' (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) ⊆ ↑(extChartAt I' (f x)).symm ⁻¹' (f '' s) ∩ range ↑I'
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>f : M → M'<VAR>f' : E →L[𝕜] E'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hd : DenseRange ⇑f'<VAR>this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x<GOAL>writtenInExtChartAt I I' x f (↑(extChartAt I x) x) = ↑(extChartAt I' (f x)) (f x)
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h0 : ¬x.gcd y = 0<GOAL>PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))
<VAR>x y : ℤ<VAR>h0 : ¬x.gcd y = 0<VAR>z0 : ℤ<VAR>h : PythagoreanTriple x y (↑(x.gcd y) * z0)<GOAL>PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (↑(x.gcd y) * z0 / ↑(x.gcd y))
<VAR>z0 : ℤ<VAR>k : ℕ<VAR>x0 y0 : ℤ<VAR>k0 : 0 < k<VAR>h2 : x0.gcd y0 = 1<VAR>h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0<VAR>h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0)<GOAL>PythagoreanTriple (x0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k))) (y0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k))) (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0 / ↑((x0 * ↑k).gcd (y0 * ↑k)))
<VAR>z0 : ℤ<VAR>k : ℕ<VAR>x0 y0 : ℤ<VAR>k0 : 0 < k<VAR>h2 : x0.gcd y0 = 1<VAR>h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0<VAR>h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0)<VAR>hk : ↑k ≠ 0<GOAL>PythagoreanTriple (x0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k))) (y0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k))) (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0 / ↑((x0 * ↑k).gcd (y0 * ↑k)))
<VAR>z0 : ℤ<VAR>k : ℕ<VAR>x0 y0 : ℤ<VAR>k0 : 0 < k<VAR>h2 : x0.gcd y0 = 1<VAR>h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0<VAR>h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑k * z0)<VAR>hk : ↑k ≠ 0<GOAL>PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
<VAR>z0 : ℤ<VAR>k : ℕ<VAR>x0 y0 : ℤ<VAR>k0 : 0 < k<VAR>h2 : x0.gcd y0 = 1<VAR>h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0<VAR>h : PythagoreanTriple x0 y0 z0<VAR>hk : ↑k ≠ 0<GOAL>PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hg : Function.Surjective ⇑g<GOAL>RingHom.ker (map (AlgHom.id R A) g) = Ideal.map includeRight (RingHom.ker g)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hg : Function.Surjective ⇑g<GOAL>Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hg : Function.Surjective ⇑g<VAR>this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)<GOAL>Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hg : Function.Surjective ⇑g<VAR>this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)<GOAL>LinearMap.ker (LinearMap.lTensor A g.toLinearMap) = LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hg : Function.Surjective ⇑g<VAR>this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)<GOAL>LinearMap.range (LinearMap.lTensor A (LinearMap.ker g.toLinearMap).subtype) = LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>b : β<VAR>hb : b ∈ B<VAR>s t : Multiset α<VAR>x✝² : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>x✝¹ : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>x✝ : s.prod = t.prod<GOAL>(map (fun x => b) s).prod = (map (fun x => b) t).prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : LinearOrder β<VAR>f : β → α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial β<GOAL>{x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : LinearOrder β<VAR>f : β → α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial β<VAR>this : Nonempty α<GOAL>{x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : LinearOrder β<VAR>f : β → α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial β<VAR>this : Nonempty α<VAR>s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}<VAR>z : β → α<VAR>hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y<GOAL>{x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : LinearOrder β<VAR>f : β → α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial β<VAR>this : Nonempty α<VAR>s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}<VAR>z : β → α<VAR>hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y<VAR>I : InjOn f s<GOAL>{x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : LinearOrder β<VAR>f : β → α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial β<VAR>this : Nonempty α<VAR>s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}<VAR>z : β → α<VAR>hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y<VAR>I : InjOn f s<VAR>fs_count : (f '' s).Countable<GOAL>{x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.128478, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_6, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ'✝ ℱ ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'<VAR>i : IsIso (whiskerLeft G.op α.val)<GOAL>IsIso α
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.128478, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_6, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ'✝ ℱ ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'<VAR>i : IsIso (whiskerLeft G.op α.val)<GOAL>α = (sheafIso (asIso (whiskerLeft G.op α.val))).hom
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.128478, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_6, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ'✝ ℱ ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'<VAR>i : IsIso (whiskerLeft G.op α.val)<GOAL>α.val = (sheafIso (asIso (whiskerLeft G.op α.val))).hom.val
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>h : 0 ≠ 1<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>p ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>h : 0 ≠ 1<VAR>p : R[X]<VAR>hp : p.Monic<VAR>inst✝ : Nontrivial R<GOAL>p ≠ 0
<VAR>α✝ : Type u_1<VAR>E✝ : Type u_2<VAR>F✝ : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν : Measure α✝<VAR>inst✝⁵ : NormedAddCommGroup E✝<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>g✝ : E✝ → F✝<VAR>c : ℝ≥0<VAR>α : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>K' : ℝ≥0<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : E → F<VAR>hL : Memℒp (g ∘ f) p μ<VAR>hg : UniformContinuous g<VAR>hg' : AntilipschitzWith K' g<VAR>g0 : g 0 = 0<GOAL>Memℒp f p μ
<VAR>α✝ : Type u_1<VAR>E✝ : Type u_2<VAR>F✝ : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν : Measure α✝<VAR>inst✝⁵ : NormedAddCommGroup E✝<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>g✝ : E✝ → F✝<VAR>c : ℝ≥0<VAR>α : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>K' : ℝ≥0<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : E → F<VAR>hL : Memℒp (g ∘ f) p μ<VAR>hg : UniformContinuous g<VAR>hg' : AntilipschitzWith K' g<VAR>g0 : g 0 = 0<VAR>A : ∀ (x : α), ‖f x‖ ≤ ↑K' * ‖g (f x)‖<GOAL>Memℒp f p μ
<VAR>α✝ : Type u_1<VAR>E✝ : Type u_2<VAR>F✝ : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν : Measure α✝<VAR>inst✝⁵ : NormedAddCommGroup E✝<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>g✝ : E✝ → F✝<VAR>c : ℝ≥0<VAR>α : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>K' : ℝ≥0<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : E → F<VAR>hL : Memℒp (g ∘ f) p μ<VAR>hg : UniformContinuous g<VAR>hg' : AntilipschitzWith K' g<VAR>g0 : g 0 = 0<VAR>A : ∀ (x : α), ‖f x‖ ≤ ↑K' * ‖g (f x)‖<VAR>B : AEStronglyMeasurable f μ<GOAL>Memℒp f p μ
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ' : QuasiIso φ'<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso φ
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>φ' : S₂ ⟶ S₃<VAR>hφ' : IsIso (homologyMap φ')<VAR>hφφ' : IsIso (homologyMap (φ ≫ φ'))<GOAL>IsIso (homologyMap φ)