mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignUnassignedLevelMVars.search.eq_def : ∀ (proof prop : Lean.Expr) (candidates : Array (Lean.Expr × Array Lean.Expr)) (us : Array Lean.Level) (i : ℕ),
  Lean.Meta.Grind.EMatch.assignUnassignedLevelMVars.search✝ proof prop candidates us i = do
    liftM (Lean.checkSystem "grind")
    if h : i < candidates.size then
        match candidates[i] with
        | (c, cs) => do
          let __s ←
            forIn cs (none, ()) fun c' __s =>
                have __r := __s;
                do
                let saved ← Lean.getMCtx
                let e ←
                  tryFinally
                      (do
                        let __do_lift ← liftM (Lean.Meta.isDefEq c c')
                        if __do_lift = true then do
                            let us ←
                              Array.filterMapM
                                  (fun u => do
                                    let u ← Lean.instantiateLevelMVars u
                                    let __do_lift ← liftM (Lean.Meta.hasAssignableLevelMVar u)
                                    if __do_lift = true then pure (some u) else pure none)
                                  us
                            if us.isEmpty = true then do
                                let prop ← Lean.instantiateMVars prop
                                let proof ← Lean.instantiateMVars proof
                                modify fun x => x.push (proof, prop)
                                EarlyReturnT.return ()
                              else do
                                let r ←
                                  Lean.Meta.Grind.EMatch.assignUnassignedLevelMVars.search✝ proof prop candidates us
                                      (i + 1)
                                ExceptT.run (pure r)
                          else ExceptT.run (pure ()))
                      (Lean.setMCtx saved)
                EarlyReturn.runK e (fun r => pure (ForInStep.done (some r, ()))) fun r =>
                    pure (ForInStep.yield (none, ()))
          have __r : Option Unit × Unit := __s
          match __r.1 with
            | some r => pure r
            | none => pure ()
      else pure ()
-- Mathlib.Order.RelSeries
RelSeries.last_snoc : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r),
  (p.snoc newLast rel).last = newLast
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β}, (t.insertIfNew k v).minKey! = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.lexOrder_def_of_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ : MvPowerSeries σ R},
  φ ≠ 0 → ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
-- Mathlib.Topology.Order.Basic
pi_Icc_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i},
  (∀ (i : ι), a i < x i) → (∀ (i : ι), x i < b i) → Set.Icc a b ∈ nhds x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_pow₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀],
  1 < a → ∀ {n : ℕ}, n ≠ 0 → 1 < a ^ n
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.binaryProductsClosure_le_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasTerminal C]
  {P Q : CategoryTheory.ObjectProperty C} [Q.IsClosedUnderBinaryProducts]
  [Q.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})], P.binaryProductsClosure ≤ Q ↔ P ≤ Q
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfcₙ_imaginaryPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] (f : ℂ → ℂ)
  (a : A),
  autoParam (ContinuousOn f (quasispectrum ℂ ↑(imaginaryPart a))) cfcₙ_imaginaryPart._auto_1 →
    autoParam (f 0 = 0) cfcₙ_imaginaryPart._auto_3 →
      autoParam (IsStarNormal a) cfcₙ_imaginaryPart._auto_5 → cfcₙ f ↑(imaginaryPart a) = cfcₙ (fun x => f ↑x.im) a
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.mk : {G : Type u_6} →
  [inst : AddGroup G] →
    (toZeroHom : ZeroHom G ℝ) →
      (∀ (r s : G), toZeroHom.toFun (r + s) ≤ max (toZeroHom.toFun r) (toZeroHom.toFun s)) →
        (∀ (r : G), toZeroHom.toFun (-r) = toZeroHom.toFun r) → NonarchAddGroupSeminorm G
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q)
  (X : C) (x : Φ.fiber.obj X) {F : A → A → Type uF} {carrier : A → Type w_1}
  {instFunLike : (X Y : A) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory A F]
  (x_1 : carrier (P.obj (Opposite.op X))),
  (CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map g))
      ((CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x P)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x Q))
      ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op X))) x_1)
