ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.448795, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>K₁ L₁ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>e₁ : T₁ ≅ CochainComplex.mappingCone.triangleh φ₁<VAR>K₂ L₂ : CochainComplex C ℤ<VAR>φ₂ : K₂ ⟶ L₂<VAR>e₂ : T₂ ≅ CochainComplex.mappingCone.triangleh φ₂<VAR>a'' : K₁ ⟶ K₂<VAR>ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>b'' : L₁ ⟶ L₂<VAR>hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)<VAR>γ : T₁ ⟶ T₂ := e₁.hom ≫ CochainComplex.mappingCone.trianglehMapOfHomotopy H ≫ e₂.inv<VAR>comm₂ : T₁.mor₂ ≫ γ.hom₃ = γ.hom₂ ≫ T₂.mor₂<VAR>comm₃ : T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map γ.hom₁ = γ.hom₃ ≫ T₂.mor₃<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<GOAL>esymm σ R n = ∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1)) 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<GOAL>esymm σ R n = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1)) 1
<VAR>n : ℕ<GOAL>Λ n ≠ 0 ↔ IsPrimePow n
<GOAL>Λ 1 ≠ 0 ↔ IsPrimePow 1
<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>Λ n ≠ 0 ↔ IsPrimePow n
<VAR>α β γ : Type u<VAR>F : Type → Type v<VAR>inst✝ : Alternative F<VAR>h : Decidable False<GOAL>guard False = failure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<GOAL>0 ≤ μ.toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<GOAL>VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict μ.toSignedMeasure univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<VAR>x✝ : j ⊆ univ<GOAL>↑0 j ≤ ↑μ.toSignedMeasure j
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousMul G<VAR>H : Subgroup G<VAR>g : G<VAR>hg : ↑H ∈ 𝓝 g<GOAL>IsOpen ↑H
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousMul G<VAR>H : Subgroup G<VAR>g : G<VAR>hg : ↑H ∈ 𝓝 g<VAR>x : G<VAR>hx : x ∈ ↑H<GOAL>↑H ∈ 𝓝 x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousMul G<VAR>H : Subgroup G<VAR>g : G<VAR>hg : ↑H ∈ 𝓝 g<VAR>x : G<VAR>hx : x ∈ ↑H<VAR>hg' : g ∈ H<GOAL>↑H ∈ 𝓝 x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousMul G<VAR>H : Subgroup G<VAR>g : G<VAR>hg : ↑H ∈ 𝓝 g<VAR>x : G<VAR>hx : x ∈ ↑H<VAR>hg' : g ∈ H<VAR>this : Filter.Tendsto (fun y => y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)<GOAL>↑H ∈ 𝓝 x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>0 < ⌈a⌉₊ ↔ 0 < a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>x : α<VAR>n : ℕ<GOAL>(insertNth n x l).length ≤ l.length + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≤ l.length<GOAL>(insertNth n x l).length ≤ l.length + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : l.length < n<GOAL>(insertNth n x l).length ≤ l.length + 1
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Set C<VAR>x✝² x✝¹ : C<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>x✝ ∈ (full ∅).arrows x✝² x✝¹ ↔ x✝ ∈ ⊥.arrows x✝² x✝¹
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>m : M<VAR>a : R[M]<GOAL>a ∈ grade R m ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>m : M<VAR>a : R[M]<GOAL>(∃ b, a = Finsupp.single m b) ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>m : M<VAR>a : R[M]<GOAL>∀ (a_1 : R), a = Finsupp.single m a_1 ↔ (Finsupp.lsingle m) a_1 = a
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>m : M<VAR>a : R[M]<VAR>r : R<GOAL>a = Finsupp.single m r ↔ (Finsupp.lsingle m) r = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.Infinite<GOAL>s.ncard = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<GOAL>p.toOuterMeasure s = 1 ↔ p.support ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<VAR>h : ∑' (x : α), s.indicator (⇑p) x = 1<VAR>a : α<VAR>hap : a ∈ p.support<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<VAR>h : p.support ⊆ s<GOAL>∑' (x : α), s.indicator (⇑p) x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝ : Zero α<VAR>A : Matrix m m α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>h : (Matrix.fromBlocks A 0 C D).IsSymm<VAR>ha : A.IsDiag<VAR>hd : D.IsDiag<GOAL>(Matrix.fromBlocks A 0 C D).IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝ : Zero α<VAR>A : Matrix m m α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>h : (Matrix.fromBlocks A 0 C D).IsSymm<VAR>ha : A.IsDiag<VAR>hd : D.IsDiag<GOAL>(Matrix.fromBlocks A 0 0ᵀ D).IsDiag
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c a : ℝ<VAR>ha : 0 < a<GOAL>IntegrableOn (fun x => f (a * x)) (Ioi c) volume ↔ IntegrableOn f (Ioi (a * c)) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c a : ℝ<VAR>ha : 0 < a<GOAL>Integrable ((Ioi c).indicator fun x => f (a * x)) volume ↔ IntegrableOn f (Ioi (a * c)) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c a : ℝ<VAR>ha : 0 < a<GOAL>Integrable ((Ioi c).indicator fun x => f (a * x)) volume ↔ Integrable ((Ioi (a * c)).indicator f) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c a : ℝ<VAR>ha : 0 < a<GOAL>((Ioi c).indicator fun x => f (a * x)) = fun x => (Ioi (a * c)).indicator f (a * x)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<GOAL>(Ioi c).indicator (fun x => f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<GOAL>(Ioi c).indicator (fun x => f (a * x)) x = (Ioi c).indicator (f ∘ HMul.hMul a) x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f a = f b<GOAL>f (a⁻¹ * b) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<VAR>h : f a = f b<VAR>this : (f a)⁻¹ * f b = 1<GOAL>f (a⁻¹ * b) = 1
<VAR>a b n : ℕ<GOAL>(if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ ((k + n - 1) / n)) = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x x_1 => x ^ x_1
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<GOAL>Indep (⨆ n, s n) (limsup s f) κ μα
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<GOAL>⨆ a, ⨆ n ∈ ns a, s n = ⨆ n, s n
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<GOAL>⨆ j, ⨆ i, ⨆ (_ : j ∈ ns i), s j = ⨆ n, s n
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>n : ι<GOAL>⨆ i, ⨆ (_ : n ∈ ns i), s n = s n
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>n : ι<VAR>h : ⨆ i, ⨆ (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n<GOAL>⨆ i, ⨆ (_ : n ∈ ns i), s n = s n
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>n : ι<VAR>h : ⨆ i, ⨆ (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n<VAR>this : Nonempty (∃ i, n ∈ ns i)<GOAL>⨆ i, ⨆ (_ : n ∈ ns i), s n = s n
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra F L<VAR>S : Set K<VAR>splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)<VAR>x : K<VAR>hx : x ∈ adjoin F S<VAR>E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)<GOAL>Splits (algebraMap F L) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra F L<VAR>S : Set K<VAR>splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)<VAR>x : K<VAR>hx : x ∈ adjoin F S<VAR>E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)<VAR>normal : Normal F ↥E<GOAL>Splits (algebraMap F L) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra F L<VAR>S : Set K<VAR>splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)<VAR>x : K<VAR>hx : x ∈ adjoin F S<VAR>E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)<VAR>normal : Normal F ↥E<VAR>this : ∀ x ∈ S, Splits (algebraMap F ↥E) (minpoly F x)<GOAL>Splits (algebraMap F L) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra F L<VAR>S : Set K<VAR>splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)<VAR>x : K<VAR>hx : x ∈ adjoin F S<VAR>E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)<VAR>normal : Normal F ↥E<VAR>this : ∀ x ∈ S, Splits (algebraMap F ↥E) (minpoly F x)<VAR>φ : ↥(adjoin F S) →ₐ[F] ↥E<GOAL>Splits (algebraMap F L) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra F L<VAR>S : Set K<VAR>splits : ∀ x ∈ S, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)<VAR>x : K<VAR>hx : x ∈ adjoin F S<VAR>E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)<VAR>normal : Normal F ↥E<VAR>this : ∀ x ∈ S, Splits (algebraMap F ↥E) (minpoly F x)<VAR>φ : ↥(adjoin F S) →ₐ[F] ↥E<GOAL>minpoly F x = minpoly F (φ ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>μ : Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>h : SigmaFinite (Measure.map f μ)<VAR>n : ℕ<GOAL>μ ((fun n => f ⁻¹' spanningSets (Measure.map f μ) n) n) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>μ : Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>h : SigmaFinite (Measure.map f μ)<GOAL>⋃ i, (fun n => f ⁻¹' spanningSets (Measure.map f μ) n) i = univ
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<GOAL>(iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<VAR>h✝ : IsEmpty ι<GOAL>(iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra
<VAR>F : Type u_1<VAR>inst✝⁵ : Field F<VAR>E : Type u_2<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<VAR>h✝ : Nonempty ι<GOAL>(iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g✝ : ι → α → β<VAR>p : ℝ≥0∞<VAR>g : α → β<VAR>hp_ne_top : p ≠ ⊤<VAR>hg : Memℒp g p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>hε_top : ¬↑ε = ⊤<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g✝ : ι → α → β<VAR>p : ℝ≥0∞<VAR>g : α → β<VAR>hp_ne_top : p ≠ ⊤<VAR>hg : Memℒp g p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>hε_top : ¬↑ε = ⊤<VAR>s : Set α<VAR>left✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hgε : eLpNorm (sᶜ.indicator g) p μ < ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x => g) i)) p μ ≤ ↑ε
<VAR>α β : BddDistLat<VAR>e : ↑α.toDistLat ≃o ↑β.toDistLat<VAR>x✝ : (forget BddDistLat).obj α<GOAL>((let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : BddDistLat<VAR>e : ↑α.toDistLat ≃o ↑β.toDistLat<VAR>x✝ : (forget BddDistLat).obj β<GOAL>((let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 β) 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>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>m₁ m₁' : M₁<GOAL>(Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁'
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a b : ℝ<VAR>h : support f ⊆ Ioc a b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a b : ℝ<VAR>h : support f ⊆ Ioc a b<VAR>hab : a ≤ b<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a b : ℝ<VAR>h : support f ⊆ Ioc a b<VAR>hab : b ≤ a<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<GOAL>a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
<VAR>o : Ordinal.{u_1}<GOAL>aleph (succ o) = succ (aleph o)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>h1 : 1 ∈ T<VAR>hg : g ∈ S<VAR>this : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g<GOAL>(hST.equiv g).1 = ⟨g, hg⟩
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>v : OrthonormalBasis (Fin 2) ℝ F<VAR>z : ℂ<GOAL>(isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>v : OrthonormalBasis (Fin 2) ℝ F<VAR>z : ℂ<GOAL>v.repr.symm (orthonormalBasisOneI.repr z) = z.re • v 0 + z.im • v 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)<GOAL>Submodule.map ((lift Q) ⟨f, cond⟩).toLinearMap (LinearMap.range (ι Q)) = LinearMap.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>x : α<VAR>y : β<GOAL>ContinuousAt (update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a✝ b : WithTop α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>↑a * ⊤ = Option.bind ⊤ fun b => Option.some (a * b)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a✝ b : WithTop α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>⊤ = Option.bind ⊤ fun b => Option.some (a * b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>hy : y ∈ EMetric.ball x r<GOAL>HasSum (fun n => (p n) fun x_1 => y - x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>hy : y ∈ EMetric.ball x r<VAR>this : y - x ∈ EMetric.ball 0 r<GOAL>HasSum (fun n => (p n) fun x_1 => y - x) (f y)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Seq α → Seq α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Seq α<VAR>r : R s₁ s₂<GOAL>s₁ = s₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Seq α → Seq α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Seq α<VAR>r : R s₁ s₂<GOAL>↑s₁ = ↑s₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Seq α → Seq α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Seq α<VAR>r : R s₁ s₂<GOAL>Stream'.IsBisimulation fun x y => ∃ s s', ↑s = x ∧ ↑s' = y ∧ R s s'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Seq α → Seq α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Seq α<VAR>r : R s₁ s₂<GOAL>∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>x : X<GOAL>IsOpenMap fun g => g • x
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MulAction G X<VAR>inst✝⁴ : SigmaCompactSpace G<VAR>inst✝³ : BaireSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : ContinuousSMul G X<VAR>inst✝ : IsPretransitive G X<VAR>x : X<GOAL>∀ (x_1 : G), ∀ s ∈ 𝓝 x_1, (fun g => g • x) '' s ∈ 𝓝 (x_1 • x)