mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Digraph.Basic
/-- The complete digraph on a type `V` (denoted by `⊤`)
is the digraph whose vertices are all adjacent.
Note that every vertex is adjacent to itself in `⊤`.
 -/
Digraph.completeDigraph : (V : Type u_1) → Digraph V
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.recvReady' : {m : Type → Type} →
  {α : Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT (Std.CloseableChannel.Bounded.State✝ α) m Bool
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.Raw.Const.toList : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → List (α × β)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.dvd_mod_iff : ∀ {R : Type u} [inst : EuclideanDomain R] {a b c : R}, c ∣ b → (c ∣ a % b ↔ c ∣ a)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.addSaturated : ∀ {M : Type u_1} [inst : AddZeroClass M] (self : SaturatedAddSubmonoid M), self.AddSaturated
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_comp_castAdd : ∀ {n m : ℕ} {α : Sort u_2} (f : Fin (n + m) → α) (a : α), Fin.snoc f a ∘ Fin.castAdd (m + 1) = f ∘ Fin.castAdd m
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- The identity as a cocompact continuous map.  -/
CocompactMap.id : (α : Type u_1) → [inst : TopologicalSpace α] → CocompactMap α α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffAt.const_smul_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {a : 𝕜} {s : (x : M) → V x} {x₀ : M},
  ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x₀ →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (a • s) x⟩) x₀
-- Init.Data.List.Lex
List.lt_irrefl : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] (l : List α), ¬l < l
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go : (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
  (w : ℕ) → ℕ → (curr : ℕ) → aig.RefVec curr → curr ≤ w → Std.Sat.AIG.RefVecEntry Std.Tactic.BVDecide.BVBit w
-- Mathlib.Data.List.Map2
List.map₂Right_nil_cons : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (b : β) (bs : List β),
  List.map₂Right f [] (b :: bs) = f none b :: List.map (f none) bs
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_zero : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : MulZeroClass α]
  (A : Matrix l m α), Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A 0 = 0
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.inv_hom_iso_homₚ_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat)
  {Z : C} (h : (HP'.Hₚ i).obj (TopPair.incl.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HP.iso i).inv.app X)
      (CategoryTheory.CategoryStruct.comp ((f.hom i).app X)
        (CategoryTheory.CategoryStruct.comp ((HP'.iso i).hom.app X) h)) =
    CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (TopPair.ofTopCat X)) h
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.StrongHomClass.realize_sentence : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {F : Type u_4}
  [inst_2 : EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.uniqueLinearEquiv_apply : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : Zero M] [inst_4 : Subsingleton M] (x : AddMonoidAlgebra S M),
  (AddMonoidAlgebra.uniqueLinearEquiv R M) x = x.coeff 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.op.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F),
  c.op = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.op c.ι }
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_one_lt_three : Real.exp 1 < 3
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl 1
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.lipschitzWith_toLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → PseudoEMetricSpace (β i)], LipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) (WithLp.toLp p)
-- Aesop.RulePattern
Aesop.RulePattern.mk.injEq : ∀ (pattern : Lean.Meta.AbstractMVarsResult) (argMap levelArgMap : Array (Option ℕ))
  (discrTreeKeys : Array Lean.Meta.DiscrTree.Key) (pattern_1 : Lean.Meta.AbstractMVarsResult)
  (argMap_1 levelArgMap_1 : Array (Option ℕ)) (discrTreeKeys_1 : Array Lean.Meta.DiscrTree.Key),
  ({ pattern := pattern, argMap := argMap, levelArgMap := levelArgMap, discrTreeKeys := discrTreeKeys } =
      { pattern := pattern_1, argMap := argMap_1, levelArgMap := levelArgMap_1, discrTreeKeys := discrTreeKeys_1 }) =
    (pattern = pattern_1 ∧ argMap = argMap_1 ∧ levelArgMap = levelArgMap_1 ∧ discrTreeKeys = discrTreeKeys_1)
-- Mathlib.Algebra.Colimit.Module
/-- The canonical map from a component to the direct limit.  -/
Module.DirectLimit.of : (R : Type u_1) →
  [inst : Semiring R] →
    (ι : Type u_2) →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                [inst_4 : DecidableEq ι] → (i : ι) → G i →ₗ[R] Module.DirectLimit G f
-- Mathlib.Order.Bounds.Basic
isGLB_Ioc : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] [DenselyOrdered γ] {a b : γ}, a < b → IsGLB (Set.Ioc a b) a
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.internalizeConst : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_contains_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {a k : α} {v : β k}, (m.insert k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.CategoryTheory.Elementwise
CategoryTheory.IsIso.hom_inv_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f]
  {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) ((CategoryTheory.ConcreteCategory.hom f) x) = x
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.bot_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R},
  ⊥.N = ⊥
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.embedding : ∀ {α : Type u_1} {β : Type u_2} (e : α ↪ β), Filter.TendstoCofinite ⇑e
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi'_η : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).Monoidal] (i : I),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Functor.pi' F) i = CategoryTheory.Functor.OplaxMonoidal.η (F i)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.Hom.fst : {J : CategoryTheory.Limits.MulticospanShape} →
  (b : J.R) →
    (CategoryTheory.Limits.WalkingMulticospan.left (J.fst b)).Hom (CategoryTheory.Limits.WalkingMulticospan.right b)
