mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- Constructor for morphisms from the point of a limit weighted cone.  -/
CategoryTheory.Limits.WeightedCone.IsLimit.lift : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {W : CategoryTheory.Functor J (Type w)} →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.WeightedCone W F} →
              c.IsLimit →
                {Z : C} →
                  (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j)) →
                    (∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
                        CategoryTheory.CategoryStruct.comp (π x) (F.map f) =
                          π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)) →
                      (Z ⟶ c.pt)
-- Mathlib.Order.WithBot
/-- Specialization of `Option.getD` to values in `WithTop α` that respects API boundaries.  -/
WithTop.untopD : {α : Type u_1} → α → WithTop α → α
-- Init.Data.UInt.Lemmas
UInt64.lt_asymm : ∀ {a b : UInt64}, a < b → ¬b < a
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_inf : ∀ {M : Type u_2} [inst : Add M] (S₁ S₂ : AddSubsemigroup Mᵃᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Std.Http.Protocol.H1.Writer
/-- Manages the writing state of the HTTP generating and writing machine.
 -/
Std.Http.Protocol.H1.Writer : Std.Http.Protocol.H1.Direction → Type
-- Mathlib.Order.Minimal
/-- If two sets are antitonically order isomorphic, their maximals/minimals are too.  -/
OrderIso.setOfPredMaximalIsoSetOfPredMinimal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} →
          {t : Set β} →
            ↑s ≃o (↑t)ᵒᵈ → ↑{x | Maximal (fun x => x ∈ s) x} ≃o ↑{x | Minimal (fun x => x ∈ t) (OrderDual.ofDual x)}
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Constructor for natural transformations between functors constructed
with `functorMk`.  -/
CategoryTheory.Pretriangulated.Triangle.functorHomMk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
          {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} →
            {mor₁ : obj₁ ⟶ obj₂} →
              {mor₂ : obj₂ ⟶ obj₃} →
                {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} →
                  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} →
                    {mor₁' : obj₁' ⟶ obj₂'} →
                      {mor₂' : obj₂' ⟶ obj₃'} →
                        {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} →
                          (hom₁ : obj₁ ⟶ obj₁') →
                            (hom₂ : obj₂ ⟶ obj₂') →
                              (hom₃ : obj₃ ⟶ obj₃') →
                                CategoryTheory.CategoryStruct.comp mor₁ hom₂ =
                                    CategoryTheory.CategoryStruct.comp hom₁ mor₁' →
                                  CategoryTheory.CategoryStruct.comp mor₂ hom₃ =
                                      CategoryTheory.CategoryStruct.comp hom₂ mor₂' →
                                    CategoryTheory.CategoryStruct.comp mor₃
                                          (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
                                        CategoryTheory.CategoryStruct.comp hom₃ mor₃' →
                                      (CategoryTheory.Pretriangulated.Triangle.functorMk mor₁ mor₂ mor₃ ⟶
                                        CategoryTheory.Pretriangulated.Triangle.functorMk mor₁' mor₂' mor₃')
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α} (fallback : β),
      Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k fallback =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if compare a k = Ordering.eq then some b else none)
              l).getD
          (Std.DTreeMap.Internal.Impl.Const.getD t k fallback)
-- Init.Data.List.MapIdx
List.mapIdx_eq_mapIdx_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f g : ℕ → α → α_1} {l : List α},
  List.mapIdx f l = List.mapIdx g l ↔ ∀ (i : ℕ) (h : i < l.length), f i l[i] = g i l[i]
-- Mathlib.CategoryTheory.Square
/-- The identity of a commutative square.  -/
CategoryTheory.Square.Hom.id : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (sq : CategoryTheory.Square C) → sq.Hom sq
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.valuesArray_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.valuesArray = t₂.valuesArray
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.sk_coreflective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F]
  [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F],
  CategoryTheory.IsIso (CategoryTheory.SimplicialObject.skAdj n).unit
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_toLp_top_le : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] {f : SchwartzMap E F} {μ : MeasureTheory.Measure E}
  [hμ : μ.HasTemperateGrowth], ‖f.toLp ⊤ μ‖ ≤ (SchwartzMap.seminorm ℝ 0 0) f
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.of_succ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiff 𝕜 (n + 1) f → ContDiff 𝕜 n f
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (toFunctor : CategoryTheory.Functor C C) →
      (η : CategoryTheory.Functor.id C ⟶ toFunctor) →
        (μ : toFunctor.comp toFunctor ⟶ toFunctor) →
          autoParam
              (∀ (X : C),
                CategoryTheory.CategoryStruct.comp (toFunctor.map (μ.app X)) (μ.app X) =
                  CategoryTheory.CategoryStruct.comp (μ.app (toFunctor.obj X)) (μ.app X))
              CategoryTheory.Monad.assoc._autoParam →
            autoParam
                (∀ (X : C),
                  CategoryTheory.CategoryStruct.comp (η.app (toFunctor.obj X)) (μ.app X) =
                    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor.obj X)))
                CategoryTheory.Monad.left_unit._autoParam →
              autoParam
                  (∀ (X : C),
                    CategoryTheory.CategoryStruct.comp (toFunctor.map (η.app X)) (μ.app X) =
                      CategoryTheory.CategoryStruct.id (toFunctor.obj ((CategoryTheory.Functor.id C).obj X)))
                  CategoryTheory.Monad.right_unit._autoParam →
                CategoryTheory.Monad C
