mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance1.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z d)
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c)) z d)
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), a = RBTree.RBNode.node RBTree.RBColor.red a_1 x b → False) →
    (match RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d with
      | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d =>
        h_1 a x b y c z d
      | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d =>
        h_2 a x b y c z d
      | a, x, b => h_3 a x b) =
      h_2 a x b y c z d
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsExtrOn.lineDerivWithin_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E},
  IsExtrOn f s a → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → lineDerivWithin ℝ f s a b = 0
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.instFunLike : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              [inst_2 : SeminormedAddCommGroup E] →
                [inst_3 : SeminormedAddCommGroup E₂] →
                  [inst_4 : Module R E] → [inst_5 : Module R₂ E₂] → FunLike (E →ₛₗᵢ[σ₁₂] E₂) E E₂
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.unit_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {inst_4 : F₁.LaxMonoidal} {inst_5 : F₂.LaxMonoidal}
  [self : CategoryTheory.NatTrans.IsMonoidal τ] {Z : D}
  (h : F₂.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F₁)
      (CategoryTheory.CategoryStruct.comp (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F₂) h
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.instFaithfulOverToOver : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (X : T) [F.Faithful], (CategoryTheory.CostructuredArrow.toOver F X).Faithful
-- Mathlib.CategoryTheory.Simple
CategoryTheory.id_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C)
  [CategoryTheory.Simple X], CategoryTheory.CategoryStruct.id X ≠ 0
