ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>m : Set X → ℝ≥0∞<VAR>s : Set X<GOAL>Tendsto (fun r => (pre m r) s) (𝓝[>] 0) (𝓝 ((mkMetric' m) s))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>m : Set X → ℝ≥0∞<VAR>s : Set X<GOAL>Tendsto ((fun r => (pre m r) s) ∘ Subtype.val) atBot (𝓝 ((mkMetric' m) s))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m✝ : Set X → ℝ≥0∞<VAR>r : ℝ≥0∞<VAR>μ : OuterMeasure X<VAR>s✝ : Set X<VAR>m : Set X → ℝ≥0∞<VAR>s : Set X<GOAL>Tendsto ((fun r => (pre m r) s) ∘ Subtype.val) atBot (𝓝 (⨆ i, (pre m ↑i) s))
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<GOAL>0 < ∫ (x : E), u x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<GOAL>Integrable u μ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<GOAL>0 < μ (support u)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>t : α → β<GOAL>⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>t : α → β<GOAL>⨆ x ∈ {a} ∪ s, t x = t a ⊔ ⨆ x ∈ s, t x
<VAR>α✝ : Type u_1<VAR>l l₁ : List α✝<VAR>a : α✝<VAR>l₂ : List α✝<VAR>h : l <+ l₁ ++ a :: l₂<GOAL>l <+ l₁ ++ l₂ ∨ a ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>i : α<GOAL>∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>i i' : α<GOAL>update f i 0 i' ≤ f i'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>i i' : α<GOAL>(if i' = i then 0 else f i') ≤ f i'
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝³ : Category.{uC', uC} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>F f : J → C<VAR>t : Bicone f<VAR>ht : IsColimit t.toCocone<VAR>j : J<VAR>j' : Discrete J<GOAL>t.toCocone.ι.app j' ≫ t.π j = t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom ⋯ else 0)
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝³ : Category.{uC', uC} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>F f : J → C<VAR>t : Bicone f<VAR>ht : IsColimit t.toCocone<VAR>j : J<VAR>j' : Discrete J<GOAL>t.toCocone.ι.app j' ≫ t.π j = (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom ⋯ else 0).ι.app j'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsPathConnected (range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsPathConnected (f '' univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>(¬∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C) ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝² : Preorder ι<VAR>G : ι → Type w<VAR>inst✝¹ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>α : Type u_1<VAR>i : ι<VAR>x : α → G i<VAR>a : α<GOAL>(f (Structure.Sigma.mk f i (x a)).fst i ⋯) (Structure.Sigma.mk f i (x a)).snd = x a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>a : α<GOAL>_root_.Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → _root_.Disjoint (f i) a
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<GOAL>(comap C P).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<GOAL>(comap C P).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<GOAL>(comap C P).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<GOAL>(comap C P).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<GOAL>(comap C P).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<GOAL>(comap C P).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>this : ⊥.IsMaximal<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>this : ⊥.IsMaximal<GOAL>(comap (algebraMap (R ⧸ P') (Localization M)) (map (algebraMap (R ⧸ P') (Localization M)) ⊥)).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this : IsDomain (Localization M')<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this✝ : IsDomain (Localization M')<VAR>this : ⊥.IsMaximal<GOAL>⊥.IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this✝ : IsDomain (Localization M')<VAR>this : ⊥.IsMaximal<GOAL>(comap (IsLocalization.map (Localization M') (quotientMap P C ⋯) ⋯) ⊥).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this✝ : IsDomain (Localization M')<VAR>this : ⊥.IsMaximal<GOAL>(IsLocalization.map (Localization M') (quotientMap P C ⋯) ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this✝ : IsDomain (Localization M')<VAR>this : ⊥.IsMaximal<VAR>isloc : IsLocalization (Submonoid.map φ M) (Localization M')<GOAL>(IsLocalization.map (Localization M') (quotientMap P C ⋯) ⋯).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this : IsDomain (Localization M')<GOAL>(map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this : IsDomain (Localization M')<VAR>bot_maximal : ⊥.IsMaximal := (bot_quotient_isMaximal_iff P).mpr hP<GOAL>(map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥).IsMaximal
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this : IsDomain (Localization M')<VAR>bot_maximal : ⊥.IsMaximal := (bot_quotient_isMaximal_iff P).mpr hP<GOAL>Function.Bijective ⇑(algebraMap (R[X] ⧸ P) (Localization M'))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>inst✝ : Nontrivial R<VAR>hP' : ∀ (x : R), C x ∈ P → x = 0<VAR>P' : Ideal R := comap C P<VAR>hP'_prime : P'.IsPrime<VAR>m : R[X]<VAR>hmem_P : m ∈ P<VAR>hm : ⟨m, hmem_P⟩ ≠ 0<VAR>hm' : m ≠ 0<VAR>φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯<VAR>a : R ⧸ P' := (Polynomial.map (Quotient.mk P') m).leadingCoeff<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers a<VAR>hp0 : a ≠ 0<VAR>hM : 0 ∉ M<VAR>M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M<VAR>hM' : 0 ∉ M'<VAR>this : IsDomain (Localization M')<VAR>bot_maximal : ⊥.IsMaximal := (bot_quotient_isMaximal_iff P).mpr hP<GOAL>IsField (R[X] ⧸ P)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing 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>c d : R<VAR>x y✝ : M<VAR>b✝ : Basis ι R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>y : M<VAR>b : Basis (Fin n) R ↥N<VAR>hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0<VAR>hsp : ∀ (z : M), ∃ c, z + c • y ∈ N<GOAL>⇑(let_fun span_b := ⋯; Basis.mk ⋯ ⋯) = Fin.cons y (Subtype.val ∘ ⇑b)
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x y : (i : I) → f✝ i<VAR>i : I<VAR>inst✝ : Div γ<VAR>f : α → β<VAR>g₁ g₂ : α → γ<VAR>e₁ e₂ : β → γ<GOAL>extend f (g₁ / g₂) (e₁ / e₂) = extend f g₁ e₁ / extend f g₂ e₂
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>m✝ : Multiset α<VAR>inst✝ : CommMonoid α<VAR>m : Multiset α<GOAL>m = map (fun x => x.fst) Finset.univ.val
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x} / closedBall 1 δ = closedBall x δ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>J : Type w<VAR>inst✝¹ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>inst✝ : PreservesColimit F (forget C)<VAR>D : Cocone F<VAR>hD : IsColimit D<VAR>ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => (D.ι.app a.fst) a.snd<VAR>x : (forget C).obj D.pt<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>hE : IsColimit E := isColimitOfPreserves (forget C) hD<GOAL>∃ a, ff a = x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>J : Type w<VAR>inst✝¹ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>inst✝ : PreservesColimit F (forget C)<VAR>D : Cocone F<VAR>hD : IsColimit D<VAR>ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => (D.ι.app a.fst) a.snd<VAR>x : (forget C).obj D.pt<VAR>E : Cocone (F ⋙ forget C) := (forget C).mapCocone D<VAR>hE : IsColimit E := isColimitOfPreserves (forget C) hD<VAR>j : J<VAR>y : (F ⋙ forget C).obj j<VAR>hy : E.ι.app j y = x<GOAL>∃ a, ff a = x
<VAR>x✝ : ℂ<GOAL>L δ x✝ = 1 x✝
<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>r : α → α → Prop<VAR>a b c d x : α<VAR>h✝ : ∀ (y : α), r y x → Acc r y<VAR>H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y<VAR>y : α<VAR>hyx : r y x<GOAL>Acc (Relation.TransGen r) y
<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>r : α → α → Prop<VAR>a b c d x : α<VAR>h✝ : ∀ (y : α), r y x → Acc r y<VAR>H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y<VAR>y z : α<VAR>hyz : Relation.TransGen r y z<VAR>hzx : r z x<GOAL>Acc (Relation.TransGen r) y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module B M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : IsScalarTower R B M<VAR>inst✝ : SMulCommClass A B M<VAR>p : AddSubmonoid M<VAR>hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p<VAR>hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p<VAR>ab : A ⊗[R] B<VAR>m : M<VAR>x✝ : m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier<GOAL>0 • m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module B M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : IsScalarTower R B M<VAR>inst✝ : SMulCommClass A B M<VAR>p : AddSubmonoid M<VAR>hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p<VAR>hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p<VAR>ab : A ⊗[R] B<VAR>m : M<VAR>a : A<VAR>b : B<VAR>hm : m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier<GOAL>a ⊗ₜ[R] b • m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module B M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : IsScalarTower R B M<VAR>inst✝ : SMulCommClass A B M<VAR>p : AddSubmonoid M<VAR>hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p<VAR>hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p<VAR>ab : A ⊗[R] B<VAR>m : M<VAR>z w : A ⊗[R] B<VAR>hz : m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier → z • m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier<VAR>hw : m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier → w • m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier<VAR>hm : m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier<GOAL>(z + w) • m ∈ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>H : ∀ x ∈ s, f x ∈ t<GOAL>s.card = ∑ a ∈ t, (filter (fun x => f x = a) s).card
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : SMul R L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : MulActionHomClass F R L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>t : R<VAR>x : L<GOAL>μ (t • x) = t • μ x
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : SMul R L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : MulActionHomClass F R L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>t : R<VAR>x : L<VAR>contra : ¬μ (t • x) = t • μ x<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : SMul R L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : MulActionHomClass F R L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>t : R<VAR>x : L<VAR>contra : ¬μ (t • x) = t • μ x<VAR>g : L → Submodule R M := fun x => ⨆ k, ((f x).genEigenspace (μ x)) k<GOAL>False