mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Poisson
/-- **Poisson integral formula** for ℂ-differentiable functions on arbitrary disks in the complex plane,
formulated with the real part of the Herglotz–Riesz kernel of integration.
 -/
DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E]
  {c : ℂ},
  DiffContOnCl ℂ f (Metric.ball c R) →
    w ∈ Metric.ball c R → Real.circleAverage (Complex.re ∘ herglotzRieszKernel c w • f) c R = f w
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `Comma L R` has colimits of shape `J` and `Comma L R` is closed under colimits of shape
`J`, then `forget L R P ⊤ ⊤` creates colimits of shape `J`.  -/
CategoryTheory.MorphismProperty.Comma.forgetCreatesColimitsOfShapeOfClosed : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      {A : Type u_2} →
        {B : Type u_3} →
          (J : Type u_4) →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} J] →
                  {L : CategoryTheory.Functor A T} →
                    {R : CategoryTheory.Functor B T} →
                      [CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Comma L R)] →
                        [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderColimitsOfShape J] →
                          CategoryTheory.CreatesColimitsOfShape J
                            (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.instInfSet : {R : Type u} → [inst : NonUnitalNonAssocRing R] → InfSet (NonUnitalSubring R)
-- Lean.Util.Trace
Lean.printTraces : {m : Type → Type} → [Monad m] → [Lean.MonadTrace m] → [MonadLiftT IO m] → m Unit
-- Mathlib.GroupTheory.FreeGroup.GeneratorEquiv
/-- Isomorphic free groups have equivalent bases.  -/
Equiv.ofFreeGroupEquiv : {α : Type u_1} → {β : Type u_2} → FreeGroup α ≃* FreeGroup β → α ≃ β
-- Mathlib.Algebra.Group.Prod
Prod.instDivInvMonoid.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : DivInvMonoid G] [inst_1 : DivInvMonoid H],
  Prod.instDivInvMonoid =
    { toMonoid := Prod.instMonoid, toInv := Prod.instInv, toDiv := Prod.instDiv,
      zpow := fun z a => (ZPow.zpow z a.1, ZPow.zpow z a.2), div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯,
      zpow_neg' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.const_smul` -/
InnerProductSpace.HarmonicContOnCl.fun_const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : ℝ), InnerProductSpace.HarmonicContOnCl (fun i => c • f i) s
-- Mathlib.Order.SymmDiff
bihimp_eq' : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b = a ⊓ b ⊔ aᶜ ⊓ bᶜ
-- Init.Meta.Defs
Lean.Syntax.isAtom : Lean.Syntax → Bool
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The data of chosen coends of shape `J` in `C`.  -/
CategoryTheory.Limits.ChosenCoendsOfShape : (J : Type u_1) →
  [CategoryTheory.Category.{v_1, u_1} J] →
    (C : Type u_2) → [CategoryTheory.Category.{v_2, u_2} C] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.instInvolutiveStarId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → InvolutiveStar (E →ₗ[𝕜] E)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap.eq_2 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → Option (γ a)) (sz : ℕ) (k' : α)
  (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.filterMap f (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr_1 =
    match f k' v' with
    | none =>
      match Std.DTreeMap.Internal.Impl.filterMap f l' ⋯ with
      | { impl := l'_1, balanced_impl := hl' } =>
        match Std.DTreeMap.Internal.Impl.filterMap f r' ⋯ with
        | { impl := r'_1, balanced_impl := hr' } => { impl := (l'_1.link2 r'_1 ⋯ ⋯).impl, balanced_impl := ⋯ }
    | some v'_1 =>
      match Std.DTreeMap.Internal.Impl.filterMap f l' ⋯ with
      | { impl := l'_1, balanced_impl := hl' } =>
        match Std.DTreeMap.Internal.Impl.filterMap f r' ⋯ with
        | { impl := r'_1, balanced_impl := hr' } =>
          { impl := (Std.DTreeMap.Internal.Impl.link k' v'_1 l'_1 r'_1 ⋯ ⋯).impl, balanced_impl := ⋯ }
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.restrict.congr_simp : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2}
  [inst_2 : SetLike σR R] [inst_3 : SetLike σS S] [inst_4 : SubsemiringClass σR R] [inst_5 : SubsemiringClass σS S]
  (f f_1 : R →+* S) (e_f : f = f_1) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s), f.restrict s' s h = f_1.restrict s' s ⋯
-- Mathlib.Algebra.Lie.Nilpotent
Function.Surjective.lieModuleIsNilpotent : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] {L₂ : Type u_1}
  {M₂ : Type u_2} [inst_7 : LieRing L₂] [inst_8 : LieAlgebra R L₂] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂},
  (∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) →
    ∀ [LieModule R L₂ M₂],
      Function.Surjective ⇑f → Function.Surjective ⇑g → ∀ [LieModule.IsNilpotent L M], LieModule.IsNilpotent L₂ M₂
-- Mathlib.FieldTheory.SeparableClosure
/-- In a finitely generated field extension, there exists a maximal
separably generated field extension.  -/
IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.EssFiniteType F E],
  ∃ s,
    MaximalFor (fun t => IsTranscendenceBasis F Subtype.val)
      (fun t => IntermediateField.restrictScalars F (separableClosure (↥(IntermediateField.adjoin F t)) E)) ↑s
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.X_negOne : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ}, CochainComplex.ConnectData.X K L (-1) = K.X 0
-- Init.Data.String.Decode
Char.utf8Size_eq_four_iff : ∀ {c : Char}, c.utf8Size = 4 ↔ 65535 < c.val
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_trans_self : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), e.symm.trans e = AddEquiv.refl N
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.codisjoint_zeroLocus : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  Codisjoint (X.zeroLocus s) ↑U
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_symm_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (p : CategoryTheory.Bicategory.Adj.Hom₂ α β), (CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj).symm p.τr = p.τl
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
CategoryTheory.Pseudofunctor.isStackFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsStack J] {S : C} (R : CategoryTheory.Presieve S),
  CategoryTheory.Sieve.generate R ∈ J S → F.IsStackFor R
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the monadic predicate `p` returns `ULift.up true` for
all elements emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of `it` are
examined in order of iteration.

This function is deprecated. Instead of `it.allowNontermination.allM`, use `it.allM`.
 -/
Std.IterM.Partial.allM : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → (β → m (ULift.{w, 0} Bool)) → Std.IterM.Partial m β → m (ULift.{w, 0} Bool)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH =
    CategoryTheory.Limits.Cofork.π c
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X₁ ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.MonObj.one)
        CategoryTheory.MonObj.mul) =
    f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The counit of an adjunction.  -/
CategoryTheory.Bicategory.Adjunction.counit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          CategoryTheory.Bicategory.Adjunction f g →
            (CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.repr : {F : Type u → Type v} → [self : QPF F] → {α : Type u} → F α → ↑(QPF.P F) α
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.nhds_one_eq : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G), nhds 1 = B.filter
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.List.takeWhile₂.match_3.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : List α) (x_1 : List β)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs))
  (h_2 : (x : List α) → (x_2 : List β) → motive x x_2),
  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) →
    (match x, x_1 with
      | a :: as, b :: bs => h_1 a as b bs
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Lean.Expr
Lean.Expr.hasLevelParamEx : Lean.Expr → Bool
-- Mathlib.Analysis.Analytic.Basic
/-- If `f` has formal power series `∑ n, pₙ` on a ball of radius `r`, then for `y, z` in any smaller
ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above by
`C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. This lemma formulates this property using `IsBigO` and
`Filter.principal` on `E × E`.  -/
HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    r' < r →
      (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[Filter.principal (Metric.eball (x, x) r')] fun y =>
        ‖y - (x, x)‖ * ‖y.1 - y.2‖
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_mul_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (a : G),
  IsOpenMap fun x => a * x
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A version of `linearIndependent_iff` where the linear combination is a `Finset` sum.  -/
linearIndependent_iff' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
-- Mathlib.Algebra.Field.Defs
DivisionRing.toZPow : {K : Type u_2} → [self : DivisionRing K] → ZPow K
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.mk.injEq : ∀ (declName oldArg : Lean.Name) (newArg? : Option Lean.Name) (text? since? : Option String)
  (declName_1 oldArg_1 : Lean.Name) (newArg?_1 : Option Lean.Name) (text?_1 since?_1 : Option String),
  ({ declName := declName, oldArg := oldArg, newArg? := newArg?, text? := text?, since? := since? } =
      { declName := declName_1, oldArg := oldArg_1, newArg? := newArg?_1, text? := text?_1, since? := since?_1 }) =
    (declName = declName_1 ∧ oldArg = oldArg_1 ∧ newArg? = newArg?_1 ∧ text? = text?_1 ∧ since? = since?_1)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_eq_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : Inhabited α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {a : α}, a ∉ m → m.get! a = default
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.eq_cyclotomic_iff : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ},
  0 < n →
    ∀ (P : Polynomial R),
      P = Polynomial.cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i R = Polynomial.X ^ n - 1
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An additive `n`-Freiman homomorphism from a set `A` to a set `B` is a bijective map which
preserves sums of `n` elements.  -/
IsAddFreimanIso : {α : Type u_2} → {β : Type u_3} → [AddCommMonoid α] → [AddCommMonoid β] → ℕ → Set α → Set β → (α → β) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- a choice of cokernel of `S.f : S.X₁ ⟶ S.X₂`  -/
CategoryTheory.ShortComplex.RightHomologyData.Q : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {S : CategoryTheory.ShortComplex C} → S.RightHomologyData → C
-- Std.Data.HashSet.Lemmas
Std.HashSet.forM_eq_forM_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : α → m' PUnit.{v + 1}}, Std.HashSet.forM (fun a => f a) m = Array.forM f m.toArray
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.augment_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C)
  (f : X.obj (Opposite.op { len := 0 }) ⟶ X₀)
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f)
  (x : SimplexCategoryᵒᵖ),
  (X.augment X₀ f w).hom.app x =
    CategoryTheory.CategoryStruct.comp (X.map ({ len := 0 }.const (Opposite.unop x) 0).op) f
-- Mathlib.CategoryTheory.Category.Cat.Op
/-- The equivalence `Cat ≌ Cat` associating each category with its opposite category.  -/
CategoryTheory.Cat.opEquivalence : CategoryTheory.Cat ≌ CategoryTheory.Cat
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'App.congr_simp : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R),
  ModuleCat.restrictScalarsId'App f hf M = ModuleCat.restrictScalarsId'App f hf M
-- Mathlib.Data.List.Infix
List.tail_subset : ∀ {α : Type u_1} (l : List α), l.tail ⊆ l
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D},
  (∀ {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π],
      CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
    F.PreservesFiniteEffectiveEpiFamilies
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.MethodsRef.toMethods : Lean.Meta.Grind.MethodsRef → Lean.Meta.Grind.Methods
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_monomial : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ), ((Polynomial.monomial n) a).leadingCoeff = a
-- Mathlib.Data.Finset.Sups
Finset.compls_univ : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : Fintype α], Finset.univ.compls = Finset.univ
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- If `f : Spec S → Spec R` is specializing and surjective, the topology on `Spec R` is the
quotient topology induced by `f`.  -/
PrimeSpectrum.isQuotientMap_of_specializingMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : R →+* S},
  Function.Surjective (PrimeSpectrum.comap f) →
    SpecializingMap (PrimeSpectrum.comap f) → Topology.IsQuotientMap (PrimeSpectrum.comap f)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedElimInfo : Inhabited Lean.Meta.ElimInfo
-- Init.Data.Int.Lemmas
Int.ofNat_mul_ofNat : ∀ (m n : ℕ), ↑m * ↑n = ↑(m * n)
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierModule` is a function space on which the Fourier transform is a linear map.  -/
FourierModule : (R : Type u_5) →
  (E : Type u_6) → (F : outParam (Type u_7)) → [Add E] → [Add F] → [SMul R E] → [SMul R F] → Type (max u_6 u_7)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.Indep.subset_finite_isBasis_of_subset_of_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α},
  M.Indep I →
    I ⊆ X →
      M.IsRkFinite X →
        autoParam (X ⊆ M.E) Matroid.Indep.subset_finite_isBasis_of_subset_of_isRkFinite._auto_1 →
          ∃ J, M.IsBasis J X ∧ I ⊆ J ∧ J.Finite
