mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.comp_convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConcaveOn 𝕜 (f '' s) g → ConvexOn 𝕜 s f → AntitoneOn g (f '' s) → Set.InjOn f s → StrictConcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Computability.Reduce
/-- `p` and `q` are one-one equivalent if each one is one-one reducible to the other.  -/
OneOneEquiv : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → Prop) → (β → Prop) → Prop
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.instIsValuedInRatOfIsCrystallographic : ∀ {ι : Type u_1} {R : Type u_2} {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] (P : RootPairing ι R M N) [P.IsCrystallographic]
  [inst_6 : Algebra ℚ R], P.IsValuedIn ℚ
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPostcompPropertyIsomorphismsOfRespectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.RespectsIso],
  W.HasOfPostcompProperty (CategoryTheory.MorphismProperty.isomorphisms C)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If `f : M → N` is a subadditive function, `f (x + y) ≤ f x + f y`, `f 0 = 0`, and `g i`,
`i ∈ s`, is a finite family of elements of `M`, then `f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`.  -/
Finset.le_sum_of_subadditive : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Preorder N]
  [IsOrderedAddMonoid N] (f : M → N),
  f 0 ≤ 0 → (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ (s : Finset ι) (g : ι → M), f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_ofNat : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) [inst_1 : n.AtLeastTwo] (a : R),
  Polynomial.eval a (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.RingTheory.Flat.Basic
/-- A retract of a flat `R`-module is flat.  -/
Module.Flat.of_retract : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [f : Module.Flat R M] (i : N →ₗ[R] M) (r : M →ₗ[R] N),
  r ∘ₗ i = LinearMap.id → Module.Flat R N
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Option.isSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_eq_zero_of_archimedean : ∀ {S : Type u_3} [inst : LinearOrder S] [inst_1 : CommRing S] [inst_2 : IsStrictOrderedRing S] [Archimedean S] {x : S},
  x ≠ 0 → ArchimedeanClass.mk x = 0
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.leftUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.LaxTrans.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm_to_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (j : ι) {Z : V} (h : C₂.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.prev j) (CategoryTheory.CategoryStruct.comp (C₂.dTo j) h) =
    CategoryTheory.CategoryStruct.comp (C₁.dTo j) (CategoryTheory.CategoryStruct.comp (f.f j) h)
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instUniformContinuousConstVAdd : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X],
  UniformContinuousConstVAdd M (UniformSpace.Completion X)
-- Mathlib.Data.List.Flatten
/-- **Alias** of `List.getLast_flatten_eq_getLast_getLast`.

---

See also `getLast_getLast_eq_getLast_flatten`, which switches around the proof obligations.  -/
List.getLast_flatten_of_flatten_ne_nil : ∀ {α : Type u_1} {l : List (List α)} (hl : l.flatten ≠ []) (hl' : l.getLast ⋯ ≠ []),
  l.flatten.getLast hl = (l.getLast ⋯).getLast hl'
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- Given `F : Pseudofunctor B Cat`, `P : F.ObjectProperty` and `X : B`, this is
the full subcategory of `F.obj X` consisting of the objects satisfying the
property `P`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.Obj : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} → F.ObjectProperty → B → Type u'
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Inv α] [inst_1 : Inv β] (s : Set α) (t : Set β), (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.comp_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x → ∀ (y : E), HasFPowerSeriesWithinAt (fun z => f (z - y)) p (s + {y}) (x + y)
-- Mathlib.Order.BourbakiWitt
NonemptyChain.ext : ∀ {α : Type u_4} {inst : LE α} {x y : NonemptyChain α}, x.carrier = y.carrier → x = y
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofEq_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : φ₁ = φ₂),
  (CategoryTheory.ShortComplex.Homotopy.ofEq h).h₁ = 0
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.mapsTo_digitsAppend : ∀ {b : ℕ}, 1 < b → ∀ (l : ℕ), Set.MapsTo (b.digitsAppend l) {n | n < b ^ l} {L | L.length = l ∧ ∀ x ∈ L, x < b}
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalProdStx : {α α' : Type} →
  Lean.Expr →
    Lean.Expr →
      (Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)) →
        (Lean.Term → Lean.Elab.TermElabM (α' × Lean.Expr)) → Lean.Term → Lean.Elab.TermElabM ((α × α') × Lean.Expr)
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsGE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Icc b a ∈ nhdsWithin b (Set.Ici b)
-- Mathlib.Order.Fin.Basic
Fin.instMax_mathlib : {n : ℕ} → Max (Fin n)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.to_mulHom_injective : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] {f g : A →ₛₙₐ[φ] B}, ↑f = ↑g → f = g
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Oplax.OplaxTrans.Modification.naturality._autoParam)
  (app_1 : (a : B) → η.app a ⟶ θ.app a)
  (naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Oplax.OplaxTrans.Modification.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_dvd_addOrderOf : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M) (a : α),
  AddAction.period m a ∣ addOrderOf m
-- Mathlib.RingTheory.TensorProduct.Maps
/-- **Alias** of `Algebra.TensorProduct.mapOfCompatibleSMul`.

