mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.match_3.eq_3 : ∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) (solverId : ℕ) (e : Lean.Expr)
  (rest : Lean.Meta.Grind.SolverTerms)
  (h_1 : Unit → motive Lean.Meta.Grind.SolverTerms.nil Lean.Meta.Grind.SolverTerms.nil)
  (h_2 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive Lean.Meta.Grind.SolverTerms.nil (Lean.Meta.Grind.SolverTerms.next solverId e rest))
  (h_3 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive (Lean.Meta.Grind.SolverTerms.next solverId e rest) Lean.Meta.Grind.SolverTerms.nil)
  (h_4 :
    (id₁ : ℕ) →
      (rhs : Lean.Expr) →
        (rhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (lhs : Lean.Expr) →
              (lhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms)),
  (match Lean.Meta.Grind.SolverTerms.next solverId e rest, Lean.Meta.Grind.SolverTerms.nil with
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.nil => h_1 ()
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.next solverId e rest => h_2 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next solverId e rest, Lean.Meta.Grind.SolverTerms.nil => h_3 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms =>
      h_4 id₁ rhs rhsTerms id₂ lhs lhsTerms) =
    h_3 solverId e rest
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Alt pu
-- Mathlib.Data.Fin.Tuple.Basic
Fin.tuple0_le : ∀ {α : Fin 0 → Type u_1} [inst : (i : Fin 0) → Preorder (α i)] (f g : (i : Fin 0) → α i), f ≤ g
-- Mathlib.LinearAlgebra.Basis.Exact
Submodule.projectionOnto_comp_bijective_of_exact : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    Function.Injective ⇑f →
      ∀ {p q : Submodule R M} (hpq : IsCompl p q),
        Disjoint g.ker q → Submodule.map g q = ⊤ → Function.Bijective ⇑(p.projectionOnto q hpq ∘ₗ f)
-- Init.Data.Int.Lemmas
Int.toNat_sub : ∀ (m n : ℕ), (↑m - ↑n).toNat = m - n
-- Lean.Elab.Do.Legacy
/-- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`.  -/
Lean.Elab.Term.Do.Alt : Type → Type
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Proof of type equality as an arrow  -/
MvPFunctor.castDropB : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {a a' : P.A} → a = a' → (P.drop.B a).Arrow (P.drop.B a')
-- Aesop.Tracing
Aesop.«doElemAesop_trace![_]__» : Lean.ParserDescr
-- Batteries.Data.String.Legacy
/-- Creates a new string that contains the first `n` characters (Unicode code points) of `s`.

If `n` is greater than `s.length`, returns `s`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.take`.

Examples:
* `"red green blue".take 3 = "red"`
* `"red green blue".take 1 = "r"`
* `"red green blue".take 0 = ""`
* `"red green blue".take 100 = "red green blue"`
 -/
String.Legacy.take : String → ℕ → String
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_eq_top_iff : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} {n : ℕ}, I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0
-- Lean.Elab.Do.InferControlInfo
/-- Registers a `ControlInfo` inference handler for the given `doElem` syntax node kind.

A handler should have type `ControlInfoHandler` (i.e. `DoElem → TermElabM ControlInfo`).
For pure handlers, use `fun stx => return ControlInfo.pure`.
 -/
Lean.Elab.Do.controlInfoElemAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Do.ControlInfoHandler
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] {p : E →L[𝕜] E}, IsIdempotentElem p → (↑p).range.HasOrthogonalProjection
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.getSepStxFromSplice : Lean.Syntax → Lean.Syntax
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.getD_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {k : α} {fallback : β k}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getD k fallback = m₂.getD k fallback
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.star.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P P_1 : Finpartition Finset.univ} (e_P : P = P_1)
  (hP : P.IsEquipartition) (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_2 : DecidableRel G.Adj} [inst_3 : DecidableRel G_1.Adj] (ε ε_1 : ℝ),
      ε = ε_1 →
        ∀ {U U_1 : Finset α} (e_U : U = U_1) (hU : U ∈ P.parts) (V V_1 : Finset α),
          V = V_1 → SzemerediRegularity.star hP G ε hU V = SzemerediRegularity.star ⋯ G_1 ε_1 ⋯ V_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_add_neg_iff_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, a + -b < 0 ↔ a < b