-- Mathlib.Tactic.Ring.Common
/-- Evaluate the sum of two coefficients.

If the result is zero returns a proof of this fact, which is used to remove zero terms.  -/
Mathlib.Tactic.Ring.Common.RingCompute.add : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα →
          {x y : Q(«$α»)} →
            BaseType x →
              BaseType y →
                Lean.MetaM
                  (Mathlib.Tactic.Ring.Common.Result BaseType q(«$x» + «$y») ×
                    Option Q(Mathlib.Meta.NormNum.IsNat («$x» + «$y») 0))
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.piObjIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D),
  CategoryTheory.Limits.piObjIso f d =
    CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (CategoryTheory.Discrete.functor f) d ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso
        (CategoryTheory.Discrete.compNatIsoDiscrete f ((CategoryTheory.evaluation D C).obj d))
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.PolyExpr : Type
-- Init.Data.List.Lemmas
List.beq_nil_eq : ∀ {α : Type u_1} [inst : BEq α] {l : List α}, (l == []) = l.isEmpty
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.restrictScalars_localized'_smul : ∀ {R : Type u_1} (S : Type u_2) {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R N] [inst_4 : Algebra R S] [inst_5 : Module S N]
  [inst_6 : IsScalarTower R S N] (p : Submonoid R) [inst_7 : IsLocalization p S] (I : Submodule R R)
  (N' : Submodule S N),
  Submodule.restrictScalars R (Submodule.localized' S p (Algebra.linearMap R S) I • N') =
    I • Submodule.restrictScalars R N'
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ofHom_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)),
  CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.desc φ α β eq) =
    CochainComplex.mappingCone.descCochain φ α (CochainComplex.HomComplex.Cochain.ofHom β) ⋯
-- Mathlib.GroupTheory.IsPerfect
/-- The commutator of the group `G` with itself is the whole group `G`.  -/
Group.IsPerfect.commutator_eq_top : ∀ {G : Type u_1} {inst : Group G} [self : Group.IsPerfect G], commutator G = ⊤
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_eq_one_iff : ∀ (x : ℝ), Real.cos x = 1 ↔ ∃ n, ↑n * (2 * Real.pi) = x
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An additive action of an additive group on a type `α`
is `n`-pretransitive if the associated action on `Fin n ↪ α` is pretransitive.  -/
AddAction.IsMultiplyPretransitive : (G : Type u_1) → (α : Type u_2) → [inst : AddGroup G] → [AddAction G α] → ℕ → Prop
-- Lean.Language.Basic
/-- Builds a function for processing a language using incremental snapshots by passing the previous
snapshot to `Language.process` on subsequent invocations.  -/
Lean.Language.mkIncrementalProcessor : {InitSnap : Type} →
  (Option InitSnap → Lean.Language.ProcessingM InitSnap) → BaseIO (Lean.Parser.InputContext → BaseIO InitSnap)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_same₁₂ : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b c : ℤ),
  IsEllipticNet.atomRel W a a b c = W a * W 0 * IsEllipticNet.atom W b c
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} (f : ℝ → ℝ),
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
      f).IsZero
