mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.Functor.mapDifferentialObject_obj_obj : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u')
  [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_6 : CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D)
  (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1))
  (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).obj = F.obj X.obj
-- Mathlib.Algebra.Order.Group.Synonym
isRightRegular_ofLex : ∀ {α : Type u_1} [inst : Monoid α] {a : Lex α}, IsRightRegular (ofLex a) ↔ IsRightRegular a
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves colimits, then `F : Cᵒᵖ ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Lean.Data.DeclarationRange
Lean.instReprDeclarationRanges : Repr Lean.DeclarationRanges
-- Aesop.Util.UnorderedArraySet
/-- O(n*log(n))  -/
Aesop.UnorderedArraySet.ofArray : {α : Type u_1} → [inst : BEq α] → [ord : Ord α] → Array α → Aesop.UnorderedArraySet α
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nonempty_image_addLeft_neg_inter_iff : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s t : Set α} {a : α},
  ((fun x => -a + x) '' s ∩ t).Nonempty ↔ ((fun x => x + a) '' (-s) ∩ -t).Nonempty
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_fun_snd : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : β → E),
  ∫ (z : α × β), f z.2 ∂μ.prod ν = μ.real Set.univ • ∫ (y : β), f y ∂ν
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.IsReduced.append_flatten_replicate_append : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
  FreeGroup.IsCyclicallyReduced L₂ →
    FreeGroup.IsReduced (L₁ ++ L₂ ++ L₃) →
      ∀ {n : ℕ}, n ≠ 0 → FreeGroup.IsReduced (L₁ ++ (List.replicate n L₂).flatten ++ L₃)
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.valid.injEq : ∀ (escaped : Bool) (acc : String) (escaped_1 : Bool) (acc_1 : String),
  (Std.Http.Internal.UnquoteState.valid✝ escaped acc = Std.Http.Internal.UnquoteState.valid✝ escaped_1 acc_1) =
    (escaped = escaped_1 ∧ acc = acc_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Implementation of the tensor product of morphisms for
`CartesianMonoidalCategory.ofChosenFiniteProducts`.  -/
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) →
      {X₁ X₂ Y₁ Y₂ : C} →
        (X₁ ⟶ Y₁) →
          (X₂ ⟶ Y₂) →
            (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ X₁ X₂ ⟶
              CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ Y₁ Y₂)
-- Mathlib.Algebra.LinearRecurrence
/-- We say that a sequence `u` is solution of `LinearRecurrence order coeffs` when we have
`u (n + order) = ∑ i : Fin order, coeffs i * u (n + i)` for any `n`.  -/
LinearRecurrence.IsSolution : {R : Type u_1} → [inst : CommSemiring R] → LinearRecurrence R → (ℕ → R) → Prop
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioc_sub_one_right_eq_Ioo : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] (a b : α),
  Set.Ioc a (b - 1) = Set.Ioo a b
-- Init.Grind.Ring.Field
Lean.Grind.Field.natCast_ne_zero : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] {n : ℕ}, n ≠ 0 → ↑n ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.inv f) z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn.eq : ∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} (t : Lean.Elab.Term.Do.Code)
  (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 = F_1 t (Lean.Elab.Term.Do.Code.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConstRingNormOfField_def : ∀ {K : Type u_1} [inst : Field K] {k : K} {g : RingSeminorm K} (hg1 : g 1 ≤ 1) (hg_k : g k ≠ 0) (hg_pm : IsPowMul ⇑g)
  (x : K), (normFromConst hg1 hg_k hg_pm) x = seminormFromConst' k g x
-- Init.Data.Option.Instances
Option.instForMOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Monad m] → ForM m (Option α) α
-- Mathlib.Computability.Language
Language.instKleeneAlgebra : {α : Type u_1} → KleeneAlgebra (Language α)
-- Mathlib.RepresentationTheory.FDRep
/-- This lemma is about `FDRep.ρ`, instead of `Action.ρ` for `of_ρ`.  -/
FDRep.of_ρ' : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] {V : Type u} [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : Module.Finite R V] (ρ : G →* V →ₗ[R] V), (FDRep.of ρ).ρ = ρ
-- Mathlib.LinearAlgebra.Dimension.RankNullity
Submodule.exists_smul_notMem_of_rank_lt : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] {N : Submodule R M},
  Module.rank R ↥N < Module.rank R M → ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_disjiUnion : ∀ {ι : Type u_1} {M : Type u_4} (s : Finset ι) (t : ι → Finset M) (h : (↑s).PairwiseDisjoint t),
  (s.disjiUnion t h).card = ∑ a ∈ s, (t a).card
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.const_linear : ∀ (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (p : P2), (AffineMap.const k P1 p).linear = 0
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.centralizer_eq_top_iff_subset : ∀ {M : Type u_1} [inst : AddSemigroup M] {s : Set M},
  AddSubsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubsemigroup.center M)
-- Init.Grind.AC
Lean.Grind.AC.simp_prefix_cert : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {x y : M.Derivation φ},
  @PresheafOfModules.Derivation.d C inst D inst_1 S F R M φ x =
      @PresheafOfModules.Derivation.d C inst D inst_1 S F R M φ y →
    x = y
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedMacroExpansionInfo : Inhabited Lean.Elab.MacroExpansionInfo
-- Mathlib.Analysis.Real.Sqrt
Real.inv_sqrt_two_sub_one : (√2 - 1)⁻¹ = √2 + 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.minKeyD fallback = t.keys.headD fallback
-- Mathlib.Logic.Function.Basic
Function.update_comp_eq_of_injective' : ∀ {α : Sort u} {β : α → Sort v} {α' : Sort w} [inst : DecidableEq α] [inst_1 : DecidableEq α'] (g : (a : α) → β a)
  {f : α' → α},
  Function.Injective f →
    ∀ (i : α') (a : β (f i)), (fun j => Function.update g (f i) a (f j)) = Function.update (fun i => g (f i)) i a
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.instSmallSubtypeEq_1 : ∀ {α : Type v} {x : α}, Std.Internal.Small { x_1 // x_1 = x }
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.IsSolvable.solvable_int : ∀ {L : Type v} {inst : LieRing L} [self : LieAlgebra.IsSolvable L], ∃ k, LieAlgebra.derivedSeries ℤ L k = ⊥
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Topology.Constructions
IsOpenQuotientMap.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i},
  (∀ (i : ι), IsOpenQuotientMap (f i)) → IsOpenQuotientMap (Pi.map f)
-- Lean.Elab.BindersUtil
Lean.Elab.Term.expandMatchAlts? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)
-- Mathlib.Data.FP.Basic
FP.FloatCfg : Type
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Multiplication of rational functions.  -/
RatFunc.mul : {K : Type u_1} → [inst : CommRing K] → RatFunc K → RatFunc K → RatFunc K
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
`cfc_integral`.  -/
cfc_integral' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [inst_6 : CompleteSpace A] [inst_7 : NormedSpace ℝ A] (f : X → 𝕜 → 𝕜)
  (a : A),
  (∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)) →
    MeasureTheory.Integrable (fun x => ContinuousMap.mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ →
      autoParam (p a) cfc_integral'._auto_1 → cfc (fun z => ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.ι_mapBifunctorFlipIso_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : TotalComplexShape c₂ c₁ c] [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_11 : DecidableEq J]
  [inst_12 : K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₁.π c₂ c (i₁, i₂) = j),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj) ((K₁.mapBifunctorFlipIso K₂ F c).inv.f j) =
    c₁.σ c₂ c i₁ i₂ • K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α}, k ∈ t₂ → Std.ExtDTreeMap.Const.get? (t₁ \ t₂) k = none
-- Mathlib.Data.List.Perm.Basic
List.perm_option_toList : ∀ {α : Type u_1} {o₁ o₂ : Option α}, o₁.toList.Perm o₂.toList ↔ o₁ = o₂
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- The map is alternating: if `v` has two equal coordinates, then `f v = 0`.  -/
ContinuousAlternatingMap.map_eq_zero_of_eq' : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (self : M [⋀^ι]→L[R] N) (v : ι → M) (i j : ι), v i = v j → i ≠ j → self.toFun v = 0
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The weighted total degree of a multivariate polynomial, taking values in `WithBot M`.  -/
MvPolynomial.weightedTotalDegree' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      {σ : Type u_3} → [AddCommMonoid M] → [SemilatticeSup M] → (σ → M) → MvPolynomial σ R → WithBot M
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.instInhabitedStatus : Inhabited Lean.Util.ParamMinimizer.Status
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.mk.inj : ∀ {α : Type u} {β : α → Type v} {_cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw._auto_1}
  {inner inner_1 : Std.DTreeMap.Internal.Impl α β}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Init.Internal.Order.Basic
Lean.Order.instCCPOEIOOfNonempty : {ε α : Type} → [Nonempty ε] → Lean.Order.CCPO (EIO ε α)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.example_oreLocalizationInstMonoid_eq_localizedModuleInstMonoid : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R}, OreLocalization.instMonoid = LocalizedModule.instMonoid
-- Init.Data.Option.Array
_private.Init.Data.Option.Array.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Addition of rational functions.  -/
RatFunc.add : {K : Type u_1} → [inst : CommRing K] → RatFunc K → RatFunc K → RatFunc K
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.toSurjectiveOnStalks : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.SurjectiveOnStalks f
-- Mathlib.Data.Nat.Factorization.PrimePow
isPrimePow_pow_iff : ∀ {n k : ℕ}, k ≠ 0 → (IsPrimePow (n ^ k) ↔ IsPrimePow n)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isThetaTVS_comm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F},
  f =Θ[𝕜; l] g ↔ g =Θ[𝕜; l] f
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- For each forall-bound variable in the type of the constructor, minus
the "params" that apply to the entire inductive type, this list contains `true`
if that variable has been kept after `compactRelation`.

For example, `List.Chain.nil` has type
```lean
  ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []`
```
and the first two variables `α` and `R` are "params", while the `a : α` gets
eliminated in a `compactRelation`, so `variablesKept = [false]`.

