mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.String.Legacy
/-- Folds a function over a substring from the right, accumulating a value starting with `init`. The
accumulated value is combined with each character in reverse order, using `f`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
Substring.Raw.Legacy.foldr : {α : Type u} → (Char → α → α) → α → Substring.Raw → α
-- Mathlib.MeasureTheory.Integral.Pi
Fin.insertNthEquiv.eq_1 : ∀ {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)),
  Fin.insertNthEquiv α p =
    { toFun := fun f => p.insertNth f.1 f.2, invFun := fun f => (f p, p.removeNth f), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Num.ZNum
PosNum.decidableDvd : DecidableRel fun x1 x2 => x1 ∣ x2
-- Lean.Util.UnusedBinders
/-- Tests if any of the binders of `(x₀ : A₀) → (x₁ : A₁) → ⋯ → X` which satisfy `p Aᵢ bi` (with `bi`
the `binderInfo`) are unused in the renainder of the type (i.e. in `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X`).

Note that the argument to `p` may have loose bvars. This is a performance optimization.

This function runs `cleanupAnnotations` on each type suffix `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X` before
examining it.

We see through `let`s, and do not report if any of them are unused.
 -/
Lean.Expr.hasUnusedForallBindersWhere : (Lean.BinderInfo → Lean.Expr → Bool) → Lean.Expr → Bool
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.Scheme.Hom.connectedComponentsHomeomorph_apply : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.GeometricallyConnected f] (hf : IsOpenMap ⇑f)
  (a : ConnectedComponents ↥X),
  (AlgebraicGeometry.Scheme.Hom.connectedComponentsHomeomorph f hf) a = ⋯.connectedComponentsMap a
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I)
  (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (i : X.I),
  (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).hom.φ i = (h i).hom
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- A functor `F : C ⥤ D` is dense at `Y : D` if the obvious natural transformation
`F ⟶ F ⋙ 𝟭 D` makes `𝟭 D` a pointwise left Kan extension of `F` along itself at `Y`,
i.e. `Y` identifies to the colimit of the obvious functor `CostructuredArrow F Y ⥤ D`.  -/
CategoryTheory.Functor.DenseAt : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → D → Type (max u₁ u₂ v₂)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.le_of_opNNNorm_le : ∀ {𝕜 : 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} {C : NNReal},
  ‖f‖₊ ≤ C → ∀ (m : ι → E), ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊
-- Batteries.Recycling.RBTree.WF
/-- The balancing properties of the `balRight` function.  -/
RBTree.RBNode.Balanced.balRight : ∀ {α : Type u_1} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α} {cl : RBTree.RBColor} {n : ℕ},
  l.Balanced cl (n + 1) →
    RBTree.RBNode.RedRed True r n → RBTree.RBNode.RedRed (cl = RBTree.RBColor.red) (l.balRight v r) (n + 1)
-- Mathlib.Order.PFilter
Order.PFilter.principal_le_iff : ∀ {P : Type u_1} [inst : Preorder P] {x : P} {F : Order.PFilter P}, Order.PFilter.principal x ≤ F ↔ x ∈ F
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.smul_mem_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Ideal R} {x : R}, a • x ∈ a • S ↔ x ∈ S
-- Init.Data.Array.Lemmas
Option.getD.eq_1 : ∀ {α : Type u_1} (dflt x : α), (some x).getD dflt = x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.beta.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Grind.SplitSource.beta e) = 1 + sizeOf e
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant functions :
When `φ : M → N` is a function, and types `X` and `Y` are endowed with actions of `M` and `N`,
a function `f : X → Y` is `φ`-equivariant if `f (m • x) = (φ m) • (f x)`.  -/
MulActionHom : {M : Type u_2} →
  {N : Type u_3} → (M → N) → (X : Type u_5) → [SMul M X] → (Y : Type u_6) → [SMul N Y] → Type (max u_5 u_6)
