mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkSemiringInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
instFiniteUnits : ∀ {α : Type u_1} [inst : Monoid α] [Finite α], Finite αˣ
-- Lean.Data.NameMap.Basic
Lean.NameMap.instEmptyCollection : (α : Type) → EmptyCollection (Lean.NameMap α)
-- Mathlib.Data.Fintype.Sets
Fintype.coe_image_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β},
  ↑(Finset.image f Finset.univ) = Set.range f
-- Mathlib.Topology.Algebra.Module.Complement
/-- If `h : IsTopCompl p q`, `h.projection` is the continuous linear projection `M →L[R] M` onto
`p` along `q`. This is the continuous version of `Submodule.IsCompl.projection`.

See also `Submodule.IsTopCompl.projectionOnto` for the same projection as an element of
`M →L[R] p`.  -/
Submodule.projectionL : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → (p q : Submodule R M) → Submodule.IsTopCompl p q → M →L[R] M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  (Std.ExtDHashMap.map f m).contains k = m.contains k
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignGenInfo? : Option Lean.Meta.Grind.GenPatternInfo →
  Lean.Meta.Grind.EMatch.Choice → Lean.Expr → OptionT Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Mathlib.Data.Sym.Sym2
Sym2.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Sym2 α)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_add_compl₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.Integrable f μ → ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- A category `J` is `κ`-filtered (for a regular cardinal `κ`) if
any functor `F : A ⥤ J` from a category `A` such that `HasCardinalLT (Arrow A) κ`
admits a cocone. See `isCardinalFiltered_iff` for a more
concrete characterization of `κ`-filtered categories.  -/
CategoryTheory.IsCardinalFiltered : (J : Type u) → [CategoryTheory.Category.{v, u} J] → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_add_right_of_mem_nhds_zero_of_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (s : Set G) {s' : Set G},
  s' ∈ nhds 0 → (∀ x ∈ s', -x ∈ s') → closure s ⊆ s + s'
-- Mathlib.Algebra.Group.Nat.Even
Nat.two_not_dvd_two_mul_sub_one : ∀ {n : ℕ}, 0 < n → ¬2 ∣ 2 * n - 1
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_indicator_one : ∀ {ι : Type u_1} {K : Type u_3} [inst : Semifield K] [inst_1 : CharZero K] [inst_2 : Fintype ι] (s : Finset ι),
  (Finset.univ.expect fun i => (↑s).indicator 1 i) = ↑s.dens
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.firstDiff_lt_shortestPrefixDiff : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)},
  IsClosed s → ∀ {x y : (n : ℕ) → E n}, x ∉ s → y ∈ s → PiNat.firstDiff x y < PiNat.shortestPrefixDiff x s
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_mul_interval : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s t : NonemptyInterval α), ↑(s * t) = ↑s * ↑t
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.SatisfiesM_mapFinIdxM.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α}
  {f : (i : ℕ) → α → i < as.size → m β} {motive : ℕ → Prop} {p : (i : ℕ) → β → i < as.size → Prop},
  (∀ (i : ℕ) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)) →
    ∀ {bs : Array β} {i j : ℕ} {h : i + j = as.size},
      j = bs.size →
        (∀ (i : ℕ) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
          motive j →
            SatisfiesM
              (fun arr =>
                motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i_1 : ℕ) (h : i_1 < as.size), p i_1 arr[i_1] h)
              (Array.mapFinIdxM.map as f i j h bs)
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_mul_left_left : ∀ (m n k : ℕ), (m + n * k).Coprime n ↔ m.Coprime n
-- Mathlib.Order.Interval.Set.ProjIcc
/-- Extend a function `[a, b] → β` to a map `α → β`.  -/
Set.IccExtend : {α : Type u_1} → {β : Type u_2} → [inst : LinearOrder α] → {a b : α} → a ≤ b → (↑(Set.Icc a b) → β) → α → β
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_id_id : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod.map (AddMonoidHom.id M) (AddMonoidHom.id N) = AddMonoidHom.id (AddMonoid.Coprod M N)
-- Mathlib.Data.Multiset.Filter
Multiset.filter_cons_of_pos : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
  p a → Multiset.filter p (a ::ₘ s) = a ::ₘ Multiset.filter p s
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.all_eq_forIn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {p : β → Bool},
  Std.IterM.all p it =
    forIn it { down := true } fun x x_1 =>
      if p x = true then pure (ForInStep.yield { down := true }) else pure (ForInStep.done { down := false })
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e),
  (CategoryTheory.CostructuredArrow.preEquivalence F f).inverse =
    CategoryTheory.CostructuredArrow.preEquivalence.inverse F f
