ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<VAR>h_disj : Pairwise (Disjoint on fun i => ↑i)<GOAL>Pairwise (Disjoint on Subtype.val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<VAR>h_disj : Pairwise (Disjoint on fun i => ↑i)<GOAL>IntegrableOn (fun x => κ.densityProcess ν n a x s) (⋃ i, ↑i) (ν a)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hα : ¬α.IsZero<GOAL>chainLength α β • x = ⁅coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hα : ¬α.IsZero<VAR>x' : L := ⋯.choose<GOAL>chainLength α β • x = ⁅coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hα : ¬α.IsZero<VAR>x' : L := ⋯.choose<VAR>h : x' ∈ rootSpace H ⇑(chainTop (⇑α) β) ∧ x' ≠ 0<GOAL>chainLength α β • x = ⁅coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<VAR>x' : L := ⋯.choose<VAR>h : x' ∈ rootSpace H ⇑(chainTop (⇑α) β) ∧ x' ≠ 0<VAR>k : K<VAR>hx : k • x' ∈ rootSpace H ⇑(chainTop (⇑α) β)<GOAL>chainLength α β • k • x' = ⁅coroot α, k • x'⁆
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : P →ₗ[R] M<GOAL>(trace R P) ((g ∘ₗ f) ∘ₗ h) = (trace R M) ((h ∘ₗ g) ∘ₗ f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>n : ℕ<VAR>inst✝ : Nontrivial R<VAR>b : Basis (Fin n) R M<VAR>x✝ : Fin n<GOAL>b.flag x✝.castSucc < b.flag x✝.succ
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Ioc a b).card = ↑b - ↑a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s<VAR>inst✝ : p.NeBot<GOAL>ContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s<VAR>inst✝ : p.NeBot<VAR>x : α<VAR>hx : x ∈ s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s<VAR>inst✝ : p.NeBot<VAR>x : α<VAR>hx : x ∈ s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set α<VAR>ht : t ∈ 𝓝[s] x<VAR>H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s<VAR>inst✝ : p.NeBot<VAR>x : α<VAR>hx : x ∈ s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set α<VAR>ht : t ∈ 𝓝[s] x<VAR>H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<VAR>n : ι<VAR>hFc : ContinuousOn (F n) s<VAR>hF : ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x✝ y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>closedBall x δ * s = x • cthickening δ s
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<GOAL>0 ≤ chaar K₀ K
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>this : chaar K₀ K ∈ (fun K => Icc 0 ↑(index ↑K ↑K₀)) K<GOAL>0 ≤ chaar K₀ K
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K : Compacts G<VAR>this : 0 ≤ chaar K₀ K ∧ chaar K₀ K ≤ ↑(index ↑K ↑K₀)<GOAL>0 ≤ chaar K₀ K
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>n : ℕ<GOAL>f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>a : A i<GOAL>(((lift R A) fun {i} => maps) ∘ₐ ι R A i) a = maps a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p : α → Prop<VAR>f✝ : (a : α) → p a → β<VAR>x✝ : Option α<VAR>g : β → γ<VAR>f : (a : α) → p a → β<VAR>x : Option α<VAR>H : ∀ (a : α), a ∈ x → p a<GOAL>Option.map g (pmap f x H) = pmap (fun a h => g (f a h)) x H
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<GOAL>(∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n
<VAR>a b m n✝ p d n : ℕ<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<GOAL>(∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d.factorization ≤ n.factorization
<VAR>a b m n✝ p✝ d n : ℕ<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<VAR>h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p<VAR>p : ℕ<VAR>hp : ¬Prime p<GOAL>d.factorization p ≤ n.factorization p
<VAR>a b m n✝ p✝ d n : ℕ<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<VAR>h : ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p<VAR>p : ℕ<VAR>hp : ¬Prime p<GOAL>0 ≤ 0
<VAR>R : Type u<VAR>inst✝³ : LinearOrder R<VAR>inst✝² : AddMonoid R<VAR>inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : Tropical R<VAR>n : ℕ<GOAL>(x + y) ^ n = x ^ n + y ^ n
<VAR>R : Type u<VAR>inst✝³ : LinearOrder R<VAR>inst✝² : AddMonoid R<VAR>inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : Tropical R<VAR>n : ℕ<VAR>h : x ≤ y<GOAL>(x + y) ^ n = x ^ n + y ^ n
<VAR>R : Type u<VAR>inst✝³ : LinearOrder R<VAR>inst✝² : AddMonoid R<VAR>inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : Tropical R<VAR>n : ℕ<VAR>h : y ≤ x<GOAL>(x + y) ^ n = x ^ n + y ^ n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<GOAL>∃ J, mk0 I = mk0 J ∧ (algebraMap R S) M ∈ ↑J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<GOAL>∃ J, mk0 I = mk0 J ∧ (algebraMap R S) M ∈ ↑J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<GOAL>∃ J, mk0 I = mk0 J ∧ (algebraMap R S) M ∈ ↑J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<GOAL>Ideal.span {b} ∣ Ideal.span {(algebraMap R S) M} * ↑I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<GOAL>∀ r ∈ Ideal.span {(algebraMap R S) M}, ∀ s ∈ ↑I, r * s ∈ Ideal.span {b}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<VAR>r' : S<VAR>hr' : r' ∈ Ideal.span {(algebraMap R S) M}<VAR>a : S<VAR>ha : a ∈ ↑I<GOAL>r' * a ∈ Ideal.span {b}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<VAR>r' : S<VAR>hr' : (algebraMap R S) M ∣ r'<VAR>a : S<VAR>ha : a ∈ ↑I<GOAL>b ∣ r' * a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<VAR>r' : S<VAR>hr' : (algebraMap R S) M ∣ r'<VAR>a : S<VAR>ha : a ∈ ↑I<VAR>q : S<VAR>r : R<VAR>r_mem : r ∈ finsetApprox bS adm<VAR>lt : abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)<GOAL>b ∣ r' * a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<VAR>r' : S<VAR>hr' : (algebraMap R S) M ∣ r'<VAR>a : S<VAR>ha : a ∈ ↑I<VAR>q : S<VAR>r : R<VAR>r_mem : r ∈ finsetApprox bS adm<VAR>lt : abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)<GOAL>q * b ∣ r' * a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<VAR>r' : S<VAR>hr' : (algebraMap R S) M ∣ r'<VAR>a : S<VAR>ha : a ∈ ↑I<VAR>q : S<VAR>r : R<VAR>r_mem : r ∈ finsetApprox bS adm<VAR>lt : abv ((Algebra.norm R) ((algebraMap R S) r * a - q * b)) < abv ((Algebra.norm R) b)<GOAL>q * b ∣ r' * a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<VAR>r' : S<VAR>hr' : (algebraMap R S) M ∣ r'<VAR>a : S<VAR>ha : a ∈ ↑I<VAR>q : S<VAR>r : R<VAR>r_mem : r ∈ finsetApprox bS adm<VAR>lt : abv ((Algebra.norm R) ((algebraMap R S) r * a - q * b)) < abv ((Algebra.norm R) b)<GOAL>(algebraMap R S) r * a ∣ r' * a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁸ : EuclideanDomain R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : IsDomain S<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra R K<VAR>inst✝¹² : IsFractionRing R K<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : FiniteDimensional K L<VAR>inst✝⁹ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁸ : IsScalarTower R K L<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝³ : Infinite R<VAR>inst✝² : DecidableEq R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>I : ↥(Ideal S)⁰<VAR>M : R := ∏ m ∈ finsetApprox bS adm, m<VAR>hM : (algebraMap R S) M ≠ 0<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0<VAR>r' : S<VAR>hr' : (algebraMap R S) M ∣ r'<VAR>a : S<VAR>ha : a ∈ ↑I<VAR>q : S<VAR>r : R<VAR>r_mem : r ∈ finsetApprox bS adm<VAR>lt : abv ((Algebra.norm R) ((algebraMap R S) r * a - q * b)) < abv ((Algebra.norm R) b)<GOAL>r ∣ M
<GOAL>Module.rank ℚ ℂ = 𝔠
<GOAL>Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ
<VAR>U : Type ?u.16921<VAR>inst✝⁴ : Quiver U<VAR>V : Type ?u.16927<VAR>inst✝³ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.16949<VAR>inst✝² : Quiver W<VAR>ψ : V ⥤q W<VAR>inst✝¹ : HasInvolutiveReverse U<VAR>inst✝ : HasInvolutiveReverse V<VAR>u : U<VAR>e : Star u<GOAL>(fun e => ⟨e.fst, reverse e.snd⟩) ((fun e => ⟨e.fst, reverse e.snd⟩) e) = e
<VAR>U : Type ?u.16921<VAR>inst✝⁴ : Quiver U<VAR>V : Type ?u.16927<VAR>inst✝³ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.16949<VAR>inst✝² : Quiver W<VAR>ψ : V ⥤q W<VAR>inst✝¹ : HasInvolutiveReverse U<VAR>inst✝ : HasInvolutiveReverse V<VAR>u : U<VAR>e : Costar u<GOAL>(fun e => ⟨e.fst, reverse e.snd⟩) ((fun e => ⟨e.fst, reverse e.snd⟩) e) = e
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s₁ s₂ : ↥S<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) = (fromLocalizedModule S f) (LocalizedModule.mk m s₂)