-- Mathlib.Order.Bounds.Basic
bddAbove_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, BddAbove (Set.Iic a)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instAdd : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → Add (ρ.IntertwiningMap σ)
-- Init.Data.Nat.Basic
Nat.ble_eq : ∀ {x y : ℕ}, (x.ble y = true) = (x ≤ y)
-- Mathlib.Order.Circular.ZMod
instCircularOrderInt : CircularOrder ℤ
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → DifferentiableAt 𝕜 (f - g) x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      (Std.DHashMap.Raw.Const.insertMany m l).contains k = (m.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_set : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g : M → M'} {s t : Set M} {x : M},
  G.LocalInvariantProp G' P →
    s =ᶠ[nhds x] t → (ChartedSpace.LiftPropWithinAt P g s x ↔ ChartedSpace.LiftPropWithinAt P g t x)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- Lemma 3.4 from [Geck](Geck2017).  -/
RootPairing.GeckConstruction.lie_e_f_same : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  (i : ↥b.support) [P.IsReduced],
  ⁅RootPairing.GeckConstruction.e i, RootPairing.GeckConstruction.f i⁆ = RootPairing.GeckConstruction.h i
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.opEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.opEquivalence.functor = (P.lift P.op.ι.leftOp ⋯).rightOp
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Matrix.discr.eq_1 : ∀ {R : Type u_1} {n : Type u_2} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n R),
  A.discr = A.charpoly.discr
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.sInf_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (S : Set (LieSubalgebra R L)), (sInf S).toSubmodule = sInf {x | ∃ s ∈ S, s.toSubmodule = x}
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.isIso_apply_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} {X Y : CategoryTheory.GradedObject β C}
  (f : X ⟶ Y) [CategoryTheory.IsIso f] (i : β), CategoryTheory.IsIso (f i)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.inf_map_atBot_neBot_iff : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] {F : Filter β} {u : α → β} [Nonempty α],
  (F ⊓ Filter.map u Filter.atBot).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≤ N, u n ∈ U
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.linearEquivMap_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) [inst_5 : Module.FinitePresentation R M]
  (f : M →ₗ[R] N),
  (Module.FinitePresentation.linearEquivMap S) ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) =
    (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.validateUTF8.go.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : false = false → motive false) (h_2 : false = true → motive true),
  (match h : false with
    | false => h_1 h
    | true => h_2 h) =
    h_1 ⋯
-- Init.Data.SInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 8-bit signed integers. Usually accessed via
the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so `Int8.complement a = -(a + 1)`.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.complement : Int8 → Int8
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.toSimpleGraph.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), C.toSimpleGraph = SimpleGraph.induce C.supp G
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.saturday.sizeOf_spec : sizeOf Std.Time.Weekday.saturday = 1
-- Mathlib.Data.Set.Card
Set.eq_insert_of_ncard_eq_succ : ∀ {α : Type u_1} {s : Set α} {n : ℕ}, s.ncard = n + 1 → ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.max?_reverse : ∀ {α : Type u_1} (t : RBTree.RBNode α), t.reverse.max? = t.min?
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.repr_floor_apply : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E) (i : ι), (b.repr ↑(ZSpan.floor b m)) i = ↑⌊(b.repr m) i⌋
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.sub_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
  (f f' : P ⟶ Q) (g : Q ⟶ R),
  CategoryTheory.CategoryStruct.comp (f - f') g =
    CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f' g
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingCofaceMapComplex.objD.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.CosimplicialObject C) (n : ℕ),
  AlgebraicTopology.AlternatingCofaceMapComplex.objD X n = ∑ i, (-1) ^ ↑i • X.δ i
-- Mathlib.Algebra.Ring.Equiv
/-- The proposition that the function preserves multiplication  -/
RingEquiv.map_mul' : ∀ {R : Type u_7} {S : Type u_8} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (self : R ≃+* S)
  (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : CochainComplex C ℕ),
  CochainComplex.IsStrictlyGE (HomologicalComplex.extend X ComplexShape.embeddingUpNat) 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_filter_eq_size_iff : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool}, m.WF → ((Std.HashSet.Raw.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (m.insertMany l).contains k = (m.contains k || (List.map Sigma.fst l).contains k)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
scalarSMulCLE_symm_apply : ∀ (H : Type u_1) [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] (c : ℂˣ) (x : H),
  (scalarSMulCLE H c).symm x = c⁻¹ • x
-- Mathlib.Algebra.Group.Basic
div_div_div_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c d : α), a / b / (c / d) = a / c / (b / d)
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.mk.inj : ∀ {α : Type u} {upper upper_1 : α}, ((*...=upper) = *...=upper_1) → upper = upper_1
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.mul_left : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s t : Set α},
  IsUpperSet t → IsUpperSet (s * t)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_le_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a b ≤ a + p
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
/-- Given a Localization map `f : M →*₀ N` for a Submonoid `S ⊆ M`,
if `M` is a cancellative monoid with zero, and all elements of `S` are
regular, then N is a cancellative monoid with zero.  -/
Submonoid.LocalizationMap.isCancelMulZero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N) [IsCancelMulZero M], IsCancelMulZero N
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.logEquiv_unitsMk0 : ∀ {G : Type u_5} [inst : AddGroup G] (x : WithZero (Multiplicative G)) (hx : x ≠ 0),
  WithZero.logEquiv (Units.mk0 x hx) = x.log
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- If `f, g` is split, then `G f, G g` is split.  -/
CategoryTheory.map_is_split_pair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.HasSplitCoequalizer f g],
  CategoryTheory.HasSplitCoequalizer (G.map f) (G.map g)