---

If A and B are both R- and S-algebras and their actions on them commute,
and if the S-action on `A ⊗[R] B` can switch between the two factors, then there is a
canonical T-algebra homomorphism from `A ⊗[S] B` to `A ⊗[R] B`,
where `T` is any other ring acting on `A` and whose action commutes with the `R` and `S`-actions.  -/
Algebra.TensorProduct.mapOfCompatibleSMul' : (R : Type u_3) →
  (S : Type u_4) →
    (T : Type u_5) →
      (A : Type u_6) →
        (B : Type u_7) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : CommSemiring T] →
                [inst_3 : Semiring A] →
                  [inst_4 : Semiring B] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra S A] →
                          [inst_8 : Algebra S B] →
                            [inst_9 : Algebra T A] →
                              [inst_10 : SMulCommClass R T A] →
                                [inst_11 : SMulCommClass S T A] →
                                  [SMulCommClass R S A] →
                                    [TensorProduct.CompatibleSMul R S A B] →
                                      TensorProduct S A B →ₐ[T] TensorProduct R A B
-- Mathlib.Algebra.Polynomial.CancelLeads
/-- `cancelLeads p q` is formed by multiplying `p` and `q` by monomials so that they
have the same leading term, and then subtracting.  -/
Polynomial.cancelLeads : {R : Type u_1} → [inst : Ring R] → Polynomial R → Polynomial R → Polynomial R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isSome_maxKey?_modify_eq_isSome : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).maxKey?.isSome = t.maxKey?.isSome
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.debug.tactic.try.onlyUserSuggestions : Lean.Option Bool
-- Init.Data.Int.Basic
Int.ofNat_one : ↑1 = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (k' : α) → (v' : β k') → motive (some ⟨k', v'⟩)),
  (match none with
    | none => h_1 ()
    | some ⟨k', v'⟩ => h_2 k' v') =
    h_1 ()
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.subtype_apply : ∀ {M : Type u_1} {A : Type u_3} [inst : AddZeroClass M] [inst_1 : SetLike A M] [hA : AddSubmonoidClass A M] {S' : A}
  (x : ↥S'), (AddSubmonoidClass.subtype S') x = ↑x
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.isUnit_map : ∀ {R : Type u} {k : Type y} [inst : Field R] {p : Polynomial R} [inst_1 : Field k] (f : R →+* k),
  IsUnit (Polynomial.map f p) ↔ IsUnit p
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.aux_spec : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (g : L ≃+* L) (n : ℕ) [inst_2 : NeZero n]
  (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ modularCyclotomicCharacter.aux g n)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj : ∀ (C : CategoryTheory.Cat),
  CategoryTheory.WithInitial.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithInitial ↑C)
-- Mathlib.Order.ModularLattice
/-- The diamond isomorphism between the closed intervals `[a ⊓ b, a]` and `[b, a ⊔ b]`  -/
infIccOrderIsoIccSup : {α : Type u_1} → [inst : Lattice α] → [IsModularLattice α] → (a b : α) → ↑(Set.Icc (a ⊓ b) a) ≃o ↑(Set.Icc b (a ⊔ b))
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_forgetStalk_inv_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
  (x_1 : ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf).obj U),
  (CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.forgetStalk IM I M R x).inv)
      ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.colimit.ι
            ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf) U))
        x_1) =
    (CategoryTheory.ConcreteCategory.hom
        (TypeCat.ofHom
          ⇑(CommRingCat.Hom.hom
              (CategoryTheory.Limits.colimit.ι
                ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))))
      x_1
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.adicAbv.congr_simp : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 →
    ∀ [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R],
      NumberField.HeightOneSpectrum.adicAbv K v = NumberField.HeightOneSpectrum.adicAbv K v_1
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_vadd_eq_zero_iff : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (c : G), μ (c +ᵥ s) = 0 ↔ μ s = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_right_unitor_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) h =
    CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b).hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom h))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.differentiable_iteratedDeriv_sinh : ∀ (n : ℕ), Differentiable ℝ (iteratedDeriv n Real.sinh)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.All.eq_2 : ∀ {α : Type u_1} (P : α → Prop) (sz : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α),
  Ordnode.All P (Ordnode.node sz l x_1 r) = (Ordnode.All P l ∧ P x_1 ∧ Ordnode.All P r)
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.mkSimpTheoremKeys : Lean.Expr → Bool → optParam Bool false → Lean.MetaM (Array Lean.Meta.SimpTheoremKey × Bool)
-- Init.Data.SInt.Bitwise
Int32.ofBitVec_or : ∀ (a b : BitVec 32), Int32.ofBitVec (a ||| b) = Int32.ofBitVec a ||| Int32.ofBitVec b
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β), (↑f.toMonoidWithZeroHom).toFun = ⇑f
-- Mathlib.Topology.Homotopy.Affine
/-- The homotopy between `f` and `g`
such that `affine f g (t, x) = AffineMap.lineMap (f x) (g x) t`.  -/
ContinuousMap.Homotopy.affine : {X : Type u_1} →
  {E : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] →
          [IsTopologicalAddGroup E] → [inst_4 : Module ℝ E] → [ContinuousSMul ℝ E] → (f g : C(X, E)) → f.Homotopy g
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equivL_apply : ∀ (R : Type u_1) {A : Type u_3} {E : Type u_4} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : UniformSpace E]
  [inst_3 : Module R E] (a : WithCStarModule A E), (WithCStarModule.equivL R) a = (WithCStarModule.equiv A E) a