-- Mathlib.Algebra.Algebra.Defs
Algebra.smul_def' : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : Algebra R A] (r : R) (x : A),
  r • x = (algebraMap R A) r * x
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforwardId.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)]
  [inst_2 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.id I)],
  CategoryTheory.ExponentiableMorphism.pushforwardId I =
    (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).rightAdjointUniq
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ext_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  (∀ (k : α), Std.ExtDTreeMap.Const.get? t₁ k = Std.ExtDTreeMap.Const.get? t₂ k) → t₁ = t₂
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.Nonempty.inl : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s.Nonempty → (s ∪ t).Nonempty
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
/-- When two morphisms `X ⟶ Y` with `X` cofibrant and `Y` fibrant are related
by a right homotopy, this is a choice of a right homotopy relative
to any good path object for `Y`.  -/
HomotopicalAlgebra.RightHomotopyRel.rightHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [HomotopicalAlgebra.IsCofibrant X] →
            [HomotopicalAlgebra.IsFibrant Y] →
              HomotopicalAlgebra.RightHomotopyRel f g →
                (P : HomotopicalAlgebra.PathObject Y) → [P.IsGood] → P.RightHomotopy f g
-- Mathlib.Data.Finset.Sups
Finset.sups_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α}, s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Given `X : CofibrantObject C`, this is a choice of bifibrant resolution of `X`.  -/
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.CofibrantObject C → HomotopicalAlgebra.BifibrantObject C
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.leftHomologyData.kernelFork.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j k : ι}
  {j' k' : ι'} (hj' : e.f j = j') (hk : c.next j = k) (hk' : c'.next j' = k')
  (cone : CategoryTheory.Limits.KernelFork (K.d j k)),
  HomologicalComplex.extend.leftHomologyData.kernelFork K e hj' hk hk' cone =
    CategoryTheory.Limits.KernelFork.ofι
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι cone) (K.extendXIso e hj').inv) ⋯
-- Mathlib.RingTheory.HahnSeries.Basic
/-- A leading coefficient of a Hahn series is the coefficient of a lowest-order nonzero term, or
zero if the series vanishes.  -/
HahnSeries.leadingCoeff : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → HahnSeries Γ R → R
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite coproducts.  -/
CategoryTheory.Limits.preservesCoproductsOfShape_of_preservesBiproductsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] [CategoryTheory.Limits.PreservesBiproductsOfShape J F],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
-- Lean.LocalContext
Lean.LocalContext.findDeclM? : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → [Monad m] → Lean.LocalContext → (Lean.LocalDecl → m (Option β)) → m (Option β)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.differentiable_cos : Differentiable ℝ Real.cos
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- Given `n+1` objects of `C`, a cofan for the last `n` with point `c₁.pt`
and a binary cofan on `c₁.X` and `f 0`, we can build a cofan for all `n+1`.

In `extendCofanIsColimit` we show that if the two given cofans are colimits,
then this cofan is also a colimit.
 -/
CategoryTheory.extendCofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {f : Fin (n + 1) → C} →
        (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) →
          CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt → CategoryTheory.Limits.Cofan f
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : A.obj₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.hom.hom₁ (CategoryTheory.CategoryStruct.comp e.inv.hom₁ h) = h
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.ExtTreeMap.maxEntry! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtTreeMap α β cmp → α × β
-- Init.Data.UInt.Lemmas
UInt32.toNat_mul : ∀ (a b : UInt32), (a * b).toNat = a.toNat * b.toNat % 2 ^ 32
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F] {Z : CategoryTheory.Functor A D}
  (h : L.comp (L.pointwiseLeftKanExtension (F.comp G)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.pointwiseLeftKanExtensionUnit F) G)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseLeftKanExtension F) G).hom
        (CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom)
          h)) =
    CategoryTheory.CategoryStruct.comp (L.pointwiseLeftKanExtensionUnit (F.comp G)) h
