ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffOn I I' n f univ ↔ ContMDiff I I' n f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.encard = t.encard<GOAL>s.Finite ↔ t.Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>(↑(suffixLevenshtein C xs ys)).minimum ≤ (↑(suffixLevenshtein C xs (y :: ys))).minimum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>∀ (a : δ), a ∈ ↑(suffixLevenshtein C xs (y :: ys)) → (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>∀ (a : δ), a ∈ List.map (fun xs' => levenshtein C xs' (y :: ys)) xs.tails → (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>∀ (a : List α), a <:+ xs → (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a (y :: ys))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>a : List α<VAR>suff : a <:+ xs<GOAL>(List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a (y :: ys))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>a : List α<VAR>suff : a <:+ xs<GOAL>(List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ (↑(suffixLevenshtein C a ys)).minimum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>a : List α<VAR>suff : a <:+ xs<GOAL>(List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ (List.map (fun xs' => levenshtein C xs' ys) a.tails).minimum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>a : List α<VAR>suff : a <:+ xs<GOAL>∀ (a_1 : δ), a_1 ∈ List.map (fun xs' => levenshtein C xs' ys) a.tails → (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>a : List α<VAR>suff : a <:+ xs<VAR>a' : List α<VAR>suff' : a' <:+ a<GOAL>(List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a' ys)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>a : List α<VAR>suff : a <:+ xs<VAR>a' : List α<VAR>suff' : a' <:+ a<GOAL>levenshtein C a' ys ∈ List.map (fun xs' => levenshtein C xs' ys) xs.tails
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>a : List α<VAR>suff : a <:+ xs<VAR>a' : List α<VAR>suff' : a' <:+ a<GOAL>∃ a, a <:+ xs ∧ levenshtein C a ys = levenshtein C a' ys
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>s : R<VAR>n : ℕ<VAR>ih : span {s} ^ n = span {s ^ n}<GOAL>span {s} ^ (n + 1) = span {s ^ (n + 1)}
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime<VAR>I : Ideal R<VAR>this : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ i ∈ s, I ≤ f i<GOAL>↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime<VAR>I : Ideal R<VAR>this : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ i ∈ s, I ≤ f i<VAR>aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x, ∃ (_ : x ∈ s), I ≤ f x<GOAL>↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime<VAR>I : Ideal R<VAR>this aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x ∈ s, I ≤ f x<GOAL>↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime<VAR>I : Ideal R<VAR>this aux : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) → ∃ x ∈ s, I ≤ f x<VAR>x✝ : ∃ i ∈ s, I ≤ f i<VAR>i : ι<VAR>his : i ∈ s<VAR>hi : I ≤ f i<GOAL>↑(f i) ⊆ ⋃ i ∈ ↑s, ↑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>inst✝ : Fintype ↑s<VAR>A : Fintype ↑∅ := Fintype.ofIsEmpty<GOAL>s.toFinset = ∅ ↔ s = ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝⁴ : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : DecidableEq (Ideal A)<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ normalizedFactors I<GOAL>multiplicity (↑((normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = multiplicity L I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝⁴ : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : DecidableEq (Ideal A)<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ normalizedFactors I<GOAL>multiplicity (↑((idealFactorsEquivOfQuotEquiv f) ⟨↑⟨L, hL⟩, ⋯⟩)) J = multiplicity L I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝⁴ : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : DecidableEq (Ideal A)<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ normalizedFactors I<GOAL>∀ (l l' : { l // l ∣ I }), ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R (-n - 1) = -U R (n - 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hR : IsJacobson R<GOAL>IsJacobson S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>I : Ideal R<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hR : IsJacobson R<GOAL>∀ (P : Ideal S), P.IsPrime → P.jacobson = P
<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>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : SFinite μ<VAR>E' : Type u_7<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>L : Type u_8<VAR>inst✝ : _root_.RCLike L<VAR>f : α → L<VAR>g : β → L<VAR>s : Set α<VAR>t : Set β<GOAL>∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
<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>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : SFinite μ<VAR>E' : Type u_7<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>L : Type u_8<VAR>inst✝ : _root_.RCLike L<VAR>f : α → L<VAR>g : β → L<VAR>s : Set α<VAR>t : Set β<GOAL>∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N✝ : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N✝<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N✝<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N✝<VAR>g : N✝ →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>N : Submodule R M<GOAL>ker (rTensor Q N.mkQ) = range (rTensor Q N.subtype)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N✝ : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N✝<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N✝<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N✝<VAR>g : N✝ →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>N : Submodule R M<GOAL>Exact ⇑(rTensor Q N.subtype) ⇑(rTensor Q N.mkQ)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M₁<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid N₁<VAR>inst✝⁸ : AddCommMonoid N₂<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module R M₂<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : Module R N₂<VAR>inst✝² : Module R P<VAR>inst✝¹ : Preorder P<VAR>inst✝ : CovariantClass P P (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M₁<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid N₁<VAR>inst✝⁸ : AddCommMonoid N₂<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module R M₂<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : Module R N₂<VAR>inst✝² : Module R P<VAR>inst✝¹ : Preorder P<VAR>inst✝ : CovariantClass P P (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(∀ (a : M₁) (b : M₂), 0 ≤ Q₁ a + Q₂ b) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ φ ↔ ¬(T ∪ {Formula.not φ}).IsSatisfiable
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<GOAL>(∀ (M : T.ModelType), ↑M ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<VAR>h : ¬Nonempty (T ∪ {Formula.not φ}).ModelType<VAR>M : T.ModelType<GOAL>↑M ⊨ φ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<VAR>M : T.ModelType<VAR>h : ¬↑M ⊨ φ<GOAL>Nonempty (T ∪ {Formula.not φ}).ModelType
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<VAR>M : T.ModelType<VAR>h : ↑M ⊨ Formula.not φ<GOAL>Nonempty (T ∪ {Formula.not φ}).ModelType
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<VAR>M : T.ModelType<VAR>h : ↑M ⊨ Formula.not φ<VAR>ψ : L.Sentence<VAR>hψ : ψ ∈ T ∪ {Formula.not φ}<VAR>h' : ψ ∈ {Formula.not φ}<GOAL>↑M ⊨ ψ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ : L.Sentence<VAR>M : T.ModelType<VAR>h : ↑M ⊨ Formula.not φ<VAR>ψ : L.Sentence<VAR>hψ : ψ ∈ T ∪ {Formula.not φ}<VAR>h' : ψ ∈ {Formula.not φ}<GOAL>↑M ⊨ Formula.not φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b < ⊤ ↔ Finite a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>inst✝¹ : Fintype ↑s<VAR>inst✝ : Fintype ↑t<GOAL>s.toFinset ⊂ t.toFinset ↔ s ⊂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf : Continuous' f<GOAL>_root_.Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf : Continuous' f<GOAL>∀ (s : Set (Scott β)), IsOpen s → IsOpen (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>s : Set (Scott β)<VAR>hs : Monotone fun x => x ∈ s<VAR>hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }<VAR>hf : Monotone f<VAR>hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }<GOAL>Continuous' (s ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>s : Set (Scott β)<VAR>hs : Monotone fun x => x ∈ s<VAR>hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }<VAR>hf : Monotone f<VAR>hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }<GOAL>OmegaCompletePartialOrder.Continuous { toFun := s ∘ f, monotone' := ?intro.intro.hf }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>s : Set (Scott β)<VAR>hs : Monotone fun x => x ∈ s<VAR>hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }<VAR>hf : Monotone f<VAR>hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }<GOAL>Monotone (s ∘ f)
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : ζ ∈ primitiveRoots (finrank K L) K<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ (finrank K L)<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ (finrank K L)<VAR>σ : L ≃ₐ[K] L<VAR>hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ (finrank K L)<VAR>σ : L ≃ₐ[K] L<VAR>hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ<VAR>hσ' : orderOf σ = Fintype.card (L ≃ₐ[K] L)<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ (finrank K L)<VAR>σ : L ≃ₐ[K] L<VAR>hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ<VAR>hσ' : orderOf σ = Fintype.card (L ≃ₐ[K] L)<VAR>this : (minpoly K σ.toLinearMap).IsRoot ζ<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ (finrank K L)<VAR>σ : L ≃ₐ[K] L<VAR>hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ<VAR>hσ' : orderOf σ = Fintype.card (L ≃ₐ[K] L)<VAR>this : (minpoly K σ.toLinearMap).IsRoot ζ<VAR>v : L<VAR>hv : Module.End.HasEigenvector σ.toLinearMap ζ v<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ (finrank K L)<VAR>σ : L ≃ₐ[K] L<VAR>hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ<VAR>hσ' : orderOf σ = Fintype.card (L ≃ₐ[K] L)<VAR>this : (minpoly K σ.toLinearMap).IsRoot ζ<VAR>v : L<VAR>hv : Module.End.HasEigenvector σ.toLinearMap ζ v<VAR>hv' : ∀ (n : ℕ), (σ.toLinearMap ^ n) v = ζ ^ n • v<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝⁵ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra K L<VAR>inst✝² : IsGalois K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsCyclic (L ≃ₐ[K] L)<VAR>hK : (primitiveRoots (finrank K L) K).Nonempty<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ (finrank K L)<VAR>σ : L ≃ₐ[K] L<VAR>hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ<VAR>hσ' : orderOf σ = Fintype.card (L ≃ₐ[K] L)<VAR>this : (minpoly K σ.toLinearMap).IsRoot ζ<VAR>v : L<VAR>hv : Module.End.HasEigenvector σ.toLinearMap ζ v<VAR>hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v<GOAL>∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁴ : CommRing R₂<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R₂ M₂<VAR>e✝ : Basis ι R M<VAR>v✝ : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>N : Type u_9<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>b✝ : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>b : Basis ι R M<VAR>v : ι' → M<VAR>e : ι ≃ ι'<VAR>i✝ j✝ : ι'<GOAL>(b.reindex e).toMatrix v i✝ j✝ = (b.toMatrix v).submatrix (⇑e.symm) _root_.id i✝ j✝
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = g ≫ h<VAR>inst✝² : HasCoequalizer f g<VAR>inst✝¹ : HasCoequalizer (G.map f) (G.map g)<VAR>inst✝ : PreservesColimit (parallelPair f g) G<VAR>W : D<VAR>k : G.obj Y ⟶ W<VAR>wk : G.map f ≫ k = G.map g ≫ k<GOAL>G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv ≫ coequalizer.desc k wk = k
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x y : M₀<VAR>h : IsUnit x<GOAL>inverse x * (x * y) = y