ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{u_8, u_1} C<VAR>inst✝⁸ : Category.{?u.49739, u_2} C₁<VAR>inst✝⁷ : Category.{?u.49743, u_3} C₂<VAR>inst✝⁶ : Category.{?u.49747, u_4} C₃<VAR>inst✝⁵ : Category.{u_10, u_5} D₁<VAR>inst✝⁴ : Category.{u_9, u_6} D₂<VAR>inst✝³ : Category.{?u.49759, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>hf : W f<GOAL>(homEquiv W L₁ L₂) (isoOfHom L₁ W f hf).inv = (isoOfHom L₂ W f hf).inv
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I✝ J : Ideal R<VAR>N P : Submodule R M<VAR>S✝ : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>S : Submodule R M'<VAR>I : Ideal R<GOAL>I • comap f S ≤ comap f (I • S)
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I✝ J : Ideal R<VAR>N P : Submodule R M<VAR>S✝ : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>S : Submodule R M'<VAR>I : Ideal R<VAR>r : R<VAR>hr : r ∈ I<VAR>x : M<VAR>hx : x ∈ comap f S<GOAL>r • x ∈ comap f (I • S)
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I✝ J : Ideal R<VAR>N P : Submodule R M<VAR>S✝ : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>S : Submodule R M'<VAR>I : Ideal R<VAR>r : R<VAR>hr : r ∈ I<VAR>x : M<VAR>hx : f x ∈ S<GOAL>f (r • x) ∈ I • S
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I✝ J : Ideal R<VAR>N P : Submodule R M<VAR>S✝ : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>S : Submodule R M'<VAR>I : Ideal R<VAR>r : R<VAR>hr : r ∈ I<VAR>x : M<VAR>hx : f x ∈ S<GOAL>r • f x ∈ I • S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] t<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<GOAL>{x | ∃ y, x ⋖ y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<GOAL>{x | ∃ y, x ⋖ y}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<GOAL>∀ (a : Set α), IsOpen a → {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<GOAL>{x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<GOAL>{x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<GOAL>{x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<VAR>t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}<GOAL>{x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<VAR>t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}<VAR>this : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a<GOAL>{x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<VAR>t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}<VAR>z : α → α<VAR>hz : ∀ x ∈ t, z x < x<VAR>h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a<VAR>this : t.PairwiseDisjoint fun x => Ioc (z x) x<GOAL>{x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<VAR>t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}<VAR>z : α → α<VAR>hz : ∀ x ∈ t, z x < x<VAR>h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a<VAR>this : t.PairwiseDisjoint fun x => Ioc (z x) x<VAR>x : α<VAR>hx : x ∈ t<GOAL>IsOpen (Ioc (z x) x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>a✝ : Nontrivial α<VAR>s : Set α := {x | ∃ y, x ⋖ y}<VAR>y : α → α<VAR>hy : ∀ x ∈ s, x ⋖ y x<VAR>Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x<VAR>a : Set α<VAR>ha : IsOpen a<VAR>t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}<VAR>z : α → α<VAR>hz : ∀ x ∈ t, z x < x<VAR>h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a<VAR>this : t.PairwiseDisjoint fun x => Ioc (z x) x<VAR>x : α<VAR>hx : x ∈ t<GOAL>Ioc (z x) x = Ioo (z x) (y x)
<VAR>m n : ℕ<GOAL>m + n + 2 = (m + 1 + n).succ
<VAR>m n : ℕ<GOAL>m + n + 2 = m + 1 + n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)<VAR>g : ↑sᶜ ≃ ↑(range ⇑f)ᶜ<GOAL>∃ g, ∀ (x : ↑s), g ↑x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h✝ : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)<VAR>g : ↑sᶜ ≃ ↑(range ⇑f)ᶜ<VAR>h : α ≃ β := (Set.sumCompl s).symm.trans (((ofInjective ⇑f ⋯).sumCongr g).trans (Set.sumCompl (range ⇑f)))<GOAL>∃ g, ∀ (x : ↑s), g ↑x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : ↑s ↪ β<VAR>h✝ : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)<VAR>g : ↑sᶜ ≃ ↑(range ⇑f)ᶜ<VAR>h : α ≃ β := (Set.sumCompl s).symm.trans (((ofInjective ⇑f ⋯).sumCongr g).trans (Set.sumCompl (range ⇑f)))<VAR>x : α<VAR>hx : x ∈ s<GOAL>h ↑⟨x, hx⟩ = f ⟨x, hx⟩
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<GOAL>∃ n f', toLaurent f' = f * T ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>∀ (p q : R[T;T⁻¹]), (∃ n f', toLaurent f' = p * T ↑n) → (∃ n f', toLaurent f' = q * T ↑n) → ∃ n f', toLaurent f' = (p + q) * T ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℤ<VAR>a : R<GOAL>∃ n_1 f', toLaurent f' = C a * T n * T ↑n_1
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>s : Finset (Box ι)<GOAL>∀ᶠ (t : Finset (ι × ℝ)) in atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>s : Finset (Box ι)<VAR>val✝ : Fintype ι<GOAL>∀ᶠ (t : Finset (ι × ℝ)) in atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J✝ : Box ι<VAR>i✝ : ι<VAR>x : ℝ<VAR>inst✝ : Finite ι<VAR>s : Finset (Box ι)<VAR>val✝ : Fintype ι<VAR>t : Finset (ι × ℝ)<VAR>ht : t ≥ s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)}<VAR>I J : Box ι<VAR>hJ : J ∈ s<VAR>J' : Box ι<VAR>hJ' : J' ∈ splitMany I t<VAR>i : ι<GOAL>{(i, J.lower i), (i, J.upper i)} ⊆ t
<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>inst✝ : Module.Finite R M<GOAL>Function.Surjective ⇑(ofTensorProduct I M)
<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>inst✝ : Module.Finite R M<VAR>n : ℕ<VAR>p : (Fin n → R) →ₗ[R] M<VAR>hp : Function.Surjective ⇑p<GOAL>Function.Surjective ⇑(ofTensorProduct I M)
<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>inst✝ : Module.Finite R M<VAR>n : ℕ<VAR>p : (Fin n → R) →ₗ[R] M<VAR>hp : Function.Surjective ⇑p<VAR>f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p<VAR>g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M := map I p ∘ₗ ofTensorProduct I (Fin n → R)<VAR>hfg : f = g<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(ofTensorProduct I M)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommSemiring E<VAR>inst✝⁵ : Semiring K<VAR>inst✝⁴ : SMul F E<VAR>inst✝³ : Algebra E K<VAR>inst✝² : CommSemiring F<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsScalarTower F E K<VAR>L : Subalgebra F K<VAR>ι : Type u_4<VAR>bL : Basis ι F ↥L<GOAL>toSubmodule L = span F (Set.range fun i => ↑(bL i))
<VAR>r p : ℝ≥0<VAR>h : p ≠ 0<GOAL>r < p⁻¹ ↔ r * p < 1
<VAR>n : ℕ<VAR>α β γ : TypeVec.{u} n<VAR>F : TypeVec.{u} n → Type v<VAR>inst✝¹ : MvFunctor F<VAR>P : α ⟹ TypeVec.repeat n Prop<VAR>R : α ⊗ α ⟹ TypeVec.repeat n Prop<VAR>inst✝ : LawfulMvFunctor F<VAR>x : F α<GOAL>∀ (u : F fun i => Subtype ((fun i x => ofRepeat (P i x)) i)), (fun i => Subtype.val) <$$> u = x ↔ subtypeVal P <$$> toSubtype P <$$> u = x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p1 p2 p1a : P<VAR>hp1a : p1a ∈ s<VAR>v1 : V<VAR>hv1 : v1 ∈ vectorSpan k s<VAR>hv1p : p1 = v1 +ᵥ p1a<VAR>p2a : P<VAR>hp2a : p2a ∈ s<VAR>v2 : V<VAR>hv2 : v2 ∈ vectorSpan k s<VAR>hv2p : p2 = v2 +ᵥ p2a<GOAL>p1 -ᵥ p2 ∈ vectorSpan k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p1 p2 p1a : P<VAR>hp1a : p1a ∈ s<VAR>v1 : V<VAR>hv1 : v1 ∈ vectorSpan k s<VAR>hv1p : p1 = v1 +ᵥ p1a<VAR>p2a : P<VAR>hp2a : p2a ∈ s<VAR>v2 : V<VAR>hv2 : v2 ∈ vectorSpan k s<VAR>hv2p : p2 = v2 +ᵥ p2a<GOAL>p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p1 p2 p1a : P<VAR>hp1a : p1a ∈ s<VAR>v1 : V<VAR>hv1 : v1 ∈ vectorSpan k s<VAR>hv1p : p1 = v1 +ᵥ p1a<VAR>p2a : P<VAR>hp2a : p2a ∈ s<VAR>v2 : V<VAR>hv2 : v2 ∈ vectorSpan k s<VAR>hv2p : p2 = v2 +ᵥ p2a<VAR>hv1v2 : v1 - v2 ∈ vectorSpan k s<GOAL>p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p1 p2 p1a : P<VAR>hp1a : p1a ∈ s<VAR>v1 : V<VAR>hv1 : v1 ∈ vectorSpan k s<VAR>hv1p : p1 = v1 +ᵥ p1a<VAR>p2a : P<VAR>hp2a : p2a ∈ s<VAR>v2 : V<VAR>hv2 : v2 ∈ vectorSpan k s<VAR>hv2p : p2 = v2 +ᵥ p2a<VAR>hv1v2 : v1 - v2 ∈ vectorSpan k s<GOAL>p1a -ᵥ p2a ∈ vectorSpan k s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>((p + q).sum fun e a => f a * x ^ e) = (p.sum fun e a => f a * x ^ e) + q.sum fun e a => f a * x ^ e
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<GOAL>sepDegree F K = sepDegree E K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<GOAL>sepDegree F K = sepDegree F ↥(separableClosure E K)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>this : IsScalarTower F (↥(separableClosure E K)) K<GOAL>sepDegree F K = sepDegree F ↥(separableClosure E K)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>this : IsScalarTower F (↥(separableClosure E K)) K<GOAL>Module.rank F ↥(IntermediateField.map (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K) (separableClosure F ↥(separableClosure E K))) = sepDegree F ↥(separableClosure E K)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>b : α i<GOAL>update f i '' Ico (f i) b = Ico f (update f i b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>A : E<VAR>U : ↥(unitary E)<GOAL>‖A * ↑U‖ = ‖((↑U)⋆ * A⋆)⋆‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>A : E<VAR>U : ↥(unitary E)<GOAL>‖((↑U)⋆ * A⋆)⋆‖ = ‖(↑U)⋆ * A⋆‖
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<GOAL>(blockDiagonal M).det = ∏ k : o, (M k).det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<GOAL>∑ σ : Perm (n × o), ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i = ∏ x : o, ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M x (σ i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<GOAL>∑ σ : Perm (n × o), ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i = ∑ p ∈ univ.pi fun x => univ, ∏ x ∈ univ.attach, ↑↑(sign (p ↑x ⋯)) * ∏ i : n, M (↑x) ((p ↑x ⋯) i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<GOAL>∑ σ : Perm (n × o), ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i = ∑ x : (a : o) → a ∈ univ → Perm n, ∏ x_1 : o, ↑↑(sign (x x_1 ⋯)) * ∏ x_2 : n, M x_1 ((x x_1 ⋯) x_2) x_2
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<VAR>preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ<GOAL>∑ σ : Perm (n × o), ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i = ∑ x : (a : o) → a ∈ univ → Perm n, ∏ x_1 : o, ↑↑(sign (x x_1 ⋯)) * ∏ x_2 : n, M x_1 ((x x_1 ⋯) x_2) x_2
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<VAR>preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ<VAR>mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2<GOAL>∑ σ : Perm (n × o), ↑↑(sign σ) * ∏ i : n × o, blockDiagonal M (σ i) i = ∑ x : (a : o) → a ∈ univ → Perm n, ∏ x_1 : o, ↑↑(sign (x x_1 ⋯)) * ∏ x_2 : n, M x_1 ((x x_1 ⋯) x_2) x_2
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<VAR>preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ<VAR>mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2<GOAL>∑ x ∈ preserving_snd, ↑↑(sign x) * ∏ i : n × o, blockDiagonal M (x i) i = ∑ x : (a : o) → a ∈ univ → Perm n, ∏ x_1 : o, ↑↑(sign (x x_1 ⋯)) * ∏ x_2 : n, M x_1 ((x x_1 ⋯) x_2) x_2
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>o : Type u_3<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>M : o → Matrix n n R<VAR>preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (σ x).2 = x.2) univ<VAR>mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2<GOAL>∀ x ∈ univ, x ∉ preserving_snd → ↑↑(sign x) * ∏ i : n × o, blockDiagonal M (x i) i = 0
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>(a ^ n) ^ (↑n)⁻¹.val = a
<VAR>R : Type u<VAR>L : Type v<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}<VAR>hs : s.Nonempty<GOAL>sInf s = 0 ↔ Subsingleton M
<VAR>R : Type u<VAR>L : Type v<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}<VAR>hs : s.Nonempty<GOAL>sInf s = 0 ↔ lowerCentralSeries R L M 0 = ⊥
<VAR>R : Type u<VAR>L : Type v<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}<VAR>hs : s.Nonempty<VAR>h : lowerCentralSeries R L M 0 = ⊥<GOAL>sInf s = 0
<VAR>R : Type u<VAR>L : Type v<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}<VAR>hs : s.Nonempty<VAR>h : lowerCentralSeries R L M 0 = ⊥<GOAL>0 ∈ s ∨ s = ∅
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(basicOpen r))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>∀ u ∈ Set.range fun r => ↑(basicOpen r), IsOpen u
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)), a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r => ↑(basicOpen r), a ∈ v ∧ v ⊆ u
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<GOAL>sinZeta a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : Perm α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<GOAL>(↑(range s.card)).PairwiseDisjoint fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : Perm α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>hs : (↑s).Subsingleton<GOAL>(↑(range s.card)).PairwiseDisjoint fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : Perm α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>h✝ : (↑s).Nontrivial<GOAL>(↑(range s.card)).PairwiseDisjoint fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s