mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- `C` has weak limits of shape `J` if there exists a weak limit for every functor
`F : J ⥤ C`.  -/
CategoryTheory.Limits.HasWeakLimitsOfShape : (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → (C : Type u_3) → [CategoryTheory.Category.{v_3, u_3} C] → Prop
-- Mathlib.Algebra.Order.Algebra
IsOrderedModule.of_algebraMap_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [PosMulMono β] [MulPosMono β],
  Monotone ⇑(algebraMap α β) → IsOrderedModule α β
-- Mathlib.Combinatorics.Enumerative.Bell
_private.Mathlib.Combinatorics.Enumerative.Bell.0.Nat.bell.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 ()
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.subsingleton_iff : ∀ {G : Type u_1} [inst : Group G], Subsingleton (Subgroup G) ↔ Subsingleton G
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.mk.injEq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (toFunctor : CategoryTheory.Functor 𝒳.obj 𝒴.obj)
  (w : autoParam (toFunctor.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam)
  (toFunctor_1 : CategoryTheory.Functor 𝒳.obj 𝒴.obj)
  (w_1 : autoParam (toFunctor_1.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam),
  ({ toFunctor := toFunctor, w := w } = { toFunctor := toFunctor_1, w := w_1 }) = (toFunctor = toFunctor_1)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- A variant of `IsPrimitiveRoot.card_rootsOfUnity` for `ζ : Rˣ`.  -/
IsPrimitiveRoot.card_rootsOfUnity' : ∀ {R : Type u_4} [inst : CommRing R] {ζ : Rˣ} [IsDomain R] {n : ℕ} [NeZero n],
  IsPrimitiveRoot ζ n → Nat.card ↥(rootsOfUnity n R) = n
-- Mathlib.Condensed.Basic
Condensed.hom_ext : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y : Condensed C} (f g : X ⟶ Y),
  (∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S) → f = g
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.hasForgetToLinOrd : CategoryTheory.HasForget₂ NonemptyFinLinOrd LinOrd
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- A morphism of `CatCospanTransform F G F' G'` is a triple of natural
transformations between the component functors, subjects to
coherence conditions respective to the squares.  -/
CategoryTheory.Limits.CatCospanTransformMorphism : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                CategoryTheory.Limits.CatCospanTransform F G F' G' →
                                  CategoryTheory.Limits.CatCospanTransform F G F' G' →
                                    Type (max (max (max (max (max u₁ u₂) u₃) v₄) v₅) v₆)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_eraseKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = true} (hl : Std.Internal.List.DistinctKeys l),
  Std.Internal.List.getValue a (Std.Internal.List.eraseKey k l) h = Std.Internal.List.getValue a l ⋯
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- The scalar factor between two left-invariant measures is non-zero when both
measures are positive on open sets.  -/
MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : μ'.IsAddHaarMeasure], 0 < μ'.addHaarScalarFactor μ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inl_iso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {Z : D} (h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).hom h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inl f g)) h
-- Mathlib.Topology.WithTopology
WithTopology.instUnique : {X : Type u_1} → (t : TopologicalSpace X) → [Unique X] → Unique (WithTopology X t)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.singleFunctorsPostcompQIso_hom_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ),
  (DerivedCategory.singleFunctorsPostcompQIso C).hom.hom n =
    CategoryTheory.CategoryStruct.id ((DerivedCategory.singleFunctors C).functor n)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_le_smul : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M M' : AddSubmonoid R} {N P : AddSubmonoid A}, M ≤ M' → N ≤ P → M • N ≤ M' • P
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionName.mk : (value : String) →
  autoParam (Std.Http.Chunk.IsValidExtensionName value) Std.Http.Chunk.ExtensionName.isValidExtensionName._autoParam →
    Std.Http.Chunk.ExtensionName
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ico_succ_succ_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Finset.Ico (Order.succ a) (Order.succ b) = Finset.Ioc a b
-- Aesop.Tree.Data
Aesop.TreeSpec.elimRapp : (self : Aesop.TreeSpec) → self.Rapp → Aesop.RappData self.Goal self.MVarCluster
-- Lean.Meta.DiscrTree.Util
/-- Fold the keys and values stored in a `Trie`.
 -/