-- Mathlib.Order.WellFounded
/-- A nonempty linear order with well-founded `>` has a top element.  -/
WellFoundedGT.toOrderTop : (α : Type u_4) → [inst : LinearOrder α] → [Nonempty α] → [h : WellFoundedGT α] → OrderTop α
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Fintype J] (X : C) (f : J → C),
  (CategoryTheory.leftDistributor X f).inv =
    ∑ j,
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j))
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_surjective_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)), Function.Surjective ⇑(IsLocalization.lift hg) ↔ ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_smul : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [inst_2 : OrderTopology R]
  [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R] [inst_6 : SecondCountableTopology R]
  [inst_7 : DenselyOrdered R] (c : NNReal) (f : StieltjesFunction R), (c • f).measure = c • f.measure
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.findMin.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.FindMin α → Sort u_2)
  (res : Batteries.BinomialHeap.Imp.FindMin α)
  (h_1 : (res : Batteries.BinomialHeap.Imp.FindMin α) → motive Batteries.BinomialHeap.Imp.Heap.nil res)
  (h_2 :
    (r : ℕ) →
      (a : α) →
        (c : Batteries.BinomialHeap.Imp.HeapNode α) →
          (s : Batteries.BinomialHeap.Imp.Heap α) →
            (res : Batteries.BinomialHeap.Imp.FindMin α) → motive (Batteries.BinomialHeap.Imp.Heap.cons r a c s) res),
  (match Batteries.BinomialHeap.Imp.Heap.nil, res with
    | Batteries.BinomialHeap.Imp.Heap.nil, res => h_1 res
    | Batteries.BinomialHeap.Imp.Heap.cons r a c s, res => h_2 r a c s res) =
    h_1 res
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_setWidth : ∀ {n : ℕ} (m : ℕ) (x : BitVec n) (i : ℕ), (BitVec.setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)
-- Mathlib.Data.Int.Init
Int.div_lt_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, b < 0 → b ∣ a → (a / b < c ↔ b * c < a)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote_mulPow_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Power)
  (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote ctx (Lean.Grind.CommRing.Mon.mulPow_nc p m) =
    Lean.Grind.CommRing.Power.denote ctx p * Lean.Grind.CommRing.Mon.denote ctx m
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_iSup_le_sum_card : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), (⨆ i, f i).card ≤ Cardinal.sum fun i => (f i).card
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_nsmul : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (n : ℕ) (f : M →ₗ⁅R,L⁆ N), ⇑(n • f) = n • ⇑f
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.ext : ∀ {X Y : Pointed} {x y : X.Hom Y}, x.toFun = y.toFun → x = y
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algebraMap_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) (x : R), (algebraMap R S) x = h.map (Polynomial.C x)
-- Init.Data.SInt.Bitwise
Int32.neg_one_and : ∀ {a : Int32}, -1 &&& a = a
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.restrictScalars_μ_tmul : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat S) (m₁ : ↑M₁) (m₂ : ↑M₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (ModuleCat.restrictScalars f) M₁ M₂))
      (m₁ ⊗ₜ[R] m₂) =
    m₁ ⊗ₜ[S] m₂
-- Init.Data.Repr
instReprTupleOfRepr : {α : Type u_1} → [Repr α] → ReprTuple α
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_pow : ∀ {S : Type u_5} [inst : Ring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] [IsDomain S]
  [Nontrivial R] (abv : R → S) [IsAbsoluteValue abv] (a : R) (n : ℕ), abv (a ^ n) = abv a ^ n
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- Coercion of a `PartialDiffeomorph` to function.
Note that a `PartialDiffeomorph` is not `DFunLike` (like `OpenPartialHomeomorph`),
as `toFun` doesn't determine `invFun` outside of `target`.  -/
instCoeFunPartialDiffeomorphForall : {𝕜 : 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] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        (I : ModelWithCorners 𝕜 E H₁) →
                          (J : ModelWithCorners 𝕜 F H₂) →
                            (M : Type u_8) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  (N : Type u_9) →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        (n : WithTop ℕ∞) → CoeFun (PartialDiffeomorph I J M N n) fun x => M → N
-- Mathlib.Dynamics.Ergodic.Ergodic
QuasiErgodic.zero_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α}, Measurable f → QuasiErgodic f 0
-- Mathlib.Lean.Expr.Basic
/-- If `e` is a projection of the structure constructor, reduce the projection.
Otherwise returns `none`. If this function detects that expression is ill-typed, throws an error.
For example, given `Prod.fst (x, y)`, returns `some x`.  -/
Lean.Expr.reduceProjStruct? : Lean.Expr → Lean.MetaM (Option Lean.Expr)