mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn.eq : ∀ {motive_1 : Lean.Elab.InfoTree → Sort u} {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u}
  {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} {motive_4 : Array Lean.Elab.InfoTree → Sort u}
  {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  {motive_6 : List Lean.Elab.InfoTree → Sort u} {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  (t : Lean.Elab.InfoTree) (F_1 : (t : Lean.Elab.InfoTree) → t.below → motive_1 t)
  (F_2 : (t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t)
  (F_3 : (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t)
  (F_5 : (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_4 t → motive_5 t)
  (F_6 : (t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_6 t → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 = F_1 t (Lean.Elab.InfoTree.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- A relation on a pre-`0`-hypercover is a commutative diagram
```
obj ----> E.X i
 |         |
 |         |
 v         v
E.X j ---> S
```
 -/
CategoryTheory.PreZeroHypercover.Relation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → E.I₀ → E.I₀ → Type (max u_1 v_1)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.incl : {R : Type u} → R → Rack.PreEnvelGroup R
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.subsingleton_iff : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Subsingleton (Submodule R M) ↔ Subsingleton M
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.mk.injEq : ∀ {R : Type u_1} (f : R) (n : ℕ) (g : Fin n → R) (f_1 : R) (n_1 : ℕ) (g_1 : Fin n_1 → R),
  ({ f := f, n := n, g := g } = { f := f_1, n := n_1, g := g_1 }) = (f = f_1 ∧ n = n_1 ∧ g ≍ g_1)
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.map_ncard_setBernoulli_real_singleton : ∀ {ι : Type u_1} [Countable ι] {u : Set ι},
  u.Finite →
    ∀ (p : ↑unitInterval) (k : ℕ),
      (MeasureTheory.Measure.map Set.ncard (ProbabilityTheory.setBernoulli u p)).real {k} =
        ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
-- Mathlib.Data.PNat.Prime
PNat.fact_prime_two : Fact (PNat.Prime 2)
-- Mathlib.Algebra.Group.Action.Basic
smul_zpow' : ∀ {M : Type u_2} {A : Type u_3} [inst : Monoid M] [inst_1 : Group A] [inst_2 : MulDistribMulAction M A] (r : M) (x : A)
  (z : ℤ), r • x ^ z = (r • x) ^ z
-- Mathlib.Data.Complex.Basic
Complex.I_pow_eq_pow_mod : ∀ (n : ℕ), Complex.I ^ n = Complex.I ^ (n % 4)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  [inst_1 : IsAdicComplete I A] {f : PowerSeries A ⧸ Ideal.span {g}},
  (Ideal.Quotient.mk (Ideal.span {g})) ↑(H.mod' f) = f
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State : Type
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given a terminal object of `J`, construct a cone for `J`,
provided that the morphisms in the diagram are isomorphisms.
In `limitOfDiagramTerminal` we show it is a limit cone.  -/
CategoryTheory.Limits.coneOfDiagramTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} →
          CategoryTheory.Limits.IsTerminal X →
            (F : CategoryTheory.Functor J C) →
              [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] → CategoryTheory.Limits.Cone F
-- Std.Http.Protocol.H1.Reader
/-- Transitions to the state for reading a fixed-length body.
 -/
Std.Http.Protocol.H1.Reader.startFixedBody : {dir : Std.Http.Protocol.H1.Direction} → ℕ → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Differentiable.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ},
  Differentiable ℂ f → Differentiable ℂ g → (∀ (x : E), f x ∈ Complex.slitPlane) → Differentiable ℂ fun x => f x ^ g x
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.Accuracy.inexact.injEq : ∀ (relativeToPlusOneHalfUlp relativeToPlusOneHalfUlp_1 : Ordering),
  (Float.Model.UnpackedFloat.Accuracy.inexact relativeToPlusOneHalfUlp =
      Float.Model.UnpackedFloat.Accuracy.inexact relativeToPlusOneHalfUlp_1) =
    (relativeToPlusOneHalfUlp = relativeToPlusOneHalfUlp_1)
-- Mathlib.Order.Preorder.Finite
Finite.exists_le_maximal : ∀ {α : Type u_2} [inst : Preorder α] [Finite α] {p : α → Prop} {a : α}, p a → ∃ b, a ≤ b ∧ Maximal p b
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addEqStep : Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.lineal_eq_sSup : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] (C : PointedCone R E), C.lineal = sSup {S | ↑S ≤ C}
-- Mathlib.Data.Int.Basic
Int.instNontrivial : Nontrivial ℤ
-- Init.Data.Array.InsertionSort
_private.Init.Data.Array.InsertionSort.0.Array.insertionSort.traverse : {α : Type u_1} → (α → α → Bool) → Array α → ℕ → ℕ → Array α
-- Mathlib.Data.Holor
HolorIndex.drop_take : ∀ {ds₁ ds₂ ds₃ : List ℕ} (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)), t.assocRight.drop.take = t.take.drop
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.cone.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))}
  (hF : ∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op))
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] (X : C) (y : (F.obj (Opposite.op 0)).obj.obj (Opposite.op X)),
  CategoryTheory.coherentTopology.cone✝ hF X y =
    {
      pt :=
        (CategoryTheory.coherentTopology C).yoneda.obj
          (CategoryTheory.Limits.limit (CategoryTheory.coherentTopology.preimageDiagram✝ hF X y)),
      π :=
        CategoryTheory.NatTrans.ofOpSequence
          (fun n =>
            CategoryTheory.CategoryStruct.comp
              ((CategoryTheory.coherentTopology C).yoneda.map
                (CategoryTheory.Limits.limit.π (CategoryTheory.coherentTopology.preimageDiagram✝ hF X y)
                  (Opposite.op n)))
              ((CategoryTheory.coherentTopology C).yonedaEquiv.symm
                (CategoryTheory.coherentTopology.struct.x✝ (CategoryTheory.coherentTopology.preimageStruct✝ hF X y) n)))
          ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The 2-morphism defined by the following pasting diagram:
```
a －－－－－－ ▸ a
  ＼    η      ◥   ＼
  f ＼   g  ／       ＼ f
       ◢  ／     ε      ◢
        b －－－－－－ ▸ b
```
 -/
CategoryTheory.Bicategory.leftZigzag : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g) →
            (CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b) →
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ⟶
                CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedAlt : Inhabited Lean.Meta.Match.Alt
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonAssocSemiring : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonAssocSemiring R] → [IsTopologicalSemiring R] → NonAssocSemiring (SeparationQuotient R)
-- Mathlib.Analysis.Complex.Circle
Circle.coe_inv : ∀ (z : Circle), ↑z⁻¹ = (↑z)⁻¹
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.self_mul_dirichletInverse : ∀ {R : Type u_1} [inst : Ring R] (f : ArithmeticFunction R) (hf : Invertible (f 1)),
  f * ArithmeticFunction.dirichletInverse (⇑f) hf = 1
-- Mathlib.Analysis.Convex.Function
ConcaveOn.right_le_of_le_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f z ≤ f x → f y ≤ f z
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_lt_pow : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ},
  Odd n → ∀ {a b : R}, a ^ n < b ^ n ↔ a < b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_eq_nc_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Bool
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_le_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, b * a⁻¹ ≤ 1 ↔ b ≤ a
-- Mathlib.Analysis.InnerProductSpace.Adjoint
IsSelfAdjoint.conj_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E},
  IsSelfAdjoint T →
    ∀ (U : Submodule 𝕜 E) [inst_4 : U.HasOrthogonalProjection],
      IsSelfAdjoint (U.starProjection ∘SL T ∘SL U.starProjection)
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rcc_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = Std.Rco.Sliceable.mkSlice xs lo...hi + 1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.quasiCoherentData_presentation_generators : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [inst_3 : q.IsLocallyFreeData] (i : q.I),
  (q.quasiCoherentData.presentation i).generators = q.generators i
-- Mathlib.Topology.Maps.Proper.Basic
/-- If `f` is proper and converges to `y` along some ultrafilter `𝒰`, then `𝒰` converges to some
`x` such that `f x = y`.  -/
IsProperMap.ultrafilter_le_nhds_of_tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f → ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x
-- Mathlib.Analysis.Normed.Group.Quotient
Ideal.Quotient.normedCommRing : {R : Type u_3} → [inst : SeminormedCommRing R] → (I : Ideal R) → [IsClosed ↑I] → NormedCommRing (R ⧸ I)
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.d.match_1.eq_5 : ∀ (motive : ℤ → ℤ → Sort u_1) (a a_1 : ℕ) (h_1 : (n m : ℕ) → motive (Int.ofNat n) (Int.ofNat m))
  (h_2 : (n m : ℕ) → motive (Int.negSucc n) (Int.negSucc m)) (h_3 : Unit → motive (Int.negSucc 0) (Int.ofNat 0))
  (h_4 : (a a_2 : ℕ) → motive (Int.ofNat a) (Int.negSucc a_2))
  (h_5 : (a a_2 : ℕ) → motive (Int.negSucc a) (Int.ofNat a_2)),
  (a = 0 → a_1 = 0 → False) →
    (match Int.negSucc a, Int.ofNat a_1 with
      | Int.ofNat n, Int.ofNat m => h_1 n m
      | Int.negSucc n, Int.negSucc m => h_2 n m
      | Int.negSucc 0, Int.ofNat 0 => h_3 ()
      | Int.ofNat a, Int.negSucc a_2 => h_4 a a_2
      | Int.negSucc a, Int.ofNat a_2 => h_5 a a_2) =
      h_5 a a_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLT.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.getKeyLT k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    if hkky : compare k ky = Ordering.gt then Std.DTreeMap.Internal.Impl.getKeyLTD k r ky
    else Std.DTreeMap.Internal.Impl.getKeyLT k l ⋯ ⋯
