ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>hg : ContinuousWithinAt g t (f x) ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑(extChartAt I' (f x)).symm) (↑(extChartAt I' (f x)).symm ⁻¹' t ∩ range ↑I') (↑(extChartAt I' (f x)) (f x))<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<VAR>st : MapsTo f s t<GOAL>ContinuousWithinAt (g ∘ f) s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) 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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>hg : ContinuousWithinAt g t (f x) ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑(extChartAt I' (f x)).symm) (↑(extChartAt I' (f x)).symm ⁻¹' t ∩ range ↑I') (↑(extChartAt I' (f x)) (f x))<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<VAR>st : MapsTo f s t<GOAL>ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) 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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>st : MapsTo f s t<VAR>e : PartialEquiv M E := extChartAt I x<VAR>e' : PartialEquiv M' E' := extChartAt I' (f x)<VAR>hg : ContinuousWithinAt g t (f x) ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I') (writtenInExtChartAt I I' x f (↑e x))<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)<VAR>this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)<GOAL>ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e 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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>st : MapsTo f s t<VAR>e : PartialEquiv M E := extChartAt I x<VAR>e' : PartialEquiv M' E' := extChartAt I' (f x)<VAR>hg : ContinuousWithinAt g t (f x) ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I') (writtenInExtChartAt I I' x f (↑e x))<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)<VAR>this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)<VAR>A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source<GOAL>ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e 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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>st : MapsTo f s t<VAR>e : PartialEquiv M E := extChartAt I x<VAR>e' : PartialEquiv M' E' := extChartAt I' (f x)<VAR>hg : ContinuousWithinAt g t (f x) ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I') (writtenInExtChartAt I I' x f (↑e x))<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)<VAR>this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)<VAR>A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source<GOAL>writtenInExtChartAt I I' x f ⁻¹' (↑e'.symm ⁻¹' t ∩ range ↑I') ∈ 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e 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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>st : MapsTo f s t<VAR>e : PartialEquiv M E := extChartAt I x<VAR>e' : PartialEquiv M' E' := extChartAt I' (f x)<VAR>hg : ContinuousWithinAt g t (f x) ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I') (writtenInExtChartAt I I' x f (↑e x))<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)<VAR>this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)<VAR>A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source<GOAL>↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm =ᶠ[𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x] (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) ∘ writtenInExtChartAt I I' x f
<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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t✝ : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>st : MapsTo f s t<VAR>e : PartialEquiv M E := extChartAt I x<VAR>e' : PartialEquiv M' E' := extChartAt I' (f x)<VAR>hg : ContinuousWithinAt g t (f x) ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I') (writtenInExtChartAt I I' x f (↑e x))<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)<VAR>this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)<VAR>A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source<GOAL>(↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) (↑e x) = ((↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) ∘ writtenInExtChartAt I I' x f) (↑e x)
<VAR>θ : ↑I<GOAL>2 * ↑(0, θ).1 / (1 + ↑(0, θ).2) ≤ 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : Nonempty α<VAR>p : α × α → Prop<GOAL>(∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>x : { x // x ∈ s }<GOAL>𝓝 x = comap Subtype.val (𝓝[s] ↑x)
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<VAR>hb₀ : b ≠ 0<VAR>hb₁ : b ≠ ⊤<VAR>h : a / b = 1<GOAL>a = b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x : φ i<VAR>j : ι<GOAL>(stdBasis R φ i) x j = (pi (diag i)) x j
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x : φ i<VAR>j : ι<GOAL>x = id x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>f : α → β × γ<VAR>b : Filter β<VAR>c : Filter γ<GOAL>comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<GOAL>multiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = multiplicity (↑p) (x - y) + multiplicity p (n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p n.succ).Dom<GOAL>multiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = multiplicity (↑p) (x - y) + multiplicity p (n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p (n + 1)).Dom<GOAL>multiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = multiplicity (↑p) (x - y) + multiplicity p (n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p (n + 1)).Dom<VAR>hpn : ¬p ^ ((multiplicity p (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = p ^ (multiplicity p (n + 1)).get h * k<GOAL>multiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = multiplicity (↑p) (x - y) + multiplicity p (n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p (n + 1)).Dom<VAR>hpn : ¬p ^ ((multiplicity p (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = p ^ (multiplicity p (n + 1)).get h * k<GOAL>multiplicity (↑p) ((x ^ p ^ (multiplicity p (n + 1)).get h) ^ k - (y ^ p ^ (multiplicity p (n + 1)).get h) ^ k) = multiplicity (↑p) (x - y) + multiplicity p (n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p (n + 1)).Dom<VAR>hpn : ¬p ^ ((multiplicity p (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = p ^ (multiplicity p (n + 1)).get h * k<GOAL>multiplicity (↑p) ((x ^ p ^ (multiplicity p (n + 1)).get h) ^ k - (y ^ p ^ (multiplicity p (n + 1)).get h) ^ k) = multiplicity (↑p) (x - y) + multiplicity p (n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p (n + 1)).Dom<VAR>hpn : ¬p ^ ((multiplicity p (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = p ^ (multiplicity p (n + 1)).get h * k<GOAL>↑p ∣ x ^ p ^ (multiplicity p (n + 1)).get h - y ^ p ^ (multiplicity p (n + 1)).get h
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p (n + 1)).Dom<VAR>hpn : ¬p ^ ((multiplicity p (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = p ^ (multiplicity p (n + 1)).get h * k<GOAL>¬↑p ∣ x ^ p ^ (multiplicity p (n + 1)).get h
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ : R<VAR>p : ℕ<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>n : ℕ<VAR>h : (multiplicity p (n + 1)).Dom<VAR>hpn : ¬p ^ ((multiplicity p (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = p ^ (multiplicity p (n + 1)).get h * k<GOAL>¬↑p ∣ ↑k
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n A<GOAL>(toFunAlgHom R A n) (invFun R A n M) = M
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n A<GOAL>∑ x : n × n, M x.1 x.2 • (stdBasisMatrix x.1 x.2 1).map ⇑(algebraMap R A) = M
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n A<GOAL>M = ∑ x : n, ∑ y : n, M (x, y).1 (x, y).2 • (stdBasisMatrix (x, y).1 (x, y).2 1).map ⇑(algebraMap R A)
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n A<GOAL>∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j) = ∑ x : n, ∑ y : n, M (x, y).1 (x, y).2 • (stdBasisMatrix (x, y).1 (x, y).2 1).map ⇑(algebraMap R A)
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n A<VAR>i : n<VAR>x✝¹ : i ∈ Finset.univ<VAR>j : n<VAR>x✝ : j ∈ Finset.univ<VAR>a b : n<GOAL>stdBasisMatrix i j (M i j) a b = (M (i, j).1 (i, j).2 • (stdBasisMatrix (i, j).1 (i, j).2 1).map ⇑(algebraMap R A)) a b
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n A<VAR>i : n<VAR>x✝¹ : i ∈ Finset.univ<VAR>j : n<VAR>x✝ : j ∈ Finset.univ<VAR>a b : n<GOAL>(if i = a ∧ j = b then M i j else 0) = M i j • (algebraMap R A) (if i = a ∧ j = b then 1 else 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<GOAL>Nat.card α = if h : Finite α then Fintype.card α else 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>h✝ : Finite α<GOAL>Nat.card α = if h : Finite α then Fintype.card α else 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>h✝ : Infinite α<GOAL>Nat.card α = if h : Finite α then Fintype.card α else 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : StrictOrderedSemiring α<VAR>inst✝¹ : Archimedean α<VAR>y : α<VAR>inst✝ : ExistsAddOfLE α<VAR>x : α<VAR>hy1 : 1 < y<GOAL>∃ n, x < y ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : StrictOrderedSemiring α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x z : α<VAR>hz : 0 < z<VAR>hy1 : 1 < 1 + z<GOAL>∃ n, x < (1 + z) ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : StrictOrderedSemiring α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x z : α<VAR>hz : 0 < z<VAR>hy1 : 1 < 1 + z<GOAL>∃ n, x < (z + 1) ^ n
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ a₃ : A<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : B<VAR>h₁ : b₁ = φ a₁<VAR>h₂ : b₂ = φ a₂<VAR>h₃ : b₃ = φ a₃<GOAL>(shiftFunctorZero (PullbackShift C φ) A).hom.app X = (pullbackShiftIso C φ 0 0 ⋯).hom.app X ≫ (shiftFunctorZero C B).hom.app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ a₃ : A<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : B<VAR>h₁ : b₁ = φ a₁<VAR>h₂ : b₂ = φ a₂<VAR>h₃ : b₃ = φ a₃<GOAL>𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>a : α<GOAL>(insert a s).diag = insert (a, a) s.diag
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>h : ∀ (g : G), 0 < orderOf g<GOAL>exponent G = 0 ↔ (Set.range orderOf).Infinite
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>h : ∀ (g : G), 0 < orderOf g<VAR>this : exponent G ≠ 0 ↔ (Set.range orderOf).Finite<GOAL>exponent G = 0 ↔ (Set.range orderOf).Infinite
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>¬(u = v ∨ ¬G.Reachable u v) ↔ u ≠ v ∧ G.Reachable u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>u ≠ v ∧ G.Reachable u v ↔ u ≠ v ∧ G.Reachable u v
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>↑⁅I, N⁆ = Submodule.span R {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = Submodule.span R {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m}
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>S : Set (NonUnitalSubsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>S : Set (NonUnitalSubsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>this : Nonempty ↑S<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<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>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<GOAL>Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y : P<VAR>h : Wbtw R x y x<VAR>hne : y ≠ x<GOAL>False