mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  {P Q : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q)
  {Z : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} (h : F.op.comp (G.obj Q) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom φ P)
      (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft (G.map f)) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom φ Q)
        h)
-- Mathlib.Algebra.Field.Opposite
MulOpposite.unop_nnratCast : ∀ {α : Type u_1} [inst : NNRatCast α] (q : ℚ≥0), MulOpposite.unop ↑q = ↑q
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddGrpCat.Hom.mk : {A B : AddGrpCat} → (↑A →+ ↑B) → A.Hom B
-- Mathlib.Combinatorics.Enumerative.Bell
/-- Number of possibilities of dividing a set with `m * n` elements into `m` groups
of `n`-element subsets.  -/
Nat.uniformBell : ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : C) {Z : B'}
  (h : G'.obj (ψ'.right.obj x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom.app x)
      (CategoryTheory.CategoryStruct.comp (G'.map (α.right.app x)) h) =
    CategoryTheory.CategoryStruct.comp (α.base.app (G.obj x))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom.app x) h)
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.instNonUnitalCommSemiringSubtypeMemNonUnitalSubalgebraOfT2Space : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] →
              [inst_5 : TopologicalSpace A] →
                [inst_6 : IsSemitopologicalSemiring A] →
                  [inst_7 : ContinuousConstSMul R A] →
                    [T2Space A] → {x : A} → NonUnitalCommSemiring ↥(NonUnitalAlgebra.elemental R x)
-- Init.Data.List.Lemmas
List.replace_replicate_ne : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} [LawfulBEq α] {a b c : α},
  (!b == a) = true → (List.replicate n a).replace b c = List.replicate n a
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp'_symm_single_eq_single_one_tmul : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] (i : ι × κ) (r : R),
  ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r) = (fun₀ | i.1 => 1) ⊗ₜ[R] fun₀ | i.2 => r
-- Mathlib.Order.Disjoint
IsCompl.le_sup_right_iff_inf_left_le : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y a b : α},
  IsCompl x y → (a ≤ b ⊔ y ↔ a ⊓ x ≤ b)
-- Init.Data.Vector.Find
Vector.find?_isSome : ∀ {α : Type} {n : ℕ} {xs : Vector α n} {p : α → Bool}, (Vector.find? p xs).isSome = true ↔ ∃ x ∈ xs, p x = true
-- Mathlib.Data.DList.Instances
/-- The natural equivalence between lists and difference lists, using
`DList.ofList` and `DList.toList`.  -/
Batteries.DList.listEquivDList : (α : Type u_1) → List α ≃ Batteries.DList α
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousAt_biSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), LowerSemicontinuousAt (f i hi) x) →
    LowerSemicontinuousAt (fun x' => ⨆ i, ⨆ (hi : p i), f i hi x') x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A bicone over `F : J → C`, which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.LimitBicone.bicone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → CategoryTheory.Limits.LimitBicone F → CategoryTheory.Limits.Bicone F
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instMul : {M : Type u_1} → [inst : CommMonoid M] → Mul (Associates M)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p)) (F.map (CategoryTheory.eqToHom q)) =
    F.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {Z : C}
  (h :
    ((TopCat.Presheaf.pushforward C f.hom.base).obj X.presheaf).obj
        (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U)
      (CategoryTheory.CategoryStruct.comp
        (f.hom.c.app (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U))) h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯)) h
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_updateCol_smul : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] (M : Matrix n n R)
  (j : n) (c : R) (u : n → R), (M.updateCol j (c • u)).permanent = c * (M.updateCol j u).permanent
-- Std.Http.Data.Body.Full
/-- Builds a response with a text body.
Sets `Content-Type: text/plain; charset=utf-8`.
 -/
