ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>E : K ⥤ J<VAR>inst✝ : HasLimit (E ⋙ F)<VAR>k : K<GOAL>pre F E ≫ π (E ⋙ F) k = π F (E.obj k)
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>E : K ⥤ J<VAR>inst✝ : HasLimit (E ⋙ F)<VAR>k : K<GOAL>(Cone.whisker E (cone F)).π.app k = π F (E.obj k)
<VAR>α : Type u_1<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>minOrder (ZMod p) = ↑p
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : ℕ → E<VAR>N : ℕ<VAR>huv : ∀ n ≥ N, u n = v n<VAR>hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k<VAR>d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k<GOAL>CauchySeq (d * fun n => ∏ k ∈ range (n + 1), v k)
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : ℕ → E<VAR>N : ℕ<VAR>huv : ∀ n ≥ N, u n = v n<VAR>hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k<VAR>d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k<GOAL>∀ n ≥ N, d n = d N
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : ℕ → E<VAR>N : ℕ<VAR>huv : ∀ n ≥ N, u n = v n<VAR>hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k<VAR>d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>∏ k ∈ range (n + 1), u k / v k = ∏ k ∈ range (N + 1), u k / v k
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : ℕ → E<VAR>N : ℕ<VAR>huv : ∀ n ≥ N, u n = v n<VAR>hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k<VAR>d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>∀ n ≥ N + 1, u n / v n = 1
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : ℕ → E<VAR>N : ℕ<VAR>huv : ∀ n ≥ N, u n = v n<VAR>hv : CauchySeq fun n => ∏ k ∈ range (n + 1), v k<VAR>d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>m : ℕ<VAR>hm : m ≥ N + 1<GOAL>u m / v m = 1
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>f : ℕ → G<VAR>hf : Multipliable f<GOAL>Tendsto f atTop (𝓝 1)
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>f : ℕ → G<VAR>hf : Multipliable f<GOAL>Tendsto f cofinite (𝓝 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>x y : S<GOAL>h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span {f}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f✝ : α ≃o β<VAR>s✝ t : UpperSet α<VAR>a : α<VAR>b : β<VAR>f : α ≃o β<VAR>s : UpperSet β<GOAL>↑((map f).symm s) = ↑((map f.symm) s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : f =o[l] g<VAR>hgk : IsBigOWith c l g k<VAR>hc : 0 < c<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hgk : IsBigOWith c l g k<VAR>hc : 0 < c<VAR>hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g<GOAL>∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hgk : IsBigOWith c l g k<VAR>hc : 0 < c<VAR>hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g<VAR>c' : ℝ<VAR>c'pos : 0 < c'<GOAL>IsBigOWith c' l f k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hgk : IsBigOWith c l g k<VAR>hc : 0 < c<VAR>hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g<VAR>c' : ℝ<VAR>c'pos : 0 < c'<VAR>this : 0 < c' / c<GOAL>IsBigOWith c' l f k
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set ↑(range f)<VAR>y : ↑(range f)<VAR>m : y ∈ s<GOAL>⟨f ↑⟨rangeSplitting f y, ⋯⟩, ⋯⟩ ∈ s
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set ↑(range f)<VAR>y : ↑(range f)<VAR>m : y ∈ s<GOAL>(fun x => ⟨rangeSplitting f ↑x, ⋯⟩) ((fun x => ⟨⟨f ↑x, ⋯⟩, ⋯⟩) ⟨rangeSplitting f y, ⋯⟩) = ⟨rangeSplitting f y, ⋯⟩
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set ↑(range f)<VAR>x : ↑s<GOAL>(fun x => ⟨⟨f ↑x, ⋯⟩, ⋯⟩) ((fun x => ⟨rangeSplitting f ↑x, ⋯⟩) x) = x
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>p : Partition 1<GOAL>p.parts = {1}
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>p : Partition 1<VAR>h : p.parts = replicate (card p.parts) 1<GOAL>p.parts = {1}
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>p : Partition 1<VAR>h : p.parts = replicate (card p.parts) 1<VAR>h' : card p.parts = 1<GOAL>p.parts = {1}
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : PartialOrder Γ✝<VAR>inst✝² : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝¹ : Zero Γ<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x + y ≠ 0<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>min x.order y.order ≤ (x + y).order
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : PartialOrder Γ✝<VAR>inst✝² : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝¹ : Zero Γ<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x + y ≠ 0<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>n : ℕ<VAR>hn : n < l.reverse.length<VAR>hn' : l.length - 1 - n < l.length<GOAL>l.reverse.nthLe n hn = l.nthLe (l.length - 1 - n) hn'
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>n : ℕ<VAR>hn : n < l.reverse.length<VAR>hn' : l.length - 1 - n < l.length<GOAL>l.nthLe (l.length - 1 - n) hn' = l.reverse.nthLe n hn
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>n : ℕ<VAR>hn : n < l.reverse.length<VAR>hn' : l.length - 1 - n < l.length<GOAL>l.nthLe (l.length - 1 - n) hn' = l.reverse.reverse.nthLe (l.reverse.length - 1 - n) ⋯
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<GOAL>∃ S, Unbounded r S ∧ type (Subrel r S) = (type r).cof.ord
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<VAR>hS : Unbounded r S<VAR>e : #↑S = (type r).cof<GOAL>∃ S, Unbounded r S ∧ type (Subrel r S) = (type r).cof.ord
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<VAR>hS : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>s : ↑S → ↑S → Prop<VAR>w✝ : IsWellOrder (↑S) s<VAR>e' : (#↑S).ord = type s<GOAL>∃ S, Unbounded r S ∧ type (Subrel r S) = (type r).cof.ord
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<VAR>hS : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>s : ↑S → ↑S → Prop<VAR>w✝ : IsWellOrder (↑S) s<VAR>e' : (#↑S).ord = type s<VAR>T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}<VAR>a : α<VAR>this : {b | ¬r (↑b) a}.Nonempty<GOAL>∃ b ∈ T, ¬r b a
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<VAR>hS : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>s : ↑S → ↑S → Prop<VAR>w✝ : IsWellOrder (↑S) s<VAR>e' : (#↑S).ord = type s<VAR>T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}<VAR>a : α<VAR>this : {b | ¬r (↑b) a}.Nonempty<VAR>b : ↑S := ⋯.min {b | ¬r (↑b) a} this<GOAL>∃ b ∈ T, ¬r b a
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<VAR>hS : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>s : ↑S → ↑S → Prop<VAR>w✝ : IsWellOrder (↑S) s<VAR>e' : (#↑S).ord = type s<VAR>T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}<VAR>a : α<VAR>this : {b | ¬r (↑b) a}.Nonempty<VAR>b : ↑S := ⋯.min {b | ¬r (↑b) a} this<VAR>ba : ¬r (↑b) a<GOAL>∃ b ∈ T, ¬r b a
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<VAR>hS : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>s : ↑S → ↑S → Prop<VAR>w✝ : IsWellOrder (↑S) s<VAR>e' : (#↑S).ord = type s<VAR>T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}<VAR>a : α<VAR>this : {b | ¬r (↑b) a}.Nonempty<VAR>b : ↑S := ⋯.min {b | ¬r (↑b) a} this<VAR>ba : ¬r (↑b) a<VAR>c : ↑S<VAR>h : ¬r ↑c ↑b<GOAL>¬s c ⟨↑b, ⋯⟩
<VAR>α : Type u_1<VAR>r✝ r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<VAR>hS : Unbounded r S<VAR>e : #↑S = (type r).cof<VAR>s : ↑S → ↑S → Prop<VAR>w✝ : IsWellOrder (↑S) s<VAR>e' : (#↑S).ord = type s<VAR>T : Set α := {a | ∃ (aS : a ∈ S), ∀ (b : ↑S), s b ⟨a, aS⟩ → r (↑b) a}<VAR>a : α<VAR>this : {b | ¬r (↑b) a}.Nonempty<VAR>b : ↑S := ⋯.min {b | ¬r (↑b) a} this<VAR>ba : ¬r (↑b) a<VAR>c : ↑S<VAR>h : ¬r ↑c ↑b<GOAL>¬s c b
<VAR>α : Type u_1<VAR>inst✝ : Mul α<VAR>a x y : α<GOAL>SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : DecidableEq κ<VAR>b : Basis ι A M<VAR>c : Basis κ A M<VAR>f : M →ₗ[A] M<GOAL>((toMatrix b b) f).det = ((toMatrix c c) f).det
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>i j : n<GOAL>(M.charmatrix i j).natDegree ≤ if i = j then 1 else 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>x : TruncatedWittVector p n R<VAR>i : Fin n<GOAL>coeff i (mk p fun i => coeff i x) = coeff i x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>a : R<VAR>x : M'<VAR>x' : M<VAR>hx : f x' = x<GOAL>IsInteger f (a • x)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>M' : Type u_3<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>a : R<VAR>x : M'<VAR>x' : M<VAR>hx : f x' = x<GOAL>f (a • x') = a • x
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>g : ↑Γ(X, X.basicOpen f)<GOAL>∃ f', X.basicOpen f' = X.basicOpen g
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>g : ↑Γ(X, X.basicOpen f)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<GOAL>∃ f', X.basicOpen f' = X.basicOpen g
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<VAR>x : ↑Γ(X, U)<VAR>n : ℕ<GOAL>∃ f', X.basicOpen f' = X.basicOpen (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩))
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<VAR>x : ↑Γ(X, U)<VAR>n : ℕ<GOAL>X.basicOpen (f * x) = X.basicOpen (x • ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩))
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<VAR>x : ↑Γ(X, U)<VAR>n : ℕ<GOAL>X.basicOpen f ⊓ X.basicOpen x = X.basicOpen ((X.presheaf.map (homOfLE ⋯).op) x) ⊓ X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<VAR>x : ↑Γ(X, U)<VAR>n : ℕ<GOAL>X.basicOpen f ⊓ X.basicOpen x = X.basicOpen f ⊓ X.basicOpen x ⊓ X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<VAR>x : ↑Γ(X, U)<VAR>n : ℕ<GOAL>X.basicOpen f ⊓ X.basicOpen x ≤ X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<VAR>x : ↑Γ(X, U)<VAR>n : ℕ<GOAL>X.basicOpen ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩) = X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)<VAR>x : ↑Γ(X, U)<VAR>n : ℕ<GOAL>IsUnit ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x => f ^ x) n, ⋯⟩)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : ↥(nonZeroDivisors R)<GOAL>0 < v.intValuationDef ↑x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : ↥(nonZeroDivisors R)<GOAL>0 < ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors)))
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>-y ≤ x ↔ -x ≤ y
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>it.atEnd = true ↔ r = []
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>utf8Len l + utf8Len r ≤ utf8Len l ↔ r = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>δ : α → Sort u_6<VAR>s : Set α<VAR>f✝ g✝ : (i : α) → δ i<VAR>inst✝ : (j : α) → Decidable (j ∈ s)<VAR>f f' g : α → β<VAR>t t' : Set α<VAR>h : EqOn f g (t ∩ s)<VAR>h' : EqOn f' g (t' ∩ sᶜ)<GOAL>EqOn (s.piecewise f f') g (s.ite t t')
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<VAR>u v : V<GOAL>(G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : DivisionRing α<VAR>p q : ℚ<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<VAR>hψ : ψ.IsPrimitive<VAR>a : ZMod n<GOAL>ψ a = 1 ↔ a = 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ψ : AddChar (ZMod n) C<VAR>hψ : ψ.IsPrimitive<VAR>a : ZMod n<VAR>h : ψ a = 1<GOAL>¬ψ.mulShift a ≠ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<GOAL>toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s✝ t r : Set α<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<GOAL>range ⇑(sigmaSet h) = ⋃ i, s i
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>((limitIsoLimitCurryCompLim G).inv ≫ (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).inv ≫ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).hom) ≫ limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim G).inv ≫ limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ (𝟙 ((Prod.braiding K J).functor ⋙ G)).app (k, j) = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim G).inv ≫ limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ 𝟙 (((Prod.braiding K J).functor ⋙ G).obj (k, j)) = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
<VAR>X✝ : Type u<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : SequentialSpace X✝<VAR>X Y : Sequential<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<VAR>x : (forget Sequential).obj X<GOAL>({ toFun := ⇑f, continuous_toFun := ⋯ } ≫ { toFun := ⇑f.symm, continuous_toFun := ⋯ }) x = (𝟙 X) x
<VAR>X✝ : Type u<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : SequentialSpace X✝<VAR>X Y : Sequential<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<VAR>x : (forget Sequential).obj Y<GOAL>({ toFun := ⇑f.symm, continuous_toFun := ⋯ } ≫ { toFun := ⇑f, continuous_toFun := ⋯ }) x = (𝟙 Y) x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : MulZeroClass α<VAR>s t : Finset α<VAR>hs : s.Nonempty<GOAL>0 ⊆ 0 * s
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<GOAL>IsIntegral A (discr K ⇑b • a * x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<GOAL>IsIntegral A (discr K ⇑b • a * x)