mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withInfoContext' : Lean.Syntax →
  Lean.Elab.TermElabM Lean.Expr →
    (Lean.Expr → Lean.Elab.TermElabM (Lean.Elab.Info ⊕ Lean.MVarId)) →
      Lean.Elab.TermElabM Lean.Elab.Info → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.IsStrictSegal.spine_bijective : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) [self : X.IsStrictSegal] (m : ℕ)
  (h : autoParam (m ≤ n + 1) SSet.Truncated.IsStrictSegal._auto_1), Function.Bijective (X.spine m h)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
              (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
                (𝒰.f j))
              (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DHashMap.Const.insertMany m l).getKey! k = m.getKey! k
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit_div : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α} (ha : IsUnit a) (hb : IsUnit b), ⋯.unit = ha.unit / hb.unit
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.basis.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ], P.basis = P.basis
-- Init.Data.Char.Basic
Char.instDecidableLe : (a b : Char) → Decidable (a ≤ b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (e_a : a = a_1) (l l_1 : List ((a : α) × β a))
  (e_l : l = l_1) (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getEntry a l h = Std.Internal.List.getEntry a_1 l_1 ⋯
-- Std.Http.Data.Method
Std.Http.Method.link.sizeOf_spec : sizeOf Std.Http.Method.link = 1
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
/-- Predicate that an array is a correct precomputation of the prefix function.  -/
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable : ByteArray → Array ℕ → Prop
-- Mathlib.Order.Hom.Bounded
TopHom.instLattice.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Lattice β] [inst_2 : OrderTop β],
  TopHom.instLattice = Function.Injective.lattice DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernstein_apply : ∀ (n ν : ℕ) (x : ↑unitInterval), (bernstein n ν) x = ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
-- Init.Prelude
/-- Handles exceptions thrown in the combined error and state monad.

The `Backtrackable δ σ` instance is used to save a snapshot of part of the state prior to running
`x`. If an exception is caught, the state is updated with the saved snapshot, rolling back part of
the state. If no instance of `Backtrackable` is provided, a fallback instance in which `δ` is `Unit`
is used, and no information is rolled back.
 -/
EStateM.tryCatch : {ε σ δ : Type u} → [EStateM.Backtrackable δ σ] → {α : Type u} → EStateM ε σ α → (ε → EStateM ε σ α) → EStateM ε σ α
-- Mathlib.MeasureTheory.Group.Arithmetic
IsAddUnit.aemeasurable_const_vadd_iff : ∀ {M : Type u_4} {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_2 : AddMonoid M] [inst_3 : AddAction M β] [MeasurableConstVAdd M β] {c : M},
  IsAddUnit c → (AEMeasurable (fun x => c +ᵥ f x) μ ↔ AEMeasurable f μ)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.gi.eq_1 : ∀ (G : Type u_1) [inst : Group G],
  Subgroup.gi G = { choice := fun s x => Subgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedElimAltInfo : Inhabited Lean.Meta.ElimAltInfo
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
/-- `pointwiseProduct` is invariant under re-indexing.  -/
CategoryTheory.Limits.Pi.equivalenceOfEquivCompPointwiseProduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type u_1} →
      {I : α → Type u_2} →
        [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] →
          [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C] →
            (F : (i : α) → CategoryTheory.Functor (I i) C) →
              {β : Type u_3} →
                (f : β ≃ α) →
                  [inst_3 : CategoryTheory.Limits.HasProductsOfShape β C] →
                    (CategoryTheory.Pi.equivalenceOfEquiv I f).inverse.comp
                        (CategoryTheory.Limits.pointwiseProduct fun i => F (f i)) ≅
                      CategoryTheory.Limits.pointwiseProduct F
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.checkDisambiguation : (s : String) → s.Pos → Bool
-- Mathlib.Algebra.CharP.Lemmas
add_pow_char_of_commute : ∀ {R : Type u_1} [inst : Semiring R] {x y : R} (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p],
  Commute x y → (x + y) ^ p = x ^ p + y ^ p
-- Init.Data.Array.Attach
Array.pmap.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f f_1 : (a : α) → P a → β),
  f = f_1 → ∀ (xs xs_1 : Array α) (e_xs : xs = xs_1) (H : ∀ a ∈ xs, P a), Array.pmap f xs H = Array.pmap f_1 xs_1 ⋯