-- Mathlib.Order.Defs.Unbundled
/-- `IsIrrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never
holds).  -/
IsIrrefl : (α : Sort u_1) → (α → α → Prop) → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k k' : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).contains k' = t.contains k'
-- Mathlib.Order.Hom.CompleteLattice
/-- Composition of `sSupHom`s as a `sSupHom`.  -/
sSupHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : SupSet α] → [inst_1 : SupSet β] → [inst_2 : SupSet γ] → sSupHom β γ → sSupHom α β → sSupHom α γ
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instBEqTag.beq : Mathlib.CrossRef.Tag → Mathlib.CrossRef.Tag → Bool
-- Std.Data.TreeMap.Raw.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.TreeMap.Raw.toArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Array (α × β)
-- Mathlib.Order.Lattice
ULift.instDistribLattice : {α : Type u} → [DistribLattice α] → DistribLattice (ULift.{v, u} α)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.ofList l).get? k = none
-- Lean.Elab.PreDefinition.WF.Fix
/-- Since `replaceRecApp` looks at the whole context (by way of `mkDecreasingProof`), a cache entry
for it is only valid in the current local context, or a sub-context. We use a `LctxId` to track
that, and ignore cache entries that come from a deeper context.

In the case where we first see a recursive application in a deeper context, and later the same
call in a less deep context, we thus get two proof obligations. We catch that situation later in
`assignSubsumed` and the user should only see the more general one.
 -/
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.RecM : Lean.Name → Type → Type
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instLinear : {k : Type u} →
  {G : Type v} → [inst : CommSemiring k] → [inst_1 : Monoid G] → CategoryTheory.Linear k (Rep.{u_1, u, v} k G)
-- Mathlib.Topology.Separation.Basic
/-- A singleton in a T₁ space is a closed set.  -/
T1Space.t1 : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T1Space X] (x : X), IsClosed {x}
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)) {Z : CategoryTheory.Limits.FormalCoproduct C}
  (h : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.WidePullback.π
          (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i)
        h) =
    CategoryTheory.CategoryStruct.comp (U.powerπ i) h
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.map : {α β : Type} → Lean.VisibilityMap✝ α → (α → β) → Lean.VisibilityMap✝ β
-- Mathlib.Algebra.Group.Conj
/-- The bijection between a `CommGroup` and its `ConjClasses`.  -/
ConjClasses.mkEquiv : {α : Type u} → [inst : CommMonoid α] → α ≃ ConjClasses α
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.mk : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_4} →
            [inst_2 : Monoid A] →
              [inst_3 : MulDistribMulAction M A] →
                {B : Type u_5} →
                  [inst_4 : Monoid B] →
                    [inst_5 : MulDistribMulAction N B] →
                      (toMulActionHom : A →ₑ[⇑φ] B) →
                        toMulActionHom.toFun 1 = 1 →
                          (∀ (x y : A),
                              toMulActionHom.toFun (x * y) = toMulActionHom.toFun x * toMulActionHom.toFun y) →
                            A →ₑ*[φ] B
-- Mathlib.Topology.Algebra.Group.Basic
continuousDiv_of_indiscreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Div H] [IndiscreteTopology H], ContinuousDiv H
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Logic.Relation
Relation.le_join_of_refl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], r ≤ Relation.Join r
-- Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
tendsto_rpow_sub_one_log : ∀ {x : ℝ}, 0 < x → Filter.Tendsto (fun p => p⁻¹ * (x ^ p - 1)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Real.log x))
-- Lean.Data.PersistentHashSet
Lean.PHashSet : (α : Type u) → [BEq α] → [Hashable α] → Type u
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self : ∀ {Ω : Type u_2} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : StandardBorelSpace Ω] (hm : m ≤ m0)
  [hμ : MeasureTheory.IsFiniteMeasure μ] {t : Set Ω},
  MeasurableSet t →
    ProbabilityTheory.CondIndepSet m hm t t μ →
      ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun ω => 1 | m] ω = 0 ∨ μ[t.indicator fun ω => 1 | m] ω = 1
-- Std.Async.Basic
/-- Runs two computations concurrently and returns both results as a pair.
 -/
Std.Async.BaseAsync.concurrently : {α β : Type} →
  Std.Async.BaseAsync α →
    Std.Async.BaseAsync β → optParam Task.Priority Task.Priority.default → Std.Async.BaseAsync (α × β)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.mk : (carrier : Type u) → [str : CommMonoid carrier] → CommMonCat
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.norm_def : ∀ {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : Norm F] (x : E × F), ‖x‖ = max ‖x.1‖ ‖x.2‖
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.unitOfArray : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : Array α}, (Std.TreeMap.Raw.unitOfArray a cmp).WF
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_eq_left : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ⊢ₛ Q ↔ Q ⊣⊢ₛ Q ∨ P
-- Init.Grind.Ring.Envelope
Quot.lift.congr_simp : ∀ {α : Sort u} {r : α → α → Prop} {β : Sort v} (f f_1 : α → β) (e_f : f = f_1) (a : ∀ (a b : α), r a b → f a = f b)
  (a_1 a_2 : Quot r), a_1 = a_2 → Quot.lift f a a_1 = Quot.lift f_1 ⋯ a_2
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.mul_polyOfInterest_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  (↑p ^ (n + 1) * WittVector.polyOfInterest p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_Ψ₂Sq : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S),
  (W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq
-- Init.Data.List.Nat.InsertIdx
List.mem_insertIdx : ∀ {α : Type u} {a b : α} {i : ℕ} {l : List α}, i ≤ l.length → (a ∈ l.insertIdx i b ↔ a = b ∨ a ∈ l)
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Nat.succ`.  -/
Mathlib.Meta.Positivity.evalNatSucc : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.LinearAlgebra.Quotient.Defs
/-- Shortcut to help the elaborator in the common case.  -/
Submodule.Quotient.instSMul : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (P : Submodule R M) → SMul R (M ⧸ P)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.isAddLeftRegular : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] {a : α}, AddLECancellable a → IsAddLeftRegular a
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Basic.0.SimplexCategory.mkOfLe.match_1.eq_1 : ∀ (motive : Fin (1 + 1) → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_1 ()
-- Init.Data.List.Control
/-- Returns true if the monadic predicate `p` returns `true` for any element of `l`.

`O(|l|)`. Short-circuits upon encountering the first `true`. The elements in `l` are examined in
order from left to right.
 -/
List.anyM : {m : Type → Type u} → [Monad m] → {α : Type v} → (α → m Bool) → List α → m Bool
-- Mathlib.Data.Finset.Max
Finset.map_toDual_min : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α),
  WithTop.map (⇑OrderDual.toDual) s.min = (Finset.image (⇑OrderDual.toDual) s).max
-- Mathlib.Order.Partition.Basic
Partition.Rel.forall : ∀ {α : Type u_1} {x y : α} {u t : Set α} {P : Partition u}, P.Rel x y → t ∈ P → (x ∈ t ↔ y ∈ t)
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- The space of multilinear maps on `Π (i : Fin (n+1)), M i` is canonically isomorphic to
the space of linear maps from `M 0` to the space of multilinear maps on
`Π (i : Fin n), M i.succ`, by separating the first variable. We register this isomorphism as a
linear isomorphism in `multilinearCurryLeftEquiv R M M₂`.

