mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- Elements which are considered equivalent if they differ only by swaps within α or β  -/
Equiv.Perm.ModSumCongr : Type u_7 → Type u_8 → Type (max u_7 u_8)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₄_app_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_361✝ ⟶ g.obj' 0 _proof_361✝) (app₁ : f.obj' 1 _proof_362✝ ⟶ g.obj' 1 _proof_362✝)
  (app₂ : f.obj' 2 _proof_363✝ ⟶ g.obj' 2 _proof_363✝) (app₃ : f.obj' 3 _proof_364✝ ⟶ g.obj' 3 _proof_364✝)
  (app₄ : f.obj' 4 _proof_365✝ ⟶ g.obj' 4 _proof_365✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
      _auto_378✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_363✝))
      _auto_380✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_364✝))
      _auto_382✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_365✝))
      _auto_384✝),
  (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 1 = app₁
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_add_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (a : G),
  IsClosedMap fun x => a + x
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N], Monoid.Coprod.fst.comp Monoid.Coprod.inr = 1
-- Batteries.Data.Char.Basic
/-- Maximum surrogate code point.
(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).)
 -/
Char.maxSurrogate : ℕ
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_eq_of_range_eq : ∀ {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max (max u v) w}} {g : ι' → Ordinal.{max (max u v) w}},
  Set.range f = Set.range g → Ordinal.lsub f = Ordinal.lsub g
-- Init.Data.UInt.Lemmas
UInt64.lt_one_iff : ∀ {a : UInt64}, a < 1 ↔ a = 0
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem: if for all closed sets `F` we have the limsup
condition `limsup μsₙ(F) ≤ μ(F)`, then the measures `μsₙ` converge weakly to the measure `μ`.
Formulated here for countably generated filters.

This lemma uses a coercion from `ProbabilityMeasure` to `Measure` in the hypothesis.
See `tendsto_of_forall_isClosed_limsup_le` for the version without coercion.  -/
MeasureTheory.tendsto_of_forall_isClosed_limsup_le' : ∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace Ω] [inst_1 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F) → Filter.Tendsto μs L (nhds μ)
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
finrank_real_of_complex : ∀ (E : Type u_1) [inst : AddCommGroup E] [inst_1 : Module ℂ E], Module.finrank ℝ E = 2 * Module.finrank ℂ E
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.OptionT.bind.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (__do_lift : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive __do_lift
-- Mathlib.LinearAlgebra.RootSystem.Basic
/-- In characteristic zero if there is no torsion, to check that two finite families of roots and
coroots form a root pairing, it is sufficient to check that they are stable under reflections.  -/
RootPairing.mk' : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  [Finite ι] →
                    [CharZero R] →
                      [IsDomain R] →
                        [Module.IsTorsionFree R M] →
                          (p : M →ₗ[R] N →ₗ[R] R) →
                            [p.IsPerfPair] →
                              (root : ι ↪ M) →
                                (coroot : ι ↪ N) →
                                  (∀ (i : ι), (p (root i)) (coroot i) = 2) →
                                    (∀ (i : ι),
                                        Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i))))
                                          (Set.range ⇑root) (Set.range ⇑root)) →
                                      (∀ (i : ι),
                                          Set.MapsTo (⇑(Module.preReflection (coroot i) (p (root i))))
                                            (Set.range ⇑coroot) (Set.range ⇑coroot)) →
                                        RootPairing ι R M N
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.HasExactLimitsOfShape.mk : ∀ {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.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim → CategoryTheory.HasExactLimitsOfShape J C
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num.congr_simp : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x x_1 : K),
  x = x_1 → IsFractionRing.num A x = IsFractionRing.num A x_1
-- Mathlib.Algebra.Group.Units.Defs
Units.mk.inj : ∀ {α : Type u} {inst : Monoid α} {val inv : α} {val_inv : val * inv = 1} {inv_val : inv * val = 1} {val_1 inv_1 : α}
  {val_inv_1 : val_1 * inv_1 = 1} {inv_val_1 : inv_1 * val_1 = 1},
  { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } =
      { val := val_1, inv := inv_1, val_inv := val_inv_1, inv_val := inv_val_1 } →
    val = val_1 ∧ inv = inv_1
-- Mathlib.Analysis.Convex.FunctionTopology
/-- The set of convex functions on a set `s` is closed.  -/
isClosed_setOfPred_convexOn : ∀ {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : PartialOrder β]
  [inst_3 : TopologicalSpace β] [OrderClosedTopology β] [inst_5 : AddCommMonoid α] [inst_6 : AddCommMonoid β]
  [inst_7 : SMul 𝕜 α] [inst_8 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α},
  IsClosed {f | ConvexOn 𝕜 s f}
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.whiskerRight_actionHomLeft : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) f)
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c'').inv)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.sub_one_lt_natAbs_cyclotomic_eval : ∀ {n q : ℕ}, 1 < n → q ≠ 1 → q - 1 < (Polynomial.eval (↑q) (Polynomial.cyclotomic n ℤ)).natAbs
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_zero_smul : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : AddZeroClass ι]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] {i : ι} (a : A 0)
  (b : A i), (DirectSum.of A i) (a • b) = (DirectSum.of A 0) a * (DirectSum.of A i) b