-- Mathlib.Topology.Compactness.Compact
isCompact_diagonal : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X], IsCompact (Set.diagonal X)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_toAddEquiv : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  e.toAddEquiv = ↑e
-- Mathlib.SetTheory.Cardinal.NatCard
Set.Finite.card_lt_card : ∀ {α : Type u_1} {s t : Set α}, t.Finite → s ⊂ t → Nat.card ↑s < Nat.card ↑t
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.lipschitz : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, ApproximatesLinearOn f f' s c → LipschitzWith (‖f'‖₊ + c) (s.domRestrict f)
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
AbsConvexOpenSets.coe_convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E] [inst_4 : PartialOrder 𝕜] (s : AbsConvexOpenSets 𝕜 E), Convex 𝕜 ↑s
-- Mathlib.Algebra.Regular.Basic
IsDedekindFiniteMonoid.iff_isLeftRegular_of_mul_eq_one : ∀ {R : Type u_1} [inst : Monoid R], IsDedekindFiniteMonoid R ↔ ∀ (x y : R), x * y = 1 → IsLeftRegular x
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.postcompEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} [inst_3 : W.RespectsIso]
  [inst_4 : W.IsCompatibleWithShift M] [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Y]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] (f : Y ⟶ Z) (hf : W f) {a : M}
  (α : CategoryTheory.Localization.SmallShiftedHom W X Y a),
  (CategoryTheory.Localization.SmallShiftedHom.postcompEquiv f hf) α =
    α.comp (CategoryTheory.Localization.SmallShiftedHom.mk₀ W 0 ⋯ f) ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), (e.restr s).toPartialEquiv = e.restr (interior s)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.norm.injEq : ∀ (post inv post_1 inv_1 : Bool),
  (Lean.Meta.Grind.AttrKind.norm post inv = Lean.Meta.Grind.AttrKind.norm post_1 inv_1) = (post = post_1 ∧ inv = inv_1)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal.mk.injEq : ∀ (rhs : Lean.Expr) (value : ℤ) (goal : Lean.MVarId) (rhs_1 : Lean.Expr) (value_1 : ℤ) (goal_1 : Lean.MVarId),
  ({ rhs := rhs, value := value, goal := goal } = { rhs := rhs_1, value := value_1, goal := goal_1 }) =
    (rhs = rhs_1 ∧ value = value_1 ∧ goal = goal_1)
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_ofUnits_iff_toUnits_mem : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gˣ) (x : G), x ∈ H.ofUnits ↔ toUnits x ∈ H
-- Mathlib.Order.ULift
ULift.down_compare : ∀ {α : Type u} [inst : Ord α] (a b : ULift.{u_1, u} α), compare a.down b.down = compare a b
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.bot_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], ⊥.toSubmodule = ⊥
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumRight_comp_rTensor : ∀ (R : Type u) [inst : CommSemiring R] {ι₁ : Type v₁} [inst_1 : DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₁' : Type w₁'}
  {M₂' : Type w₂'} [inst_2 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [inst_3 : AddCommMonoid M₁']
  [inst_4 : AddCommMonoid M₂'] [inst_5 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_6 : Module R M₁'] [inst_7 : Module R M₂']
  (f : M₁' →ₗ[R] M₂'),
  ↑(TensorProduct.directSumRight R R M₂' M₁) ∘ₗ LinearMap.rTensor (DirectSum ι₁ fun i => M₁ i) f =
    (DirectSum.lmap fun x => LinearMap.rTensor (M₁ x) f) ∘ₗ ↑(TensorProduct.directSumRight R R M₁' M₁)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_v_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m)
  (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      ((CochainComplex.mappingCone.snd φ).v p₂ p₂ ⋯) =
    β.v p₁ p₂ h₁₂
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_lt_mk : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedCancelAddMonoid M] {m m' : M}
  {s s' : ℕ+}, DivisibleHull.mk m s < DivisibleHull.mk m' s' ↔ ↑s' • m < ↑s • m'
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- In a ring, every two-sided ideal is induced by a ring congruence relation.  -/
TwoSidedIdeal.ofRingCon : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → RingCon R → TwoSidedIdeal R
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_normal : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.normalCore.Normal
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involuteEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a : CliffordAlgebra Q), CliffordAlgebra.involuteEquiv a = CliffordAlgebra.involute a
-- Init.Data.Bool
Bool.instLawfulIdentityBeqTrue : Std.LawfulIdentity (fun x1 x2 => x1 == x2) true
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size.eq_1 : ∀ {α : Type u_1}, Batteries.PairingHeapImp.Heap.nil.size = 0
-- Mathlib.Algebra.Polynomial.Splits
/-- **Alias** of `Polynomial.Splits.of_natDegree_le_one_of_invertible`. -/
Polynomial.splits_of_natDegree_le_one_of_invertible : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.natDegree ≤ 1 → ∀ (h : Invertible f.leadingCoeff), f.Splits
-- Lean.Server.References
Lean.Server.Ilean.mk : ℕ → Lean.Name → Array Lean.Lsp.ImportInfo → Lean.Lsp.ModuleRefs → Lean.Lsp.Decls → Lean.Server.Ilean
-- Init.Data.List.Erase
List.mem_eraseP_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, ¬p a = true → (a ∈ List.eraseP p l ↔ a ∈ l)
-- Mathlib.MeasureTheory.Integral.CompactlySupported
CompactlySupportedContinuousMap.integrable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X] {E : Type u_2}
  [inst_3 : NormedAddCommGroup E] (f : CompactlySupportedContinuousMap X E) {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ], MeasureTheory.Integrable (⇑f) μ
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sphere_subset_preimage_metric_sphere : ∀ {n d k : ℕ}, ↑(Behrend.sphere n d k) ⊆ (fun x => WithLp.toLp 2 (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 √↑k
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The `fixingSubgroup` of `g • s` is the conjugate of the `fixingSubgroup` of `s` by `g`.  -/
SubMulAction.fixingSubgroup_smul_eq_fixingSubgroup_map_conj : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (s : Set α) (g : M),
  fixingSubgroup M (g • s) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄}
  (f f_1 :
    (i₁ : ι₁) →
      (i₂ : ι₂) →
        (i₃ : ι₃) →
          c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A)),
  f = f_1 →
    HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f = HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f_1
-- Mathlib.RepresentationTheory.Coinvariants
/-- The quotient map `A → A_S` as a representation morphism.  -/
Rep.toCoinvariantsMkQ : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] → (A : Rep.{w, u, v} k G) → (S : Subgroup G) → [inst_2 : S.Normal] → A ⟶ A.toCoinvariants S
-- Mathlib.GroupTheory.Congruence.Defs
/-- Definition of the infimum of two congruence relations.  -/
Con.inf_iff_and : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M} {x y : M}, (c ⊓ d) x y ↔ c x y ∧ d x y
-- Mathlib.CategoryTheory.Monad.Basic
/-- A morphism of monads is a natural transformation compatible with η and μ.  -/
CategoryTheory.MonadHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Monad C → CategoryTheory.Monad C → Type (max u₁ v₁)
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The positive part of `log` is never negative.  -/
Real.posLog_nonneg : ∀ {x : ℝ}, 0 ≤ x.posLog
-- Mathlib.Topology.CompactOpen
/-- Composition is a continuous map from `C(X, Y) × C(Y, Z)` to `C(X, Z)`,
provided that `Y` is locally compact.
This is Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's *Topologie Générale*.  -/
ContinuousMap.continuous_comp' : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactPair Y Z], Continuous fun x => x.2.comp x.1
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.rightUnitor_inv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor α).inv.τl = (CategoryTheory.Bicategory.rightUnitor α.l).inv
-- Mathlib.Order.WithBot
WithBot.eq_top_iff_forall_ge : ∀ {α : Type u_1} [inst : PartialOrder α] [Nonempty α] [NoTopOrder α] {x : WithBot (WithTop α)},
  x = ⊤ ↔ ∀ (a : α), ↑↑a ≤ x
-- Init.Data.ByteArray.Extra
/-- Interprets a `ByteArray` of size 8 as a little-endian `UInt64`.

Panics if the array's size is not 8.
 -/
ByteArray.toUInt64LE! : ByteArray → UInt64
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.isEllipticSequence : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R}, IsEllipticNet W → IsEllipticSequence W
-- Mathlib.Order.CompleteLattice.Basic
iInf_and : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∧ q → α}, iInf s = ⨅ (h₁ : p), ⨅ (h₂ : q), s ⋯
-- Init.SizeOfLemmas
Char.sizeOf : ∀ (a : Char), sizeOf a = a.toNat + 4
-- Mathlib.FieldTheory.Fixed
AlgEquiv.fintype : (K : Type u) →
  (V : Type v) →
    [inst : Field K] → [inst_1 : Field V] → [inst_2 : Algebra K V] → [FiniteDimensional K V] → Fintype Gal(V/K)