`List.Chain.cons` has type
```lean
  ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
     R a b → List.Chain R b l → List.Chain R a (b :: l)
```
and the `a : α` gets eliminated, so `variablesKept = [false,true,true,true,true]`.
 -/
Mathlib.Tactic.MkIff.Shape.variablesKept : Mathlib.Tactic.MkIff.Shape → List Bool
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.quotientKerEquivOfRightInverse.apply : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} {g : S → R}
  (hf : Function.RightInverse g ⇑f) (x : R ⧸ RingHom.ker f), (RingHom.quotientKerEquivOfRightInverse hf) x = f.kerLift x
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → sSup S = ⊤ → ComplementedLattice α
-- Mathlib.Order.Filter.Pointwise
/-- The singleton operation as an `AddHom`.  -/
Filter.pureAddHom : {α : Type u_2} → [inst : Add α] → α →ₙ+ Filter α
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_eq_top_iff_summable_norm : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), p.radius = ⊤ ↔ ∀ (r : NNReal), Summable fun n => ‖p n‖ * ↑r ^ n
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- When the additive subgroup `N < G` is not necessarily `Normal`, we have an `AddCosetSpace` as
opposed to `QuotientAddGroup` (the next `instance`).
TODO: typeclass inference should normally find this, but currently doesn't.
E.g., `MeasurableVAdd G (G ⧸ Γ)` fails to synthesize, even though `G ⧸ Γ` is the quotient
of `G` by the action of `Γ`; it seems unable to pick up the `BorelSpace` instance.  -/
AddCosetSpace.borelSpace : ∀ {G : Type u_3} [inst : TopologicalSpace G] [PolishSpace G] [inst_2 : AddGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] {N : AddSubgroup G} [T2Space (G ⧸ N)] [SecondCountableTopology (G ⧸ N)], BorelSpace (G ⧸ N)
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_counitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Functor.fromPUnit
            (CategoryTheory.MorphismProperty.Under.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)).comp
        (CategoryTheory.Functor.star (P.Under Q X)))
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_4 : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ), Int.Internal.Linear.Expr.denote ctx (Int.Internal.Linear.Expr.num k) = k
-- Mathlib.Order.Interval.Finset.Basic
Finset.left_mem_Ico : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], a ∈ Finset.Ico a b ↔ a < b
-- Std.Sync.Notify
/-- Notify exactly one waiting consumer (if any). Returns true if a consumer
was notified, false if no consumers were waiting.
 -/
