ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i < n<GOAL>↑p ^ i ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i < n<VAR>this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)<GOAL>↑p ^ i ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i < n<VAR>this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)<GOAL>∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i < n<GOAL>∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i < n<GOAL>¬coeff ⟨i, hin⟩ ((WittVector.truncate n) (↑p ^ i)) = coeff ⟨i, hin⟩ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i < n<GOAL>¬1 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i < n<VAR>this : Nontrivial R<GOAL>¬1 = 0
<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✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f✝ : β → α<VAR>t : Finset γ<VAR>h : (s ×ˢ t).Nonempty<VAR>f : β × γ → α<GOAL>(s ×ˢ t).sup' h f = t.sup' ⋯ fun i' => s.sup' ⋯ fun i => f (i, i')
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>Function.Commute ⇑f fun x => x + ↑-[n+1]
<VAR>p✝ : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p✝)<VAR>inst✝² : Fintype ι<VAR>p : ℝ≥0∞<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>β : ι → Type u_5<VAR>hp : p ≠ ⊤<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>f : PiLp p β<GOAL>↑‖f‖₊ = ↑((∑ i : ι, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a✝ b : α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∉ s₂<VAR>x : α<VAR>this : ¬(x = a ∧ x ∈ s₂)<GOAL>x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : LinearOrder α<VAR>a b c d : α<GOAL>a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>inst✝³ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝² : G.PreservesZeroMorphisms<VAR>inst✝¹ : HasKernel f<VAR>inst✝ : HasKernel (G.map f)<VAR>Z : C<VAR>h : Z ⟶ X<VAR>w : h ≫ f = 0<GOAL>G.map h ≫ G.map f = 0
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>inst✝³ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝² : G.PreservesZeroMorphisms<VAR>inst✝¹ : HasKernel f<VAR>inst✝ : HasKernel (G.map f)<VAR>Z : C<VAR>h : Z ⟶ X<VAR>w : h ≫ f = 0<GOAL>(G.map (kernel.lift f h w) ≫ kernelComparison f G) ≫ equalizer.ι (G.map f) 0 = kernel.lift (G.map f) (G.map h) ⋯ ≫ equalizer.ι (G.map f) 0
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A : Type u₃<VAR>inst✝⁸ : Category.{v₃, u₃} A<VAR>inst✝⁷ : EssentiallySmall.{w, v₁, u₁} C<VAR>B : Type u_1<VAR>inst✝⁶ : Category.{?u.102181, u_1} B<VAR>F : A ⥤ B<VAR>inst✝⁵ : HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A<VAR>inst✝⁴ : ((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F<VAR>inst✝³ : G.IsCoverDense J<VAR>inst✝² : G.IsContinuous K J<VAR>inst✝¹ : G.Full<VAR>inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj<VAR>P Q : Cᵒᵖ ⥤ A<VAR>f : P ⟶ Q<VAR>h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj<GOAL>K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f ↔ J.W f
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A : Type u₃<VAR>inst✝⁸ : Category.{v₃, u₃} A<VAR>inst✝⁷ : EssentiallySmall.{w, v₁, u₁} C<VAR>B : Type u_1<VAR>inst✝⁶ : Category.{?u.102181, u_1} B<VAR>F : A ⥤ B<VAR>inst✝⁵ : HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A<VAR>inst✝⁴ : ((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F<VAR>inst✝³ : G.IsCoverDense J<VAR>inst✝² : G.IsContinuous K J<VAR>inst✝¹ : G.Full<VAR>inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj<VAR>P Q : Cᵒᵖ ⥤ A<VAR>f : P ⟶ Q<VAR>h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj<VAR>h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g<GOAL>K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f ↔ J.W f
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A : Type u₃<VAR>inst✝⁸ : Category.{v₃, u₃} A<VAR>inst✝⁷ : EssentiallySmall.{w, v₁, u₁} C<VAR>B : Type u_1<VAR>inst✝⁶ : Category.{?u.102181, u_1} B<VAR>F : A ⥤ B<VAR>inst✝⁵ : HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A<VAR>inst✝⁴ : ((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F<VAR>inst✝³ : G.IsCoverDense J<VAR>inst✝² : G.IsContinuous K J<VAR>inst✝¹ : G.Full<VAR>inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj<VAR>P Q : Cᵒᵖ ⥤ A<VAR>f : P ⟶ Q<VAR>h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj<VAR>h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g<GOAL>LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f) ↔ LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) 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>P✝ : Type u_3<VAR>inst✝⁸ : AddCommMonoid P✝<VAR>inst✝⁷ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf1 : (LinearMap.ker f).FG<VAR>hf2 : (LinearMap.ker g).FG<VAR>hsur : Surjective ⇑f<GOAL>(LinearMap.ker (g ∘ₗ f)).FG
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁸ : AddCommMonoid P✝<VAR>inst✝⁷ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf1 : (LinearMap.ker f).FG<VAR>hf2 : (LinearMap.ker g).FG<VAR>hsur : Surjective ⇑f<GOAL>(comap f (LinearMap.ker g)).FG
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁸ : AddCommMonoid P✝<VAR>inst✝⁷ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf1 : (LinearMap.ker f).FG<VAR>hf2 : (LinearMap.ker g).FG<VAR>hsur : Surjective ⇑f<GOAL>(map f (comap f (LinearMap.ker g))).FG
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>P✝ : Type u_3<VAR>inst✝⁸ : AddCommMonoid P✝<VAR>inst✝⁷ : Module R✝ P✝<VAR>f✝ : M✝ →ₗ[R✝] P✝<VAR>R : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf1 : (LinearMap.ker f).FG<VAR>hf2 : (LinearMap.ker g).FG<VAR>hsur : Surjective ⇑f<GOAL>(comap f (LinearMap.ker g) ⊓ LinearMap.ker f).FG
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>f : Γ → R<VAR>h : (Function.support f).IsPWO<GOAL>{ coeff := f, isPWO_support' := h }.coeff = coeff 0 ↔ f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>hs : s.offDiag.Nonempty<GOAL>(↑s).infsep = s.offDiag.inf' hs (uncurry dist)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : p ^ (k - s + 1) = 2<GOAL>p = 2
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : p ^ (k - s + 1) = 2<GOAL>↑p = 2
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : p ^ (k - s + 1) = 2<GOAL>↑p ^ (k - s).succ = 2 ^ ?m.293414
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : p ^ (k - s + 1) = 2<GOAL>ℕ
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : p ^ (k - s + 1) = 2<GOAL>↑p ^ (k - s).succ = 2
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H I a b c : OplaxFunctor B C<VAR>f g : a ⟶ b<VAR>h i : b ⟶ c<VAR>η : f ⟶ g<VAR>θ : h ⟶ i<VAR>b✝ : B<GOAL>((fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) f h i θ ≫ (fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η i).app b✝ = ((fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η h ≫ (fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) g h i θ).app b✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<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>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherian R M<VAR>rs rs' : List R<VAR>h2 : rs ~ rs'<VAR>h3 : IsWeaklyRegular M rs<VAR>h4 : ⊤ ≠ Ideal.ofList rs • ⊤<GOAL>IsRegular M rs'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<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>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherian R M<VAR>rs rs' : List R<VAR>h2 : rs ~ rs'<VAR>h3 : IsWeaklyRegular M rs<VAR>h4 : ⊤ ≠ Ideal.ofList rs • ⊤<GOAL>∀ r ∈ rs, r ∈ LocalRing.maximalIdeal R
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<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>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherian R M<VAR>rs rs' : List R<VAR>h2 : rs ~ rs'<VAR>h3 : IsWeaklyRegular M rs<VAR>h4 : ⊤ ≠ Ideal.ofList rs • ⊤<GOAL>⊤ ≠ Ideal.ofList rs' • ⊤
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<GOAL>IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>hS : S.Nonempty<GOAL>IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
<VAR>n : ℕ+<VAR>T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<GOAL>IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension (∅ ∪ {1}) A B
<VAR>n : ℕ+<VAR>T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<GOAL>IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>upperCrossingTime a b f N N ω = N
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hN' : N < Nat.find ⋯<GOAL>upperCrossingTime a b f N N ω = N
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f✝ : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω✝ : Ω<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hN' : ¬N < Nat.find ⋯<GOAL>upperCrossingTime a b f N N ω = N
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝ : Norm E<VAR>l✝ : Filter α<VAR>f : α → ℝ<VAR>l : Filter α<GOAL>(fun x => ‖↑(f x)‖) =Θ[l] f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.107784, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(δ 0 1 (snd φ)).v p q hpq = (-(↑(fst φ)).comp (Cochain.ofHom φ) ⋯).v p q hpq
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y : C<VAR>hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr<VAR>hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl<GOAL>EckmannHilton.IsUnital (fun x x_1 => leftAdd X Y x x_1) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type u_4<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R N<VAR>inst✝¹ : IsArtinian R M<VAR>inst✝ : IsArtinian R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>h : LinearMap.range f = LinearMap.ker g<GOAL>∀ (a : Submodule R N), Submodule.map f (Submodule.comap f a) = a ⊓ LinearMap.range f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type u_4<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R N<VAR>inst✝¹ : IsArtinian R M<VAR>inst✝ : IsArtinian R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>h : LinearMap.range f = LinearMap.ker g<GOAL>∀ (a : Submodule R N), Submodule.comap g (Submodule.map g a) = a ⊔ LinearMap.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<GOAL>Tendsto defaultRatCDF atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<GOAL>(fun x => 0) =ᶠ[atBot] defaultRatCDF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<GOAL>∃ a, ∀ b ≤ a, 0 = defaultRatCDF b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>q : ℚ<VAR>hq : q ≤ -1<GOAL>-1 < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Ioo s t).card = 2 ^ (t.card - s.card) - 2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace B<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>inst✝ : Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>(Pretrivialization.linearMapAt R e b) ((Pretrivialization.symmₗ R e b) y) = y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace B<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>inst✝ : Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>↑(linearEquivAt R e b hb) ((Pretrivialization.symmₗ R e b) y) = y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Tendsto (fun x => f x / r) l atBot ↔ Tendsto f l atTop
<VAR>a✝ b : Cardinal.{u}<VAR>n m : ℕ<VAR>a : Cardinal.{u_1}<GOAL>Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
<VAR>a✝ b : Cardinal.{u}<VAR>n m : ℕ<VAR>a : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<GOAL>Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
<VAR>a✝ b : Cardinal.{u}<VAR>n m : ℕ<VAR>a : Cardinal.{u_1}<VAR>h : a < ℵ₀<GOAL>Prime a ↔ ℵ₀ ≤ a ∨ ∃ p, a = ↑p ∧ Nat.Prime p
<VAR>a✝ b : Cardinal.{u}<VAR>n m a : ℕ<VAR>h : ↑a < ℵ₀<GOAL>Prime ↑a ↔ ℵ₀ ≤ ↑a ∨ ∃ p, ↑a = ↑p ∧ Nat.Prime p
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>inst✝⁶ : Preadditive C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{v₁, u_1} D<VAR>inst✝⁴ : Preadditive D<VAR>E : Type u_2<VAR>inst✝³ : Category.{v₁, u_2} E<VAR>inst✝² : Preadditive E<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>G : D ⥤ E<VAR>inst✝ : G.Additive<VAR>ι✝¹ : Type<VAR>fintype✝¹ : Fintype ι✝¹<VAR>X✝¹ : ι✝¹ → C<VAR>i✝ : ((F ⋙ G).mapMat_.obj (Mat_.mk ι✝¹ X✝¹)).ι<VAR>ι✝ : Type<VAR>fintype✝ : Fintype ι✝<VAR>X✝ : ι✝ → C<VAR>j✝ : ((F.mapMat_ ⋙ G.mapMat_).obj (Mat_.mk ι✝ X✝)).ι<VAR>f : Mat_.mk ι✝¹ X✝¹ ⟶ Mat_.mk ι✝ X✝<GOAL>((F ⋙ G).mapMat_.map f ≫ ((fun M => eqToIso ⋯) (Mat_.mk ι✝ X✝)).hom) i✝ j✝ = (((fun M => eqToIso ⋯) (Mat_.mk ι✝¹ X✝¹)).hom ≫ (F.mapMat_ ⋙ G.mapMat_).map f) i✝ j✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (y * z + x) y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (x + y * z) y
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsVonNBounded 𝕜 s<GOAL>Bornology.IsBounded s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsVonNBounded 𝕜 s<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1<GOAL>Bornology.IsBounded s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsVonNBounded 𝕜 s<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1<VAR>a : 𝕜<VAR>ha : ρ < ‖a‖<GOAL>Bornology.IsBounded s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsVonNBounded 𝕜 s<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>a : 𝕜<VAR>ha : ρ < ‖a‖<VAR>hρball : s ⊆ a • Metric.ball 0 1<GOAL>Bornology.IsBounded s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<VAR>h : Bornology.IsVonNBounded 𝕜 s<VAR>ρ : ℝ<VAR>hρ : ρ > 0<VAR>a : 𝕜<VAR>ha : ρ < ‖a‖<VAR>hρball : s ⊆ Metric.ball 0 (‖a‖ * 1)<GOAL>Bornology.IsBounded s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a b : α<GOAL>interior (Icc a b) = Ioo a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l x : Filter α<VAR>g : Filter (α → β)<VAR>h : Filter (β → γ)<GOAL>h.seq (g.seq x) = ((map (fun x x_1 => x ∘ x_1) h).seq g).seq x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l x : Filter α<VAR>g : Filter (α → β)<VAR>h : Filter (β → γ)<VAR>s : Set (α → γ)<VAR>hs : s ∈ (map (fun x x_1 => x ∘ x_1) h).seq g<VAR>t : Set α<VAR>ht : t ∈ x<GOAL>s.seq t ∈ h.seq (g.seq x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l x : Filter α<VAR>g : Filter (α → β)<VAR>h : Filter (β → γ)<VAR>s : Set (β → γ)<VAR>hs : s ∈ h<VAR>t : Set β<VAR>ht : t ∈ g.seq x<GOAL>s.seq t ∈ ((map (fun x x_1 => x ∘ x_1) h).seq g).seq x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y : P<GOAL>affineSegment R x y = affineSegment R y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<GOAL>z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x