Lean.Meta.DiscrTree.Trie.fold : {σ : Type u_1} →
  {α : Type} →
    Array Lean.Meta.DiscrTree.Key → (σ → Array Lean.Meta.DiscrTree.Key → α → σ) → σ → Lean.Meta.DiscrTree.Trie α → σ
-- Mathlib.Data.Sigma.Basic
Function.Injective.of_sigma_map : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂}
  {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)}, Function.Injective (Sigma.map f₁ f₂) → ∀ (a : α₁), Function.Injective (f₂ a)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Extension of `MvPolynomial.comp_toFun'`  -/
PolynomialLaw.toFun_comp : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (S : Type u_7) [inst_7 : CommSemiring S] [inst_8 : Algebra R S],
  PolynomialLaw.toFun S (g.comp f) = PolynomialLaw.toFun S g ∘ PolynomialLaw.toFun S f
-- Mathlib.FieldTheory.Finite.Polynomial
/-- The submodule of multivariate polynomials whose degree of each variable is strictly less
than the cardinality of K.  -/
MvPolynomial.R : Type u → (K : Type u) → [Fintype K] → [CommRing K] → Type u
-- Mathlib.RingTheory.Invariant.Basic
instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          {G : Type u_3} →
            [inst_3 : Group G] →
              [inst_4 : MulSemiringAction G B] →
                [inst_5 : SMulCommClass G A B] →
                  (H : Subgroup G) → [inst_6 : H.Normal] → MulSemiringAction (G ⧸ H) ↥(FixedPoints.subalgebra A B ↥H)
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.mul b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_5 a b
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), ∅ ∉ hC.disjointOfDiffUnion hs hI
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_31 : HAdd Std.Time.Day.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Lean.Widget.InteractiveGoal
/-- Syntactic range of the term.  -/
Lean.Widget.InteractiveTermGoal.range : Lean.Widget.InteractiveTermGoal → Lean.Lsp.Range
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Currying in a monoidal closed category.  -/
CategoryTheory.MonoidalClosed.curry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A X Y : C} →
        [inst_2 : CategoryTheory.Closed A] → (CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X) → (Y ⟶ A ⟹ X)
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.adj₁_counit_app_rightToLeft_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} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  (X : C),
  CategoryTheory.CategoryStruct.comp (t.adj₁.counit.app (H.obj X)) (t.rightToLeft.app X) = F.map (t.adj₂.counit.app X)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.truth`.

---

Notation for the "truth arrow" in an arbitrary choice of a subobject classifier  -/
CategoryTheory.HasClassifier.truth : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasSubobjectClassifier C] →
      CategoryTheory.HasSubobjectClassifier.Ω₀ C ⟶ CategoryTheory.HasSubobjectClassifier.Ω C
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.nameStart : (s : String) → s.Pos → Lean.Name → Lean.Name
-- Qq.Macro
Qq.Impl.UnquoteState.mk.inj : ∀ {mvars : List (Lean.Expr × Qq.Impl.MVarSynth)} {levelSubst : Std.HashMap Lean.Expr Lean.Level}
  {exprSubst : Std.HashMap Lean.Expr Lean.Expr} {unquoted : Lean.LocalContext}
  {exprBackSubst : Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult}
  {levelBackSubst : Std.HashMap Lean.Level Lean.Expr} {abstractedFVars : Array Lean.FVarId}
  {levelNames : List Lean.Name} {mayPostpone : Bool} {mvars_1 : List (Lean.Expr × Qq.Impl.MVarSynth)}
  {levelSubst_1 : Std.HashMap Lean.Expr Lean.Level} {exprSubst_1 : Std.HashMap Lean.Expr Lean.Expr}
  {unquoted_1 : Lean.LocalContext} {exprBackSubst_1 : Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult}
  {levelBackSubst_1 : Std.HashMap Lean.Level Lean.Expr} {abstractedFVars_1 : Array Lean.FVarId}
  {levelNames_1 : List Lean.Name} {mayPostpone_1 : Bool},
  { mvars := mvars, levelSubst := levelSubst, exprSubst := exprSubst, unquoted := unquoted,
        exprBackSubst := exprBackSubst, levelBackSubst := levelBackSubst, abstractedFVars := abstractedFVars,
        levelNames := levelNames, mayPostpone := mayPostpone } =
      { mvars := mvars_1, levelSubst := levelSubst_1, exprSubst := exprSubst_1, unquoted := unquoted_1,
        exprBackSubst := exprBackSubst_1, levelBackSubst := levelBackSubst_1, abstractedFVars := abstractedFVars_1,
        levelNames := levelNames_1, mayPostpone := mayPostpone_1 } →
    mvars = mvars_1 ∧
      levelSubst = levelSubst_1 ∧
        exprSubst = exprSubst_1 ∧
          unquoted = unquoted_1 ∧
            exprBackSubst = exprBackSubst_1 ∧
              levelBackSubst = levelBackSubst_1 ∧
                abstractedFVars = abstractedFVars_1 ∧ levelNames = levelNames_1 ∧ mayPostpone = mayPostpone_1
-- Lean.Elab.ConfigEval.Commands
Lean.Elab.ConfigEval.configEntry : Lean.ParserDescr
-- ProofWidgets.Component.Panel.Basic
/-- Display the selected panel widgets in the nested tactic script. For example,
assuming we have written a `GeometryDisplay` component,
```lean
by with_panel_widgets [GeometryDisplay]
  simp
  rfl
```
will show the geometry display alongside the usual tactic state throughout the proof.
 -/
ProofWidgets.withPanelWidgetsTacticStx : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getEntry_eq_getEntryₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (h : m.contains a = true), m.getEntry a h = m.getEntryₘ a h
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instCommSemigroup : {d : ℤ} → CommSemigroup (ℤ√d)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).edges = p.edges
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.isIso_counit_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R)
  (j : R.comp L ≅ CategoryTheory.Functor.id D), CategoryTheory.IsIso adj.counit
-- Mathlib.Order.Category.BoolAlg
/-- Typecheck a `BoundedLatticeHom` as a morphism in `BoolAlg`.  -/
BoolAlg.ofHom : {X Y : Type u} →
  [inst : BooleanAlgebra X] →
    [inst_1 : BooleanAlgebra Y] →
      BoundedLatticeHom X Y → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Mathlib.Topology.Constructions.SumProd
isClosedMap_sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `MonoidAlgebra.coeff` as a linear equiv.  -/
AddMonoidAlgebra.coeffLinearEquiv : (R : Type u_1) →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : Module R S] → AddMonoidAlgebra S M ≃ₗ[R] M →₀ S
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.GrpCat.Hom.mk.inj : ∀ {A B : GrpCat} {hom' hom'_1 : ↑A →* ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.awayMap_awayToSection_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) {Z : CommRingCat}
  (h : (AlgebraicGeometry.Proj 𝒜).presheaf.obj (Opposite.op (AlgebraicGeometry.Proj.basicOpen 𝒜 x)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 x) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 f)
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).presheaf.map (CategoryTheory.homOfLE ⋯).op) h)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.mk_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f : C(N → ↑unitInterval, X))
  (H : f ∈ GenLoop N X x) (y : N → ↑unitInterval), ⟨f, H⟩ y = f y
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.instAddCommGroupPreGNS : {A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → AddCommGroup f.PreGNS
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (m : ℕ) → motive m.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | m.succ.succ => h_3 m) =
    h_2 ()
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.ofUpper_lt_ofUpper : ∀ {α : Type u_1} [inst : Preorder α] {x y : Topology.WithUpper α},
  Topology.WithUpper.ofUpper x < Topology.WithUpper.ofUpper y ↔ x < y
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat.eq_1 : ∀ (p n : ℕ), padicValNat p n = (p.maxPowDvdDiv n).1
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.pow_mem : ∀ {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) {x : R}, x ∈ s → ∀ (n : ℕ), x ^ n ∈ s
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.isClosed_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsCoinducing f → ∀ {s : Set Y}, IsClosed (f ⁻¹' s) ↔ IsClosed s
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
fourier_gaussian_innerProductSpace' : ∀ {b : ℂ} {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V],
  0 < b.re →
    ∀ (x w : V),
      FourierTransform.fourier (fun v => Complex.exp (-b * ↑‖v‖ ^ 2 + 2 * ↑Real.pi * Complex.I * ↑(inner ℝ x v))) w =
        (↑Real.pi / b) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑‖x - w‖ ^ 2 / b)
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi_mem_range_eq_inverseImage_epimorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [G.Faithful] [G.Full],
  (CategoryTheory.ObjectProperty.localEpi fun x => x ∈ Set.range G.obj) =
    (CategoryTheory.MorphismProperty.epimorphisms D).inverseImage F
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.univ : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α], DirSupInaccOn D Set.univ
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.Meta.Origin.fvar fvarId) = 1 + sizeOf fvarId
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**, strict version: if an integrable function `f : α → E` takes values in a
convex closed set `s`, and `g : E → ℝ` is continuous and strictly convex on `s`, then
either `f` is a.e. equal to its average value, or `g (⨍ x, f x ∂μ) < ⨍ x, g (f x) ∂μ`.  -/
StrictConvexOn.ae_eq_const_or_map_average_lt : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  StrictConvexOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ →
              f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When a short complex has homology, this is the canonical isomorphism
`S.rightHomology ≅ S.homology`.  -/
CategoryTheory.ShortComplex.rightHomologyIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasHomology] → S.rightHomology ≅ S.homology
-- Mathlib.Algebra.Exact.Basic
Function.Exact.split_tfae' : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    [Function.Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Function.Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
        ∃ e, f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE
-- Mathlib.Topology.UnitInterval
/-- like `unitInterval.le_one`, but with the inequality in `I`.  -/
unitInterval.le_one' : ∀ {t : ↑unitInterval}, t ≤ 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_nonneg_of_lt : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, 0 ≤ a → b < c → b < a + c
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- action on objects  -/
CategoryTheory.StrictlyUnitaryPseudofunctorCore.obj : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.StrictlyUnitaryPseudofunctorCore B C → B → C
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.iSup_lintegral_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_4} (f : ι → α → ENNReal),
  ⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), ⨆ i, f i a ∂μ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableOn_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'},
  MDiff[Set.univ] f ↔ MDiff f
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.faithful_whiskeringLeft : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (E : Type u_4)
  [inst_3 : CategoryTheory.Category.{v_4, u_4} E], ((CategoryTheory.Functor.whiskeringLeft C D E).obj L).Faithful
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Turn a morphism in `CommHopfAlgCat` back into a `BialgHom`.  -/
CommHopfAlgCat.Hom.hom : {R : Type u} → [inst : CommRing R] → {A B : CommHopfAlgCat R} → A.Hom B → ↑A →ₐc[R] ↑B
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.PenroseVar.mk.sizeOf_spec : ∀ (ident : String) (indices : List ℕ) (e : Lean.Expr),
  sizeOf { ident := ident, indices := indices, e := e } = 1 + sizeOf ident + sizeOf indices + sizeOf e
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.pi.eq_1 : Real.pi = 2 * Classical.choose Real.exists_cos_eq_zero
-- Init.Data.BitVec.Lemmas
BitVec.or_self : ∀ {w : ℕ} {x : BitVec w}, x ||| x = x