mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Option.NAry
Option.map_uncurry : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : Option (α × β)),
  Option.map (Function.uncurry f) x = Option.map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)
-- Mathlib.Order.SuccPred.Basic
Order.le_of_pred_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α}, Order.pred b < a → b ≤ a
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.eq_5 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : Unit → motive PosNum.one PosNum.one)
  (h_2 : (x : PosNum) → motive x PosNum.one) (h_3 : (x : PosNum) → motive PosNum.one x)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit0) (h_5 : (a b : PosNum) → motive a.bit0 b.bit1)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit0) (h_7 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit0, b.bit1 with
    | PosNum.one, PosNum.one => h_1 ()
    | x, PosNum.one => h_2 x
    | PosNum.one, x => h_3 x
    | a.bit0, b.bit0 => h_4 a b
    | a.bit0, b.bit1 => h_5 a b
    | a.bit1, b.bit0 => h_6 a b
    | a.bit1, b.bit1 => h_7 a b) =
    h_5 a b
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableColimits C],
  CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Analysis.Fourier.Notation
FourierInvSMul.mk : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : SMul R E] [inst_1 : SMul R F]
  [inst_2 : FourierTransformInv E F],
  (∀ (r : R) (f : E), FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f) →
    FourierInvSMul R E F
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_iff_norm_div_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F}
  {C : NNReal}, LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.contains_prop_eq_contains_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String}, s.contains p = s.contains fun x => decide (p x)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The sequence of finite-rank projections.  -/
SchauderBasis.RankOneDecomposition.P : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] →
        [inst_2 : NormedSpace 𝕜 X] → SchauderBasis.RankOneDecomposition 𝕜 X → ℕ → X →L[𝕜] X
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)},
  F.IsRepresentedBy x ↔ CategoryTheory.IsIso (CategoryTheory.uliftYonedaEquiv.symm { down := x })
-- Mathlib.Algebra.Lie.Subalgebra
LieEquiv.ofEq_apply : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  (L L' : LieSubalgebra R L₁) (h : ↑L = ↑L') (x : ↥L), ↑((LieEquiv.ofEq L L' h) x) = ↑x
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mk.injEq : ∀ {P : Type u_2} [inst : MetricSpace P] (center : P) (radius : ℝ) (center_1 : P) (radius_1 : ℝ),
  ({ center := center, radius := radius } = { center := center_1, radius := radius_1 }) =
    (center = center_1 ∧ radius = radius_1)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The carrier of a subsemigroup.  -/
Subsemigroup.carrier : {M : Type u_3} → [inst : Mul M] → Subsemigroup M → Set M
-- Mathlib.Data.Quot
Quotient.instDecidableLiftOnOfDecidablePred_mathlib : {α : Sort u_1} →
  {sa : Setoid α} →
    (q : Quotient sa) →
      (f : α → Prop) → (h : ∀ (a b : α), a ≈ b → f a = f b) → [DecidablePred f] → Decidable (q.liftOn f h)
-- Mathlib.Algebra.Group.Action.Pretransitive
AddAction.instIsPretransitiveOfSubsingleton : ∀ {M : Type u_5} {α : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α] [Subsingleton α],
  AddAction.IsPretransitive M α
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.of_forall_source_exists : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  Function.Injective ⇑f →
    (∀ (x : ↥X),
        ∃ U i,
          ∃ (x_1 : AlgebraicGeometry.IsOpenImmersion i),
            x ∈ AlgebraicGeometry.Scheme.Hom.opensRange i ∧
              AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp i f)) →
      AlgebraicGeometry.IsOpenImmersion f
-- Mathlib.RingTheory.Ideal.Height
Ideal.eq_span_singleton_of_height_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {p : Ideal R} [p.IsPrime],
  p.height = 1 → ∀ {x : R}, x ∈ p → Prime x → p = Ideal.span {x}
-- Lean.Linter.Init
Lean.Linter.LinterOptions.linterSets : Lean.Linter.LinterOptions → Lean.Linter.LinterSets
-- Mathlib.FieldTheory.Fixed
/-- The intermediate field between `K` and `F` fixed by the field endomorphism `m`.  -/
FixedBy.intermediateField : {M : Type u} →
  [inst : Monoid M] →
    (K : Type u_1) →
      (F : Type v) →
        [inst_1 : Field F] →
          [inst_2 : MulSemiringAction M F] →
            M → [inst_3 : Field K] → [inst_4 : Algebra K F] → [SMulCommClass M K F] → IntermediateField K F
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.exists_eq_append_singleton_of_ne_startPos : ∀ {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.startPos),
  p.Splits t₁ t₂ → ∃ t₁', t₁ = t₁' ++ String.singleton ((p.prev hp).get ⋯)
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.objectFieldKeys : Lean.Json.CompressWorkItemQueue✝ → Array String
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} {f g : M ⟶ N}, f = g ↔ f.hom = g.hom
-- Mathlib.Data.Int.Init
/-- The negative case of `Int.inductionOn'`.  -/
Int.inductionOn'.neg : {motive : ℤ → Sort u_1} →
  (b : ℤ) → motive b → ((k : ℤ) → k ≤ b → motive k → motive (k - 1)) → (n : ℕ) → motive (b + Int.negSucc n)