-- Init.Data.UInt.Bitwise
UInt32.toNat_xor : ∀ (a b : UInt32), (a ^^^ b).toNat = a.toNat ^^^ b.toNat
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.mk : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [toModule : Module 𝕜 E] → (∀ (a : 𝕜) (b : E), ‖a • b‖ ≤ ‖a‖ * ‖b‖) → NormedSpace 𝕜 E
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Iio : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α}, IsPreconnected (Set.Iio a)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instIsMonHomHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (f : M ⟶ N), CategoryTheory.IsMonHom f.hom
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₂ = f.left.hom
-- Lean.Meta.Basic
/-- Helper method for `isClassExpensive?`. The type `type` is in WHNF.
 -/
_private.Lean.Meta.Basic.0.Lean.Meta.isClassApp? : Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_le_of_isSuccLimit : ∀ {c : Cardinal.{u_1}}, Order.IsSuccLimit c → Cardinal.aleph0 ≤ c
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.homRel_iff_leftHomotopyRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.BifibrantObject C} {f g : X ⟶ Y},
  HomotopicalAlgebra.BifibrantObject.homRel C f g ↔ HomotopicalAlgebra.LeftHomotopyRel f.hom g.hom
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.sum_map_zero : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {l : List ι}, (List.map (fun x => 0) l).sum = 0
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Make a `GenContFract.Pair` printable.  -/
GenContFract.Pair.instRepr : {α : Type u_1} → [Repr α] → Repr (GenContFract.Pair α)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_sq_eq_of_L2 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (x y : PiLp 2 β), dist x y ^ 2 = ∑ i, dist (x.ofLp i) (y.ofLp i) ^ 2
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν] {f : β → E},
  MeasureTheory.Integrable f ν →
    ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
      MeasureTheory.Integrable (fun x => f x.2) (μ.prod ν)
-- Init.Data.SInt.Lemmas
ISize.toInt_div_of_ne_left : ∀ (a b : ISize), a ≠ ISize.minValue → (a / b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.SetTheory.Cardinal.NatCard
Set.Finite.eq_of_subset_of_card_le : ∀ {α : Type u_1} {s t : Set α}, t.Finite → s ⊆ t → Nat.card ↑t ≤ Nat.card ↑s → s = t
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimitSMulAux_eq_of_rel : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (r : R)
  (x y : (j : J) × ↑(F.obj j)),
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget (ModuleCat R))) x y →
    ModuleCat.FilteredColimits.colimitSMulAux F r x = ModuleCat.FilteredColimits.colimitSMulAux F r y
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite
intervals.  -/
MeasureTheory.Measure.ext_of_Ici : ∀ {α : Type u_5} [inst : TopologicalSpace α] {x : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ], (∀ (a : α), μ (Set.Ici a) = ν (Set.Ici a)) → μ = ν
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.Legacy.Iterator.remainingBytes.match_1.eq_1 : ∀ (motive : String.Legacy.Iterator → Sort u_1) (s : String) (i : String.Pos.Raw)
  (h_1 : (s : String) → (i : String.Pos.Raw) → motive { s := s, i := i }),
  (match { s := s, i := i } with
    | { s := s, i := i } => h_1 s i) =
    h_1 s i
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.oneUnique : (G : Type u_2) → [inst : Group G] → Unique ↑(Equiv.Perm.vectorsProdEqOne G 1)
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Iic : ∀ (a : ℝ), UniqueDiffOn ℝ (Set.Iic a)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instFaithfulSMulCore : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ}, FaithfulSMul P.Core R
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.eq_sign_of_surjective_hom : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {s : Equiv.Perm α →* ℤˣ},
  Function.Surjective ⇑s → s = Equiv.Perm.sign
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
/-- Pull a subalgebra back to a subalgebra along `MulOpposite.op`  -/
Subalgebra.unop : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R Aᵐᵒᵖ → Subalgebra R A
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.mem_colorClass : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) (v : V), v ∈ C.colorClass (C v)
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.cycleCons.match_1.eq_1 : ∀ (n : ℕ) (motive : Fin (n + 3) → Sort u_1) (h : 0 < n + 3) (h_1 : (h : 0 < n + 3) → motive ⟨0, h⟩)
  (h_2 : (m : ℕ) → (h : m + 1 < n + 3) → motive ⟨m.succ, h⟩),
  (match ⟨0, h⟩ with
    | ⟨0, h⟩ => h_1 h
    | ⟨m.succ, h⟩ => h_2 m h) =
    h_1 h
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.of_comp_right : ∀ {U : Type u_3} [inst : Quiver U] {V : Type u_1} [inst_1 : Quiver V] (φ : U ⥤q V) {W : Type u_2} [inst_2 : Quiver W]
  (ψ : V ⥤q W), ψ.IsCovering → (φ ⋙q ψ).IsCovering → φ.IsCovering
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.isEmpty = (t.size == 0)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} {s : Set β}, MeasurableSet s → ρ.snd s = ρ (Prod.snd ⁻¹' s)
-- Mathlib.NumberTheory.NumberField.ClassNumber
RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  (∀ ⦃I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))⦄,
      (↑I).IsPrime →
        ↑(Ideal.absNorm ↑I) ≤
            (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
              (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
                √|↑(NumberField.discr K)|) →
          Submodule.IsPrincipal ↑I) →
    IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Mathlib.GroupTheory.GroupAction.CardCommute
