mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.match_3.eq_2 : ∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) (solverId : ℕ) (e : Lean.Expr)
  (rest : Lean.Meta.Grind.SolverTerms)
  (h_1 : Unit → motive Lean.Meta.Grind.SolverTerms.nil Lean.Meta.Grind.SolverTerms.nil)
  (h_2 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive Lean.Meta.Grind.SolverTerms.nil (Lean.Meta.Grind.SolverTerms.next solverId e rest))
  (h_3 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive (Lean.Meta.Grind.SolverTerms.next solverId e rest) Lean.Meta.Grind.SolverTerms.nil)
  (h_4 :
    (id₁ : ℕ) →
      (rhs : Lean.Expr) →
        (rhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (lhs : Lean.Expr) →
              (lhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms)),
  (match Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.next solverId e rest with
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.nil => h_1 ()
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.next solverId e rest => h_2 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next solverId e rest, Lean.Meta.Grind.SolverTerms.nil => h_3 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms =>
      h_4 id₁ rhs rhsTerms id₂ lhs lhsTerms) =
    h_2 solverId e rest
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {f : ι → α × α}
  {l : Filter ι}, Filter.Tendsto f l (uniformity α) → Filter.Tendsto f⁻¹ l (uniformity α)
-- Mathlib.Data.ZMod.Basic
ZMod.val_add_of_lt : ∀ {n : ℕ} {a b : ZMod n}, a.val + b.val < n → (a + b).val = a.val + b.val
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects limits of shape `Jᵒᵖ`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits of
shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsColimitsOfShape J F.op
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.isOpenImmersion_iff_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y),
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion f ↔ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f.hom
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_eq_filter_range : ∀ (n : ℕ), n.primesBelow = Finset.filter Nat.Prime (Finset.range n)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.coeff_toAdditiveAlgEquiv_apply : ∀ (R : Type u_1) (A : Type u_4) (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (x : MonoidAlgebra A M),
  ((MonoidAlgebra.toAdditiveAlgEquiv R A M) x).coeff = Finsupp.mapDomain (⇑Additive.ofMul) x.coeff
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.isBoundedUnder_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α] {f : Filter ι}
  {u : ι → α} {a : α}, Filter.Tendsto u f (nhds a) → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.eraseAux : {α : Type u_1} →
  {β : Type u_2} → [BEq α] → Lean.PersistentHashMap.Node α β → USize → α → Lean.PersistentHashMap.Node α β
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The underlying object in the ambient category  -/
CategoryTheory.AddMod.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.AddMonObj A] → CategoryTheory.AddMod D A → D
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.lift_linear : ∀ (R : Type u_1) [inst : CommRing R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {D : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D),
  CategoryTheory.Functor.Linear R (CategoryTheory.Free.lift R F)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects colimits, then `F.leftOp : Cᵒᵖ ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_leftOp : ∀ {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.ReflectsColimits F],
  CategoryTheory.Limits.ReflectsLimits F.leftOp
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the morphism that is part of the factorization `fac`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.q : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {X : C} →
                {data : F.OneHypercoverDenseData J₀ J X} →
                  {X₀ : C₀} →
                    {f : F.obj X₀ ⟶ X} →
                      {Y₀ : C₀} → {g : Y₀ ⟶ X₀} → (self : data.SieveStruct f g) → F.obj Y₀ ⟶ F.obj (data.X self.i₀)
-- Mathlib.Topology.Order.ExtrClosure
IsMaxOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder Y]
  [OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X},
  IsMaxOn f s a → ContinuousOn f (closure s) → IsMaxOn f (closure s) a
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- For a "`C^n` ring" `R` and open sets `U ⊆ V` in `N`, the "restriction" ring homomorphism from
`C^n⟮I, V; I', R⟯` to `C^n⟮I, U; I', R⟯`.  -/
ContMDiffMap.restrictRingHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          (I' : ModelWithCorners 𝕜 E' H') →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    (R : Type u_10) →
                                      [inst_9 : Ring R] →
                                        [inst_10 : TopologicalSpace R] →
                                          [inst_11 : ChartedSpace H' R] →
                                            [inst_12 : ContMDiffRing I' n R] →
                                              {U V : TopologicalSpace.Opens N} →
                                                U ≤ V → ContMDiffMap I I' (↥V) R n →+* ContMDiffMap I I' (↥U) R n
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
/-- **Monotone convergence theorem** for an infimum over a directed family and indexed by a
countable type.  -/
MeasureTheory.lintegral_iInf_directed_of_measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Countable β] {f : β → α → ENNReal}
  {μ : MeasureTheory.Measure α},
  μ ≠ 0 →
    (∀ (b : β), Measurable (f b)) →
      (∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤) →
        Directed (fun x1 x2 => x1 ≥ x2) f → ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Aesop.RuleSet.Filter
Aesop.RuleFilter : Type
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNat_natEnd : ∀ (n : ℕ), ∀ x ∈ Turing.PartrecToTM2.trNat n, Turing.PartrecToTM2.natEnd x = false
-- Mathlib.Algebra.Lie.Basic
/-- The constant 0 map is a Lie algebra morphism.  -/
LieHom.instZero : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → Zero (L₁ →ₗ⁅R⁆ L₂)
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_comp : ∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {p : Submodule R M} {p₂ : Submodule R₂ M₂}
  {p₃ : Submodule R₃ M₃} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₃] M₃} (hf : Set.MapsTo ⇑f ↑p ↑p₂)
  (hg : Set.MapsTo ⇑g ↑p₂ ↑p₃) (hfg : optParam (Set.MapsTo ⇑(g ∘ₛₗ f) ↑p ↑p₃) ⋯),
  (g ∘ₛₗ f).restrict hfg = g.restrict hg ∘ₛₗ f.restrict hf
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.indiscrete.eq_1 : ∀ (n : ℕ), Nat.Partition.indiscrete n = Nat.Partition.ofSums n {n} ⋯
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- If a continuous function `c` realizes its maximum at a unique point `x₀` in a compact set `s`,
then the sequence of functions `(c x) ^ n / ∫ (c x) ^ n` is a sequence of peak functions
concentrating around `x₀`. Therefore, `∫ (c x) ^ n * g / ∫ (c x) ^ n` converges to `g x₀` if `g` is
continuous on `s`.  -/
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn : ∀ {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E} {x₀ : α} {s : Set α}
  [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure],
  IsCompact s →
    ∀ {c : α → ℝ},
      ContinuousOn c s →
        (∀ y ∈ s, y ≠ x₀ → c y < c x₀) →
          (∀ x ∈ s, 0 ≤ c x) →
            0 < c x₀ →
              x₀ ∈ closure (interior s) →
                ContinuousOn g s →
                  Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ)
                    Filter.atTop (nhds (g x₀))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
CategoryTheory.Sheaf.pushforwardOverMapIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] (F : CategoryTheory.Sheaf J A) {X Y : C} (f : X ⟶ Y),
  F.pushforwardOverMapIso f =
    CategoryTheory.ObjectProperty.isoMk (CategoryTheory.Presheaf.IsSheaf (J.over X))
      (CategoryTheory.NatIso.ofComponents
        (fun x =>
          CategoryTheory.Iso.refl
            ((((CategoryTheory.Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y)).obj.obj
              x))
        ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_leftShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n'),
  (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.of_isUnit_or_isUnit_one_sub_self : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R], (∀ (a : R), IsUnit a ∨ IsUnit (1 - a)) → IsLocalRing R
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.match_1.eq_4 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 :
    ByteArray.utf8DecodeChar?.FirstByte.twoMore = ByteArray.utf8DecodeChar?.FirstByte.invalid →
      motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 :
    ByteArray.utf8DecodeChar?.FirstByte.twoMore = ByteArray.utf8DecodeChar?.FirstByte.done →
      motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 :
    ByteArray.utf8DecodeChar?.FirstByte.twoMore = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 :
    ByteArray.utf8DecodeChar?.FirstByte.twoMore = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 :
    ByteArray.utf8DecodeChar?.FirstByte.twoMore = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match h : ByteArray.utf8DecodeChar?.FirstByte.twoMore with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) =
    h_4 ⋯
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_id_eq_factorial : ∀ (n : ℕ), ∏ x ∈ Finset.Ico 1 (n + 1), x = n.factorial
-- Mathlib.CategoryTheory.Adjunction.Comma
/-- If each structured arrow category on `G` has an initial object, construct a left adjoint to `G`. It
is shown that it is a left adjoint in `adjunctionOfStructuredArrowInitials`.
 -/
CategoryTheory.leftAdjointOfStructuredArrowInitials : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor D C) →
          [∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)] →
            CategoryTheory.Functor C D
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_subset_sdiff_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (u : Finset α), s ⊆ t → s \ u ⊆ t \ u
-- Init.Data.Function
Function.Injective.ne_iff : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ {x y : α}, f x ≠ f y ↔ x ≠ y
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Extend `f` to a larger partial linear map by adding a new `x`.  -/
HahnEmbedding.Partial.extendFun : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                (f : HahnEmbedding.Partial seed) →
                                  [IsOrderedAddMonoid R] →
                                    [Archimedean R] →
                                      {x : M} → x ∉ (↑f).domain → M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_two_mul : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b c d : ℤ),
  IsEllipticNet.atomRel W (2 * a) (2 * b) (2 * c) (2 * d) = IsEllipticNet.rel W (a - d) (b - d) (c - d) (2 * d)
-- Mathlib.Topology.Constructions
/-- If `f : X → Y` is a quotient map,
then its restriction to the preimage of an open set is a quotient map too.  -/
Topology.IsQuotientMap.restrictPreimage_isOpen : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsQuotientMap f → ∀ {s : Set Y}, IsOpen s → Topology.IsQuotientMap (s.restrictPreimage f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DHashMap.filterMap f m).contains k = true → m.contains k = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k}
  {fallback : β k'},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (t.insertMany l).getD k' fallback = cast ⋯ v
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer_le_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.centralizer s ≤ AddSubgroup.normalizer s
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- A surjective linear map to functions on a finite type has a splitting.  -/
LinearMap.splittingOfFunOnFintypeSurjective : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {α : Type u_5} → [Finite α] → (f : M →ₗ[R] α → R) → Function.Surjective ⇑f → (α → R) →ₗ[R] M
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.Decl.falseToCNF_eval : ∀ {α : Type u_1} {output : α} {assign : α → Bool},
  Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.falseToCNF✝ output) = (assign output == false)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- `ContinuousMultilinearMap.restrictScalars` as a `LinearIsometry`.  -/
ContinuousMultilinearMap.restrictScalarsₗᵢ : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [inst_5 : Fintype ι] →
                    (𝕜' : Type u_1) →
                      [inst_6 : NontriviallyNormedField 𝕜'] →
                        [inst_7 : NormedAlgebra 𝕜' 𝕜] →
                          [inst_8 : NormedSpace 𝕜' G] →
                            [inst_9 : IsScalarTower 𝕜' 𝕜 G] →
                              [inst_10 : (i : ι) → NormedSpace 𝕜' (E i)] →
                                [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] →
                                  ContinuousMultilinearMap 𝕜 E G →ₗᵢ[𝕜'] ContinuousMultilinearMap 𝕜' E G
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Upper hemicontinuous functions always have closed domain.

The more general fact is that if `f` is upper hemicontinuous at `x₀` within `s`, and if
`x₀` is a cluster point of `s ∩ {x | (f x).Nonempty}`, then `(f x₀).Nonempty`.  -/
UpperHemicontinuous.isClosed_domain : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f → IsClosed {x | (f x).Nonempty}
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
_private.Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm.0.PiTensorProduct.mapL_add_smul_aux : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {ι : Type u_7} {E : ι → Type u_8}
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_9}
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i) [inst_5 : DecidableEq ι] (i : ι) (u : E i →L[𝕜] E' i),
  (fun j => ↑(Function.update f i u j)) = Function.update (fun j => ↑(f j)) i ↑u
-- Init.Data.Int.Order
Int.one_pos : 0 < 1
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.op_neg : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (f : X ⟶ Y), (-f).op = -f.op
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.get?.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.gt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.gt = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.gt = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.gt with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_2 ⋯
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (S' : Type u_5)
  [inst_3 : CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [inst_6 : Algebra S S']
  [IsFractionRing S S'], IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) S'
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instFinite : ∀ {n : Type u_7} {m : Type u_8} [Finite m] [Finite n] (α : Type u_9) [Finite α], Finite (CStarMatrix m n α)
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.instNormedSpaceSmallComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    (hf : Manifold.IsSubmersionAtOfComplement F I J n f x) →
                                                      NormedSpace 𝕜 hf.smallComplement
-- Init.Data.SInt.Lemmas
Int64.toInt32_ofInt : ∀ {n : ℤ}, (Int64.ofInt n).toInt32 = Int32.ofInt n
-- Mathlib.Topology.EMetricSpace.Defs
instEMetricSpaceAdditive : {X : Type u_1} → [EMetricSpace X] → EMetricSpace (Additive X)
-- Init.Data.Int.LemmasAux
Int.blt'.eq_1 : ∀ (a b : ℤ),
  a.blt' b =
    Int.rec (fun a => Int.rec (fun b => a.blt b) (fun x => false) b)
      (fun a => Int.rec (fun x => true) (fun b => b.blt a) b) a
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.add_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a + b).toProd.2 = a.toProd.2 + b.toProd.2