The direct and inverse maps are given by `f.curryLeft` and `f.uncurryLeft`. Use these
unless you need the full framework of linear equivs.  -/
multilinearCurryLeftEquiv : (R : Type uR) →
  {n : ℕ} →
    (M : Fin n.succ → Type v) →
      (M₂ : Type v₂) →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] → MultilinearMap R M M₂ ≃ₗ[R] M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_surj : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {o : Ordinal.{u}},
  o < Ordinal.type r → o ∈ Set.range ⇑(Ordinal.typein r).toRelEmbedding
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.getMethodsRef : Lean.Meta.Grind.GrindM Lean.Meta.Grind.MethodsRef
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- A subcomplex is again a CW complex.  -/
Topology.CWComplex.Subcomplex.instCWComplex : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C : Set X} →
      [T2Space X] → [inst : Topology.CWComplex C] → (E : Topology.RelCWComplex.Subcomplex C) → Topology.CWComplex ↑E
-- Mathlib.Order.Types.Arithmetic
OrderType.liftOn₂.congr_simp : ∀ {δ : Sort v} (o₁ o₁_1 : OrderType.{u_1}),
  o₁ = o₁_1 →
    ∀ (o₂ o₂_1 : OrderType.{u_2}),
      o₂ = o₂_1 →
        ∀ (f f_1 : (α : Type u_1) → [LinearOrder α] → (β : Type u_2) → [LinearOrder β] → δ) (e_f : f = f_1)
          (c :
            ∀ (α₁ : Type u_1) [inst : LinearOrder α₁] (β₁ : Type u_2) [inst_1 : LinearOrder β₁] (α₂ : Type u_1)
              [inst_2 : LinearOrder α₂] (β₂ : Type u_2) [inst_3 : LinearOrder β₂],
              OrderType.type α₁ = OrderType.type α₂ → OrderType.type β₁ = OrderType.type β₂ → f α₁ β₁ = f α₂ β₂),
          o₁.liftOn₂ o₂ f c = o₁_1.liftOn₂ o₂_1 f_1 ⋯
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.inclusion.congr_simp : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S), R.inclusion S h = R.inclusion S h
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.eLpNormLESNormFDerivOneConst_def : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure]
  (p : ℝ),
  MeasureTheory.eLpNormLESNormFDerivOneConst μ p = MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.mk.sizeOf_spec : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  [inst_1 : SizeOf B] (τl : α.l ⟶ β.l) (τr : β.r ⟶ α.r)
  (conjugateEquiv_τl :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) τl = τr)
      CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl._autoParam),
  sizeOf { τl := τl, τr := τr, conjugateEquiv_τl := conjugateEquiv_τl } =
    1 + sizeOf τl + sizeOf τr + sizeOf conjugateEquiv_τl
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to a `UInt64`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toUInt64 : Float32.Model → UInt64
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_union : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s t : Subtype MeasurableSet), ↑(s ∪ t) = ↑s ∪ ↑t
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.Indep.finite_of_subset_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.Indep I → I ⊆ X → M.IsRkFinite X → I.Finite
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.mapIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (p : X ≅ X') (q : Y ≅ Y')
  (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f'),
  (CategoryTheory.Limits.kernel.mapIso f f' p q w).hom = CategoryTheory.Limits.kernel.map f f' p.hom q.hom w
-- Mathlib.RingTheory.SimpleModule.Basic
instIsSemisimpleModuleForallOfFinite : ∀ {R : Type u_2} [inst : Ring R] {ι : Type u_7} [Finite ι] (M : ι → Type u_6) [inst_2 : (i : ι) → AddCommGroup (M i)]
  [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), IsSemisimpleModule R (M i)], IsSemisimpleModule R ((i : ι) → M i)
-- Mathlib.Logic.Equiv.Defs
Equiv.nonempty : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) [Nonempty β], Nonempty α
-- Mathlib.Geometry.Euclidean.Projection
/-- The continuous linear map corresponding to `orthogonalProjection`.  -/
EuclideanGeometry.orthogonalProjection_contLinear : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection],
  (EuclideanGeometry.orthogonalProjection s).contLinear = s.direction.orthogonalProjectionOnto
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
aemeasurable_coe_nnreal_real_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal} {μ : MeasureTheory.Measure α},
  AEMeasurable (fun x => ↑(f x)) μ ↔ AEMeasurable f μ