-- Aesop.RuleTac.GoalDiff
/-- The new goal.  -/
Aesop.GoalDiff.newGoal : Aesop.GoalDiff → Lean.MVarId
-- Mathlib.Logic.Embedding.Set
Function.Embedding.optionEmbeddingEquiv_apply_fst : ∀ (α : Type u_1) (β : Type u_2) (f : Option α ↪ β),
  ((Function.Embedding.optionEmbeddingEquiv α β) f).fst = Function.Embedding.some.trans f
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.OptionT.orElse.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (__do_lift : Option α) →
      ((a : α) → motive (some a)) → ((x : Option α) → (∀ (a : α), x = some a → False) → motive x) → motive __do_lift
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image_image2_antidistrib_right`.  -/
Set.image_image2_right_anticomm : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} {f : α → β' → γ}
  {g : β → β'} {f' : β → α → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f a (g b) = g' (f' b a)) → Set.image2 f s (g '' t) = g' '' Set.image2 f' t s
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
/-- If `‖f‖` is bounded almost everywhere by `R`, then so is its conditional expectation.  -/
MeasureTheory.ae_bdd_norm_condExp_of_ae_bdd_norm : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {R : ℝ} {f : α → E},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ R) → ∀ᵐ (x : α) ∂μ, ‖μ[f | m] x‖ ≤ R
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos`.  -/
Right.add_pos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b : α},
  0 < a → 0 < b → 0 < a + b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_some_zero : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} (h : W'.Nonsingular x y),
  (WeierstrassCurve.Affine.Point.some x y h).sym2x 0 = ![x, 1, 0]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.filter f t) k =
    (Std.DTreeMap.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.isProbabilityMeasure : ∀ {Ω : Type u_1} {ι : Type u_2} {π : ι → Set (Set Ω)} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.iIndepSets π μ → MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.instCategory : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → CategoryTheory.Category.{v_1, max u_1 v_2} (Φ.RightResolution X₂)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorRId_toLinearEquiv : ∀ {R : Type uR} {M₁ : Type uM₁} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Invertible 2] (Q₁ : QuadraticForm R M₁), Q₁.tensorRId.toLinearEquiv = TensorProduct.rid R M₁
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.inner_gramSchmidtOrthonormalBasis_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) {f : ι → E} {i : ι},
  InnerProductSpace.gramSchmidtNormed 𝕜 f i = 0 →
    ∀ (j : ι), inner 𝕜 ((InnerProductSpace.gramSchmidtOrthonormalBasis h f) i) (f j) = 0
-- Init.Meta.Defs
Lean.Meta.ApplyConfig.newGoals : Lean.Meta.ApplyConfig → Lean.Meta.ApplyNewGoals
-- Lean.Elab.InfoTree.Main
Lean.Elab.withEnableInfoTree : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → [MonadFinally m] → Bool → m α → m α
-- Mathlib.Algebra.Group.Defs
/-- Commutative version of `CancelMonoid`.  -/
CancelCommMonoid : Type u → Type u
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.postponed : Aesop.PostponedSafeRule → Aesop.SafeRuleResult
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction_le_iff : ∀ {k : ℕ} {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size},
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst ≤ k ↔
    ∀ (k' : ℕ),
      k < k' → k' ≤ stackPos → ¬String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat k' (stackPos + 1)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_eq_preOmega : ∀ (o : Ordinal.{u_1}), Ordinal.omega o = Ordinal.preOmega (Ordinal.omega0 + o)
-- Mathlib.Geometry.Manifold.Immersion
/-- Every `ModelWithCorners 𝕜 E H` is an immersion when viewed as a map `H → E`.  -/
ModelWithCorners.isImmersionAtOfComplement : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : ℕ} {x : H},
  Manifold.IsImmersionAtOfComplement PUnit.{u_15 + 1} I (modelWithCornersSelf 𝕜 E) (↑n) (↑I) x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.filtration_succ : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : SuccOrder ι] (i : ι), ¬IsMax i → f.filtration (Order.succ i) = f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex
-- Mathlib.Analysis.Seminorm
_private.Mathlib.Analysis.Seminorm.0.Seminorm.isLUB_sSup : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (s : Set (Seminorm 𝕜 E)), BddAbove s → s.Nonempty → IsLUB s (sSup s)
-- Mathlib.Analysis.Complex.AbsMax
Complex.eventually_eq_or_eq_zero_of_isLocalMin_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {c : E},
  (∀ᶠ (z : E) in nhds c, DifferentiableAt ℂ f z) → IsLocalMin (norm ∘ f) c → (∀ᶠ (z : E) in nhds c, f z = f c) ∨ f c = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_eq_some_iff_ne_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : Associates α},
  (∃ s, a.factors = ↑s) ↔ a ≠ 0