Std.Http.Response.Builder.text : Std.Http.Response.Builder → String → Std.Async.Async (Std.Http.Response Std.Http.Body.Full)
-- Mathlib.Data.Rel
SetRel.preimage_id : ∀ {α : Type u_1} (s : Set α), SetRel.id.preimage s = s
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instDecidableMem : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → {t : Std.DTreeMap.Raw α β cmp} → {a : α} → Decidable (a ∈ t)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.isEquivalence_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence], F.inv.IsEquivalence
-- Init.Meta.Defs
Lean.Syntax.instReprPreresolved.repr : Lean.Syntax.Preresolved → ℕ → Std.Format
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyEntourage_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X), Antitone fun U => Dynamics.netEntropyEntourage T F U
-- Mathlib.Tactic.Ring.Common
/-- Get the leading coefficient of an `ExProd`.  -/
Mathlib.Tactic.Ring.Common.ExProd.coeff : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.Common.ExProd bt sα e → (c : Q(«$α»)) × bt c
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_fun_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 f x → deriv (fun y => c y • f y) x = c x • deriv f x + deriv c x • f x
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.ixRSS : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
AddMonoidHom.exists_nhds_isBounded : ∀ {G : Type u_1} {H : Type u_2} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [LocallyCompactSpace G] [inst_6 : MeasurableSpace H]
  [inst_7 : SeminormedAddGroup H] [OpensMeasurableSpace H] (f : G →+ H),
  Measurable ⇑f → ∀ (x : G), ∃ s ∈ nhds x, Bornology.IsBounded (⇑f '' s)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_and : ∀ {v : ℕ} (x y : BitVec v), (x &&& y).toNat = x.toNat &&& y.toNat
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.prod_antidiagonal_swap : ∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ} {f : ℕ × ℕ → M},
  ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p.swap = ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorPower.toTensorAlgebra_tprod : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (x : Fin n → M), TensorPower.toTensorAlgebra ((PiTensorProduct.tprod R) x) = (TensorAlgebra.tprod R M n) x
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_prod_le`. -/
EMetric.hausdorffEdist_prod_le : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s₁ t₁ : Set α}
  {s₂ t₂ : Set β},
  Metric.hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ max (Metric.hausdorffEDist s₁ t₁) (Metric.hausdorffEDist s₂ t₂)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_whiskerLeft_hom_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h k : c ⟶ d} (η : h ≅ k)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.hom))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.inv)) h_1) =
    h_1
-- Mathlib.Analysis.RCLike.Basic
RCLike.lipschitzWith_re : ∀ {K : Type u_1} [inst : RCLike K], LipschitzWith 1 ⇑RCLike.re
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.conjugator.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (l : List (α × Bool)),
  FreeAddGroup.reduceCyclically.conjugator l =
    List.bidirectionalRec [] (fun x => []) (fun a x b rCC => if b.1 = a.1 ∧ (!b.2) = a.2 then a :: rCC else []) l
-- Mathlib.Data.Matrix.Basic
Matrix.transposeAddEquiv_symm : ∀ (m : Type u_2) (n : Type u_3) (α : Type u_11) [inst : Add α],
  (Matrix.transposeAddEquiv m n α).symm = Matrix.transposeAddEquiv n m α
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_ofSnowflaking_closedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : X) {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' Metric.closedBall x r =
      Metric.closedBall (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Lean.CoreM
Lean.DeclNameGenerator.mk.injEq : ∀ (namePrefix : Lean.Name) (idx : ℕ) (parentIdxs : List ℕ) (namePrefix_1 : Lean.Name) (idx_1 : ℕ)
  (parentIdxs_1 : List ℕ),
  ({ namePrefix := namePrefix, idx := idx, parentIdxs := parentIdxs } =
      { namePrefix := namePrefix_1, idx := idx_1, parentIdxs := parentIdxs_1 }) =
    (namePrefix = namePrefix_1 ∧ idx = idx_1 ∧ parentIdxs = parentIdxs_1)
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.isFredholm_iff_exists_isQuasiInverse : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space E] [T2Space F] {u : E →L[𝕜] F},
  u.IsFredholm ↔ ∃ v, (↑v).IsQuasiInverse ↑u
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.isEmbedding_coe : Topology.IsEmbedding UpperHalfPlane.coe
-- Mathlib.Topology.Algebra.Module.LocallyConvex
Convex.eventually_nhdsWithin_segment : ∀ {E : Type u_1} {𝕜 : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] {s : Set E},
  Convex 𝕜 s →
    ∀ {x₀ : E},
      x₀ ∈ s →
        ∀ {p : E → Prop},
          (∀ᶠ (x : E) in nhdsWithin x₀ s, p x) → ∀ᶠ (x : E) in nhdsWithin x₀ s, ∀ y ∈ segment 𝕜 x₀ x, p y
-- Mathlib.Data.Setoid.Basic
Setoid.coe_map_of_ker_le : ∀ {α : Type u_1} {β : Type u_2} (r : Setoid α) (f : α → β),
  Setoid.ker f ≤ r → ⇑(r.map f) = Relation.Map (⇑r) f f ⊔ fun x1 x2 => x1 = x2
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_fract_right' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ),
  Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Ici ↑n)) (nhds 0)
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.constantsToVars.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_4} →
    {γ : Type u_2} →
      (motive : (L.withConstants γ).Term α → Sort u_5) →
        (x : (L.withConstants γ).Term α) →
          ((a : α) → motive (FirstOrder.Language.var a)) →
            ((f : (L.withConstants γ).Functions 0) →
                (ts : Fin 0 → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts)) →
              ((_n : ℕ) →
                  (f : (L.withConstants γ).Functions (_n + 1)) →
                    (ts : Fin (_n + 1) → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts)) →
                motive x
-- Mathlib.Algebra.Group.Hom.Defs
/-- `ZeroHomClass F M N` states that `F` is a type of zero-preserving homomorphisms.

You should extend this typeclass when you extend `ZeroHom`.
 -/
ZeroHomClass : (F : Type u_10) → (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [Zero M] → [Zero N] → [FunLike F M N] → Prop
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.map_vadd : ∀ {M' : Type u_1} {X : Type u_5} [inst : VAdd M' X] {Y : Type u_6} [inst_1 : VAdd M' Y] (f : X →ₑ[id] Y) (m : M')
  (x : X), f (m +ᵥ x) = m +ᵥ f x
-- Lean.Elab.Command
Lean.Elab.Command.Context.macroStack : Lean.Elab.Command.Context → Lean.Elab.MacroStack
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- The natural map from a Lie module to the derivations taking values in it.  -/
LieDerivation.inner : (R : Type u_1) →
  (L : Type u_2) →
    (M : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → M →ₗ[R] LieDerivation R L M
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.instIsFractionRing : ∀ (R : Type u_1) [inst : CommRing R], IsFractionRing (FractionRing R) (FractionRing R)
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.changed.inj : ∀ {goal : Lean.MVarId} {script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))}
  {goal_1 : Lean.MVarId} {script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))},
  Aesop.NormSeqResult.changed goal script = Aesop.NormSeqResult.changed goal_1 script_1 →
    goal = goal_1 ∧ script = script_1
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.brecOn_1.go : {motive_1 : Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
  {motive_2 : Array Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
    {motive_3 : List Lean.Lsp.Ipc.ModuleHierarchy → Sort u} →
      (t : Array Lean.Lsp.Ipc.ModuleHierarchy) →
        ((t : Lean.Lsp.Ipc.ModuleHierarchy) → t.below → motive_1 t) →
          ((t : Array Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_1 t → motive_2 t) →
            ((t : List Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_2 t → motive_3 t) →
              motive_2 t ×' Lean.Lsp.Ipc.ModuleHierarchy.below_1 t
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_inf_eq_inf_comp_of_nonempty : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} {f : ι → α} [inst_1 : OrderTop α]
  [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β] {g : α → β}, Monotone g → s.Nonempty → g (s.inf f) = s.inf (g ∘ f)
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.instLawfulVecOperatorIfInputIte : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec.IfInput fun {len} => Std.Sat.AIG.RefVec.ite
-- Mathlib.Data.Fin.VecNotation
Matrix.empty_val' : ∀ {α : Type u} {n' : Type u_1} (j : n'), (fun i => ![] i j) = ![]
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀ArrowIso_inv_right : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.d₁₀ArrowIso A).inv.right = (groupHomology.chainsIso₀ A).inv
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.lexOrder_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  [NoZeroDivisors R] (φ ψ : MvPowerSeries σ R), (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.instToStringException : ToString Lean.MetavarContext.MkBinding.Exception
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d),
  (I.multiforkEquivPiForkOfIsLimit hc hd).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun K =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯)
      ⋯
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- The Hadamard product of Hermitian matrices is Hermitian.  -/
Matrix.IsHermitian.hadamard : ∀ {α : Type u_1} {n : Type u_4} [inst : CommMonoid α] [inst_1 : StarMul α] {A B : Matrix n n α},
  A.IsHermitian → B.IsHermitian → (A.hadamard B).IsHermitian
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCancelCommMonoidOfMulOpposite : {M : Type u_1} → [CancelCommMonoid Mᵐᵒᵖ] → CancelCommMonoid Mᵈᵐᵃ
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- The Iwasawa generator property: when `Fintype.card ι = 2`, the supremum of the
`iwasawaT` subgroups equals all of `PSL`.  -/
PSL.iSup_iwasawaT_eq_top : ∀ {F : Type u_2} [inst : Field F], iSup PSL.iwasawaT = ⊤
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.lift_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : CommMonoid M] [inst_1 : CommGroup G] (f : M →* G)
  (x : Algebra.GrothendieckGroup M),
  (Algebra.GrothendieckGroup.lift f) x = f ((Localization.monoidOf ⊤).sec x).1 / f ↑((Localization.monoidOf ⊤).sec x).2
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Mapping from Lean expressions to their representations as `AC.Expr`  -/
Lean.Meta.Grind.AC.Struct.denote : Lean.Meta.Grind.AC.Struct → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Expr
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.add : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f g : V →ₗ[K] V₂},
  f.HasNoetherianRange → g.HasNoetherianRange → (f + g).HasNoetherianRange
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.instEpiFst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y], CategoryTheory.Epi (CategoryTheory.Limits.coprod.fst X Y)
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_sub_of_le : ∀ {a b : Int16}, 0 ≤ b → b ≤ a → (a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.lhomWithConstants_onFunction : ∀ (L : FirstOrder.Language) (α : Type w') (_n : ℕ) (val : L.Functions _n),
  (L.lhomWithConstants α).onFunction val = Sum.inl val
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Adding a point in the affine span and a vector in the spanning submodule produces a point in the
affine span.  -/
vadd_mem_affineSpan_of_mem_affineSpan_of_mem_vectorSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : P} {v : V},
  p ∈ affineSpan k s → v ∈ vectorSpan k s → v +ᵥ p ∈ affineSpan k s
-- Mathlib.SetTheory.Lists
Lists'.Subset.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : Lists' α true}, l₁ ⊆ l₂ → l₂ ⊆ l₃ → l₁ ⊆ l₃
-- Lean.DocString.Markdown
/-- Wraps a typed block renderer as a `BlockMdRenderer` by decoding the `Dynamic` custom element as `α`.
 -/
Lean.Doc.mkBlockMdRenderer : (α : Type) → [TypeName α] → Lean.Doc.BlockMdRendererOf α → Lean.Doc.BlockMdRenderer
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofIso_Ω : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞 : CategoryTheory.Subobject.Classifier C) {Ω₀ Ω : C}
  (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω)
  (ht :
    autoParam (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
      CategoryTheory.Subobject.Classifier.ofIso._auto_1),
  (𝒞.ofIso eΩ eΩ₀ from' t ht).Ω = Ω
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIco.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  Set.instFintypeIco a b = Fintype.ofFinset (Finset.Ico a b) ⋯
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.getConst.eq_1 : ∀ (k : ℤ), (Int.Internal.Linear.Poly.num k).getConst = k
-- Plausible.Arbitrary
Plausible.List.Arbitrary : {α : Type u_1} → [Plausible.Arbitrary α] → Plausible.Arbitrary (List α)