-- Mathlib.Data.Finset.Max
Finset.le_max' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s), x ≤ s.max' ⋯
-- Mathlib.Topology.MetricSpace.Defs
/-- Two metric space structures with the same distance coincide.  -/
MetricSpace.ext : ∀ {α : Type u_3} {m m' : MetricSpace α}, m.toDist = m'.toDist → m = m'
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_eq_false_iff_not_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {k : α}, m.contains k = false ↔ k ∉ m
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Mapping by the composite morphism `f ≫ g` is the same as mapping by `f` then by `g`.  -/
CategoryTheory.Over.mapComp_eq : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.Over.map f).comp (CategoryTheory.Over.map g)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal₂.eq_1 : ∀ (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] [inst_2 : CategoryTheory.IsIdempotentComplete D],
  CategoryTheory.Idempotents.karoubiUniversal₂ C D =
    (CategoryTheory.Idempotents.toKaroubi D).asEquivalence.congrRight.trans
      (CategoryTheory.Idempotents.karoubiUniversal₁ C D)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.pushNone.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_toInt16 : ∀ (n : ISize) (h : System.Platform.numBits = 64), n.toInt16.toBitVec = BitVec.signExtend 16 (n.toBitVec64 h)
-- Mathlib.Algebra.Module.LinearMap.Basic
/-- `A`-linearly coerce an `R`-linear map from `M` to `N` to a function, when `N` has
commuting `R`-module and `A`-module structures.  -/
LinearMap.ltoFun : (R : Type u_6) →
  (M : Type u_7) →
    (N : Type u_8) →
      (A : Type u_9) →
        [inst : Semiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module A N] → [inst_7 : SMulCommClass R A N] → (M →ₗ[R] N) →ₗ[A] M → N
-- Mathlib.NumberTheory.Modular
ModularGroup.fd_eq_closure_fdo : ModularGroup.fd = closure ModularGroup.fdo
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.add_sub_of_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ξ : MeasureTheory.Measure α},
  μ.MutuallySingular ξ → μ + (ν - ξ) = μ + ν - ξ
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Types.instIsCorepresentableForgetTypeFun : (CategoryTheory.forget (Type u)).IsCorepresentable
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The `vectorSpan` of a single point is `⊥`.  -/
vectorSpan_singleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P), vectorSpan k {p} = ⊥
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the forward direction of `isMaxOn_dual_iff`. -/
IsMaxOn.undual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn (⇑OrderDual.toDual ∘ f) s a → IsMinOn f s a
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y Z : AlgebraicGeometry.Scheme}
  (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] [inst : AlgebraicGeometry.IsAffine Z]
  [inst_1 : AlgebraicGeometry.IsAffine Y], P (CategoryTheory.CategoryStruct.comp f g) ↔ P f
-- Mathlib.Algebra.Order.Group.Synonym
isLeftRegular_toDual : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsLeftRegular (OrderDual.toDual a) ↔ IsLeftRegular a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
OrderDual.instConditionallyCompleteLattice : (α : Type u_5) → [ConditionallyCompleteLattice α] → ConditionallyCompleteLattice αᵒᵈ
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toTopCat),
  AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (CategoryTheory.CategoryStruct.comp f g) x =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g ((CategoryTheory.ConcreteCategory.hom f.base) x))
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} {x y : X ⟶ Y},
  x.f = y.f → x.F = y.F → x = y
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.infinite_not_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {x : G}, ¬IsOfFinAddOrder x → {y | ¬IsOfFinAddOrder y}.Infinite
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Rii α} [inst : LT α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_3 : Std.Rxi.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ}
  {m : Type u → Type w} [inst_5 : Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a x acc => f a ⋯ acc
-- Mathlib.Algebra.Order.Sub.Defs
tsub_le_iff_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}, a - b ≤ c ↔ a ≤ c + b
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch.mk : String → String → Option String → LeanSearchClient.LoogleMatch
-- Init.Data.List.MinMaxIdx
List.minIdxOn_eq_iff_eq_minOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : ℕ},
  List.minIdxOn f xs h = i ↔
    ∃ (hi : i < xs.length), xs[i] = List.minOn f xs h ∧ ∀ (j : ℕ) (hj : j < i), f (List.minOn f xs h) < f xs[j]