-- Mathlib.Data.List.ReduceOption
List.reduceOption_concat_of_some : ∀ {α : Type u_1} (l : List (Option α)) (x : α), (l.concat (some x)).reduceOption = l.reduceOption.concat x
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The derivative of a continuous multilinear map, as a continuous linear map
from `∀ i, M₁ i` to `M₂`; see `ContinuousMultilinearMap.hasFDerivAt`.  -/
ContinuousMultilinearMap.linearDeriv : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] →
                      ContinuousMultilinearMap R M₁ M₂ →
                        [ContinuousAdd M₂] →
                          [DecidableEq ι] → [Fintype ι] → ((i : ι) → M₁ i) → ((i : ι) → M₁ i) →L[R] M₂
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.congr : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f g : E →L[R] F}, f.HasRightInverse → g = f → g.HasRightInverse
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.iso₂Mk_inv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (el : α.l ≅ β.l) (er : β.r ≅ α.r)
  (h :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) el.hom = er.hom)
      CategoryTheory.Bicategory.Adj.iso₂Mk._auto_1),
  (CategoryTheory.Bicategory.Adj.iso₂Mk el er h).inv.τl = el.inv
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.length_lt_card_boundaries : ∀ {n : ℕ} (c : CompositionAsSet n), c.length < c.boundaries.card
-- Mathlib.Algebra.Group.Subgroup.Pointwise
coe_sub_coe : ∀ {G : Type u_2} {S : Type u_4} [inst : SetLike S G] [inst_1 : SubtractionMonoid G] [AddSubgroupClass S G] (H : S),
  ↑H - ↑H = ↑H
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.complexConj.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K], NumberField.IsCMField.complexConj K = NumberField.IsCMField.complexConj K
-- Init.Data.SInt.Basic
instPowISizeNat : Pow ISize ℕ
-- Mathlib.Probability.Independence.Integration
/-- If a random variable `f` in `ℝ≥0∞` is independent of an event `T`, then if you restrict the
random variable to `T`, then `E[f * indicator T c 0]=E[f] * E[indicator T c 0]`. It is useful for
`lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace`.  -/
ProbabilityTheory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator : ∀ {Ω : Type u_1} {f : Ω → ENNReal} {Mf mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  Mf ≤ mΩ →
    ∀ (c : ENNReal) {T : Set Ω},
      MeasurableSet T →
        ProbabilityTheory.IndepSets {s | MeasurableSet s} {T} μ →
          Measurable f →
            ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ =
              (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
-- Mathlib.Order.Fin.Basic
Fin.instHeytingAlgebra : {n : ℕ} → [NeZero n] → HeytingAlgebra (Fin n)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
AddSubgroup.intCast_mem_zmultiples_one : ∀ {R : Type u_4} [inst : Ring R] (k : ℤ), ↑k ∈ AddSubgroup.zmultiples 1
-- Mathlib.AlgebraicGeometry.Restrict
/-- The restrictions onto two equal open sets are isomorphic. This currently has bad defeqs when
unfolded, but it should not matter for now. Replace this definition if better defeqs are needed.  -/
AlgebraicGeometry.morphismRestrictEq : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → {U V : Y.Opens} → U = V → (CategoryTheory.Arrow.mk (f ∣_ U) ≅ CategoryTheory.Arrow.mk (f ∣_ V))
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Ico : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  NNRat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.of_denote_le_cancel : ∀ {ctx : Nat.Internal.Linear.Context} {m₁ m₂ : Nat.Internal.Linear.Poly},
  Nat.Internal.Linear.Poly.denote_le ctx (m₁.cancel m₂) → Nat.Internal.Linear.Poly.denote_le ctx (m₁, m₂)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_obj_a : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : G ⟶ F)
  (A : CategoryTheory.Endofunctor.Algebra F), ((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).obj A).a = A.a
-- Mathlib.Algebra.Order.Monovary
antivaryOn_iff_forall_smul_nonpos : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map.hcongr_8 : ∀ (V V' : Type u),
  V = V' →
    ∀ (V'_1 V'' : Type v),
      V'_1 = V'' →
        ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
          G ≍ G' →
            ∀ (G'_1 : SimpleGraph V'_1) (G'' : SimpleGraph V''),
              G'_1 ≍ G'' →
                ∀ (f : G →g G'_1) (f' : G' →g G''),
                  f ≍ f' →
                    ∀ (u : V) (u' : V'),
                      u ≍ u' →
                        ∀ (v : V) (v' : V'),
                          v ≍ v' →
                            ∀ (a : G.Walk u v) (a' : G'.Walk u' v'),
                              a ≍ a' → SimpleGraph.Walk.map f a ≍ SimpleGraph.Walk.map f' a'
-- Lean.Data.Json.Basic
Lean.instInhabitedJson.default : Lean.Json
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C}
  (x : (F.obj X).obj) (y : (F.obj Y).obj),
  (CategoryTheory.ConcreteCategory.hom (F.map CategoryTheory.Limits.prod.fst))
      ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) =
    x
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
polynomial over the fraction field. Compared to `minpoly.isIntegrallyClosed_eq_field_fractions`,
this version is useful if the element is in a ring that is already a `K`-algebra.  -/
minpoly.isIntegrallyClosed_eq_field_fractions' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  (K : Type u_3) [inst_4 : Field K] [inst_5 : Algebra R K] [IsFractionRing R K] [IsIntegrallyClosed R] [IsDomain S]
  [inst_9 : Algebra K S] [IsScalarTower R K S] {s : S},
  IsIntegral R s → minpoly K s = Polynomial.map (algebraMap R K) (minpoly R s)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapAddGrp_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal], e.mapAddGrp.inverse = e.inverse.mapAddGrp
-- Init.Data.UInt.Bitwise
UInt8.shiftLeft_and : ∀ {a b c : UInt8}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddRightCancelSemigroup : {α : Type u_1} → [AddRightCancelSemigroup α] → AddRightCancelSemigroup αᵒᵈ
-- Lean.Meta.Tactic.Grind.LawfulEqCmp
Lean.Meta.Grind.propagateLawfulEqCmp : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Topology.CompactOpen
/-- A family `F` of functions in `C(X, Y)` converges in the compact-open topology, if and only if
it converges in the compact-open topology on each compact subset of `X`.  -/
ContinuousMap.exists_tendsto_compactOpen_iff_forall : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [WeaklyLocallyCompactSpace X]
  [T2Space Y] {ι : Type u_6} {l : Filter ι} [l.NeBot] (F : ι → C(X, Y)),
  (∃ f, Filter.Tendsto F l (nhds f)) ↔
    ∀ (s : Set X), IsCompact s → ∃ f, Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (nhds f)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The negative logarithmic derivative of the L-function of a nontrivial Dirichlet character
is continuous away from the zeros of the L-function.  -/
DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv : ∀ {n : ℕ} [inst : NeZero n] {χ : DirichletCharacter ℂ n},
  χ ≠ 1 →
    ContinuousOn (fun s => -deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s)
      {s | DirichletCharacter.LFunction χ s ≠ 0}
-- Mathlib.Computability.TuringDegree
TuringReducible.refl : ∀ (f : ℕ →. ℕ), TuringReducible f f
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fract_add_of_mem_closure : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] {x y : ι → ℕ},
  y ∈ AddSubmonoid.closure (IsProperLinearSet.basisSet✝ hs) →
    IsProperLinearSet.fract✝ hs (x + y) = IsProperLinearSet.fract✝ hs x
