ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>a : α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<GOAL>s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>a : α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<GOAL>s ∈ ⋃ i ∈ {s | a ∈ s ∧ s ∈ b}, (𝓟 i).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>a : α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<GOAL>DirectedOn (𝓟 ⁻¹'o fun x x_1 => x ≥ x_1) {s | a ∈ s ∧ s ∈ b}
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>a : α<VAR>s : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<GOAL>{s | a ∈ s ∧ s ∈ b}.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : β → Measure α<VAR>h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => (f b) s<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>borel ℝ≥0∞ ≤ MeasurableSpace.map (fun μ => μ s) (MeasurableSpace.map f inst✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : β → Measure α<VAR>h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => (f b) s<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun μ => μ s) ∘ f) inst✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>-[[a, b]] = [[-a, -b]]
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>t.card = s.card / P.parts.card ↔ t.card ≠ s.card / P.parts.card + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<VAR>a : t.card = s.card / P.parts.card ∨ t.card = s.card / P.parts.card + 1<GOAL>t.card = s.card / P.parts.card ↔ t.card ≠ s.card / P.parts.card + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<VAR>a : t.card = s.card / P.parts.card ∨ t.card = s.card / P.parts.card + 1<VAR>b : ¬(t.card = s.card / P.parts.card ∧ t.card = s.card / P.parts.card + 1)<GOAL>t.card = s.card / P.parts.card ↔ t.card ≠ s.card / P.parts.card + 1
<VAR>i j : ℕ<VAR>h : i < j<GOAL>i.dist j = max i j - min i j
<VAR>i j : ℕ<VAR>h : i ≥ j<GOAL>i.dist j = max i j - min i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>x : Subtype p<GOAL>Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ ↑x
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)<VAR>hp : ∀ J ∈ π, (πi J).IsPartition<VAR>hc : l.bDistortion = true → π.compl.distortion ≤ c<GOAL>l.MemBaseSet I c r (π.biUnionTagged πi)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)<VAR>hp : ∀ J ∈ π, (πi J).IsPartition<VAR>hc : l.bDistortion = true → π.compl.distortion ≤ c<VAR>hD : l.bDistortion = true<GOAL>(π.biUnionTagged πi).distortion ≤ c
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)<VAR>hp : ∀ J ∈ π, (πi J).IsPartition<VAR>hc : l.bDistortion = true → π.compl.distortion ≤ c<VAR>hD : l.bDistortion = true<GOAL>∃ π', π'.iUnion = ↑I \ (π.biUnionTagged πi).iUnion ∧ π'.distortion ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a : α<VAR>f : α →₀ M<GOAL>(erase a f) a = 0
<VAR>σ✝ : Type u<VAR>R✝ : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<GOAL>#(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
<VAR>σ✝ : Type u<VAR>R✝ : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>h✝ : Subsingleton R<GOAL>#(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
<VAR>σ✝ : Type u<VAR>R✝ : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>h✝ : Nontrivial R<GOAL>#(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
<VAR>σ✝ : Type u<VAR>R✝ : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>h✝¹ : Nontrivial R<VAR>h✝ : IsEmpty σ<GOAL>#(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
<VAR>σ✝ : Type u<VAR>R✝ : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nonempty σ<GOAL>#(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>pNilradical R p = nilradical R
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B₁ B₂ : Set X<VAR>h₁ : IsBlock G B₁<VAR>h₂ : IsBlock G B₂<GOAL>IsBlock G (B₁ ∩ B₂)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B₁ B₂ : Set X<VAR>h₁ : IsBlock G B₁<VAR>h₂ : IsBlock G B₂<GOAL>∀ (g : G), g • (B₁ ∩ B₂) = B₁ ∩ B₂ ∨ Disjoint (g • (B₁ ∩ B₂)) (B₁ ∩ B₂)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B₁ B₂ : Set X<VAR>h₁ : IsBlock G B₁<VAR>h₂ : IsBlock G B₂<VAR>g : G<GOAL>g • (B₁ ∩ B₂) = B₁ ∩ B₂ ∨ Disjoint (g • (B₁ ∩ B₂)) (B₁ ∩ B₂)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B₁ B₂ : Set X<VAR>h₁ : IsBlock G B₁<VAR>h₂ : IsBlock G B₂<VAR>g : G<GOAL>g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B₁ B₂ : Set X<VAR>h₁✝ : IsBlock G B₁<VAR>h₂ : IsBlock G B₂<VAR>g : G<VAR>h₁ : g • B₁ = B₁<GOAL>g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B₁ B₂ : Set X<VAR>h₁✝ : IsBlock G B₁<VAR>h₂ : IsBlock G B₂<VAR>g : G<VAR>h₁ : Disjoint (g • B₁) B₁<GOAL>g • B₁ ∩ g • B₂ = B₁ ∩ B₂ ∨ Disjoint (g • B₁ ∩ g • B₂) (B₁ ∩ B₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>z : Sym2 α<GOAL>z ∈ fromRel ⋯ ↔ z ∈ {z | ¬z.IsDiag}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c✝ d a b c x : α<GOAL>a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c✝ d a b c x : α<GOAL>(a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h_ne : A ≠ 0<GOAL>∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>toFinsupp✝¹ toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).toFinsupp = { toFinsupp := toFinsupp✝¹ }.toFinsupp + { toFinsupp := toFinsupp✝ }.toFinsupp
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : StandardBorelSpace α<VAR>inst✝¹ : Infinite α<VAR>inst✝ : Countable α<GOAL>Nonempty (α ≃ᵐ ↑(range Nat.cast))
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : StandardBorelSpace α<VAR>inst✝¹ : Infinite α<VAR>inst✝ : Countable α<VAR>this : PolishSpace ↑(range Nat.cast)<GOAL>Nonempty (α ≃ᵐ ↑(range Nat.cast))
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : StandardBorelSpace α<VAR>inst✝¹ : Infinite α<VAR>inst✝ : Countable α<VAR>this : PolishSpace ↑(range Nat.cast)<GOAL>ℕ ≃ ↑(range Nat.cast)
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u<VAR>inst✝⁶ : NormedAddCommGroup E✝<VAR>inst✝⁵ : NormedSpace 𝕜 E✝<VAR>F : Type v<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝² : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n✝ : ℕ∞<VAR>x✝ : (i : ι) → E i<VAR>n : ℕ<VAR>x : (i : ι) → E i<GOAL>‖iteratedFDeriv 𝕜 n (⇑f) x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u<VAR>inst✝⁶ : NormedAddCommGroup E✝<VAR>inst✝⁵ : NormedSpace 𝕜 E✝<VAR>F : Type v<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝² : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n✝ : ℕ∞<VAR>x✝ : (i : ι) → E i<VAR>n : ℕ<VAR>x : (i : ι) → E i<GOAL>‖f.iteratedFDeriv n x‖ ≤ ↑((Fintype.card ι).descFactorial n) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>x : Π₀ (i : ι), β i<VAR>i : ι<VAR>inst✝ : (i' : ι) → Decidable (i' ∈ {i})<VAR>j : ι<GOAL>((single i (x i)).piecewise (erase i x) {i}) j = x j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>x : Π₀ (i : ι), β i<VAR>i : ι<VAR>inst✝ : (i' : ι) → Decidable (i' ∈ {i})<VAR>j : ι<GOAL>(if j ∈ {i} then (single i (x i)) j else (erase i x) j) = x j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>inst✝ : PosSMulStrictMono α β<VAR>h : a < 0<GOAL>a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : CancelCommMonoid α<VAR>s : Set α<VAR>a : α<GOAL>ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : CancelCommMonoid α<VAR>s : Set α<VAR>a : α<GOAL>(ThreeGPFree s ∧ (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) → ThreeGPFree (insert a s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : CancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ThreeGPFree s<VAR>ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b<VAR>ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a<VAR>b : α<VAR>hb : b ∈ insert a s<VAR>c : α<VAR>hc : c ∈ insert a s<VAR>d : α<VAR>hd : d ∈ insert a s<VAR>h : b * d = c * c<GOAL>b = c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝ : CancelCommMonoid α<VAR>s : Set α<VAR>a : α<VAR>hs : ThreeGPFree s<VAR>ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b<VAR>ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a<VAR>b : α<VAR>hb : b = a ∨ b ∈ s<VAR>c : α<VAR>hc : c = a ∨ c ∈ s<VAR>d : α<VAR>hd : d = a ∨ d ∈ s<VAR>h : b * d = c * c<GOAL>b = c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>S T : Seq (Seq1 α)<GOAL>(S.append T).join = S.join.append T.join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>S T : Seq (Seq1 α)<GOAL>IsBisimulation fun s1 s2 => ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>S T : Seq (Seq1 α)<GOAL>∃ s S_1 T_1, (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 0<GOAL>clog b r = 0
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 0<GOAL>⌊r⁻¹⌋₊ < b ∨ b ≤ 1
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 0<VAR>hb : b ≤ 1<GOAL>⌊r⁻¹⌋₊ < b ∨ b ≤ 1
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hr : r ≤ 0<VAR>hb : 1 < b<GOAL>⌊r⁻¹⌋₊ < b ∨ b ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : α →ₘ[μ] β<VAR>H : f.toGerm = g.toGerm<GOAL>↑↑f = ↑↑g
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommRing P<GOAL>coeSubmodule S ⊥ = ⊥
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hlt : q < p<GOAL>∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hlt : q < p<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hlt : q < p<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)<GOAL>∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hlt : q < p<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)<GOAL>∀ (x_1 : ℕ), (C < ↑x_1 ^ (p - q) ∧ 1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < ↑x_1 ^ (-q)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>hlt✝ : q < p<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)<VAR>n : ℕ<VAR>hnC : C < ↑n ^ (p - q)<VAR>hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>hlt✝ : q < p<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)<VAR>n : ℕ<VAR>hnC : C < ↑n ^ (p - q)<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>hn : 0 < ↑n<GOAL>∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>hlt✝ : q < p<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)<VAR>n : ℕ<VAR>hnC : C < ↑n ^ (p - q)<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>hn : 0 < ↑n<GOAL>C < ↑n ^ (-q) * ↑n ^ p
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<GOAL>Function.Surjective (WType.elim (↥(closure s)) (Subfield.operate s))
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<GOAL>Set.range (WType.elim (↥(closure s)) (Subfield.operate s)) = Set.univ
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Preorder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hb : b ≤ 0<VAR>h : a ≤ 1<GOAL>b ≤ a * b
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ t : R<VAR>m : M<VAR>hm : m ∈ ⨆ k, (f.genEigenspace μ) k<GOAL>m ∈ ⨆ k, ((t • f).genEigenspace (t * μ)) k
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ t : R<VAR>m : M<VAR>hm : ∃ k, ((f - μ • 1) ^ k) m = 0<GOAL>∃ k, ((t • f - (t * μ) • 1) ^ k) m = 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ t : R<VAR>m : M<VAR>hm : ∃ k, ((f - μ • 1) ^ k) m = 0<VAR>k : ℕ<VAR>hk : ((f - μ • 1) ^ k) m = 0<GOAL>((t • f - (t * μ) • 1) ^ k) m = 0
<VAR>x y : ℝ<VAR>h : 0 ≤ x<GOAL>√x ^ 2 = x
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>i : ℤ<VAR>g : G<VAR>a : α<GOAL>g ^ (i + ↑(period g a)) • a = g ^ i • a
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommMonoid β<VAR>n : ℕ<GOAL>stoppedProcess u τ n = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω | τ ω = i}.indicator (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommMonoid β<VAR>n : ℕ<GOAL>{a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i) = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω | τ ω = i}.indicator (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommMonoid β<VAR>n i : ℕ<GOAL>i ∈ Finset.Iio n ↔ i ∈ Finset.range n
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Ioi a).card = n - 1 - ↑a
<VAR>F : Type u<VAR>E✝ : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E✝<VAR>inst✝⁵ : Algebra F E✝<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>E : Type v<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hfd : FiniteDimensional F E<GOAL>finSepDegree F E = finrank F E
<VAR>F : Type u<VAR>E✝ : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E✝<VAR>inst✝⁵ : Algebra F E✝<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>E : Type v<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hfd : FiniteDimensional F E<GOAL>finSepDegree F ↥⊤ = finrank F ↥⊤
<VAR>F : Type u<VAR>E✝ : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E✝<VAR>inst✝⁵ : Algebra F E✝<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>E : Type v<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hfd : FiniteDimensional F E<VAR>L : IntermediateField F E<VAR>x : E<VAR>h : (fun K => finSepDegree F ↥K = finrank F ↥K) L<GOAL>(fun K => finSepDegree F ↥K = finrank F ↥K) (restrictScalars F (↥L)⟮x⟯)
<VAR>F : Type u<VAR>E✝ : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E✝<VAR>inst✝⁵ : Algebra F E✝<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>E : Type v<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>hfd : FiniteDimensional F E<VAR>L : IntermediateField F E<VAR>x : E<VAR>h : finSepDegree F ↥L = finrank F ↥L<VAR>M : IntermediateField (↥L) E := (↥L)⟮x⟯<VAR>heq : finSepDegree F ↥L * finSepDegree ↥L ↥M = finrank F ↥L * finrank ↥L ↥M<VAR>this : Algebra.IsAlgebraic ↥L ↥M<GOAL>finSepDegree F ↥(restrictScalars F M) = finrank F ↥(restrictScalars F M)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>S ∈ rightTransversals T ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>(∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g) ↔ ∀ (g : G), ∃! s, g * (↑s)⁻¹ ∈ T
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ : ?m.316755<VAR>F₂ : BilinForm R M<VAR>f : Module.End R₁ M₁<GOAL>(∀ (x y : M₁), (B₁ (f x)) y = (B₁ x) ((-f) y)) ↔ ∀ (x y : M₁), (B₁ (f x)) y = ((-B₁) x) (f y)
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t : Set A<VAR>a : M<VAR>hs : IsSubmonoid s<VAR>h : a ∈ s<GOAL>a ^ 0 ∈ s
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t : Set A<VAR>a : M<VAR>hs : IsSubmonoid s<VAR>h : a ∈ s<GOAL>1 ∈ s
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t : Set A<VAR>a : M<VAR>hs : IsSubmonoid s<VAR>h : a ∈ s<VAR>n : ℕ<GOAL>a ^ (n + 1) ∈ s
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t : Set A<VAR>a : M<VAR>hs : IsSubmonoid s<VAR>h : a ∈ s<VAR>n : ℕ<GOAL>a ^ n * a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : CommGroup G<VAR>inst✝² : TopologicalGroup G<VAR>f : α → G<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : T1Space G<VAR>hf : Multipliable f<GOAL>(mulSupport f).Countable
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>inst✝² : MulZeroOneClass M₀<VAR>inst✝¹ : Nontrivial M₀<VAR>G₀ : Type u_3<VAR>inst✝ : GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>inst✝² : MulZeroOneClass M₀<VAR>inst✝¹ : Nontrivial M₀<VAR>G₀ : Type u_3<VAR>inst✝ : GroupWithZero G₀<VAR>a : G₀<VAR>h : a ≠ 0<GOAL>a⁻¹ * a⁻¹⁻¹ = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra F L<VAR>hL : ∀ (x : E), Splits (algebraMap F L) (minpoly F x)<GOAL>Fintype.card (E →ₐ[F] L) = finrank F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra F L<VAR>hL : ∀ (x : E), Splits (algebraMap F L) (minpoly F x)<GOAL>Fintype.card (E →ₐ[F] AlgebraicClosure L) = finrank F E
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g✝ : ι → Set X<VAR>g : ι' → ι<VAR>hf : LocallyFinite f<VAR>hg : InjOn g {i | (f (g i)).Nonempty}<VAR>x : X<VAR>t : Set X<VAR>htx : t ∈ 𝓝 x<VAR>htf : {i | (f i ∩ t).Nonempty}.Finite<GOAL>∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite