ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : Opens ↑Y.toTopCat<VAR>x : ↥((Opens.map f.val.base).obj V)<VAR>a : ↑(Y.presheaf.obj (op V))<GOAL>(residueFieldMap f ↑x) ((Y.evaluation ⟨f.val.base ↑x, ⋯⟩) a) = (X.evaluation x) ((f.val.c.app (op V)) a)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>H✝ K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝² : Group N<VAR>P : Type u_6<VAR>inst✝¹ : Group P<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>inst✝ : (i : η) → Group (f i)<VAR>H : (i : η) → Subgroup (f i)<VAR>x : (i : η) → f i<GOAL>x ∈ pi ∅ H ↔ x ∈ ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>h_inj : Function.Injective ⇑(algebraMap R P)<GOAL>num 0 = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f<VAR>F : Presheaf C X<VAR>x : ↑X<GOAL>IsIso (stalkPushforward C f F x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f<VAR>F : Presheaf C X<VAR>x : ↑X<VAR>this : (⋯.functorNhds x).Initial<GOAL>IsIso (stalkPushforward C f F x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f<VAR>F : Presheaf C X<VAR>x : ↑X<VAR>this : (⋯.functorNhds x).Initial<VAR>e_3✝ : ((pushforward C f).obj F).stalk (f x) = colimit ((OpenNhds.inclusion (f x)).op ⋙ (pushforward C f).obj F)<VAR>e_4✝ : F.stalk x = colim.obj (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)<GOAL>stalkPushforward C f F x = ((Functor.Final.colimitIso (⋯.functorNhds x).op ((OpenNhds.inclusion (f x)).op ⋙ (pushforward C f).obj F)).symm ≪≫ colim.mapIso ?convert_2).hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f<VAR>F : Presheaf C X<VAR>x : ↑X<VAR>this : (⋯.functorNhds x).Initial<GOAL>(⋯.functorNhds x).op ⋙ (OpenNhds.inclusion (f x)).op ⋙ (pushforward C f).obj F ≅ ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<GOAL>∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<VAR>M : MeasurableSet (Set.Ioc 0 A)<GOAL>∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<VAR>M : MeasurableSet (Set.Ioc 0 A)<VAR>M' : MeasurableSet (Set.Ioc A 0)<GOAL>∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<VAR>M : MeasurableSet (Set.Ioc 0 A)<VAR>M' : MeasurableSet (Set.Ioc A 0)<GOAL>∫ (x : α), ((Set.Ioc 0 A).indicator id ∘ f) x ^ n ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<VAR>M : MeasurableSet (Set.Ioc 0 A)<VAR>M' : MeasurableSet (Set.Ioc A 0)<GOAL>∫ (x : α), (fun z => (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<VAR>M : MeasurableSet (Set.Ioc 0 A)<VAR>M' : MeasurableSet (Set.Ioc A 0)<VAR>hA : 0 ≤ A<GOAL>∫ (x : α), (fun z => (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h'f : 0 ≤ f<VAR>M : MeasurableSet (Set.Ioc 0 A)<VAR>M' : MeasurableSet (Set.Ioc A 0)<VAR>hA : A < 0<GOAL>∫ (x : α), (fun z => (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ = ∫ (y : ℝ) in 0 ..A, y ^ n ∂Measure.map f μ
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>(x / y).toNNReal = x.toNNReal / y.toNNReal
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<GOAL>(aeval ⟨x, ⋯⟩) (minpoly R x) = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁶ : CommRing R<VAR>inst✝¹⁵ : AddCommGroup L<VAR>inst✝¹⁴ : Module R L<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝¹¹ : Fintype ι<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ιM<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq ι'<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : Nontrivial R<VAR>x : L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<GOAL>∃ x, φ.IsNilRegular x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁶ : CommRing R<VAR>inst✝¹⁵ : AddCommGroup L<VAR>inst✝¹⁴ : Module R L<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝¹¹ : Fintype ι<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ιM<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq ι'<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : Nontrivial R<VAR>x : L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<GOAL>↑(finrank R M) ≤ Cardinal.mk R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : 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>inst✝⁴ : One M<VAR>inst✝³ : One N<VAR>inst✝² : One P<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq M<VAR>f : α → M<VAR>x : α<VAR>y : M<GOAL>mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ pure x ≤ F.lift' closure
<VAR>T : ℝ<VAR>x : AddCircle T<GOAL>↑(toCircle 0) = 1
<VAR>T : ℝ<VAR>x : AddCircle T<VAR>this : (fourier 0) x = ↑(toCircle 0)<GOAL>↑(toCircle 0) = 1
<VAR>T : ℝ<VAR>x : AddCircle T<VAR>this : (fourier 0) x = ↑(toCircle 0)<GOAL>(fourier 0) x = 1
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>I : Ideal R<VAR>a b : R<VAR>S✝ : Type v<VAR>x✝ y : R<VAR>inst✝ : Semiring S✝<VAR>S T : Ideal R<VAR>H : S ≤ T<VAR>x : R<GOAL>((factor S T H).comp (mk S)) x = (mk T) x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype p<VAR>inst✝ : LinearOrderedRing R<VAR>v : n → R<GOAL>(∀ i ∈ Finset.univ, v i * v i = 0) ↔ v = 0
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(loopyOn E).Indep I ↔ I = ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>I = ∅ → I ⊆ E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B X R J : Set α<GOAL>∅ ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<VAR>b : β<VAR>hb : b ∈ t<GOAL>∃ a, ∃ (ha : a ∈ s), b = f a ha
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<VAR>b : β<VAR>hb : b ∈ t<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<GOAL>∃ a, ∃ (ha : a ∈ s), b = f a ha
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<VAR>b : β<VAR>hb : b ∈ t<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<VAR>finj : Function.Injective f'<VAR>hft : Fintype ↑t<VAR>hft' : Fintype ↑s<VAR>f'' : (a : α) → a ∈ s.toFinset → β := fun a h => f a ⋯<GOAL>∃ a, ∃ (ha : a ∈ s), b = f a ha
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<VAR>b : β<VAR>hb : b ∈ t<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<VAR>finj : Function.Injective f'<VAR>hft : Fintype ↑t<VAR>hft' : Fintype ↑s<VAR>f'' : (a : α) → a ∈ s.toFinset → β := fun a h => f a ⋯<VAR>x✝ : α<GOAL>x✝ ∈ s ↔ x✝ ∈ s.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<VAR>b : β<VAR>hb : b ∈ t<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<VAR>finj : Function.Injective f'<VAR>hft : Fintype ↑t<VAR>hft' : Fintype ↑s<VAR>f'' : (a : α) → a ∈ s.toFinset → β := fun a h => f a ⋯<GOAL>∀ (a : α) (ha : a ∈ s.toFinset), f'' a ha ∈ t.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<VAR>b : β<VAR>hb : b ∈ t<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<VAR>finj : Function.Injective f'<VAR>hft : Fintype ↑t<VAR>hft' : Fintype ↑s<VAR>f'' : (a : α) → a ∈ s.toFinset → β := fun a h => f a ⋯<GOAL>∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s.toFinset) (ha₂ : a₂ ∈ s.toFinset), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<VAR>b : β<VAR>hb : b ∈ t<VAR>f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩<VAR>finj : Function.Injective f'<VAR>hft : Fintype ↑t<VAR>hft' : Fintype ↑s<VAR>f'' : (a : α) → a ∈ s.toFinset → β := fun a h => f a ⋯<GOAL>t.toFinset.card ≤ s.toFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : Cardinal.{u_3}<VAR>n : ℕ<GOAL>toPartENat c ≤ ↑n ↔ c ≤ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : β → α<VAR>i₀ : β<GOAL>⨆ i, f i = f i₀ ⊔ ⨆ i, ⨆ (_ : i ≠ i₀), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : β → α<VAR>i₀ : β<GOAL>f i₀ = ⨆ i, ⨆ (_ : i = i₀), f i
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : α → F α<VAR>x : α<GOAL>(corecF g x).dest = (P F).map (corecF g) (repr (g x))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field L'<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K L'<VAR>S F E : IntermediateField K L<VAR>inst✝ : FiniteDimensional K L<VAR>h_le : F ≤ E<VAR>h_finrank : finrank (↥F) L ≤ finrank (↥E) L<GOAL>F = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field L'<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K L'<VAR>S F E : IntermediateField K L<VAR>inst✝ : FiniteDimensional K L<VAR>h_le : F ≤ E<VAR>h_finrank : finrank (↥F) L ≤ finrank (↥E) L<GOAL>finrank K ↥E ≤ finrank K ↥F
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field L'<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K L'<VAR>S F E : IntermediateField K L<VAR>inst✝ : FiniteDimensional K L<VAR>h_le : F ≤ E<VAR>h_finrank : finrank (↥F) L ≤ finrank (↥E) L<VAR>h1 : finrank K ↥F * finrank (↥F) L = finrank K L<GOAL>finrank K ↥E ≤ finrank K ↥F
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field L'<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K L'<VAR>S F E : IntermediateField K L<VAR>inst✝ : FiniteDimensional K L<VAR>h_le : F ≤ E<VAR>h_finrank : finrank (↥F) L ≤ finrank (↥E) L<VAR>h1 : finrank K ↥F * finrank (↥F) L = finrank K L<VAR>h2 : finrank K ↥E * finrank (↥E) L = finrank K L<GOAL>finrank K ↥E ≤ finrank K ↥F
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field L'<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K L'<VAR>S F E : IntermediateField K L<VAR>inst✝ : FiniteDimensional K L<VAR>h_le : F ≤ E<VAR>h_finrank : finrank (↥F) L ≤ finrank (↥E) L<VAR>h1 : finrank K ↥F * finrank (↥F) L = finrank K L<VAR>h2 : finrank K ↥E * finrank (↥E) L = finrank K L<VAR>h3 : 0 < finrank (↥E) L<GOAL>finrank K ↥E ≤ finrank K ↥F
<VAR>R : Type u_1<VAR>inst✝ : OrderedCommSemiring R<VAR>s : Multiset R<GOAL>(∀ a ∈ s, 0 ≤ a) → 0 ≤ s.prod
<VAR>R : Type u_1<VAR>inst✝ : OrderedCommSemiring R<VAR>s : Multiset R<GOAL>(∀ a ∈ 0, 0 ≤ a) → 0 ≤ prod 0
<VAR>R : Type u_1<VAR>inst✝ : OrderedCommSemiring R<VAR>s✝ : Multiset R<VAR>a : R<VAR>s : Multiset R<VAR>hs : (∀ a ∈ s, 0 ≤ a) → 0 ≤ s.prod<VAR>ih : ∀ a_1 ∈ a ::ₘ s, 0 ≤ a_1<GOAL>0 ≤ (a ::ₘ s).prod
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<GOAL>IsNormalClosure F K L ↔ (∀ (x : K), Splits (algebraMap F L) (minpoly F x)) ∧ normalClosure F K L = ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>K : ℝ≥0<VAR>hL : AntilipschitzWith K ⇑L<VAR>φ : X → E<VAR>h : ¬Integrable φ μ<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>K : ℝ≥0<VAR>hL : AntilipschitzWith K ⇑L<VAR>φ : X → E<VAR>h : ¬Integrable φ μ<VAR>this : ¬Integrable (fun x => L (φ x)) μ<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<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>ζ : C<VAR>hζ : ζ ^ n = 1<VAR>a : ℕ<GOAL>(zmodChar n hζ) ↑a = ζ ^ a
<VAR>R : Type u_1<VAR>n k : ℕ<GOAL>∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
<VAR>R : Type u_1<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
<VAR>R : Type u_1<VAR>n k : ℕ<VAR>h : k > n<GOAL>∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>s : Finset ℕ<GOAL>∏ p ∈ filter Nat.Prime s, (1 - f p)⁻¹ = ∑' (m : ↑(factoredNumbers s)), f ↑m
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →* F<VAR>hsum : Summable ⇑f<VAR>s : Finset ℕ<GOAL>∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>f : ↑(Iic b) → β<GOAL>range (IicExtend f) = range f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d : α<VAR>n : ℤ<VAR>a : α<GOAL>a - a / 2 = a / 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d : α<VAR>n : ℤ<VAR>a : α<GOAL>a / 2 + a / 2 - a / 2 = a / 2
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>p✝ q✝ : R[X]<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>x : S<VAR>hx : (aeval x) q = 0<GOAL>(aeval x) (p %ₘ q) = (aeval x) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hs' : μ s = 0<GOAL>∫⁻ (x : α) in s, f x ∂μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hs' : μ s = 0<GOAL>μ.restrict s = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Computation α → Computation α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Computation α<VAR>r : R s₁ s₂<GOAL>s₁ = s₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Computation α → Computation α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Computation α<VAR>r : R s₁ s₂<GOAL>↑s₁ = ↑s₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Computation α → Computation α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Computation α<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 : Computation α → Computation α → Prop<VAR>bisim : IsBisimulation R<VAR>s₁ s₂ : Computation α<VAR>r : R s₁ s₂<GOAL>∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>h : padicNorm p q = 0<GOAL>q = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>h : padicNorm p q = 0<GOAL>¬q = 0 → False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>h : (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) = 0<VAR>hq : ¬q = 0<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>h : ↑p ^ (-padicValRat p q) = 0<VAR>hq : ¬q = 0<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>h : ↑p ^ (-padicValRat p q) = 0<VAR>hq : ¬q = 0<GOAL>¬↑p ^ (-padicValRat p q) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>h : ↑p ^ (-padicValRat p q) = 0<VAR>hq : ¬q = 0<GOAL>↑p ≠ 0
<VAR>α : Type u_1<VAR>I✝ B X✝ : Set α<VAR>P : Set α → Prop<VAR>X : Set α<VAR>n : ℕ<VAR>hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n<VAR>I : Set α<VAR>hI : P I<VAR>hIX : I ⊆ X<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>I✝ B X✝ : Set α<VAR>P : Set α → Prop<VAR>X : Set α<VAR>n : ℕ<VAR>hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n<VAR>I : Set α<VAR>hI : P I<VAR>hIX : I ⊆ X<VAR>hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>I✝ B X✝ : Set α<VAR>P : Set α → Prop<VAR>X : Set α<VAR>n : ℕ<VAR>hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n<VAR>I : Set α<VAR>hI : P I<VAR>hIX : I ⊆ X<VAR>hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite<VAR>Y : Set α<VAR>hY : Y ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>I✝ B X✝ : Set α<VAR>P : Set α → Prop<VAR>X : Set α<VAR>n : ℕ<VAR>hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n<VAR>I : Set α<VAR>hI : P I<VAR>hIX : I ⊆ X<VAR>hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite<VAR>Y : Set α<VAR>hY : Y ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard<VAR>J : Set α<VAR>x✝ : J ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hYJ : Y ⊆ J<VAR>hJ : P J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<GOAL>J ⊆ Y
<VAR>α : Type u_1<VAR>I✝ B X✝ : Set α<VAR>P : Set α → Prop<VAR>X : Set α<VAR>n : ℕ<VAR>hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n<VAR>I : Set α<VAR>hI : P I<VAR>hIX : I ⊆ X<VAR>hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite<VAR>Y : Set α<VAR>hY : Y ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard<VAR>J : Set α<VAR>x✝ : J ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hYJ : Y ⊆ J<VAR>hJ : P J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<VAR>hJfin : J.Finite<GOAL>J ⊆ Y
<VAR>α : Type u_1<VAR>I✝ B X✝ : Set α<VAR>P : Set α → Prop<VAR>X : Set α<VAR>n : ℕ<VAR>hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n<VAR>I : Set α<VAR>hI : P I<VAR>hIX : I ⊆ X<VAR>hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite<VAR>Y : Set α<VAR>hY : Y ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard<VAR>J : Set α<VAR>x✝ : J ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hYJ : Y ⊆ J<VAR>hJ : P J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<VAR>hJfin : J.Finite<GOAL>J.ncard ≤ Y.ncard
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : InnerProductSpace 𝕜 G<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : CompleteSpace G<VAR>inst✝¹ : CompleteSpace F<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<GOAL>orthogonalProjection U = adjoint U.subtypeL
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : InnerProductSpace 𝕜 G<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : CompleteSpace G<VAR>inst✝¹ : CompleteSpace F<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<GOAL>∀ (x : E) (y : ↥U), ⟪(orthogonalProjection U) x, y⟫_𝕜 = ⟪x, U.subtypeL y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : InnerProductSpace 𝕜 G<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : CompleteSpace G<VAR>inst✝¹ : CompleteSpace F<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<VAR>x : E<VAR>u : ↥U<GOAL>⟪(orthogonalProjection U) x, u⟫_𝕜 = ⟪x, U.subtypeL u⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : InnerProductSpace 𝕜 G<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : CompleteSpace G<VAR>inst✝¹ : CompleteSpace F<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<VAR>x : E<VAR>u : ↥U<GOAL>⟪x, ↑u⟫_𝕜 = ⟪x, U.subtypeL u⟫_𝕜
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b < 1 * a ↔ b < a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>r : R<GOAL>(p.comp (X + C r)).Monic