-- Mathlib.Algebra.Category.Ring.Under.Basic
AlgHom.toUnder_comp : ∀ {R : CommRingCat} {A B C : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra (↑R) A] [inst_4 : Algebra (↑R) B] [inst_5 : Algebra (↑R) C] (f : A →ₐ[↑R] B) (g : B →ₐ[↑R] C),
  (g.comp f).toUnder = CategoryTheory.CategoryStruct.comp f.toUnder g.toUnder
-- Init.Data.UInt.Lemmas
UInt32.mod_def : ∀ (a b : UInt32), a % b = { toBitVec := a.toBitVec % b.toBitVec }
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- A version of `FractionalIdeal.den_mul_self_eq_num` in terms of fractional ideals.  -/
FractionalIdeal.den_mul_self_eq_num' : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (I : FractionalIdeal S P),
  FractionalIdeal.spanSingleton S ((algebraMap R P) ↑I.den) * I = ↑I.num
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_monic : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L), (φ.polyCharpoly b).Monic
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {x : M} {n : WithTop ℕ∞} {g : N → N'} {y : N},
  ContMDiffAt I I' n f x → ContMDiffAt J J' n g y → ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.add_isBigOWith : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c₁ c₂ : ℝ}
  {g : α → F} {l : Filter α} {f₁ f₂ : α → E'},
  f₁ =o[l] g → Asymptotics.IsBigOWith c₁ l f₂ g → c₁ < c₂ → Asymptotics.IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.dividedPowers.congr_simp : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI hI_1 : DividedPowers I) (e_hI : hI = hI_1) {J : Ideal A}
  (hJ : hI.IsSubDPIdeal J) [inst_1 : (x : A) → Decidable (x ∈ J)],
  DividedPowers.IsSubDPIdeal.dividedPowers hI hJ = DividedPowers.IsSubDPIdeal.dividedPowers hI_1 ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.CXY : ∀ {R : Type u_1} [inst : CommRing R] {i j : Fin 3} {a : R},
  (MvPolynomial.C a * MvPolynomial.X i * MvPolynomial.X j).IsHomogeneous 2
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_lt_top : ∀ {r : NNReal}, ↑r < ⊤
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
_private.Mathlib.NumberTheory.NumberField.Units.DirichletTheorem.0.NumberField.Units.dirichletUnitTheorem.seq.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (size : ℕ) (k : α) (v : β k)
  (r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntry! = ⟨k, v⟩
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineMap.instFinite : ∀ {R : Type u_1} {S : Type u_2} {V : Type u_3} {W : Type u_4} {P : Type u_5} [inst : Ring R] [inst_1 : Ring S]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [Module.Finite R V] [Module.Free R V] [inst_6 : AddTorsor V P]
  [inst_7 : AddCommGroup W] [inst_8 : Module R W] [inst_9 : Module S W] [Module.Finite S W]
  [inst_11 : SMulCommClass R S W], Module.Finite S (P →ᵃ[R] W)
-- Mathlib.Algebra.Field.Opposite
AddOpposite.unop_nnratCast : ∀ {α : Type u_1} [inst : NNRatCast α] (q : ℚ≥0), AddOpposite.unop ↑q = ↑q
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.left_comm : ∀ {S : Type u_3} [inst : AddSemigroup S] {a b : S}, AddCommute a b → ∀ (c : S), a + (b + c) = b + (a + c)
-- Lean.Elab.Tactic.Basic
/-- Non-backtracking `try`/`catch`.
 -/
Lean.Elab.Tactic.tryCatch : {α : Type} → Lean.Elab.Tactic.TacticM α → (Lean.Exception → Lean.Elab.Tactic.TacticM α) → Lean.Elab.Tactic.TacticM α
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.bounds_bddBelow : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {f : E [⋀^ι]→L[𝕜] F},
  BddBelow {c | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i, ‖m i‖}
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.isSMulApply : ∀ {X : Type u_1} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : CommRing R] [inst_5 : TopologicalSpace R]
  [inst_6 : IsTopologicalRing R] [inst_7 : Module R E] [inst_8 : ContinuousSMul R E],
  IsSMulApply R (AbstractMeasure X R E) C(X, R) E