-- Init.Grind.AC
Lean.Grind.AC.Var : Type
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_inter_union_compl_left : ∀ {α : Type u_1} (s t : Set α), t ⊆ s ∩ t ∪ sᶜ
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel κ]
  [inst : ProbabilityTheory.IsFiniteKernel η] {a : α} {s : Set γ},
  MeasurableSet s → s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ → ((η.withDensity (κ.rnDeriv η)) a) s = (κ a) s
-- Init.Data.List.Erase
List.eraseP_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  List.eraseP p (List.replicate n a) = if p a = true then List.replicate (n - 1) a else List.replicate n a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.Data.ENat.Basic
instLinearOrderENat : LinearOrder ℕ∞
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.Fin.sum_insertNth_go : ∀ {M : Type u_2} [inst : AddCommMonoid M] (n i : ℕ) (h : i < n + 1) (x : M) (p : Fin n → M),
  ∑ j, ⟨i, h⟩.insertNth x p j = x + ∑ j, p j
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.iff_exists_open : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y),
  IsLocallyConstant f ↔ ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `B` contains `C` and `A` contains `B`, then `A` contains `C`.  -/
SimpleGraph.IsContained.trans' : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ},
  B.IsContained C → A.IsContained B → A.IsContained C
-- Mathlib.Computability.Partrec
Nat.Partrec.brecOn : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop} {a : ℕ →. ℕ} (t : Nat.Partrec a),
  (∀ (a : ℕ →. ℕ) (t : Nat.Partrec a), Nat.Partrec.below t → motive a t) → motive a t
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.integral_density : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s → ∫ (x : γ), κ.density ν a x s ∂ν a = (κ a).real (Set.univ ×ˢ s)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Iio : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.map (Fin.castAddEmb m) (Finset.Iio i) = Finset.Iio (Fin.castAdd m i)
-- Mathlib.Data.Finsupp.Basic
Finsupp.curryEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α × β →₀ M), Finsupp.curryEquiv f = f.curry
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.coeff_pow_eq_ite_of_natDegree_le_of_le : ∀ {R : Type u} {m n : ℕ} [inst : Semiring R] {p : Polynomial R} {o : ℕ},
  p.natDegree ≤ n → m * n ≤ o → (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.comp_div_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.GrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) {Z : C} (h_1 : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g / h) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g / CategoryTheory.CategoryStruct.comp f h)
      h_1
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingEquiv.subsemiringMap_symm_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S) (s : Subsemiring R)
  (x : ↥(Subsemiring.map e.toRingHom s)), ↑((e.subsemiringMap s).symm x) = e.symm ↑x
-- Init.Data.Fin.Lemmas
Fin.le_zero_iff : ∀ {n : ℕ} {k : Fin (n + 1)}, k ≤ 0 ↔ k = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [inst_1 : EquivBEq α] (k k' : α) (f : Option β → Option β)
  (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l)
  (hc : Std.Internal.List.containsKey k' (Std.Internal.List.Const.alterKey k f l) = true),
  Std.Internal.List.getValue k' (Std.Internal.List.Const.alterKey k f l) hc =
    if h : (k == k') = true then (f (Std.Internal.List.getValue? k l)).get ⋯ else Std.Internal.List.getValue k' l ⋯
-- Mathlib.Data.TypeVec
/-- take the last value of a `(n+1)-length` vector  -/
TypeVec.last : {n : ℕ} → TypeVec.{u} (n + 1) → Type u
-- Init.Data.Array.Lemmas
Array.foldr_cons_eq_append : ∀ {α : Type u_1} {β : Type u_2} {start : ℕ} {as : Array α} {bs : List β} {f : α → β},
  start = as.size → Array.foldr (fun a acc => f a :: acc) bs as start = (Array.map f as).toList ++ bs
-- Mathlib.Data.Nat.Size
Nat.shiftLeft'_true_ne_zero : ∀ (m : ℕ) {n : ℕ}, n ≠ 0 → Nat.shiftLeft' true m n ≠ 0
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The isomorphism of functors `toOverUnit C ⋙ ChosenPullbacksAlong.pullback (toUnit X)` and
`toOver X`.  -/
CategoryTheory.toOverUnitPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (CategoryTheory.toOverUnit C).comp
            (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)) ≅
          CategoryTheory.toOver X
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X) h)
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiff.deriv' : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F}, ContDiff 𝕜 (n + 1) f → ContDiff 𝕜 n (deriv f)
-- Mathlib.Topology.UniformSpace.Basic
toTopologicalSpace_subtype : ∀ {α : Type ua} [u : UniformSpace α] {p : α → Prop},
  instUniformSpaceSubtype.toTopologicalSpace = instTopologicalSpaceSubtype
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension : ∀ {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) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H)
  [L.HasPointwiseRightKanExtension F] [inst_6 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F],
  CategoryTheory.IsIso ((L.ranAdjunction H).counit.app F)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- If `t` is a colimit pushout cocone over `f` and `g` and `h : Y ⟶ W` and `k : Z ⟶ W` are