Std.Notify.notifyOne : Std.Notify → BaseIO Bool
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
/-- `ContinuousLinearMap.restrictScalars` as a `LinearMap`. See also
`ContinuousLinearMap.restrictScalarsL`.  -/
ContinuousLinearMap.restrictScalarsₗ : (A : Type u_1) →
  (M₁ : Type u_2) →
    (M₂ : Type u_3) →
      (R : Type u_4) →
        (S : Type u_5) →
          [inst : Semiring A] →
            [inst_1 : Semiring R] →
              [inst_2 : Semiring S] →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : Module A M₁] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : TopologicalSpace M₁] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module A M₂] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : TopologicalSpace M₂] →
                                [LinearMap.CompatibleSMul M₁ M₂ R A] →
                                  [inst_12 : Module S M₂] →
                                    [inst_13 : ContinuousConstSMul S M₂] →
                                      [inst_14 : SMulCommClass A S M₂] →
                                        [inst_15 : SMulCommClass R S M₂] →
                                          [inst_16 : ContinuousAdd M₂] → (M₁ →L[A] M₂) →ₗ[S] M₁ →L[R] M₂
-- Mathlib.Logic.Equiv.Multiset
Denumerable.lower.eq_def : ∀ (x : List ℕ) (x_1 : ℕ),
  Denumerable.lower x x_1 =
    match x, x_1 with
    | [], x => []
    | m :: l, n => (m - n) :: Denumerable.lower l m
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.blocks_sum : ∀ {n : ℕ} (c : CompositionAsSet n), c.blocks.sum = n
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesPointwiseRightKanExtensions L` means that `G : B ⥤ D` preserves all pointwise right
Kan extensions along `L : A ⥤ C` of every functor `A ⥤ B`.  -/
CategoryTheory.Functor.PreservesPointwiseRightKanExtensions : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A C → Prop
-- Mathlib.Topology.Separation.Hausdorff
t2Space_antitone : ∀ {X : Type u_4}, Antitone (@T2Space X)
-- Mathlib.Data.Sym.Sym2
Sym2.coe_mk : ∀ {α : Type u_1} {x y : α}, ↑s(x, y) = {x, y}
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- An alternative characterization of a maximal linearly independent family,
quantifying over types (in the same universe as `M`) into which the indexing family injects.
 -/
LinearIndependent.maximal_iff : ∀ {ι : Type w} {R : Type u} [inst : Semiring R] [Nontrivial R] {M : Type v} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {v : ι → M} (i : LinearIndependent R v),
  i.Maximal ↔ ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Function.Surjective j
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.acc_of_single : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) →
    ∀ [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)] (x : Π₀ (i : ι), α i),
      (∀ i ∈ x.support, Acc (DFinsupp.Lex r s) fun₀ | i => x i) → Acc (DFinsupp.Lex r s) x
-- Mathlib.Topology.Bases
isTopologicalBasis_singletons : ∀ (α : Type u_1) [inst : TopologicalSpace α] [DiscreteTopology α],
  TopologicalSpace.IsTopologicalBasis {s | ∃ x, s = {x}}