mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.match_1.splitter : (C : Type u_1) →
  (motive :
      CategoryTheory.FreeMonoidalCategory C →
        (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C → Sort u_2) →
    (x : CategoryTheory.FreeMonoidalCategory C) →
      (x_1 : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
        ((a : C) →
            (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
              motive (CategoryTheory.FreeMonoidalCategory.of a) x) →
          ((x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
              motive CategoryTheory.FreeMonoidalCategory.unit x) →
            ((X a : CategoryTheory.FreeMonoidalCategory C) →
                (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C) →
                  motive (X.tensor a) n) →
              motive x x_1
-- Mathlib.CategoryTheory.Products.Associator
/-- The inverse associator functor `C × (D × E) ⥤ (C × D) × E `.
 -/
CategoryTheory.prod.inverseAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) → [inst_2 : CategoryTheory.Category.{v₃, u₃} E] → CategoryTheory.Functor (C × D × E) ((C × D) × E)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mk.inj : ∀ {R : Type u_1} {S : Type u_2} {inst : Ring R} {inst_1 : Ring S} {σ : R →+* S} {E : Type u_3} {inst_2 : AddCommGroup E}
  {inst_3 : Module R E} {F : Type u_4} {inst_4 : AddCommGroup F} {inst_5 : Module S F} {domain : Submodule R E}
  {toFun : ↥domain →ₛₗ[σ] F} {domain_1 : Submodule R E} {toFun_1 : ↥domain_1 →ₛₗ[σ] F},
  { domain := domain, toFun := toFun } = { domain := domain_1, toFun := toFun_1 } → domain = domain_1 ∧ toFun ≍ toFun_1
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
/-- The quadratic form on `Module.Dual R M × M` defined as `Q (f, x) = f x`.  -/
QuadraticForm.dualProd : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → QuadraticForm R (Module.Dual R M × M)
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.closure_sphere : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, closure (Metric.sphere x ε) = Metric.sphere x ε
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.withNamespaces : Array Lean.Name → Bool → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Analysis.Normed.Group.Basic
norm_mul_eq_norm_left : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E) {y : E}, ‖y‖ = 0 → ‖x * y‖ = ‖x‖
-- Init.Data.List.Lex
_private.Init.Data.List.Lex.0.List.lex.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (as : List α) (b : α) (bs : List α)
  (h_1 : (head : α) → (tail : List α) → motive [] (head :: tail)) (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match a :: as, b :: bs with
    | [], head :: tail => h_1 head tail
    | x, [] => h_2 x
    | a :: as, b :: bs => h_3 a as b bs) =
    h_3 a as b bs
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdxD.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : ℕ) (x_2 : α × β),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdxD x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback =>
      match compare n l.size with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.entryAtIdxD l n fallback
      | Ordering.eq => (k, v)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.entryAtIdxD r (n - l.size - 1) fallback
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Unpacks the exponent portion of the packed float.
 -/
Float.Model.UnpackedFloat.unpackExponent : {spec : Float.Model.Format} → BitVec spec.numBits → BitVec spec.exponentBits
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.factorsThroughLocalization : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.LeftHomotopyRel.FactorsThroughLocalization (HomotopicalAlgebra.weakEquivalences C)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.toComonad_coe : ∀ {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} (h : L ⊣ R), h.toComonad.toFunctor = R.comp L
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_hom_add_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] {f g : α →₀ M}
  (h : α → M →+ N), ((f + g).sum fun x => ⇑(h x)) = (f.sum fun x => ⇑(h x)) + g.sum fun x => ⇑(h x)