-- Mathlib.Topology.UnitInterval
unitInterval.coe_lt_one : ∀ {x : ↑unitInterval}, ↑x < 1 ↔ x < 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smulRight_id : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁],
  (ContinuousLinearMap.id R₁ R₁).smulRight = ContinuousLinearMap.toSpanSingleton R₁
-- Lean.Message
Lean.instReprTraceResult.repr : Lean.TraceResult → ℕ → Std.Format
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Function.Exact.splitSurjectiveEquiv.eq_1 : ∀ {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} (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f),
  h.splitSurjectiveEquiv hf =
    { toFun := fun l => ⟨(LinearEquiv.ofBijective (f ∘ₗ LinearMap.fst R M P + ↑l ∘ₗ LinearMap.snd R M P) ⋯).symm, ⋯⟩,
      invFun := fun e => ⟨↑(↑e).symm ∘ₗ LinearMap.inr R M P, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Slice.Array.Lemmas
Subarray.sliceSize_eq_size : ∀ {α : Type u_1} {xs : Subarray α}, Std.Slice.size xs = Std.Slice.size xs
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommSemigroup.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : CommSemigroup M] [inst_2 : ContinuousMul M],
  SeparationQuotient.instCommSemigroup = { toSemigroup := SeparationQuotient.instSemigroup, mul_comm := ⋯ }
-- Mathlib.RingTheory.MvPolynomial.Tower
Subalgebra.mvPolynomial_aeval_coe : ∀ {R : Type u_1} {A : Type u_2} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (x : σ → ↥S) (p : MvPolynomial σ R),
  (MvPolynomial.aeval fun i => ↑(x i)) p = ↑((MvPolynomial.aeval x) p)
-- Mathlib.Order.WithBot
WithTop.toDual_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithTop α),
  WithTop.toDual (WithTop.map f a) = WithBot.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithTop.toDual a)
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.lift_seqLeft : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] {lift : ⦃α : Type u⦄ → m α → n α}
  {α β : Type u} [LawfulMonad m] [LawfulMonad n] [Std.Internal.LawfulMonadLiftFunction lift] (x : m α) (y : m β),
  lift (x <* y) = lift x <* lift y
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_ι_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_3 : Finite J]
  (F : J → CategoryTheory.Idempotents.Karoubi C) (j : J),
  ((CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).ι j).f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => (F j).X) j)
      (CategoryTheory.Limits.biproduct.map fun j => (F j).p)
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.checkMVars.getParentInfo : Aesop.Rapp → Lean.CoreM (Lean.MVarId × Lean.Meta.SavedState)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstants_expansion : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] (α : Type u_1)
  [inst_1 : (FirstOrder.Language.constantsOn α).Structure M], (L.lhomWithConstants α).IsExpansionOn M
-- Mathlib.Geometry.Euclidean.Incenter
/-- The incenter of a simplex.  -/
Affine.Simplex.incenter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → P
-- Mathlib.CategoryTheory.Sites.Over
/-- The pullback functor `Sheaf J A ⥤ Sheaf (J.over X) A`  -/
CategoryTheory.GrothendieckTopology.overPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u') →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          (X : C) → CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf (J.over X) A)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.eq_2 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match Turing.ToPartrec.Code.succ, k with
    | Turing.ToPartrec.Code.zero', k => h_1 k
    | Turing.ToPartrec.Code.succ, k => h_2 k
    | Turing.ToPartrec.Code.tail, k => h_3 k
    | f.cons fs, k => h_4 f fs k
    | f.comp g, k => h_5 f g k
    | f.case g, k => h_6 f g k
    | f.fix, k => h_7 f k) =
    h_2 k
-- Mathlib.Topology.Germ
/-- Given a predicate on germs `P : Π x : X, germ (𝓝 x) Y → Prop` and `A : set X`,
build a new predicate on germs `RestrictGermPredicate P A` such that
`(∀ x, RestrictGermPredicate P A x f) ↔ ∀ᶠ x near A, P x f`, see
`forall_restrictGermPredicate_iff` for this equivalence.  -/
RestrictGermPredicate : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → ((x : X) → (nhds x).Germ Y → Prop) → Set X → (x : X) → (nhds x).Germ Y → Prop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_eq_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {a : α}, t.get? a = t[a]?
-- Init.Data.SInt.Lemmas
Int32.le_antisymm_iff : ∀ {a b : Int32}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.mem_closedCompactCylinders : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] (t : Set ((i : ι) → X i)),
  t ∈ MeasureTheory.closedCompactCylinders X ↔ ∃ s S, IsClosed S ∧ IsCompact S ∧ t = MeasureTheory.cylinder s S
-- Mathlib.Data.Nat.Choose.Central
/-- An inductive property of the central binomial coefficient.
 -/
Nat.succ_mul_centralBinom_succ : ∀ (n : ℕ), (n + 1) * (n + 1).centralBinom = 2 * (2 * n + 1) * n.centralBinom