-- Init.Data.Int.Basic
/-- `-[n+1]` is suggestive notation for `negSucc n`, which is the second constructor of
`Int` for making strictly negative numbers by mapping `n : Nat` to `-(n + 1)`.
 -/
Int.«term-[_+1]» : Lean.ParserDescr
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] [Nontrivial R],
  M ≤ nonZeroDivisors R → ∀ {x : R}, x ∈ nonZeroDivisors R → (algebraMap R S) x ≠ 0
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- In a finite-dimensional `InnerProductSpace`, any orthonormal subset can be extended to an
orthonormal basis.  -/
Orthonormal.exists_orthonormalBasis_extension : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v : Set E} [FiniteDimensional 𝕜 E], Orthonormal 𝕜 Subtype.val → ∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonTextDocumentClientCapabilities : Lean.ToJson Lean.Lsp.TextDocumentClientCapabilities
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- If vector fields coincide on a neighborhood of a point within a set, then the Lie brackets
also coincide on a neighborhood of this point within this set. Version where one considers the Lie
bracket within a subset.  -/
Filter.EventuallyEq.mlieBracketWithin_vectorField' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhdsWithin x s] V →
    W₁ =ᶠ[nhdsWithin x s] W →
      t ⊆ s → VectorField.mlieBracketWithin I V₁ W₁ t =ᶠ[nhdsWithin x s] VectorField.mlieBracketWithin I V W t
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.num.injEq : ∀ (i i_1 : ℕ), (Nat.Internal.SOM.Expr.num i = Nat.Internal.SOM.Expr.num i_1) = (i = i_1)
-- Lean.Meta.Closure
Lean.Meta.Closure.State.newLetDecls : Lean.Meta.Closure.State → Array Lean.LocalDecl
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- The current tactic-mode goals.  -/
SelectInsertParams.goals : SelectInsertParams → Array Lean.Widget.InteractiveGoal
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Given a simplicial set `X`, this constructs a `StrictSegal` structure for `X` from
`StrictSegalCore` structures for all `n : ℕ`.  -/
SSet.StrictSegal.ofCore : {X : SSet} → ((n : ℕ) → X.StrictSegalCore n) → X.StrictSegal
-- Mathlib.Topology.Homotopy.Lifting
/-- **Alias** of the forward direction of `IsQuotientCoveringMap.monodromy_ext_iff`. -/
IsQuotientCoveringMap.monodromy_ext : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x y : X}
  {γ γ' : Path.Homotopic.Quotient x y} (e : ↑(p ⁻¹' {x})),
  ⋯.monodromy γ e = ⋯.monodromy γ' e → ⋯.monodromy γ = ⋯.monodromy γ'