-- Mathlib.Topology.Separation.Basic
nhdsSet_le_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s t : Set X}, nhdsSet s ≤ nhdsSet t ↔ s ⊆ t
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.map_topologicalClosure_le : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : TopologicalSpace A]
  [inst_2 : NonUnitalSemiring A] [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A]
  [inst_5 : IsSemitopologicalSemiring A] [inst_6 : TopologicalSpace B] [inst_7 : NonUnitalSemiring B]
  [inst_8 : Module R B] [inst_9 : IsTopologicalSemiring B] [inst_10 : ContinuousConstSMul R B]
  (s : NonUnitalSubalgebra R A) {φ : A →ₙₐ[R] B},
  Continuous ⇑φ → NonUnitalSubalgebra.map φ s.topologicalClosure ≤ (NonUnitalSubalgebra.map φ s).topologicalClosure
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet_iff_iIndep : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepSet s μ ↔ ProbabilityTheory.iIndep (fun i => MeasurableSpace.generateFrom {s i}) μ
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_sub : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a b : AsBoolRing α),
  ofBoolRing (a - b) = symmDiff (ofBoolRing a) (ofBoolRing b)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.instInhabitedWithInitial : {a : Type u_1} → Inhabited (CategoryTheory.WithInitial a)
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An additive `n`-Freiman homomorphism preserves sums of `n` elements.  -/
IsAddFreimanIso.map_sum_eq_map_sum : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  IsAddFreimanIso n A B f →
    ∀ ⦃s t : Multiset α⦄,
      (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
        (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
          s.card = n → t.card = n → ((Multiset.map f s).sum = (Multiset.map f t).sum ↔ s.sum = t.sum)
-- Mathlib.Algebra.AffineMonoid.Embedding
Module.finBasis.congr_simp : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : StrongRankCondition R] [inst_5 : Module.Finite R M],
  Module.finBasis R M = Module.finBasis R M
-- Mathlib.Data.Set.List
_private.Mathlib.Data.Set.List.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- Smallest `b i`  -/
AkraBazziRecurrence.min_bi : {α : Type u_1} → [Finite α] → [Nonempty α] → (α → ℝ) → α
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.productEquiv.eq_1 : ∀ {ι : Type u_1} [inst : Finite ι] (X : ι → FintypeCat),
  CategoryTheory.Limits.FintypeCat.productEquiv X =
    (equivEquivIso.symm (CategoryTheory.Limits.PreservesProduct.iso FintypeCat.incl fun i => X i)).trans
      ((equivEquivIso.symm (CategoryTheory.Limits.Types.Small.productIso fun i => (X i).obj)).trans
        (equivShrink ((i : ι) → (X i).obj)).symm)
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- A variant of `HasSubst.of_constantCoeff_zero` for `PowerSeries`
to avoid the expansion of `Unit`.  -/
PowerSeries.HasSubst.of_constantCoeff_zero' : ∀ {S : Type u_4} [inst : CommRing S] {a : PowerSeries S}, PowerSeries.constantCoeff a = 0 → PowerSeries.HasSubst a
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instHashableLambdaTheoremArgs.hash : Mathlib.Meta.FunProp.LambdaTheoremArgs → UInt64
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given a family of vertex types indexed by `ι`, pulling back from `⊤ : SimpleGraph ι`
yields the complete multipartite graph on the family.
Two vertices are adjacent if and only if their indices are not equal.  -/
SimpleGraph.completeMultipartiteGraph : {ι : Type u_5} → (V : ι → Type u_6) → SimpleGraph ((i : ι) × V i)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The angle ∡ABB at a point.  -/
EuclideanGeometry.oangle_self_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ : P), EuclideanGeometry.oangle p₁ p₂ p₂ = 0
-- Mathlib.RingTheory.HopkinsLevitzki
/-- A finitely generated Artinian module over a commutative ring is Noetherian. This is not
necessarily the case over a noncommutative ring, see https://mathoverflow.net/a/61700.  -/
isNoetherian_of_finite_isArtinian : ∀ (M : Type u) [inst : AddCommGroup M] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Module R M] [Module.Finite R M]
  [IsArtinian R M], IsNoetherian R M
-- Mathlib.Topology.NhdsWithin
nhdsWithin_pi_univ_eq : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] [Finite ι] (s : (i : ι) → Set (X i))
  (x : (i : ι) → X i), nhdsWithin x (Set.univ.pi s) = ⨅ i, Filter.comap (fun x => x i) (nhdsWithin (x i) (s i))
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrder.toLocallyFiniteOrderBot.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderBot α],
  LocallyFiniteOrder.toLocallyFiniteOrderBot =
    { finsetIio := fun b => Finset.Ico ⊥ b, finsetIic := fun b => Finset.Icc ⊥ b, finset_mem_Iic := ⋯,
      finset_mem_Iio := ⋯ }
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.transition.sizeOf_spec : ∀ (thm : Mathlib.Meta.FunProp.GeneralTheorem), sizeOf (Mathlib.Meta.FunProp.Theorem.transition thm) = 1 + sizeOf thm