ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (Set.univ ×ˢ t) ρ<GOAL>∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>inst✝ : StrongEpi (f ≫ g)<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>x✝ : Mono z<VAR>u : Q ⟶ X<VAR>v : R ⟶ Y<VAR>sq : CommSq u g z v<GOAL>sq.HasLift
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>inst✝ : StrongEpi (f ≫ g)<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>x✝ : Mono z<VAR>u : Q ⟶ X<VAR>v : R ⟶ Y<VAR>sq : CommSq u g z v<VAR>h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v<GOAL>sq.HasLift
<VAR>l m r : List Char<VAR>p : Nat<GOAL>{ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } }.atEnd { byteIdx := p } = true ↔ p = utf8Len m
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>f : V₁ →ₗ[K] V₂<VAR>not_surj : ¬Function.Surjective ⇑f<VAR>inj : Function.Injective ⇑f.dualMap<GOAL>False
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>f : V₁ →ₗ[K] V₂<VAR>not_surj : range f < ⊤<VAR>inj : Function.Injective ⇑f.dualMap<GOAL>False
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>f : V₁ →ₗ[K] V₂<VAR>not_surj : range f < ⊤<VAR>inj : Function.Injective ⇑f.dualMap<VAR>φ : V₂ →ₗ[K] K<VAR>φ0 : φ ≠ 0<VAR>range_le_ker : range f ≤ ker φ<GOAL>False
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>∃ φ, f = φ.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)<VAR>eq : f.op = φ.map L.op ⋯<GOAL>∃ φ, f = φ.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)<VAR>eq : f.op = φ.map L.op ⋯<GOAL>f.op = (φ.unop.map L ⋯).op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)<VAR>eq : f.op = φ.map L.op ⋯<GOAL>φ.map L.op ⋯ = φ.unop.op.map L.op ⋯
<VAR>G : Type u_1<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>inst✝ : DecidableEq G<VAR>hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<GOAL>(graph (Corners.triangleIndices A)).FarFromTriangleFree (ε / 9)
<VAR>G : Type u_1<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>inst✝ : DecidableEq G<VAR>hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<GOAL>ε / 9 * ↑((Fintype.card G + Fintype.card G + Fintype.card G) ^ 2) ≤ ↑(Corners.triangleIndices A).card
<VAR>G : Type u_1<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>inst✝ : DecidableEq G<VAR>hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<GOAL>ε * ((↑(Fintype.card G) + ↑(Fintype.card G) + ↑(Fintype.card G)) ^ 2 / 9) ≤ ↑A.card
<VAR>G : Type u_1<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Fintype G<VAR>A B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>inst✝ : DecidableEq G<VAR>hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<GOAL>ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>t u : Finset α<VAR>hf : 0 ≤ f<VAR>ht : t ∈ 𝒜<VAR>ha : a ∉ t<GOAL>f t ≤ collapse 𝒜 a f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>t u : Finset α<VAR>hf : 0 ≤ f<VAR>ht : t ∈ 𝒜<VAR>ha : a ∉ t<GOAL>f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β → β<VAR>a : β<VAR>l : List α<VAR>L : List (List α)<GOAL>foldr f a (l :: L).join = foldr (fun l b => foldr f b l) a (l :: L)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>D₃ : Type u_6<VAR>inst✝⁵ : Category.{u_11, u_1} C₁<VAR>inst✝⁴ : Category.{u_7, u_2} C₂<VAR>inst✝³ : Category.{u_8, u_3} C₃<VAR>inst✝² : Category.{u_12, u_4} D₁<VAR>inst✝¹ : Category.{u_9, u_5} D₂<VAR>inst✝ : Category.{u_10, u_6} D₃<VAR>H₁ : C₁ ⥤ D₁<VAR>L₁ : C₁ ⥤ C₂<VAR>R₁ : D₁ ⥤ D₂<VAR>H₂ : C₂ ⥤ D₂<VAR>w : TwoSquare H₁ L₁ R₁ H₂<VAR>L₂ : C₂ ⥤ C₃<VAR>R₂ : D₂ ⥤ D₃<VAR>H₃ : C₃ ⥤ D₃<VAR>w'✝ : TwoSquare H₂ L₂ R₂ H₃<VAR>E : C₂ ≌ C₃<VAR>E' : D₂ ≌ D₃<VAR>w' : H₂ ⋙ E'.functor ≅ E.functor ⋙ H₃<VAR>L₁₂ : C₁ ⥤ C₃<VAR>R₁₂ : D₁ ⥤ D₃<VAR>eL : L₁ ⋙ E.functor ≅ L₁₂<VAR>eR : R₁ ⋙ E'.functor ≅ R₁₂<GOAL>(w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝² : Fintype (Sym2 α)<VAR>inst✝¹ : NonAssocSemiring R<VAR>a b : α<VAR>e : Sym2 α<VAR>inst✝ : Fintype ↑(G.neighborSet a)<GOAL>∑ e : Sym2 α, incMatrix R G a e = ↑(G.degree a)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>g : ArithmeticFunction R<VAR>hg : g.IsMultiplicative<VAR>h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)<VAR>n : ℕ<VAR>hn : ¬n = 0<GOAL>f n = g n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>g : ArithmeticFunction R<VAR>hg : g.IsMultiplicative<VAR>h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)<VAR>n : ℕ<VAR>hn : ¬n = 0<GOAL>(n.factorization.prod fun p k => f (p ^ k)) = n.factorization.prod fun p k => g (p ^ k)
<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 a' : α<VAR>b✝ : M<VAR>a₁ a₂ : α<VAR>b : M<GOAL>(single a₁ b) a₂ = (single a₂ b) a₁
<VAR>x✝ : Iterator<VAR>h✝ : x✝.Valid<VAR>l r : List Char<VAR>h : ValidFor l r x✝<GOAL>x✝.remainingBytes ≤ x✝.s.utf8ByteSize
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>x✝ : ∀ i < 0, m.IsCaratheodory (s i)<GOAL>m.IsCaratheodory (⋃ i, ⋃ (_ : i < 0), s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>n : ℕ<VAR>h : ∀ i < n + 1, m.IsCaratheodory (s i)<GOAL>m.IsCaratheodory (⋃ i, ⋃ (_ : i < n + 1), s i)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s✝ s₁ s₂ : Set α<VAR>s : ℕ → Set α<VAR>n : ℕ<VAR>h : ∀ i < n + 1, m.IsCaratheodory (s i)<GOAL>m.IsCaratheodory ((⋃ k, ⋃ (_ : k < n), s k) ∪ s n)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>s : CostructuredArrow yoneda A<VAR>x : F.obj (op s)<GOAL>op s = op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F s x).val))
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b : A<GOAL>2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b : A<GOAL>2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b : A<GOAL>2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = ⁅L (a + b), L ((a + b) * (a + b))⁆
<VAR>A : Type u_1<VAR>inst✝¹ : NonUnitalNonAssocCommRing A<VAR>inst✝ : IsCommJordan A<VAR>a b : A<GOAL>⁅L a, L (a * b)⁆ + ⁅L a, L (a * b)⁆ + (⁅L b, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = ⁅L b, L (a * a)⁆ + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆ + ⁅L a, L (b * b)⁆)
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F₁ : B ⥤ C<VAR>F₂ : D ⥤ E<VAR>G : C × E ⥤ H<VAR>x✝² x✝¹ : B × D<VAR>x₁ : B<VAR>x₂ : D<VAR>y₁ : B<VAR>y₂ : D<VAR>x✝ : (x₁, x₂) ⟶ (y₁, y₂)<VAR>f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1<VAR>f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2<GOAL>G.map (F₁.map f₁, 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁), F₂.map f₂) = 𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁, F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ : Subgroup α<VAR>a b : α<VAR>N : Subgroup α<VAR>s : Set α<GOAL>∀ (x : ↥N), (fun x_1 => x_1 * ↑x⁻¹) '' s = (fun x_1 => x_1 * ↑x) ⁻¹' s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeSup B<VAR>inst✝¹ : Add B<VAR>inst✝ : OrderBot B<VAR>D : A → B<VAR>a : A<VAR>r : R<GOAL>supDegree D (single a r) = if r = 0 then ⊥ else D a
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p i : Fin (n + 1)<VAR>h : i < p<VAR>hi : optParam (i ≠ last n) ⋯<GOAL>p.succAbove (i.castPred hi) = i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : α<VAR>h : ¬Finite a b<VAR>n : ℕ<GOAL>a ^ zero ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : α<VAR>h : ¬Finite a b<VAR>n : ℕ<GOAL>1 ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : α<VAR>h : ¬Finite a b<VAR>n : ℕ<GOAL>∀ (n : ℕ), a ^ n.succ ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : α<GOAL>(∀ (n : ℕ), a ^ n ∣ b) → ¬Finite a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : α<GOAL>(∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F ↥L ↥(adjoin (↥L) S)) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F ↥L ↥(adjoin (↥L) S)) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<VAR>s : E<VAR>h : s ∈ S<GOAL>s ∈ ↑(extendScalars ⋯)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<VAR>s : E<VAR>h : s ∈ S<VAR>this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra<VAR>this✝ : SMul ↥L ↥φ.carrier := Algebra.toSMul<VAR>this : IsScalarTower (↥L) (↥φ.carrier) E<GOAL>s ∈ ↑(extendScalars ⋯)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<VAR>s : E<VAR>h : s ∈ S<VAR>this✝² : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra<VAR>this✝¹ : SMul ↥L ↥φ.carrier := Algebra.toSMul<VAR>this✝ : IsScalarTower (↥L) (↥φ.carrier) E<VAR>this : ∃ y, φ ≤ y ∧ s ∈ y.carrier<GOAL>s ∈ ↑(extendScalars ⋯)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Splits f.toRingHom (minpoly (↥L) s)<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<VAR>s : E<VAR>h : s ∈ S<VAR>this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra<VAR>this✝ : SMul ↥L ↥φ.carrier := Algebra.toSMul<VAR>this : IsScalarTower (↥L) (↥φ.carrier) E<GOAL>Splits (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝¹ : IsOrderConnected α r<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ l₃ : List α<VAR>h : Lex r l₁ l₃<GOAL>Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝¹ : IsOrderConnected α r<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ l₃ : List α<VAR>h : Lex r l₁ l₃<VAR>ab : r a b<GOAL>Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝¹ : IsOrderConnected α r<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ l₂ l₃ : List α<VAR>h : Lex r l₁ l₃<GOAL>Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝¹ : IsOrderConnected α r<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ l₃ : List α<VAR>h : Lex r l₁ l₃<VAR>ab : r b a<GOAL>Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<GOAL>∃ c ∈ P.parts, c ≤ b
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<VAR>H : ¬∃ c ∈ P.parts, c ≤ b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<VAR>H : ¬∃ c ∈ P.parts, c ≤ b<GOAL>Disjoint b a
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<VAR>H : ¬∃ c ∈ P.parts, c ≤ b<GOAL>∀ ⦃i : α⦄, i ∈ P.parts → Disjoint b (id i)
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<VAR>H : ¬∃ c ∈ P.parts, c ≤ b<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>d : α<VAR>hd : d ∈ Q.parts<VAR>hcd : c ≤ d<GOAL>Disjoint b (id c)
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<VAR>H : ¬∃ c ∈ P.parts, c ≤ b<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>d : α<VAR>hd : d ∈ Q.parts<VAR>hcd : c ≤ d<GOAL>b ≠ d
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<VAR>H : ¬∃ c ∈ P.parts, c ≤ b<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>hd : b ∈ Q.parts<VAR>hcd : c ≤ b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>hd : b ∈ Q.parts<VAR>hcd : c ≤ b<VAR>H : ∀ x ∈ P.parts, ¬x ≤ b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝³ : ConditionallyCompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<GOAL>sSup s⁻¹ = (sInf s)⁻¹
<VAR>α : Type u_1<VAR>inst✝³ : ConditionallyCompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddBelow s<GOAL>sSup (Inv.inv '' s) = (sInf s)⁻¹
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>M : Matrix n n α<VAR>v : n → α<GOAL>M = (diagonal v)ᴴ ↔ M = diagonal (star v)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ⋃₀ 𝔖 = univ<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Inducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Inducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)<GOAL>Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Inducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)<GOAL>Inducing (⇑φ.symm ∘ F) ↔ Inducing F
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : MulOneClass M<GOAL>1 ∈ S.centralizer
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<GOAL>m.toEnumFinset.card = card m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<GOAL>card (map Prod.fst m.toEnumFinset.val) = card m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<GOAL>map Prod.fst m.toEnumFinset.val = m
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>t : Multiset ι<VAR>f₁ f₂ : ι → Set α<VAR>hf : ∀ i ∈ t, f₁ i ⊆ f₂ i<GOAL>(Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>f₁ f₂ : ι → Set α<VAR>a✝ : List ι<VAR>hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i<GOAL>(Multiset.map f₁ ⟦a✝⟧).prod ⊆ (Multiset.map f₂ ⟦a✝⟧).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>f₁ f₂ : ι → Set α<VAR>a✝ : List ι<VAR>hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i<GOAL>(List.map f₁ a✝).prod ⊆ (List.map f₂ a✝).prod
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>n : ℕ<GOAL>drop n l.tail = drop (n + 1) l
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Monoid G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulAction G M<VAR>f : G → M<VAR>hf : IsMulOneCocycle f<GOAL>f 1 = 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<GOAL>(p.append (singleton r newLast) rel).head = p.head
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<GOAL>iterate f a n = [] ↔ n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<GOAL>∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<GOAL>∫⁻ (x : α) in univ, μ.rnDeriv ν x ∂ν < ⊤
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i<GOAL>‖g.compContinuousLinearMap fun i => (f i).toContinuousLinearMap‖ ≤ ‖g‖