morphisms satisfying `f ≫ h = g ≫ k`, then we have a factorization `l : t.pt ⟶ W` such that
`inl t ≫ l = h` and `inr t ≫ l = k`, see `IsColimit.inl_desc` and `IsColimit.inr_desc`.  -/
CategoryTheory.Limits.PushoutCocone.IsColimit.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {t : CategoryTheory.Limits.PushoutCocone f g} →
            CategoryTheory.Limits.IsColimit t →
              {W : C} →
                (h : Y ⟶ W) →
                  (k : Z ⟶ W) →
                    CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k → (t.pt ⟶ W)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.denote : {α : Type u_1} → [Lean.Grind.Ring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Expr → α
-- Std.Http.Data.Body.Length
Std.Http.Body.instReprLength : Repr Std.Http.Body.Length
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_le_maxKey_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {he : l.isEmpty = false},
      (compare (Std.Internal.List.maxKey l he)
            (Std.Internal.List.maxKey (Std.Internal.List.insertEntry k v l) ⋯)).isLE =
        true
-- Mathlib.Order.WithBot
WithTop.map_top : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithTop.map f ⊤ = ⊤
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_succ_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a < Order.succ b → Set.Ioc a (Order.succ b) = insert (Order.succ b) (Set.Ioc a b)
-- Mathlib.Tactic.FunProp.Decl
/-- Is `e` a function property statement? If yes return function property declaration and
the function it talks about.  -/
Mathlib.Meta.FunProp.getFunProp? : Lean.Expr → Lean.MetaM (Option (Mathlib.Meta.FunProp.FunPropDecl × Lean.Expr))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.termY : Lean.ParserDescr
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.small_Iic : ∀ (a : Cardinal.{u}), Small.{u, u + 1} ↑(Set.Iic a)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The projection into `U` from an orthogonal submodule `V` is the zero map.  -/
Submodule.IsOrtho.orthogonalProjectionOnto_comp_subtypeL : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection], U ⟂ V → U.orthogonalProjectionOnto ∘SL V.subtypeL = 0
-- Mathlib.Algebra.Module.Torsion.Free
/-- **Alias** of `Module.IsTorsionFree.isSMulRegular`. -/
IsRegular.isSMulRegular : ∀ {R : Type u_1} {M : Type u_3} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.IsTorsionFree R M] ⦃r : R⦄, IsRegular r → IsSMulRegular M r
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instGroup.eq_1 : ∀ {α : Type u},
  FreeGroup.instGroup =
    { toMul := FreeGroup.instMul, mul_assoc := ⋯, toOne := FreeGroup.instOne, one_mul := ⋯, mul_one := ⋯,
      npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, toInv := FreeGroup.instInv, div := DivInvMonoid.div',
      zpow := zpowRec, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.range_nontrivial : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] [Nontrivial H] (f : G →*₀ H),
  (Set.range ⇑f).Nontrivial
-- Std.Internal.UV.System
Std.Internal.UV.System.GroupInfo.mk.injEq : ∀ (groupname : String) (gid : UInt64) (members : Array String) (groupname_1 : String) (gid_1 : UInt64)
  (members_1 : Array String),
  ({ groupname := groupname, gid := gid, members := members } =
      { groupname := groupname_1, gid := gid_1, members := members_1 }) =
    (groupname = groupname_1 ∧ gid = gid_1 ∧ members = members_1)
-- Mathlib.Algebra.Group.Action.Defs
Commute.smul_right_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : Group G] {g : G} [inst_1 : Mul H] [inst_2 : MulAction G H] [SMulCommClass G H H]
  [IsScalarTower G H H] {a b : H}, Commute a (g • b) ↔ Commute a b
-- Mathlib.Topology.ContinuousOn
/-- If a function is continuous on open sets `s i`, it is continuous on their union  -/
ContinuousOn.iUnion_of_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_5}
  {s : ι → Set α}, (∀ (i : ι), ContinuousOn f (s i)) → (∀ (i : ι), IsOpen (s i)) → ContinuousOn f (⋃ i, s i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k},
  (t.modify k f).getKey? k' = if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Init.Data.String.Decode
ByteArray.lt_size_of_validateUTF8At : ∀ {b : ByteArray} {i : ℕ}, b.validateUTF8At i = true → i < b.size
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.instOplaxMonoidalSkeletonMapSkeleton : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) → [F.OplaxMonoidal] → F.mapSkeleton.OplaxMonoidal
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.inductionOn : ∀ {α₁ : Type u_2} {rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop} {δ : PresentedMonoid rels₁ → Prop}
  (q : PresentedMonoid rels₁), (∀ (a : FreeMonoid α₁), δ ((PresentedMonoid.mk rels₁) a)) → δ q
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.mem_lowerCentralSeries_succ_iff`. -/
mem_lowerCentralSeries_succ_iff : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) (n : ℕ) (q : G),
  q ∈ S.lowerCentralSeries (n + 1) ↔ q ∈ Subgroup.closure {x | ∃ p ∈ S.lowerCentralSeries n, ∃ q ∈ S, ⁅p, q⁆ = x}
-- Mathlib.CategoryTheory.IsConnected
/-- If any maximal connected component containing some element j₀ of J is all of J, then J is connected.

The converse of `induct_on_objects`.
 -/
CategoryTheory.IsConnected.of_induct : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₀ : J},
  (∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p) →
    CategoryTheory.IsConnected J
-- Mathlib.Order.CompleteLattice.Basic
Antitone.map_iSup₂_le : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α]
  [inst_1 : CompleteLattice β] {f : α → β},
  Antitone f → ∀ (s : (i : ι) → κ i → α), f (⨆ i, ⨆ j, s i j) ≤ ⨅ i, ⨅ j, f (s i j)
-- Mathlib.Algebra.Group.Action.Defs
/-- An instance of `SMulDistribClass G R S` states that the multiplicative
action of `G` on `S` is determined by the multiplicative actions of `G` on `R`
and `R` on `S`.

This is similar to `IsScalarTower` except that the action of `G` distributes
over the action of `R` on `S`.

E.g. if `M/L/K` is a tower of galois extensions then `SMulDistribClass Gal(M/K) L M`.  -/
SMulDistribClass : (G : Type u_9) → (R : Type u_10) → (S : Type u_11) → [SMul G R] → [SMul G S] → [SMul R S] → Prop
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.ofAddEquiv : ∀ {G : Type u_1} [inst : AddGroup G] [IsFreeAddGroup G] {H : Type u_2} [inst_2 : AddGroup H] (e : G ≃+ H),
  IsFreeAddGroup H
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Working in continuous functions into a topological field,
a subalgebra of functions that separates points also separates points strongly.

By the hypothesis, we can find a function `f` so `f x ≠ f y`.
By an affine transformation in the field we can arrange so that `f x = a` and `f x = b`.
 -/
Subalgebra.SeparatesPoints.strongly : ∀ {α : Type u_1} [inst : TopologicalSpace α] {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : Field 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] {s : Subalgebra 𝕜 C(α, 𝕜)}, s.SeparatesPoints → (↑s).SeparatesPointsStrongly
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.swap_θ : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  Polynomial.Bivariate.swap (RatFunc.Luroth.θ✝ E) = -RatFunc.Luroth.θ✝ E
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `F` is of exponential characteristic `q`, then `F(S) / F` is a purely inseparable extension
if and only if for any `x ∈ S`, `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`.  -/
IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
  {S : Set E}, IsPurelyInseparable F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
-- Mathlib.Algebra.Order.Round
/-- `round x` rounds `x` to the nearest integer, breaking ties towards positive infinity.

`round (0.5 : ℚ) = 1`.
 -/
round : {α : Type u_2} → [inst : Ring α] → [inst_1 : LinearOrder α] → [FloorRing α] → α → ℤ
-- Mathlib.Topology.Path
Path.neg.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : Neg X] [inst_2 : ContinuousNeg X] (γ : Path a b),
  γ.neg = γ.map ⋯
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.preprocess.sizeOf_spec : sizeOf Aesop.RuleTacDescr.preprocess = 1
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.antitoneOn_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ}, ConcaveOn ℝ S f → DifferentiableOn ℝ f S → AntitoneOn (derivWithin f S) S