-- Mathlib.Data.Matrix.Mul
Matrix.smul_vecMul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  [inst_2 : DistribSMul R α] [IsScalarTower R α α] (b : R) (v : m → α) (M : Matrix m n α),
  Matrix.vecMul (b • v) M = b • Matrix.vecMul v M
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.locallySmall_congr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (e : C ≌ D), CategoryTheory.LocallySmall.{w, v, u} C ↔ CategoryTheory.LocallySmall.{w, v', u'} D
-- Mathlib.Order.RelClasses
/-- A well order is a well-founded linear order.  -/
IsWellOrder : (α : Type u) → (α → α → Prop) → Prop
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.some_getEntryLT_eq_getEntryLT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (t : Std.DTreeMap.Internal.Impl α β)
  {ho : t.Ordered} {he : ∃ a ∈ t, compare a k = Ordering.lt},
  some (Std.DTreeMap.Internal.Impl.getEntryLT k t ho he) = Std.DTreeMap.Internal.Impl.getEntryLT? k t
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx : Type
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_iUnion_mem_option`. -/
EMetric.diam_iUnion_mem_option : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] {ι : Type u_3} (o : Option ι) (s : ι → Set X),
  Metric.ediam (⋃ i ∈ o, s i) = ⨆ i ∈ o, Metric.ediam (s i)
-- Mathlib.LinearAlgebra.SModEq.Pow
SModEq.pow_pow_add_one : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {p : ℕ},
  ↑p ∈ I → ∀ {x y : R}, x ≡ y [SMOD I] → ∀ (m : ℕ), x ^ p ^ m ≡ y ^ p ^ m [SMOD I ^ (m + 1)]
-- Init.Data.Range.Polymorphic.PRange
/-- `a...<b` is the range of elements greater than or equal to `a` and less than `b`.
See also `Std.Rco`.
 -/
Std.«term_...<_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A nontrivial finite tree has at least two leaves.  -/
SimpleGraph.IsTree.exists_ne_and_degree_eq_one : ∀ {V : Type u_1} {G : SimpleGraph V} [Nontrivial V] [Finite ↑G.edgeSet] [inst : G.LocallyFinite],
  G.IsTree → ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- Infinite places are represented by non-trivial absolute values.  -/
NumberField.InfinitePlace.isNontrivial : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), (↑v).IsNontrivial
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_part_ofSetoid_iff_rel : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} [inst_1 : Fintype α] {s : Setoid α} [inst_2 : DecidableRel ⇑s] {b : α},
  b ∈ (Finpartition.ofSetoid s).part a ↔ s a b
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.mk_left_as : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F'), (CategoryTheory.Functor.LeftExtension.mk F' α).left.as = PUnit.unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanIsoMk_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
  (z : F.obj CategoryTheory.Limits.WalkingSpan.zero ≅ G.obj CategoryTheory.Limits.WalkingSpan.zero)
  (l : F.obj CategoryTheory.Limits.WalkingSpan.left ≅ G.obj CategoryTheory.Limits.WalkingSpan.left)
  (r : F.obj CategoryTheory.Limits.WalkingSpan.right ≅ G.obj CategoryTheory.Limits.WalkingSpan.right)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) l.hom =
        CategoryTheory.CategoryStruct.comp z.hom (G.map CategoryTheory.Limits.WalkingSpan.Hom.fst))
      CategoryTheory.Limits.spanIsoMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd) r.hom =
        CategoryTheory.CategoryStruct.comp z.hom (G.map CategoryTheory.Limits.WalkingSpan.Hom.snd))
      CategoryTheory.Limits.spanIsoMk._auto_3)
  (X : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.spanIsoMk z l r hl hr).hom.app X =
    (Option.rec z (fun val => CategoryTheory.Limits.WalkingPair.rec l r val) X).hom
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_of_contains_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).contains a = true → t.contains a = true
-- Mathlib.Algebra.Group.Action.End
/-- Given an action of an additive group `G` on a set `α`, each `g : G` defines a permutation of
`α`.  -/
AddAction.toPermHom : (G : Type u_1) → (α : Type u_5) → [inst : AddGroup G] → [AddAction G α] → G →+ Additive (Equiv.Perm α)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mk_coe : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂)
  (h₁ :
    ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
      f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y))
  (h₂ :
    ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
      f (Function.update m i (c • x)) = c • f (Function.update m i x)),
  { toFun := ⇑f, map_update_add' := h₁, map_update_smul' := h₂ } = f
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α}, m.getKey? k = some k' ↔ ∃ (h : k ∈ m), m.getKey k h = k'
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_eq_filter_Ioo_zero : ∀ (n : ℕ), n.primesBelow = Finset.filter Nat.Prime (Finset.Ioo 0 n)
-- Init.Data.SInt.Lemmas
Int64.toInt16_ofNat' : ∀ {n : ℕ}, (Int64.ofNat n).toInt16 = Int16.ofNat n
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.add_subset_iff_right : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] {s t u : Finset α},
  s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.Clause.maxLiteral.eq_1 : ∀ (c : Std.Sat.CNF.Clause ℕ), c.maxLiteral = (List.map (fun x => x.1) c).max?
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.inl.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousAddMonoidHom.inl A B = (ContinuousAddMonoidHom.id A).prod 0
-- Mathlib.Algebra.Ring.Subring.Pointwise
/-- The action on a subring corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Subring.pointwiseMulAction : {M : Type u_1} →
  {R : Type u_2} → [inst : Monoid M] → [inst_1 : Ring R] → [MulSemiringAction M R] → MulAction M (Subring R)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  [toIsStableUnderComposition : W.IsStableUnderComposition] [toHasOfPostcompProperty : W.HasOfPostcompProperty W]
  [toHasOfPrecompProperty : W.HasOfPrecompProperty W], W.HasTwoOutOfThreeProperty
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.toOrderHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : TopologicalSpace α] → [inst_3 : TopologicalSpace β] → (α →Co β) → α →o β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, a ∈ t → Std.DTreeMap.Const.get? t a = some (Std.DTreeMap.Const.getD t a fallback)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.prodAddEquiv_symm_apply : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H)
  [inst_2 : A.Normal] [inst_3 : B.Normal] (q : (G ⧸ A) × H ⧸ B),
  (QuotientAddGroup.prodAddEquiv A B).symm q = Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.mk : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c.ord.cof ≠ c → c.IsSingular
-- Init.Data.UInt.Lemmas
UInt32.ofNatClamp_finVal : ∀ (n : Fin UInt32.size), UInt32.ofNatClamp ↑n = UInt32.ofFin n
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : CategoryTheory.Cat),
  ↑((CategoryTheory.Join.pseudofunctorRight C).obj D) = CategoryTheory.Join C ↑D
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map.eq_1 : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph),
  SimpleGraph.Subgraph.map f H =
    { verts := ⇑f '' H.verts, Adj := Relation.Map H.Adj ⇑f ⇑f, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toList_insert_perm : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k : α} {v : β},
      (Std.DHashMap.Raw.Const.toList (m.insert k v)).Perm
        ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) (Std.DHashMap.Raw.Const.toList m))
-- Batteries.Data.AssocList
Batteries.AssocList.forM.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : α → β → m PUnit.{u_1 + 1})
  (x : Batteries.AssocList α β),
  Batteries.AssocList.forM f x =
    match x with
    | Batteries.AssocList.nil => pure PUnit.unit
    | Batteries.AssocList.cons a b es => do
      f a b
      Batteries.AssocList.forM f es
-- Mathlib.CategoryTheory.CofilteredSystem
/-- The functor `F : J ⥤ Type v` satisfies the Mittag-Leffler condition if for all `j : J`,
there exists some `i : J` and `f : i ⟶ j` such that for all `k : J` and `g : k ⟶ j`, the range
of `F.map f` is contained in that of `F.map g`;
in other words (see `isMittagLeffler_iff_eventualRange`), the eventual range at `j` is attained
by some `f : i ⟶ j`.  -/
CategoryTheory.Functor.IsMittagLeffler : {J : Type u} → [inst : CategoryTheory.Category.{v_1, u} J] → CategoryTheory.Functor J (Type v) → Prop
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (S : CategoryTheory.Sieve X) (e : C ≌ D),
  CategoryTheory.Sieve.functorPushforward e.functor S =
    CategoryTheory.Sieve.functorPullback e.inverse (CategoryTheory.Sieve.pullback (e.unitInv.app X) S)