-- Mathlib.Topology.Category.TopPair
/-- The map between the first spaces  -/
TopPair.Hom.fst : {X Y : TopPair} → (X ⟶ Y) → (TopPair.fst ⟶ TopPair.fst)
-- Init.Data.Int.Order
Int.add_lt_add : ∀ {a b c d : ℤ}, a < b → c < d → a + c < b + d
-- Init.Data.Fin.Lemmas
Fin.coe_sub_iff_lt : ∀ {n : ℕ} {a b : Fin n}, ↑(a - b) = n + ↑a - ↑b ↔ a < b
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.nextn : ∀ {m₁ m₂ : List Char} {s : Substring.Raw},
  s.Valid →
    s.toString.toList = m₁ ++ m₂ →
      ∀ (n : ℕ),
        s.nextn n { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + String.utf8Len (List.take n m₂) }
-- Mathlib.RingTheory.Noetherian.Basic
Module.instFiniteSubtypeMemIdealOfIsNoetherian : ∀ {R₁ : Type u_5} {S : Type u_6} [inst : CommSemiring R₁] [inst_1 : Semiring S] [inst_2 : Algebra R₁ S]
  [IsNoetherian R₁ S] (I : Ideal S), Module.Finite R₁ ↥I
-- Mathlib.Algebra.FreeMonoid.Count
FreeAddMonoid.countP'.eq_1 : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : FreeAddMonoid α),
  FreeAddMonoid.countP' p l = List.countP (fun b => decide (p b)) (FreeAddMonoid.toList l)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.coevaluation_evaluation' : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X Y : C}
  [self : CategoryTheory.ExactPairing X Y],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y CategoryTheory.ExactPairing.coevaluation')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ExactPairing.evaluation' Y)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- The differential in the complex of inhomogeneous cochains used to