-- Mathlib.Algebra.Ring.Pi
/-- **Alias** of `RingHom.pi_apply`. -/
Pi.ringHom_apply : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [inst : (i : I) → NonAssocSemiring (f i)] [inst_1 : NonAssocSemiring γ]
  (g : (i : I) → γ →+* f i) (x : γ) (b : I), (RingHom.pi g) x b = (g b) x
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjoint_apply_of_dense : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E] (hT : Dense ↑T.domain) (y : ↥T.adjoint.domain), ↑T.adjoint y = (LinearPMap.adjointAux hT) y
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_conj : ∀ {d : ℤ} (x : ℤ√d), (star x).norm = x.norm
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd_inv_app : ∀ {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] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a b : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (e₂ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) (X : C),
  (CategoryTheory.Functor.CommShift.isoAdd e₁ e₂).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map (e₁.inv.app X))
        (CategoryTheory.CategoryStruct.comp (e₂.inv.app ((CategoryTheory.shiftFunctor C a).obj X))
          (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X))))
-- Mathlib.Algebra.Group.Units.Defs
Group.isUnit : ∀ {α : Type u} [inst : Group α] (a : α), IsUnit a
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instFunLikeForall : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] → FunLike (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.GroupTheory.Exponent
AddSubmonoid.nsmul_exponent_eq_zero : ∀ {G : Type u} [inst : AddMonoid G] {S : AddSubmonoid G} {g : G}, g ∈ S → AddMonoid.exponent ↥S • g = 0
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ici₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Ici a = Set.Ici (a / c)
-- Mathlib.Order.Category.Lat
/-- The category of lattices.  -/
Lat : Type (u_1 + 1)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.brecOn_3.eq : ∀ {α : Type} {motive_1 : Lean.Meta.DiscrTree.Trie α → Sort u}
  {motive_2 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_3 : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Sort u}
  {motive_4 : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α → Sort u}
  (t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)
  (F_1 : (t : Lean.Meta.DiscrTree.Trie α) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) →
      Lean.Meta.DiscrTree.Trie.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) → Lean.Meta.DiscrTree.Trie.below_2 t → motive_3 t)
  (F_4 : (t : Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree.Trie.below_3 t → motive_4 t),
  Lean.Meta.DiscrTree.Trie.brecOn_3 t F_1 F_2 F_3 F_4 = F_4 t (Lean.Meta.DiscrTree.Trie.brecOn_3.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.dens_stable_of_terminated : ∀ {K : Type u_1} {g : GenContFract K} {n m : ℕ} [inst : DivisionRing K], n ≤ m → g.TerminatedAt n → g.dens m = g.dens n
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- A product monoid algebra is a nested monoid algebra.  -/
AddMonoidAlgebra.curryAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddMonoid M] →
                [inst_4 : AddMonoid N] → AddMonoidAlgebra A (M × N) ≃ₐ[R] AddMonoidAlgebra (AddMonoidAlgebra A N) M