instInfiniteProdSubtypeCommute : ∀ {α : Type u_1} [inst : Mul α] [Infinite α], Infinite { p // Commute p.1 p.2 }
-- Mathlib.Order.Circular
/-- For any fixed `c`, `fun a b ↦ sbtw a b c` is a transitive relation.

I.e., given `a` `b` `d` `c` in that "order", if we have `b` strictly between `a` and `c`, and `d`
strictly between `b` and `c`, then `d` is strictly between `a` and `c`.  -/
CircularPreorder.sbtw_trans_left : ∀ {α : Type u_1} [self : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d c
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.mem_unop : ∀ {G : Type u_2} [inst : Group G] {x : G} {S : Subgroup Gᵐᵒᵖ}, x ∈ S.unop ↔ MulOpposite.op x ∈ S
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.add_compContinuous : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Add β]
  [inst_3 : BoundedAdd β] [inst_4 : ContinuousAdd β] [inst_5 : TopologicalSpace γ] (f g : BoundedContinuousFunction α β)
  (h : C(γ, α)), (g + f).compContinuous h = g.compContinuous h + f.compContinuous h
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Equations to process.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.queue : Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Meta.Grind.Arith.CommRing.Queue
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSet_empty_left : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ] (s : Set Ω),
  ProbabilityTheory.Kernel.IndepSet ∅ s κ μ
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.replaceEntry : {α : Type u} → {β : α → Type v} → [BEq α] → (k : α) → β k → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instIsIsoFunctorUnitTopCatAdj : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  CategoryTheory.IsIso GeneratedByTopCat.adj.unit
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_insert' : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {s : Set M},
  x ∈ Submodule.span R (insert y s) ↔ ∃ a, x + a • y ∈ Submodule.span R s
-- Mathlib.NumberTheory.NumberField.DedekindZeta
/-- **Dirichlet class number formula**
 -/
NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Filter.Tendsto (fun s => (↑s - 1) * NumberField.dedekindZeta K ↑s) (nhdsWithin 1 (Set.Ioi 1))
    (nhds ↑(NumberField.dedekindZeta_residue K))
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_cons_succ : ∀ {a : Bool} {w : ℕ} {x : BitVec w} {i : ℕ}, (BitVec.cons a x).getMsbD (i + 1) = x.getMsbD i
-- Mathlib.ModelTheory.Basic
/-- A language is algebraic when it has no relation symbols.  -/
FirstOrder.Language.IsAlgebraic : FirstOrder.Language → Prop
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.comp.inj : ∀ {a : Turing.ToPartrec.Code} {a_1 : Turing.ToPartrec.Cont} {a_2 : Turing.ToPartrec.Code} {a_3 : Turing.ToPartrec.Cont},
  Turing.ToPartrec.Cont.comp a a_1 = Turing.ToPartrec.Cont.comp a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.complexBasis.eq_1 : ∀ (α : Type u_1) [inst : AddCommGroup α] [inst_1 : Finite α],
  AddChar.complexBasis α = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getNatStructId?.go? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.smul_bot : ∀ {M : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : DistribSMul M V] [inst_4 : SMulCommClass M k V] (a : M), a • ⊥ = ⊥
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_monomial_le : ∀ {R : Type u} [inst : Semiring R] (a : R) {m : ℕ}, ((Polynomial.monomial m) a).natDegree ≤ m
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.replace.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → α → α → Sort u_2) (x x_1 : α) (h_1 : (x x_2 : α) → motive [] x x_2)
  (h_2 : (a : α) → (as : List α) → (b c : α) → motive (a :: as) b c),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | a :: as, b, c => h_2 a as b c) =
    h_1 x x_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictDerivAt.ccosh : ∀ {f : ℂ → ℂ} {f' x : ℂ},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- `S.leftInv` is the submonoid containing all the left inverses of `S`.  -/
Submonoid.leftInv : {M : Type u_1} → [inst : Monoid M] → Submonoid M → Submonoid M
-- Mathlib.Order.BoundedOrder.Basic
isMin_iff_eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsMin a ↔ a = ⊥
-- Mathlib.ModelTheory.Bundled
Equiv.bundledInduced_α : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {N : Type w'} (g : M ≃ N),
  ↑(Equiv.bundledInduced L g) = N
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- The lift of a presheaf morphism onto the sheafification subpresheaf.  -/
CategoryTheory.Subfunctor.sheafifyLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F F' : CategoryTheory.Functor Cᵒᵖ (Type w)} →
        (G : CategoryTheory.Subfunctor F) →
          (G.toFunctor ⟶ F') →
            CategoryTheory.Presieve.IsSheaf J F' → ((CategoryTheory.Subfunctor.sheafify J G).toFunctor ⟶ F')
-- Mathlib.Algebra.Group.Action.Defs
eq_neg_vadd_iff : ∀ {G : Type u_3} {α : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α}, a = -g +ᵥ b ↔ g +ᵥ a = b
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instIsUniformAddGroup : ∀ {R : Type u_3} {M : Type u_4} [inst : UniformSpace R] [inst_1 : UniformSpace M] [inst_2 : AddGroup R]
  [inst_3 : AddGroup M] [IsUniformAddGroup R] [IsUniformAddGroup M], IsUniformAddGroup (TrivSqZeroExt R M)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The equivalence between a topological group `G` and `Gᵐᵒᵖ` as a uniform equivalence when `G`
is equipped with the left uniformity and `Gᵐᵒᵖ` with the right uniformity.  -/
MulOpposite.opUniformEquivLeft : (G : Type u_2) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalGroup G] → G ≃ᵤ Gᵐᵒᵖ
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.integrable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} ⦃f : γ → E⦄,
  MeasureTheory.AEStronglyMeasurable f ((η.comp κ) a) →
    (MeasureTheory.Integrable f ((η.comp κ) a) ↔
      (∀ᵐ (y : β) ∂κ a, MeasureTheory.Integrable f (η y)) ∧
        MeasureTheory.Integrable (fun y => ∫ (z : γ), ‖f z‖ ∂η y) (κ a))
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTop_isNonZero' : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  α ≠ 0 → LieModule.genWeightSpace M α ≠ ⊥ → (LieModule.chainTop α β).IsNonZero
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isStrictValue.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.mk.inj : ∀ {root : Lean.TSyntax `tactic} {terminal : Bool} {config : Lean.Try.Config} {originalMaxHeartbeats : ℕ}
  {root_1 : Lean.TSyntax `tactic} {terminal_1 : Bool} {config_1 : Lean.Try.Config} {originalMaxHeartbeats_1 : ℕ},
  { root := root, terminal := terminal, config := config, originalMaxHeartbeats := originalMaxHeartbeats } =
      { root := root_1, terminal := terminal_1, config := config_1, originalMaxHeartbeats := originalMaxHeartbeats_1 } →
    root = root_1 ∧ terminal = terminal_1 ∧ config = config_1 ∧ originalMaxHeartbeats = originalMaxHeartbeats_1
-- Mathlib.Data.FunLike.IsApply
/-- `IsSMulApply M F α β` states for all `f : F`, `n : M` and `x : α`, `(n • f) x = n • f x`.  -/
IsSMulApply : (M : Type u_1) →
  (F : Type u_2) →
    (α : outParam (Type u_3)) → (β : outParam (Type u_4)) → [FunLike F α β] → [SMul M β] → [SMul M F] → Prop
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.ofSubsingleton_relation : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Subsingleton S]
  (x : PUnit.{u_1 + 1}), (Algebra.SubmersivePresentation.ofSubsingleton R S).relation x = 1
-- Mathlib.Algebra.Group.Defs
neg_eq_of_add_eq_zero_left : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, a + b = 0 → -b = a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.differentiableAt_cos : ∀ {x : ℝ}, DifferentiableAt ℝ Real.cos x
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.map_I₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D) (i₁ i₂ : E.I₀),
  (E.map F).I₁ i₁ i₂ = E.I₁ i₁ i₂
-- Init.GrindInstances.Ring.Nat
Lean.Grind.instCommSemiringNat : Lean.Grind.CommSemiring ℕ