-- Lean.Elab.ConfigEval.Types
_private.Lean.Elab.ConfigEval.Types.0.Lean.Elab.ConfigEval.ReflectConfigItems.mk.injEq : ∀ {α : Type} (reflect reflect_1 : α → Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.configItem)),
  ({ reflect := reflect } = { reflect := reflect_1 }) = (reflect = reflect_1)
-- Init.Data.SInt.Basic
instHashableInt8 : Hashable Int8
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableAt.clm_comp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {H : Type u_5} [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 d x → DifferentiableAt 𝕜 (fun y => c y ∘SL d y) x
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
MonoidHom.coe_finsetProd : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : CommMonoid N] (f : ι → M →* N)
  (s : Finset ι), ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)
-- Init.Coe
/-- The resulting value of type `β`. The input `x : α` is a parameter to
the type class, so the value of type `β` may possibly depend on additional
typeclasses on `x`.  -/
CoeT.coe : {α : Sort u} → (x : α) → {β : Sort v} → [self : CoeT α x β] → β
-- Mathlib.GroupTheory.Coxeter.Inversion
/-- The proposition that `t` is a right inversion of `w`; i.e., `t` is a reflection and
$\ell (w t) < \ell(w)$.  -/
CoxeterSystem.IsRightInversion : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W → W → Prop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (t.insertMany l)[k]? =
    (List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if cmp a k = Ordering.eq then some b else none)
          l).or
      t[k]?
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.pullbackMk_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X₁ X₂ S : C}
  (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [inst_3 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
  (x₁ : CategoryTheory.ToType X₁) (x₂ : CategoryTheory.ToType X₂)
  (h : (CategoryTheory.ConcreteCategory.hom f₁) x₁ = (CategoryTheory.ConcreteCategory.hom f₂) x₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f₁ f₂))
      (CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h) =
    x₁
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.toList'_cons : ∀ {α : Type u} (l : List α) (s : Stream'.WSeq α) (a : α),
  Computation.corec
      (fun x =>
        match x with
        | (l, s) =>
          match Stream'.Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, Stream'.WSeq.cons a s) =
    (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Stream'.Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (a :: l, s)).think
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `a ≤ x`. Basically `Set.Ici a` as a multiset.  -/
Multiset.Ici : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderTop α] → α → Multiset α
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.toLinearMap_mulCoalgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  ↑(Bialgebra.mulCoalgHom R A) = LinearMap.mul' R A
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.nat_gcd_helper_1 : ∀ (d x y a b : ℕ), x % d = 0 → y % d = 0 → y * b = x * a + d → x.gcd y = d
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Two functors from a free groupoid to a group are equal when they agree on the generating
quiver.  -/
IsFreeGroupoid.ext_functor : ∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G] {X : Type v} [inst_2 : Group X]
  (f g : CategoryTheory.Functor G (CategoryTheory.SingleObj X)),
  (∀ (a b : IsFreeGroupoid.Generators G) (e : a ⟶ b), f.map (IsFreeGroupoid.of e) = g.map (IsFreeGroupoid.of e)) → f = g
-- Mathlib.Algebra.Ring.Pi
Pi.nonUnitalNonAssocRing : {I : Type u} → {f : I → Type v} → [(i : I) → NonUnitalNonAssocRing (f i)] → NonUnitalNonAssocRing ((i : I) → f i)
-- Mathlib.Tactic.NormNum.Inv
/-- Helper function to synthesize a typed `CharZero α` expression given `AddMonoidWithOne α`, if it
exists.  -/
Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne? : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_i : autoParam Q(AddMonoidWithOne «$α») Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne?._auto_1) →
      Lean.MetaM (Option Q(CharZero «$α»))
-- Init.PropLemmas
or_or_or_comm : ∀ {a b c d : Prop}, (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d
-- Mathlib.Data.ENat.Basic
/-- A version of `top_mul` where the RHS is stated as an `ite`  -/
ENat.top_mul' : ∀ {m : ℕ∞}, ⊤ * m = if m = 0 then 0 else ⊤
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_inverse_map_natTrans : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {X Y : CategoryTheory.Functor C V} (α : X ⟶ Y),
  ((CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).inverse.map α).natTrans = α
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquivOfSurjective.eq_1 : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] {f : α →* H} (hf : Function.Surjective ⇑f)
  (h h' : H),
  MonoidHom.fiberEquivOfSurjective hf h h' =
    (MonoidHom.fiberEquivKerOfSurjective hf h).trans (MonoidHom.fiberEquivKerOfSurjective hf h').symm
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_congr_r : ∀ {σs : List (Type u)} {P Q Q' : Std.Do.SPred σs}, (Q ⊣⊢ₛ Q') → (P → Q) ⊣⊢ₛ P → Q'
-- Mathlib.Topology.Algebra.Module.Star
StarModule.decomposeProdAdjointL_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] [inst_8 : TopologicalSpace A] [inst_9 : IsTopologicalAddGroup A] [inst_10 : ContinuousStar A]
  [inst_11 : ContinuousConstSMul R A] (i : A),
  (StarModule.decomposeProdAdjointL R A) i = ((selfAdjointPart R) i, (skewAdjointPart R) i)
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instIsCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsCancelMul α], IsCancelMul αᵐᵒᵖ
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.addCommute_neg_coe : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α), AddCommute ↑(-a) ↑a
-- Init.Data.List.Nat.Basic
List.length_filterMap_pos_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β},
  0 < (List.filterMap f xs).length ↔ ∃ x, ∃ (_ : x ∈ xs), ∃ b, f x = some b
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_mul_X : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S],
  (p * Polynomial.X).smeval x = p.smeval x * x
-- Std.Data.Iterators.Lemmas.Combinators.Drop
Std.Iter.step_drop : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} {it : Std.Iter β},
  (Std.Iter.drop n it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ =>
      match n with
      | 0 => Std.PlausibleIterStep.yield (Std.Iter.drop 0 it') out ⋯
      | k.succ => Std.PlausibleIterStep.skip (Std.Iter.drop k it') ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.drop n it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Mathlib.Analysis.Asymptotics.LinearGrowth
InfTopHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] [inst_2 : Top α] [inst_3 : Top β]
  (toInfHom toInfHom_1 : InfHom α β) (e_toInfHom : toInfHom = toInfHom_1) (map_top' : toInfHom.toFun ⊤ = ⊤),
  { toInfHom := toInfHom, map_top' := map_top' } = { toInfHom := toInfHom_1, map_top' := ⋯ }
-- Init.Grind.Ring.Field
Lean.Grind.Field.inv_mul_cancel : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a : α}, a ≠ 0 → a⁻¹ * a = 1
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- If `α` is an isomorphism between right adjoints, then its conjugate transformation is an
isomorphism. The converse is given in `conjugateEquiv_symm_of_iso`.
 -/
CategoryTheory.conjugateEquiv_symm_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : R₁ ⟶ R₂) [CategoryTheory.IsIso α], CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α)
-- Mathlib.Logic.Relation
Relation.EqvGen.below.trans : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a a_1 : α) → Relation.EqvGen r a a_1 → Prop} (x y z : α)
  (a : Relation.EqvGen r x y) (a_1 : Relation.EqvGen r y z),
  Relation.EqvGen.below a → motive x y a → Relation.EqvGen.below a_1 → motive y z a_1 → Relation.EqvGen.below ⋯
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β},
  f₂ ≤ᶠ[l] f₁ → g₂ ≤ᶠ[l] g₁ → f₂ ⊓ g₂ ≤ᶠ[l] f₁ ⊓ g₁
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : FreeMonoid α} {m : β}, m ∈ (FreeMonoid.map f) a ↔ ∃ n ∈ a, f n = m
-- Init.Prelude
instLEUInt32 : LE UInt32
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [toRespects : P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)],
  (∀ {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X} {U : C} {g : U ⟶ X},
      R ∈ K.coverings X →
        R g → P f → ∀ [inst_1 : CategoryTheory.Limits.HasPullback f g], P (CategoryTheory.Limits.pullback.snd f g)) →
    (∀ {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X},
        R ∈ K.coverings X →
          (∀ {U : C} {g : U ⟶ X} [inst_1 : CategoryTheory.Limits.HasPullback f g],
              R g → P (CategoryTheory.Limits.pullback.snd f g)) →
            P f) →
      P.IsLocalAtTarget K
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.noSpace : Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instEssFiniteTypeResidueField_1 : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.EssFiniteType R A] (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal A) [inst_5 : q.IsPrime]
  [inst_6 : q.LiesOver p] [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q], Algebra.EssFiniteType p.ResidueField q.ResidueField
-- Mathlib.Analysis.Convex.Caratheodory
Caratheodory.minCardFinsetOfMemConvexHull_card_le_card : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E} (hx : x ∈ (convexHull 𝕜) s) {t : Finset E},
  ↑t ⊆ s → x ∈ (convexHull 𝕜) ↑t → (Caratheodory.minCardFinsetOfMemConvexHull hx).card ≤ t.card
-- Mathlib.RingTheory.PrincipalIdealDomain
exists_associated_pow_of_mul_eq_pow' : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R] {a b c : R},
  IsCoprime a b → ∀ {k : ℕ}, a * b = c ^ k → ∃ d, Associated (d ^ k) a
-- Mathlib.Util.Notation3
Mathlib.Notation3.instInhabitedMatcher : Inhabited Mathlib.Notation3.Matcher
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.α_inv_hom : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z).comp (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z))
    (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor (Y.tensor Z)))
-- Batteries.Data.BinomialHeap.Basic
/-- A [binomial heap](https://en.wikipedia.org/wiki/Binomial_heap) is a data structure which supports
the following primary operations:

* `insert : α → BinomialHeap α → BinomialHeap α`: add an element to the heap
* `deleteMin : BinomialHeap α → Option (α × BinomialHeap α)`:
  remove the minimum element from the heap
* `merge : BinomialHeap α → BinomialHeap α → BinomialHeap α`: combine two heaps

The first two operations are known as a "priority queue", so this could be called
a "mergeable priority queue". The standard choice for a priority queue is a binary heap,
which supports `insert` and `deleteMin` in `O(log n)`, but `merge` is `O(n)`.
With a `BinomialHeap`, all three operations are `O(log n)`.
 -/
Batteries.BinomialHeap : (α : Type u) → (α → α → Bool) → Type (max 0 u)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Chord
/-- A walk is chordless if it has no chords.  -/
SimpleGraph.Walk.IsChordless : {V : Type u_1} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → Prop
-- Batteries.Data.List.Lemmas
List.findIdxNth.go.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (n s : ℕ), List.findIdxNth.go p [] n s = s
-- Mathlib.Topology.Algebra.Group.Basic
topologicalAddGroup_sInf : ∀ {G : Type w} [inst : AddGroup G] {ts : Set (TopologicalSpace G)},
  (∀ t ∈ ts, IsTopologicalAddGroup G) → IsTopologicalAddGroup G
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.isCoprime_of_ne : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (P Q : IsDedekindDomain.HeightOneSpectrum R),
  P ≠ Q → IsCoprime P.asIdeal Q.asIdeal
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable : ∀ {α : Type u_5} {β : Type u_6} {ι : Type u_7} [inst : TopologicalSpace ι] [TopologicalSpace.MetrizableSpace ι]
  [inst_2 : MeasurableSpace ι] [SecondCountableTopology ι] [OpensMeasurableSpace ι] [inst_5 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_7 : MeasurableSpace α] {u : ι → α → β},
  (∀ (x : α), Continuous fun i => u i x) →
    (∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)) → MeasureTheory.StronglyMeasurable (Function.uncurry u)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- Any `n`-th primitive root of unity is a root of `cyclotomic n R`.  -/
IsPrimitiveRoot.isRoot_cyclotomic : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R],
  0 < n → ∀ {μ : R}, IsPrimitiveRoot μ n → (Polynomial.cyclotomic n R).IsRoot μ
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.State.mk.inj : ∀ {visited : Std.HashSet (ℕ × Lean.Expr)} {bvars : Std.HashSet ℕ} {visited_1 : Std.HashSet (ℕ × Lean.Expr)}
  {bvars_1 : Std.HashSet ℕ},
  { visited := visited, bvars := bvars } = { visited := visited_1, bvars := bvars_1 } →
    visited = visited_1 ∧ bvars = bvars_1
-- Lean.Level
Lean.Level.brecOn.eq : ∀ {motive : Lean.Level → Sort u} (t : Lean.Level) (F_1 : (t : Lean.Level) → Lean.Level.below t → motive t),
  Lean.Level.brecOn t F_1 = F_1 t (Lean.Level.brecOn.go t F_1).2
-- Mathlib.Data.List.TakeWhile
List.takeWhile_takeWhile : ∀ {α : Type u_1} (p q : α → Bool) (l : List α),
  List.takeWhile p (List.takeWhile q l) = List.takeWhile (fun a => decide (p a = true ∧ q a = true)) l
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.constantCoeff_surjective : ∀ {R : Type u} [inst : Semiring R], Function.Surjective ⇑Polynomial.constantCoeff
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.orderOf_pos : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x → 0 < orderOf x