-- Mathlib.CategoryTheory.Galois.Basic
/-- The cardinality of morphisms `A ⟶ X` is smaller than the cardinality of
the fiber of the target if the source is connected.  -/
CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected A], Nat.card (A ⟶ X) ≤ Nat.card (F.obj X).obj
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∏ i ∈ t, f i x
-- Init.Data.Dyadic.Basic
Dyadic.mul.eq_3 : ∀ (n₁ k₁ : ℤ) (hn₁ : n₁ % 2 = 1) (n₂ k₂ : ℤ) (hn₂ : n₂ % 2 = 1),
  (Dyadic.ofOdd n₁ k₁ hn₁).mul (Dyadic.ofOdd n₂ k₂ hn₂) = Dyadic.ofOdd (n₁ * n₂) (k₁ + k₂) ⋯
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ↑0 = 0
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_zero_self : ∀ {w acc : ℕ} {x : BitVec w}, x.cpopNatRec 0 acc = acc
-- Init.Control.Lawful.Basic
/-- Use `simp [← bind_pure_comp]` rather than `simp [map_eq_pure_bind]`,
as `bind_pure_comp` is in the default simp set, so also using `map_eq_pure_bind` would cause a loop.
 -/
map_eq_pure_bind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β) (x : m α),
  f <$> x = do
    let a ← x
    pure (f a)
-- Mathlib.Algebra.Lie.CartanCriterion
LieAlgebra.hasTrivialRadical_iff_isKilling : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
  [inst_4 : LieAlgebra R L] [IsNoetherian R L] [Module.Free R L] [IsPrincipalIdealRing R],
  LieAlgebra.HasTrivialRadical R L ↔ LieAlgebra.IsKilling R L
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- A homomorphism between isocrystals respects the Frobenius map.
Notation `M →ᶠⁱ [p, k]` in the `Isocrystal` namespace.  -/
Isocrystal.«term_→ᶠⁱ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instAddCommGroupWithOne : {R : Type u_1} → [AddCommGroupWithOne R] → AddCommGroupWithOne Rᵒᵈ
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} (f : 𝕜 → α) (c : 𝕜),
  Filter.Tendsto (fun x => f (c - x⁻¹)) Filter.atTop l →
    Filter.Tendsto (fun x => f (c + x⁻¹)) Filter.atTop l → Filter.Tendsto f (nhdsWithin c {c}ᶜ) l
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.refineOneHypercover_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  [inst_1 : E.HasPullbacks]
  (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) (i j : E.I₀)
  (k : (F i j).I₀), (E.refineOneHypercover F).Y k = (F i j).X k
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalarsComp_hom_app_one_tmul : ∀ {R₁ R₂ R₃ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] (f₁₂ : R₁ →+* R₂)
  (f₂₃ : R₂ →+* R₃) (M : ModuleCat R₁) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) =
    1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If `s` is a limit trident over `f`, then a morphism `k : W ⟶ X` satisfying
`∀ j₁ j₂, k ≫ f j₁ = k ≫ f j₂` induces a morphism `l : W ⟶ s.X` such that
`l ≫ Trident.ι s = k`.  -/
CategoryTheory.Limits.Trident.IsLimit.lift' : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {s : CategoryTheory.Limits.Trident f} →
              CategoryTheory.Limits.IsLimit s →
                {W : C} →
                  (k : W ⟶ X) →
                    (∀ (j₁ j₂ : J),
                        CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) →
                      { l // CategoryTheory.CategoryStruct.comp l s.ι = k }
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.instCoeFunForallType : CoeFun PFunctor.{uA, uB} fun x => Type v → Type (max v uA uB)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_base_app : ∀ {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') (X : B),
  φ.leftUnitor.inv.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balance'.eq_1 : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α),
  l.balance' x r =
    if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > Ordnode.delta * l.size then l.rotateL x r
      else if l.size > Ordnode.delta * r.size then l.rotateR x r else l.node' x r
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.coe_inj : ∀ {α : Type u} {a b : α}, ↑a = ↑b ↔ a = b
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.ApplyRulesConfig.toApplyConfig : Lean.Meta.SolveByElim.ApplyRulesConfig → Lean.Meta.ApplyConfig
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whiskerRight_comp : ∀ {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) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (Q : CategoryTheory.LocalizedMonoidal L W ε) {X Y Z : CategoryTheory.LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Q =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Q)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.map_deg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] {𝒜 : ι → σ} {B : Type u_4} {τ : Type u_5} [inst_3 : CommRing B] [inst_4 : SetLike τ B]
  [inst_5 : AddSubgroupClass τ B] {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) {W₁ : Submonoid A} {W₂ : Submonoid B}
  (hw : W₁ ≤ Submonoid.comap f W₂) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 W₁),
  (HomogeneousLocalization.NumDenSameDeg.map f hw c).deg = c.deg
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context.mk : Option Lean.MetavarContext → Lean.MetavarContext → Lean.MetavarContext → Bool → Aesop.EqualUpToIdsM.Context