-- Mathlib.Data.Set.Function
/-- **Alias** of `Set.image_eq_preimage_of_leftInvOn_injOn`. -/
Set.image_eq_preimage_of_leftInvOn_injOn_mapsTo : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {s : Set α},
  Set.LeftInvOn g f s → Set.InjOn g (g ⁻¹' s) → f '' s = g ⁻¹' s
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instSMulCommClassCircle_2 : SMulCommClass Complex.UnitClosedDisc Circle Complex.UnitClosedDisc
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of measure `μ` on set `s` is `μ` restricted to `s`
and scaled by the inverse of `μ s` (to make it a probability measure):
`(μ s)⁻¹ • μ.restrict s`.  -/
ProbabilityTheory.«term__[|_]» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map, `j : M →+ M'` is a monoid map,
such that they are both injective, and compatible with the scalar
multiplications on `M` and `M'`, then `j` sends linearly independent families of vectors to
linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map_injOn`.
TODO : `LinearIndepOn` version.  -/
LinearIndependent.map_of_injective_injectiveₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {R' : Type u_6} {M' : Type u_7} [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R' M'],
  LinearIndependent R v →
    ∀ (i : R' → R) (j : M →+ M'),
      Function.Injective i →
        Function.Injective ⇑j → (∀ (r : R') (m : M), j (i r • m) = r • j m) → LinearIndependent R' (⇑j ∘ v)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
/-- The (global) interval version of the *Lebesgue Differentiation Theorem*: if `f : ℝ → E` is
locally integrable, then for almost every `x`, for any `c : ℝ`, the derivative of
`∫ (t : ℝ) in c..x, f t` at `x` is equal to `f x`.  -/
LocallyIntegrable.ae_hasDerivAt_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E},
  MeasureTheory.LocallyIntegrable f MeasureTheory.volume →
    ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun x => ∫ (t : ℝ) in c..x, f t) (f x) x
-- Mathlib.Algebra.Group.Action.Defs
/-- A typeclass mixin saying that two additive actions on the same space commute.  -/
VAddCommClass : (M : Type u_9) → (N : Type u_10) → (α : Type u_11) → [VAdd M α] → [VAdd N α] → Prop
-- Mathlib.Order.Interval.Finset.Defs
Iio_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : αᵒᵈ),
  Finset.Iio a = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi (OrderDual.ofDual a))
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_lt_coe_ennreal_iff : ∀ {x y : ENNReal}, ↑x < ↑y ↔ x < y
-- Mathlib.Algebra.Field.IsField
instIsDomain : ∀ {R : Type u} [inst : Semifield R], IsDomain R
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The constant functor and limit functor are adjoint to each other  -/
CategoryTheory.Limits.constLimAdj : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] →
          CategoryTheory.Functor.const J ⊣ CategoryTheory.Limits.lim
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two zero-preserving morphisms `f`, `g`,
`f + g` is the zero-preserving morphism sending `x` to `f x + g x`.  -/
ZeroHom.instAdd : {M : Type u_2} → {N : Type u_3} → [inst : Zero M] → [inst_1 : AddZeroClass N] → Add (ZeroHom M N)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Infinite sums commute with scalar multiplication. Version for scalars living in a `Group`, but
not requiring any summability hypothesis.  -/
tsum_const_smul' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α] {f : β → α}
  {L : SummationFilter β} {γ : Type u_5} [inst_2 : Group γ] [inst_3 : DistribMulAction γ α] [ContinuousConstSMul γ α]
  [T2Space α] (g : γ), ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.nodup_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.keys.Nodup
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The C⋆-algebra instance when `𝕜 := ℂ` can be found in
`Mathlib/Analysis/CStarAlgebra/ContinuousLinearMap.lean`.  -/
ContinuousLinearMap.instCStarRingId : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], CStarRing (E →L[𝕜] E)
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x y : α},
  x ≠ 0 →
    y ≠ 0 → (x ∣ y ↔ UniqueFactorizationMonoid.normalizedFactors x ≤ UniqueFactorizationMonoid.normalizedFactors y)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.embDomain_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  {Γ' : Type u_6} [inst_3 : AddCommMonoid Γ'] [inst_4 : PartialOrder Γ'] [inst_5 : IsOrderedCancelAddMonoid Γ']
  [inst_6 : NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ'),
  (∀ (x y : Γ), f (x + y) = f x + f y) →
    ∀ (x y : HahnSeries Γ R), HahnSeries.embDomain f (x * y) = HahnSeries.embDomain f x * HahnSeries.embDomain f y
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    (CategoryTheory.IsIso (f ∣_ U) ↔ CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.app f U))
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Evaluation of an exact pairing.  -/
CategoryTheory.ExactPairing.termε_ : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The terms of the sequence are nonzero.  -/
NumberField.Units.dirichletUnitTheorem.seq_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ}
  (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
  (n : ℕ), (algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n) ≠ 0
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of a constant function is `0`.
 -/
MeromorphicOn.divisor_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (e : E), MeromorphicOn.divisor (fun x => e) U = 0
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orImpR.inj : ∀ {p p_1 : Mathlib.Tactic.ITauto.Proof}, p.orImpR = p_1.orImpR → p = p_1
-- Init.Data.Float.Model.Float
Float.Model.instSub : Sub Float.Model
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addGroup.eq_1 : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M),
  c.addGroup =
    { toAddMonoid := c.addMonoid, toNeg := c.hasNeg, toSub := c.hasSub, toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯,
      zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.Topology.MetricSpace.Lipschitz
LocallyLipschitz.const_max : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ},
  LocallyLipschitz f → ∀ (a : ℝ), LocallyLipschitz fun x => max a (f x)
-- Mathlib.Analysis.Normed.Operator.Banach
/-- Intermediate definition used to show
`ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot`.

This is `f.coprod G.subtypeL` as a `ContinuousLinearEquiv`.  -/
ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace E] →
            {F : Type u_5} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [CompleteSpace F] →
                    (f : E →L[𝕜] F) →
                      {G : Submodule 𝕜 F} → IsCompl (↑f).range G → [CompleteSpace ↥G] → (↑f).ker = ⊥ → (E × ↥G) ≃L[𝕜] F
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductDisjoint.mono_inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {ι : Type u_1} {X : ι → C}
  [self : CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X}
  (hc : CategoryTheory.Limits.IsColimit c) (i : ι), CategoryTheory.Mono (c.inj i)
-- Mathlib.Topology.Algebra.Order.Group
continuous_abs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G], Continuous abs
-- Mathlib.Data.Set.Subsingleton
Set.not_subsingleton_iff : ∀ {α : Type u} {s : Set α}, ¬s.Subsingleton ↔ s.Nontrivial
-- Lean.Elab.Tactic.Omega.Frontend
/-- Add an integer inequality to the `Problem`.

We solve equalities as they are discovered, as this often results in an earlier contradiction.
 -/
Lean.Elab.Tactic.Omega.MetaProblem.addIntInequality : Lean.Elab.Tactic.Omega.MetaProblem →
  Lean.Expr → Lean.Expr → Lean.Elab.Tactic.Omega.OmegaM Lean.Elab.Tactic.Omega.MetaProblem
-- Mathlib.Algebra.Lie.Submodule
/-- The natural equivalence between the 'top' Lie submodule and the enclosing Lie module.  -/
LieModuleEquiv.ofTop : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        (M : Type u_1) → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → ↥⊤ ≃ₗ⁅R,L⁆ M
-- Mathlib.Tactic.FunProp.Core
/-- Main `funProp` function. Returns proof of `e`.  -/
Mathlib.Meta.FunProp.funProp : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitEpi f] {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).snd = f
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_compTendsto' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (f : α → β) {lc : Filter γ} {g : lc.Germ α}
  (hg : g.Tendsto l), (↑f).compTendsto' g hg = Filter.Germ.map f g
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.toHoCat_obj_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  Function.Surjective HomotopicalAlgebra.FibrantObject.toHoCat.obj
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mem_of_isSquare' : ∀ {R : Type u_1} [inst : CommRing R] (self : RingPreordering R) {x : R}, IsSquare x → x ∈ (↑self).carrier
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.Intermediate.dropWhileWithPostcondition.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool))
  (dropping : Bool) (it : Std.IterM m β),
  Std.IterM.Intermediate.dropWhileWithPostcondition P dropping it =
    { internalState := { dropping := dropping, inner := it } }
-- Mathlib.Algebra.Order.Ring.Canonical
tsub_one_mul : ∀ {R : Type u} [inst : NonAssocSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [MulRightMono R] [AddLeftReflectLE R] (a b : R),
  (a - 1) * b = a * b - b
-- Mathlib.Topology.Bornology.Basic
Bornology.IsBounded.subset : ∀ {α : Type u_2} {x : Bornology α} {s t : Set α}, Bornology.IsBounded t → s ⊆ t → Bornology.IsBounded s
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_ne_one_iff : ∀ {α : Type u_1} [inst : One α] (a : αˢʸᵐ), SymAlg.unsym a ≠ 1 ↔ a ≠ 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Lean.Elab.ConfigEval.DeriveEvalExpr
Lean.Elab.ConfigEval.evalMetaEval : (α : Type) → Lean.Name → Option Lean.Name → Lean.Expr → Lean.MetaM α
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the month to the given `month` value.
The day remains unchanged, and any invalid days for the new month will be handled according to the `clip` behavior.
 -/
Std.Time.DateTime.withMonthClip : Std.Time.DateTime → Std.Time.Month.Ordinal → Std.Time.DateTime
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYonedaComponents_hom_apply : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : LightProfinite) [inst_1 : Finite ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop),
  (CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F X).hom) y x =
    (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op)) y
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite' : ∀ {R : Type u_1} [inst : Semiring R] {m n o : ℕ} {a : R} {p : Polynomial R},
  p.natDegree ≤ n → m * n ≤ o → p.coeff n = a → (p ^ m).coeff o = if o = m * n then a ^ m else 0
-- Mathlib.Topology.Bornology.Basic
Bornology.cobounded_eq_bot_iff : ∀ {α : Type u_2} [inst : Bornology α], Bornology.cobounded α = ⊥ ↔ BoundedSpace α
-- Mathlib.Tactic.Widget.Calc
CalcParams.mk.inj : ∀ {toSelectInsertParams : SelectInsertParams} {isFirst : Bool} {indent : ℕ}
  {toSelectInsertParams_1 : SelectInsertParams} {isFirst_1 : Bool} {indent_1 : ℕ},
  { toSelectInsertParams := toSelectInsertParams, isFirst := isFirst, indent := indent } =
      { toSelectInsertParams := toSelectInsertParams_1, isFirst := isFirst_1, indent := indent_1 } →
    toSelectInsertParams = toSelectInsertParams_1 ∧ isFirst = isFirst_1 ∧ indent = indent_1
-- Mathlib.Analysis.Normed.Ring.Basic
List.norm_prod : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] [NormMulClass α] (l : List α),
  ‖l.prod‖ = (List.map norm l).prod
-- Mathlib.Data.ZMod.Units
ZMod.unitsMap_surjective : ∀ {n m : ℕ} [hm : NeZero m] (h : n ∣ m), Function.Surjective ⇑(ZMod.unitsMap h)
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.mem_codChart_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), f x ∈ h.codChart.source
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.skipSuffix?_char_eq_some_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  s.skipSuffix? c = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c
-- Mathlib.Util.FormatTable
Alignment.left : Alignment
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.PostponeBehavior.noConfusionType : Sort v✝ → Lean.Elab.Term.PostponeBehavior → Lean.Elab.Term.PostponeBehavior → Sort v✝
-- Mathlib.Data.Finset.NAry
Finset.mem_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {c : γ}, c ∈ Finset.image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c
-- Mathlib.LinearAlgebra.Ray
Module.Ray.map_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  {N : Type u_3} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (f : M ≃ₗ[R] N) (v : Module.Ray R M), (Module.Ray.map f) (-v) = -(Module.Ray.map f) v
-- Lean.Elab.App
/-- The position of the motive parameter.  -/
Lean.Elab.Term.ElabElimInfo.motivePos : Lean.Elab.Term.ElabElimInfo → ℕ
-- Mathlib.GroupTheory.Divisible
DivisibleBy.mk : {A : Type u_1} →
  {α : Type u_2} →
    [inst : AddMonoid A] →
      [inst_1 : SMul α A] →
        [inst_2 : Zero α] →
          (div : A → α → A) → (∀ (a : A), div a 0 = 0) → (∀ {n : α} (a : A), n ≠ 0 → n • div a n = a) → DivisibleBy A α
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function commutes with the additive actions.  -/
AddActionHom.map_vadd' : ∀ {M : Type u_8} {N : Type u_9} {φ : M → N} {X : Type u_10} [inst : VAdd M X] {Y : Type u_11} [inst_1 : VAdd N Y]
  (self : X →ₑ[φ] Y) (m : M) (x : X), self.toFun (m +ᵥ x) = φ m +ᵥ self.toFun x
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.second_contAux_eq : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K] {gp : GenContFract.Pair K},
  g.s.get? 0 = some gp → g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }
-- Mathlib.Data.Int.Cast.Lemmas
/-- If two `MonoidWithZeroHom`s agree on `-1` and the _positive_ naturals then they are equal.  -/
ext_int' : ∀ {F : Type u_1} {α : Type u_3} [inst : MonoidWithZero α] [inst_1 : FunLike F ℤ α] [MonoidWithZeroHomClass F ℤ α]
  {f g : F}, f (-1) = g (-1) → (∀ (n : ℕ), 0 < n → f ↑n = g ↑n) → f = g
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `{ m_i }` is an `R`-basis of `M`, which is also `N`-linearly independent
(in this result it is stated as `Submodule.mulLeftMap` is injective),
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_basis_left' : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {ι : Type u_1} (m : Module.Basis ι R ↥M), Function.Injective ⇑(Submodule.mulLeftMap N ⇑m) → M.LinearDisjoint N
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharRole.tail : Lean.FuzzyMatching.CharRole
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.epsilon_zero_lt_gamma`. -/
Ordinal.epsilon0_lt_gamma : ∀ (o : Ordinal.{u_1}), Ordinal.epsilon 0 < o.gamma
-- Lean.Parser.Term
Lean.Parser.Term.letId.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_trans_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 F' F'' : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) (x : C),
  CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app x) ((adj2.leftAdjointUniq adj3).hom.app x) =
    (adj1.leftAdjointUniq adj3).hom.app x