ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ↥(Lp E p μ)<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C<VAR>hμ : ¬μ = 0<GOAL>C • μ Set.univ ^ p.toReal⁻¹ = ↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C)
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x<GOAL>HasStrictFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' (l.get i)).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) x
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x<GOAL>HasStrictFDerivAt (fun x => (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.finRange l.length)).prod) (∑ x_1 : Fin l.length, (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod • (f' (l.get x_1)).smulRight (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod) x
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x<GOAL>(∑ i : Fin l.length, (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.take (↑i) (List.finRange l.length))).prod • (proj i).smulRight (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.drop (↑i).succ (List.finRange l.length))).prod).comp (ContinuousLinearMap.pi fun i => f' (l.get i)) = ∑ x_1 : Fin l.length, (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod • (f' (l.get x_1)).smulRight (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp (a + p) b = toIcoMod hp a b + p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<GOAL>l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<GOAL>l₁ <+~ l₂ → ∃ l, l ~ l₂ ∧ l₁ <+ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>h₁ : l ~ l₁<VAR>h₂ : l <+ l₂<GOAL>∃ l, l ~ l₂ ∧ l₁ <+ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>h₁ : l ~ l₁<VAR>h₂✝ : l <+ l₂<VAR>l' : List α<VAR>h₂ : l₂ ~ l ++ l'<GOAL>∃ l, l ~ l₂ ∧ l₁ <+ l
<VAR>x y : PartENat<VAR>hx : x.Dom<VAR>hy : y.Dom<GOAL>x.get hx ≤ y.get hy ↔ x ≤ y
<VAR>α : Type u<VAR>inst✝³ : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space β<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>extend f (pureCauchy a) = f a
<VAR>α : Type u<VAR>inst✝³ : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space β<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>⋯.extend f (pureCauchy a) = f a
<VAR>F : Type u → Type v<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>G : Type u → Type w<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>x : α → β<VAR>y : F α<GOAL>(fun {α} => η.app α) (x <$> y) = x <$> (fun {α} => η.app α) y
<VAR>x : ℂ<VAR>h : cos x ≠ 0<GOAL>HasStrictDerivAt tan (1 / cos x ^ 2) x
<VAR>x : ℂ<VAR>h : cos x ≠ 0<GOAL>1 / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
<VAR>x : ℂ<VAR>h : ¬cos x = 0<GOAL>(sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
<VAR>R R' : Type u<VAR>M M' : Type v<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousConstSMul R M<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : ContinuousConstSMul R' M'<VAR>inst✝ : ContinuousAdd M<VAR>s : Set M<GOAL>closure s ⊆ ↑(span R s).topologicalClosure
<VAR>R R' : Type u<VAR>M M' : Type v<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousConstSMul R M<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : ContinuousConstSMul R' M'<VAR>inst✝ : ContinuousAdd M<VAR>s : Set M<GOAL>closure s ⊆ closure ↑(span R s)
<VAR>R : Type u<VAR>S : Type u'<VAR>M✝ : Type v<VAR>N : Type w<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Ring M<VAR>inst✝⁵ : Algebra K M<VAR>inst✝⁴ : Module.Free K M<VAR>inst✝³ : Module.Finite K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>Nat.card (M →ₐ[K] L) ≤ finrank K M
<VAR>R : Type u<VAR>S : Type u'<VAR>M✝ : Type v<VAR>N : Type w<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Ring M<VAR>inst✝⁵ : Algebra K M<VAR>inst✝⁴ : Module.Free K M<VAR>inst✝³ : Module.Finite K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>finrank K M = toNat (lift.{v, u_2} (Module.rank K M))
<VAR>R : Type u<VAR>S : Type u'<VAR>M✝ : Type v<VAR>N : Type w<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>inst✝⁷ : CommRing K<VAR>inst✝⁶ : Ring M<VAR>inst✝⁵ : Algebra K M<VAR>inst✝⁴ : Module.Free K M<VAR>inst✝³ : Module.Finite K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>lift.{v, u_2} (Module.rank K M) < ℵ₀
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<GOAL>residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<GOAL>LocalRing.ResidueField.map (𝟙 (X.presheaf.stalk x)) = 𝟙 (X.residueField x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<GOAL>mex f < (succ #ι).ord
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>h : (succ #ι).ord ≤ mex f<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>h : (succ #ι).ord ≤ mex f<GOAL>succ #ι ≤ #ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>h : (succ #ι).ord ≤ mex f<VAR>H : ∀ (a : (Quotient.out (succ #ι).ord).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a<GOAL>succ #ι ≤ #ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>h : (succ #ι).ord ≤ mex f<VAR>H : ∀ (a : (Quotient.out (succ #ι).ord).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a<VAR>g : (Quotient.out (succ #ι).ord).α → ι := fun a => Classical.choose ⋯<VAR>hg : Injective g<GOAL>succ #ι ≤ #ι
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>h : (succ #ι).ord ≤ mex f<VAR>H : ∀ (a : (Quotient.out (succ #ι).ord).α), ∃ i, f i = typein (fun x x_1 => x < x_1) a<VAR>g : (Quotient.out (succ #ι).ord).α → ι := fun a => Classical.choose ⋯<VAR>hg : Injective g<GOAL>succ #ι = #(Quotient.out (succ #ι).ord).α
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>h : W.Equation 0 0<VAR>hΔ : Δ W ≠ 0<GOAL>W.Nonsingular 0 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>hΔ : Δ W ≠ 0<VAR>h : W.a₆ = 0<GOAL>W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>h : W.a₆ = 0<VAR>hΔ : W.a₆ = 0 → W.a₃ = 0 ∧ W.a₄ = 0<GOAL>Δ W = 0
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : T2Space M<VAR>f : ℕ → M<VAR>hf : Multipliable f<GOAL>HasProd f m ↔ Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : T2Space M<VAR>f : ℕ → M<VAR>hf : Multipliable f<VAR>h : Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)<GOAL>HasProd f m
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : T2Space M<VAR>f : ℕ → M<VAR>hf : Multipliable f<VAR>h : Tendsto (fun n => ∏ i ∈ range n, f i) atTop (𝓝 m)<GOAL>HasProd f (∏' (b : ℕ), f b)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G<GOAL>MeasurableSet (a • s)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G<GOAL>MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>a : α<VAR>g : G<GOAL>g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>a : α<VAR>g : G<GOAL>g • a = a ↔ a ∈ fixedBy α g
<VAR>a b c : Ordinal.{u}<GOAL>0 ♯ a = a
<VAR>n k s : ℕ<VAR>hkn : k ≤ n<VAR>hsk : s ≤ k<GOAL>0 < (n - k)! * (k - s)! * s !
<VAR>n k s : ℕ<VAR>hkn : k ≤ n<VAR>hsk : s ≤ k<VAR>h : 0 < (n - k)! * (k - s)! * s !<GOAL>n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) = n.choose k * (k.choose s * s ! * (k - s)!) * (n - k)!
<VAR>n k s : ℕ<VAR>hkn : k ≤ n<VAR>hsk : s ≤ k<VAR>h : 0 < (n - k)! * (k - s)! * s !<GOAL>n.choose k * (k.choose s * s ! * (k - s)!) * (n - k)! = n !
<VAR>n k s : ℕ<VAR>hkn : k ≤ n<VAR>hsk : s ≤ k<VAR>h : 0 < (n - k)! * (k - s)! * s !<GOAL>n ! = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)
<VAR>n k s : ℕ<VAR>hkn : k ≤ n<VAR>hsk : s ≤ k<VAR>h : 0 < (n - k)! * (k - s)! * s !<GOAL>n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<GOAL>(gradedComm R 𝒜 ℬ).symm = gradedComm R ℬ 𝒜
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<GOAL>(TensorProduct.directSum R R ℬ 𝒜).trans ((TensorProduct.directSum R R 𝒜 ℬ).trans (LinearEquiv.ofLinear (gradedCommAux R 𝒜 ℬ) (gradedCommAux R ℬ 𝒜) ⋯ ⋯)).symm = ((TensorProduct.directSum R R ℬ 𝒜).trans (LinearEquiv.ofLinear (gradedCommAux R ℬ 𝒜) (gradedCommAux R 𝒜 ℬ) ⋯ ⋯)).trans (TensorProduct.directSum R R 𝒜 ℬ).symm
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a / c < b ↔ a < b * c
<VAR>m n k : ℕ<GOAL>m.Coprime (m * k + n) ↔ m.Coprime n
<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✝⁴ : NonUnitalNonAssocSemiring T<VAR>inst✝³ : FunLike F R S<VAR>inst✝² : NonUnitalRingHomClass F R S<VAR>S' : Type u_2<VAR>inst✝¹ : SetLike S' S<VAR>inst✝ : NonUnitalSubsemiringClass S' S<VAR>s : NonUnitalSubsemiring R<VAR>f : F<GOAL>↑(srange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>f : Ultrafilter (OnePoint X)<GOAL>↑f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' s ∉ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : HereditarilyLindelofSpace X<VAR>s : Set X<GOAL>IsLindelof s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : HereditarilyLindelofSpace X<VAR>s : Set X<GOAL>s ⊆ univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>(∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty) ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Finset (Set X)<GOAL>(∀ u ∈ t, IsOpen u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔ (∀ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, IsClosed z) → s ⊆ ⋃₀ ↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t) → ∃ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, s ⊆ z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Finset (Set X)<GOAL>(∀ u ∈ t, IsOpen u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔ (∀ u ∈ t, IsOpen u) → s ⊆ ⋃ x ∈ ↑t, xᶜ → ∃ a ∈ t, s ⊆ aᶜ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Finset (Set X)<VAR>x✝ : ∀ u ∈ t, IsOpen u<GOAL>(∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔ (¬∃ a ∈ t, s ⊆ aᶜ) → ¬s ⊆ ⋃ x ∈ ↑t, xᶜ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>r : R<VAR>h : r - 1 ∈ ⊥.jacobson<GOAL>IsUnit r
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>r : R<VAR>h : r - 1 ∈ ⊥.jacobson<VAR>s : R<VAR>hs : s * r - 1 ∈ ⊥<GOAL>IsUnit r
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>r : R<VAR>h : r - 1 ∈ ⊥.jacobson<VAR>s : R<VAR>hs : r * s = 1<GOAL>IsUnit r
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>h : IsConj σ τ<GOAL>σ.cycleType = τ.cycleType
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ π : Perm α<VAR>h : IsConj σ (π * σ * π⁻¹)<GOAL>σ.cycleType = (π * σ * π⁻¹).cycleType
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u_3<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>T : Type u_5<VAR>inst✝¹ : AddCommGroup T<VAR>inst✝ : Module (AdicCompletion I R) T<VAR>f g : AdicCompletion I M →ₗ[R] N<VAR>h : f ∘ₗ mk I M = g ∘ₗ mk I M<VAR>x : AdicCompletion I M<GOAL>f x = g x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : AEStronglyMeasurable f (μ.prod ν)<GOAL>Integrable f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y)) ν) ∧ Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Field R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h1 : 1 ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<GOAL>Function.Injective ⇑f
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Field R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h1 : 1 ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<VAR>r : R<VAR>hr : r ≠ 0<VAR>hr' : (algebraMap R A) r ∈ s<GOAL>False
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Field R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h1 : 1 ∉ s<VAR>inst✝¹ : FunLike F (Unitization R ↥s) A<VAR>inst✝ : AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<VAR>r : R<VAR>hr : r ≠ 0<VAR>hr' : r • 1 ∈ s<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set β<GOAL>(e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (↑e ⁻¹' s)).source
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>w₀ : { w // w.IsComplex }<VAR>x : K<GOAL>(mixedEmbedding K) x ∈ convexBodyLT' K f w₀ ↔ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧ |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>w₀ : { w // w.IsComplex }<VAR>x : K<GOAL>((∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)) ∧ ∀ (a : InfinitePlace K) (b : a.IsComplex), if ⟨a, b⟩ = w₀ then |(a.embedding x).re| < 1 ∧ |(a.embedding x).im| < ↑(f a) ^ 2 else a x < ↑(f a)) ↔ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧ |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>IsCompact s ↔ IsCompact univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<GOAL>M.Flat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed ⟨F, h⟩
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅<GOAL>∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅<GOAL>∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅<GOAL>∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>h : (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧ (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅<GOAL>sumLexLift f₁ f₂ g₁ g₂ a b = ∅
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>(((PInfty.f n ≫ (Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) ≫ PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op [n]))) ≫ PInfty.f n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op [n]))) ≫ PInfty.f n = PInfty.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>PInfty.f n ≫ ((Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) ≫ PInfty.f n = PInfty.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>PInfty.f n ≫ ((Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) ≫ PInfty.f n = PInfty.f n ≫ PInfty.f n