-- Mathlib.Data.Fin.Basic
Fin.ne_zero_of_lt : ∀ {n : ℕ} {a b : Fin (n + 1)}, a < b → b ≠ 0
-- Mathlib.Data.ENNReal.Operations
ENNReal.lt_add_of_sub_lt_left : ∀ {a b c : ENNReal}, a ≠ ⊤ ∨ b ≠ ⊤ → a - b < c → a < b + c
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂ comm h₁₂ h₂₃ h₁₃ h).hom₃ =
    CategoryTheory.CategoryStruct.id X₃
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_univ_iff : ∀ {α : Type u}, Set.univ.Subsingleton ↔ Subsingleton α
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.eq_of_forall_apply_eq : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ ν : MeasureTheory.ProbabilityMeasure Ω),
  (∀ (s : Set Ω), MeasurableSet s → μ s = ν s) → μ = ν
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.splitter : (motive : Lean.Grind.Linarith.Expr → Sort u_1) →
  (x : Lean.Grind.Linarith.Expr) →
    ((a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) →
      ((a : Lean.Grind.Linarith.Expr) → motive a.neg) →
        ((k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a)) →
          (Unit → motive Lean.Grind.Linarith.Expr.zero) →
            ((v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v)) →
              ((a b : Lean.Grind.Linarith.Expr) → motive (a.add b)) →
                ((k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)) → motive x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.mk.inj : ∀ {α : Type u_4} {inst : TopologicalSpace α} {toCompacts : TopologicalSpace.Compacts α}
  {isOpen' : IsOpen toCompacts.carrier} {toCompacts_1 : TopologicalSpace.Compacts α}
  {isOpen'_1 : IsOpen toCompacts_1.carrier},
  { toCompacts := toCompacts, isOpen' := isOpen' } = { toCompacts := toCompacts_1, isOpen' := isOpen'_1 } →
    toCompacts = toCompacts_1
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Context.mk.sizeOf_spec : ∀ (quotContext : Lean.Name) (preserveOrder : Bool) (binderInfoForMVars : Lean.BinderInfo)
  (mvarIdsToAbstract : Lean.MVarIdSet),
  sizeOf
      { quotContext := quotContext, preserveOrder := preserveOrder, binderInfoForMVars := binderInfoForMVars,
        mvarIdsToAbstract := mvarIdsToAbstract } =
    1 + sizeOf quotContext + sizeOf preserveOrder + sizeOf binderInfoForMVars + sizeOf mvarIdsToAbstract
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →ₙ* N` denotes the type of multiplication-preserving maps from `M` to `N`.  -/
«term_→ₙ*_» : Lean.TrailingParserDescr
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanlMFast.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] (f : β → α → m β) (as : Vector α n)
  (h_su : n < USize.size) (cur : β) (i n_usize : USize) (h_n : n_usize.toNat = n) (h_i : i.toNat ≤ n)
  (acc : Vector β i.toNat),
  Vector.scanlMFast.loop✝ f as h_su cur i n_usize h_n h_i acc =
    if h_lt : i < n_usize then
      have h_lt_nat := ⋯;
      have h_inc := ⋯;
      do
      let next ← f cur (as.uget i h_lt_nat)
      Vector.scanlMFast.loop✝ f as h_su next (i + 1) n_usize h_n ⋯ (Vector.cast ⋯ (acc.push cur))
    else
      have this := ⋯;
      pure (Vector.cast ⋯ (acc.push cur))
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_comp : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i]
  [inst_4 : ∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ] [hφ' : QuasiIso φ'],
  QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.map_id : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → AddCommMonoid (α i)],
  (DirectSum.map fun i => AddMonoidHom.id (α i)) = AddMonoidHom.id (DirectSum ι fun i => α i)
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.readLspRequestAs : IO.FS.Stream → String → (α : Type) → [Lean.FromJson α] → IO (Lean.JsonRpc.Request α)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
commAlgCatEquivUnder_unitIso : ∀ (R : CommRingCat),
  (commAlgCatEquivUnder R).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun A =>
        CommAlgCat.isoMk
          (let __RingEquiv := RingEquiv.refl ↑A;
          { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }))
      ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toLaxFunctor : CategoryTheory.LaxFunctor B C}
  {map_id :
    autoParam
      (∀ (X : B),
        toLaxFunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toLaxFunctor.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam}
  {mapId_eq_eqToHom :
    autoParam (∀ (X : B), toLaxFunctor.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam}
  {toLaxFunctor_1 : CategoryTheory.LaxFunctor B C}
  {map_id_1 :
    autoParam
      (∀ (X : B),
        toLaxFunctor_1.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toLaxFunctor_1.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam}
  {mapId_eq_eqToHom_1 :
    autoParam (∀ (X : B), toLaxFunctor_1.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam},
  { toLaxFunctor := toLaxFunctor, map_id := map_id, mapId_eq_eqToHom := mapId_eq_eqToHom } =
      { toLaxFunctor := toLaxFunctor_1, map_id := map_id_1, mapId_eq_eqToHom := mapId_eq_eqToHom_1 } →
    toLaxFunctor = toLaxFunctor_1
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.isBasis_of_isBasis_of_subset_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I X Y J : Set α}, M.IsBasis I X → M.IsBasis J Y → J ⊆ X → I ⊆ Y → M.IsBasis I Y
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_cast_divConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑A.card * ↑(A.divConst B) = ↑(A / B).card
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `not_isAddTorsionFree_of_isAddTorsion`.

---

A nontrivial torsion additive abelian group is not torsion-free.  -/
not_isAddTorsionFree_of_isTorsion : ∀ {G : Type u_1} [inst : AddCommGroup G] [Nontrivial G], IsAddTorsion G → ¬IsAddTorsionFree G
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IntermediateField.isPurelyInseparable_tower_bot : ∀ (F : Type u) [inst : Field F] (K : Type w) [inst_1 : Field K] [inst_2 : Algebra F K] (M : IntermediateField F K)
  [IsPurelyInseparable F K], IsPurelyInseparable F ↥M
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- **Alias** of `MeromorphicOn.circleIntegrable_posLog_norm_of_nonneg`.

---

Variant of `MeromorphicOn.circleIntegrable_posLog_norm` for non-negative radii.
 -/
circleIntegrable_posLog_norm_meromorphicOn_of_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c R) → 0 ≤ R → CircleIntegrable (fun x => ‖f x‖.posLog) c R
-- Lean.Elab.Term.TermElabM
/-- We can optionally associate an error context with a metavariable (see `MVarErrorInfo`).
We have three different kinds of error context.
 -/
Lean.Elab.Term.MVarErrorKind : Type
-- Mathlib.Tactic.FBinop
/-- Computes `S x := c a1 ... an x` if it is type correct.
Inserts instance arguments after `x`.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.applyS : FBinopElab.SRec → Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.Order.RelSeries
/-- If `a₀ -r→ a₁ -r→ ... -r→ aₙ` and `b₀ -r→ b₁ -r→ ... -r→ bₘ` are two strict series
such that `r aₙ b₀`, then there is a chain of length `n + m + 1` given by
`a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ b₀ -r→ b₁ -r→ ... -r→ bₘ`.
 -/
RelSeries.append : {α : Type u_1} → {r : SetRel α α} → (p q : RelSeries r) → (p.last, q.head) ∈ r → RelSeries r
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- The given function index is assigned 1, the rest 0  -/
Lean.Elab.WF.GuessLex.MutualMeasure.func : ℕ → Lean.Elab.WF.GuessLex.MutualMeasure
-- Mathlib.Tactic.Peel
/-- Throws an error saying `ty` and `target` could not be matched up.  -/
Mathlib.Tactic.Peel.throwPeelError : {α : Type} → Lean.Expr → Lean.Expr → Lean.MetaM α
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.instNorm : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Norm ℚ_[p]
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₃_map_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7}
  [inst_3 : CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [inst_4 : CategoryTheory.Category.{v_8, u_8} E']
  {X Y : CategoryTheory.Functor E E'} (f : X ⟶ Y)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (c : C₁) (c_1 : C₂)
  (c_2 : C₃),
  ((((CategoryTheory.Functor.postcompose₃.map f).app F).app c).app c_1).app c_2 = f.app (((F.obj c).obj c_1).obj c_2)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.coe_mapCycles₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↑(ModuleCat.of k ↥(groupHomology.cycles₁ A))),
  ↑((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ f φ)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsMap₁ f φ)) ↑x
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_comp_symm_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g) h ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h).inv h_1))
-- Mathlib.FieldTheory.RatFunc.Valuation
/-- The uniform space structure on `RatFunc F` coming from the valuation at infinity.  -/
RatFunc.CompletionAtInfty.instUniformSpace : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → UniformSpace (RatFunc F)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.coe_set_mk : ∀ {R : Type u_1} [inst : CommRing R] (toSubsemiring : Subsemiring R)
  (mem_of_isSquare : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) (neg_one_notMem : -1 ∉ toSubsemiring.carrier),
  ↑{ toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare, neg_one_notMem' := neg_one_notMem } =
    ↑toSubsemiring
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.hyp : Lean.LocalDecl → Aesop.IndexMatchLocation
-- Mathlib.Order.OrderDual
OrderDual.instNontrivial : ∀ {α : Type u_1} [h : Nontrivial α], Nontrivial αᵒᵈ
-- Mathlib.Algebra.Quandle
Rack.act'_symm_apply : ∀ {R : Type u_1} [inst : Rack R] (x y : R), (Rack.act' x).symm y = Rack.invAct x y
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.zero_ne_of : ∀ {α : Type u_1} (a : α), 0 ≠ FreeAddGroup.of a
-- Mathlib.Order.Compare
Ordering.Compares.inj : ∀ {α : Type u_1} [inst : Preorder α] {o₁ o₂ : Ordering} {a b : α}, o₁.Compares a b → o₂.Compares a b → o₁ = o₂