-- Init.SizeOf
Lean.ParserDescr.binary.sizeOf_spec : ∀ (name : Lean.Name) (p₁ p₂ : Lean.ParserDescr),
  sizeOf (Lean.ParserDescr.binary name p₁ p₂) = 1 + sizeOf name + sizeOf p₁ + sizeOf p₂
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesOfIsMulCocycle₁_coe : ∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M] {f : G → M}
  (hf : groupCohomology.IsMulCocycle₁ f) (a : G),
  ↑(groupCohomology.cocyclesOfIsMulCocycle₁ hf) a = (⇑Additive.ofMul ∘ f) a
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioc_intCast : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  Pairwise (Function.onFun Disjoint fun n => Set.Ioc (↑n) (↑n + 1))
-- Init.System.IO
/-- Converts an `EIO ε` action into an `IO` action by translating any exceptions that it throws into
`IO.Error`s using `f`.
 -/
EIO.toIO : {ε α : Type} → (ε → IO.Error) → EIO ε α → IO α
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalClosed_closed_rightAdj : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X : (i : I) → C i), CategoryTheory.Closed.rightAdj X = CategoryTheory.Pi.ihom X
-- Mathlib.Order.Notation
/-- Return `true` if `LinearOrder` is imported and `inst` comes from a `LinearOrder e` instance.

We use a `try catch` block to make sure there are no surprising errors during delaboration.
 -/
_private.Mathlib.Order.Notation.0.Mathlib.Meta.hasLinearOrder : (u : Lean.Level) →
  (α : Q(Type u)) →
    (cls : Q(Type u → Type u)) →
      (have a := Mathlib.Meta.linearOrderExpr✝ u;
        Q((α : Type u) → «$a» α → «$cls» α)) →
        Q(«$cls» «$α») → Lean.MetaM Bool
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ioc_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₁ ≤ b₁ → (Set.Icc a₁ b₁ ⊆ Set.Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂)
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on a space of continuous linear maps  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromCLM : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq_of_ge : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] {i : ι} {ω : Ω}, τ ω ≤ ↑i → MeasureTheory.stoppedProcess u τ i ω = u (τ ω).untopA ω
-- Mathlib.Data.Subtype
Subtype.map_coe : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a))
  (a : Subtype p), ↑(Subtype.map f h a) = f ↑a
-- Mathlib.Data.Prod.PProd
Function.Injective.pprod_map : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : γ → δ},
  Function.Injective f → Function.Injective g → Function.Injective fun x => ⟨f x.fst, g x.snd⟩
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_comp_whiskerRight_assoc : ∀ {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 G : CategoryTheory.Functor C D}
  {H K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ K) {Z : CategoryTheory.Functor C E} (h : G.comp K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.whiskerLeft β)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α K) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α H)
      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft β) h)