calculate group cohomology.  -/
inhomogeneousCochains.d : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Monoid G] →
      (A : Rep.{u_1, u, u} k G) → (n : ℕ) → ModuleCat.of k ((Fin n → G) → ↑A) ⟶ ModuleCat.of k ((Fin (n + 1) → G) → ↑A)
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.toFormalMultilinearSeries.eq_1 : ∀ {𝕜 : Type u} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousAdd F] [inst_5 : ContinuousConstSMul 𝕜 F] {ι : Type u_1}
  {E : ι → Type u_2} [inst_6 : (i : ι) → AddCommGroup (E i)] [inst_7 : (i : ι) → Module 𝕜 (E i)]
  [inst_8 : (i : ι) → TopologicalSpace (E i)] [inst_9 : ∀ (i : ι), IsTopologicalAddGroup (E i)]
  [inst_10 : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] [inst_11 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (n : ℕ),
  f.toFormalMultilinearSeries n =
    if h : Fintype.card ι = n then
      ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq h)
        (f.compContinuousLinearMap ContinuousLinearMap.proj)
    else 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Composition of morphisms in `P.Comma L R Q W`.  -/
CategoryTheory.MorphismProperty.Comma.Hom.comp : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [Q.IsStableUnderComposition] →
                        [W.IsStableUnderComposition] →
                          {X Y Z : CategoryTheory.MorphismProperty.Comma L R P Q W} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves finite coproducts, then `F.leftOp : Cᵒᵖ ⥤ D` preserves finite
products.  -/
CategoryTheory.Limits.preservesFiniteProducts_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteCoproducts F],
  CategoryTheory.Limits.PreservesFiniteProducts F.leftOp
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : 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 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum_right_neg : ∀ {n : ℕ} {G : Type u_3} [inst : AddGroup G] (f : Fin n → G) (i : Fin n),
  -Fin.partialSum f i.castSucc + Fin.partialSum f i.succ = f i
-- Mathlib.Order.Hom.Basic
OrderHom.prodMap_coe : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (f : α →o β) (g : γ →o δ) (a : α × γ),
  (f.prodMap g) a = Prod.map (⇑f) (⇑g) a
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationProps.expr : ProofWidgets.ExprPresentationProps → Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx